D: Generating help pt1

This commit is contained in:
Ivan 2025-08-15 21:53:49 +03:00
parent 5836e48b22
commit 1d182f4417
20 changed files with 1053 additions and 24 deletions

View File

@ -35,8 +35,8 @@ export function HelpConceptSystem() {
экспликации. Портал поддерживает <LinkTopic text='экспликацию в родах структур' topic={HelpTopic.RSLANG} />.
Помимо аксиом также могут приводиться дополнительные утверждения, называемые <b>теоремами</b>. Понятия, которым
даются формальные определения называют <b>производными</b>. Следует отметить, что в родоструктурной экспликации
к аксиомам также относят соотношения <LinkTopic text='типизации' topic={HelpTopic.RSL_TYPES} />, а к производным
понятиям, термы, терм-функции и предикат-функции.
к аксиомам также относят соотношения <LinkTopic text='типизации' topic={HelpTopic.RSL_TYPIFICATION} />, а к
производным понятиям, термы, терм-функции и предикат-функции.
</p>
<p>

View File

@ -1,23 +1,66 @@
import { external_urls, videos } from '@/utils/constants';
import { BadgeVideo } from '../components/badge-video';
import { LinkTopic } from '../components/link-topic';
import { Subtopics } from '../components/subtopics';
import { HelpTopic } from '../models/help-topic';
export function HelpRSLang() {
// prettier-ignore
return (
<div className='flex flex-col gap-4'>
<div className='dense'>
<div>
<h1>Родоструктурная экспликация</h1>
<p>Формальная запись (<i>экспликация</i>) концептуальных схем осуществляется с помощью языка родов структур.</p>
<p>Для ознакомления с основами родов структур можно использовать следующие материалы:</p>
<p>1. <BadgeVideo className='inline-icon' video={videos.explication} /> Видео: Краткое введение в мат. аппарат</p>
<p>2. <a className='underline' href={external_urls.ponomarev}>Текст: Учебник И. Н. Пономарева</a></p>
<p>3. <a className='underline' href={external_urls.full_course}>Видео: лекции для 4 курса (второй семестр 2022-23 год)</a></p>
</div>
<div className='dense'>
<p>
Формальная запись (<i>экспликация</i>) концептуальных схем осуществляется с помощью языка родов структур (далее
Язык). В данном разделе поясняются основные понятия и формальные конструкции Языка. В своей основе Язык
является формальной логикой первого порядка, все дополнительные обозначения основываются на предикате
принадлежности <code>xy</code>.
</p>
<p>
Используются строгие правила написания идентификаторов для обозначений понятий, локальных переменных и
литералов.
</p>
<p>
Элементы Языка подразделяются на теоретико-множественные выражения и логические выражения. Упрощенно говоря,
теоретико-множественное выражение возвращает элемент некоторой{' '}
<LinkTopic topic={HelpTopic.RSL_TYPIFICATION} text='ступени' />, логическое выражение возвращает логическое
значение ИСТИНА или ЛОЖЬ.
</p>
<p>
Помимо указанных выражений также допускаются параметризованные и шаблонные выражения, значения и типизация
которых зависят от вводимых параметров. Такие выражения используются в определениях{' '}
<LinkTopic
topic={HelpTopic.CC_CONSTITUENTA}
text='терм-функций и
предикат-функций'
/>
.
</p>
<p>Выражения, позволяющие манипулировать ступенями операндов называются структурными выражениями.</p>
<p>
Отдельно рассматриваются сложные конструкции, задающие множество через отбор элементов, императивно или
рекурсивно.
</p>
<Subtopics headTopic={HelpTopic.RSLANG} />
<div className='dense'>
<p>Для глубокого ознакомления с основами родов структур можно использовать следующие материалы:</p>
<p>
1. <BadgeVideo className='inline-icon' video={videos.explication} /> Видео: Краткое введение в мат. аппарат
</p>
<p>
2.{' '}
<a className='underline' href={external_urls.ponomarev}>
Текст: Учебник И. Н. Пономарева
</a>
</p>
<p>
3.{' '}
<a className='underline' href={external_urls.full_course}>
Видео: лекции для 4 курса (второй семестр 2022-23 год)
</a>
</p>
</div>
</div>);
</div>
);
}

View File

@ -137,7 +137,7 @@ export function HelpThesaurus() {
<IconCstStructured size='1rem' className='inline-icon' />
{'\u2009'}родовая структура (S#) неопределяемое понятие, имеющее структуру, построенную на базисных
множествах и константных множеств. Содержание родовой структуры формируется{' '}
<LinkTopic text='отношением типизации' topic={HelpTopic.RSL_TYPES} />, аксиомами и конвенцией.
<LinkTopic text='отношением типизации' topic={HelpTopic.RSL_TYPIFICATION} />, аксиомами и конвенцией.
</li>
<li>
<IconCstAxiom size='1rem' className='inline-icon' />

View File

@ -18,7 +18,7 @@ export function HelpRSLangCorrect() {
Правила проверки теоретико-множественных выражений выводятся из условия биективной переносимости предиката
принадлежности элемент должен соответствовать множеству, для которого проверяется принадлежность. Необходимым
условием биективной переносимости является выполнение{' '}
<LinkTopic text='соотношения типизации' topic={HelpTopic.RSL_TYPES} /> для всех локальных и глобальных
<LinkTopic text='соотношения типизации' topic={HelpTopic.RSL_TYPIFICATION} /> для всех локальных и глобальных
идентификаторов.
</p>
<p>

View File

@ -0,0 +1,99 @@
export function HelpRSLangExpressionArithmetic() {
return (
<div>
<h1>Арифметические выражения</h1>
<p>
Арифметические выражения в языке родов структур позволяют выполнять математические операции над числовыми
данными. Эти выражения работают с целыми числами и возвращают числовые результаты.
</p>
<h2>Основные арифметические операции</h2>
<ul>
<li>
<b>Сложение</b>: <code>a + b</code> - сумма чисел a и b
</li>
<li>
<b>Вычитание</b>: <code>a - b</code> - разность чисел a и b
</li>
<li>
<b>Умножение</b>: <code>a × b</code> или <code>a * b</code> - произведение чисел a и b
</li>
<li>
<b>Деление</b>: <code>a ÷ b</code> или <code>a / b</code> - частное от деления a на b
</li>
<li>
<b>Остаток от деления</b>: <code>a mod b</code> - остаток от деления a на b
</li>
<li>
<b>Возведение в степень</b>: <code>a^b</code> или <code>a**b</code> - a в степени b
</li>
</ul>
<h2>Операции сравнения</h2>
<ul>
<li>
<b>Равенство</b>: <code>a = b</code> - a равно b
</li>
<li>
<b>Неравенство</b>: <code>a b</code> - a не равно b
</li>
<li>
<b>Меньше</b>: <code>{'a < b'}</code> - a меньше b
</li>
<li>
<b>Меньше или равно</b>: <code>a b</code> - a меньше или равно b
</li>
<li>
<b>Больше</b>: <code>{'a > b'}</code> - a больше b
</li>
<li>
<b>Больше или равно</b>: <code>a b</code> - a больше или равно b
</li>
</ul>
<h2>Специальные функции</h2>
<ul>
<li>
<b>Абсолютное значение</b>: <code>|a|</code> - модуль числа a
</li>
<li>
<b>Минимум</b>: <code>min(a, b)</code> - минимальное из чисел a и b
</li>
<li>
<b>Максимум</b>: <code>max(a, b)</code> - максимальное из чисел a и b
</li>
<li>
<b>Факториал</b>: <code>n!</code> - факториал числа n
</li>
</ul>
<h2>Примеры арифметических выражений</h2>
<ul>
<li>
<code>(a + b) × c</code> - произведение суммы a и b на c
</li>
<li>
<code>a^2 + b^2</code> - сумма квадратов a и b
</li>
<li>
<code>|x - y|</code> - абсолютная разность x и y
</li>
<li>
<code>min(a, b) + max(c, d)</code> - сумма минимума a и b с максимумом c и d
</li>
</ul>
<h2>Типизация арифметических выражений</h2>
<p>
Все арифметические выражения имеют типизацию <code>Z</code> (целые числа). Результат арифметической операции
всегда является целым числом.
</p>
<h2>Применение в концептуальных схемах</h2>
<p>
Арифметические выражения используются для определения числовых характеристик объектов предметной области,
вычисления количественных показателей и формулировки числовых ограничений в аксиомах и теоремах.
</p>
</div>
);
}

View File

@ -0,0 +1,97 @@
export function HelpRSLangExpressionDeclarative() {
return (
<div>
<h1>Декларативные выражения</h1>
<p>
Декларативные выражения в языке родов структур используются для определения понятий через их свойства и
характеристики. Эти выражения описывают "что есть" объект, а не "как его получить".
</p>
<h2>Основные типы декларативных выражений</h2>
<ul>
<li>
<b>Определение через свойства</b>: <code>{'A = {x | P(x)}'}</code> - A есть множество всех x, обладающих
свойством P
</li>
<li>
<b>Определение через равенство</b>: <code>A = B</code> - A равно B по определению
</li>
<li>
<b>Определение через включение</b>: <code>A B</code> - A является подмножеством B
</li>
<li>
<b>Аксиоматическое определение</b>: <code>x A: P(x)</code> - для всех x из A выполняется свойство P
</li>
</ul>
<h2>Структура декларативных определений</h2>
<ul>
<li>
<b>Определяемый объект</b>: понятие, которое определяется
</li>
<li>
<b>Определяющие свойства</b>: характеристики, которые задают определяемый объект
</li>
<li>
<b>Область определения</b>: множество, в рамках которого происходит определение
</li>
<li>
<b>Условия корректности</b>: ограничения, обеспечивающие корректность определения
</li>
</ul>
<h2>Примеры декларативных выражений</h2>
<ul>
<li>
<code>{'EVEN = {x ∈ Z | x mod 2 = 0}'}</code> - четные числа есть множество целых чисел, делящихся на 2
</li>
<li>
<code>{'PRIME = {x ∈ N | x > 1 ∧ ∀y ∈ N: y | x → y = 1 y = x}'}</code> - простые числа
</li>
<li>
<code>x A: x B x C</code> - все элементы A, принадлежащие B, принадлежат также C
</li>
<li>
<code>{'MAX = {x ∈ A | ∀y ∈ A: y ≤ x}'}</code> - максимум множества A
</li>
</ul>
<h2>Свойства декларативных определений</h2>
<ul>
<li>
<b>Ясность</b>: определение должно однозначно определять объект
</li>
<li>
<b>Непротиворечивость</b>: определение не должно содержать логических противоречий
</li>
<li>
<b>Полнота</b>: определение должно содержать все необходимые характеристики
</li>
<li>
<b>Минимальность</b>: определение не должно содержать избыточных условий
</li>
</ul>
<h2>Типизация декларативных выражений</h2>
<p>Декларативные выражения могут иметь различные типизации в зависимости от типа определяемого объекта:</p>
<ul>
<li>
Определения множеств имеют типизацию <code>(H)</code>
</li>
<li>
Определения свойств имеют типизацию <b>Logic</b>
</li>
<li>
Определения отношений имеют типизацию <code>(H × H × ... × Hₙ)</code>
</li>
</ul>
<h2>Применение в концептуальных схемах</h2>
<p>
Декларативные выражения используются для определения понятий в концептуальных схемах, формулировки аксиом и
теорем, а также для описания свойств объектов предметной области. Они составляют основу формального описания
концептуальных схем.
</p>
</div>
);
}

View File

@ -0,0 +1,98 @@
export function HelpRSLangExpressionImperative() {
return (
<div>
<h1>Императивные выражения</h1>
<p>
Императивные выражения в языке родов структур используются для задания множеств через последовательность
действий или операций. Эти выражения описывают "как получить" объект, а не "что он есть".
</p>
<h2>Основные императивные конструкции</h2>
<ul>
<li>
<b>Последовательность операций</b>: <code>op; op; ...; opₙ</code> - выполнение операций в заданном порядке
</li>
<li>
<b>Условные операции</b>: <code>if P then op else op</code> - условное выполнение операций
</li>
<li>
<b>Циклические операции</b>: <code>while P do op</code> - повторение операции пока выполняется условие P
</li>
<li>
<b>Присваивание</b>: <code>x := expr</code> - присваивание значения выражения переменной
</li>
</ul>
<h2>Операции построения множеств</h2>
<ul>
<li>
<b>Добавление элемента</b>: <code>{'A := A {x}'}</code> - добавление элемента x к множеству A
</li>
<li>
<b>Удаление элемента</b>: <code>{'A := A {x}'}</code> - удаление элемента x из множества A
</li>
<li>
<b>Объединение множеств</b>: <code>A := A B</code> - объединение множеств A и B
</li>
<li>
<b>Пересечение множеств</b>: <code>A := A B</code> - пересечение множеств A и B
</li>
</ul>
<h2>Примеры императивных выражений</h2>
<ul>
<li>
<code>{'result := ∅; for x ∈ A do if P(x) then result := result {x}'}</code> - построение множества
элементов A, удовлетворяющих условию P
</li>
<li>
<code>sum := 0; for x A do sum := sum + x</code> - вычисление суммы элементов множества A
</li>
<li>
<code>{'max := first(A); for x ∈ A do if x > max then max := x'}</code> - поиск максимального элемента в A
</li>
<li>
<code>{'B := ∅; while A ≠ ∅ do {x := choose(A); B := B {f(x)}; A := A {x}}'}</code> - применение функции f
к элементам A
</li>
</ul>
<h2>Свойства императивных выражений</h2>
<ul>
<li>
<b>Детерминированность</b>: результат должен быть однозначно определен
</li>
<li>
<b>Корректность</b>: операции должны быть корректными для заданных типов данных
</li>
<li>
<b>Завершаемость</b>: императивное выражение должно завершаться за конечное число шагов
</li>
<li>
<b>Эффективность</b>: выражение должно быть эффективным с точки зрения вычислительных ресурсов
</li>
</ul>
<h2>Типизация императивных выражений</h2>
<p>Императивные выражения могут иметь различные типизации в зависимости от результата выполнения:</p>
<ul>
<li>
Построение множеств имеет типизацию <code>(H)</code>
</li>
<li>
Вычисление значений имеет типизацию <code>H</code>
</li>
<li>
Логические операции имеют типизацию <b>Logic</b>
</li>
</ul>
<h2>Применение в концептуальных схемах</h2>
<p>
Императивные выражения используются для определения алгоритмов построения множеств, вычисления характеристик
объектов и реализации операций над данными в концептуальных схемах. Они позволяют задавать конструктивные
способы получения объектов.
</p>
</div>
);
}

View File

@ -0,0 +1,81 @@
export function HelpRSLangExpressionLogic() {
return (
<div>
<h1>Логические выражения</h1>
<p>
Логические выражения в языке родов структур возвращают логическое значение ИСТИНА или ЛОЖЬ. Они используются для
формулировки аксиом, теорем и условий.
</p>
<h2>Основные логические операторы</h2>
<ul>
<li>
<b>Отрицание</b>: <code>¬P</code> или <code>!P</code> - "не P"
</li>
<li>
<b>Конъюнкция</b>: <code>P Q</code> или <code>P && Q</code> - "P и Q"
</li>
<li>
<b>Дизъюнкция</b>: <code>P Q</code> или <code>P || Q</code> - "P или Q"
</li>
<li>
<b>Импликация</b>: <code>P Q</code> или <code>{'P => Q'}</code> - "если P, то Q"
</li>
<li>
<b>Эквивалентность</b>: <code>P Q</code> или <code>{'P <=> Q'}</code> - "P эквивалентно Q"
</li>
</ul>
<h2>Кванторы</h2>
<ul>
<li>
<b>Универсальный квантор</b>: <code>x A: P(x)</code> - "для всех x из A выполняется P(x)"
</li>
<li>
<b>Экзистенциальный квантор</b>: <code>x A: P(x)</code> - "существует x из A такой, что P(x)"
</li>
<li>
<b>Единственность</b>: <code>!x A: P(x)</code> - "существует единственный x из A такой, что P(x)"
</li>
</ul>
<h2>Теоретико-множественные предикаты</h2>
<ul>
<li>
<b>Принадлежность</b>: <code>x A</code> - "x принадлежит множеству A"
</li>
<li>
<b>Непринадлежность</b>: <code>x A</code> - "x не принадлежит множеству A"
</li>
<li>
<b>Включение</b>: <code>A B</code> - "A является подмножеством B"
</li>
<li>
<b>Строгое включение</b>: <code>A B</code> - "A является собственным подмножеством B"
</li>
<li>
<b>Равенство множеств</b>: <code>A = B</code> - "множества A и B равны"
</li>
</ul>
<h2>Примеры логических выражений</h2>
<ul>
<li>
<code>x A: x B</code> - "все элементы A принадлежат B"
</li>
<li>
<code>x A: P(x) Q(x)</code> - "существует элемент x из A, для которого выполняются P(x) и Q(x)"
</li>
<li>
<code>A B B A A = B</code> - "если A включено в B и B включено в A, то A равно B"
</li>
</ul>
<h2>Типизация логических выражений</h2>
<p>
Все логические выражения имеют типизацию <b>Logic</b> и могут использоваться в качестве аксиом, теорем или
условий в определениях конституент.
</p>
</div>
);
}

View File

@ -0,0 +1,119 @@
export function HelpRSLangExpressionParameter() {
return (
<div>
<h1>Параметризованные выражения</h1>
<p>
Параметризованные выражения в языке родов структур позволяют создавать шаблоны выражений, которые могут быть
применены к различным наборам параметров. Такие выражения используются в определениях терм-функций и
предикат-функций.
</p>
<h2>Основные типы параметризованных выражений</h2>
<ul>
<li>
<b>Параметризованная функция</b>: <code>f(x, x, ..., xₙ) = expr</code> - функция с параметрами
</li>
<li>
<b>Параметризованный предикат</b>: <code>P(x, x, ..., xₙ) = condition</code> - предикат с параметрами
</li>
<li>
<b>Шаблонное выражение</b>: <code>template(param, param, ...)</code> - шаблон с параметрами
</li>
<li>
<b>Параметризованное множество</b>: <code>{'A(param) = {x | P(x, param)}'}</code> - множество, зависящее от
параметра
</li>
</ul>
<h2>Типы параметров</h2>
<ul>
<li>
<b>Формальные параметры</b>: параметры в определении функции или предиката
</li>
<li>
<b>Фактические параметры</b>: конкретные значения, подставляемые при вызове
</li>
<li>
<b>Типизированные параметры</b>: параметры с указанием их типизации
</li>
<li>
<b>Шаблонные параметры</b>: параметры, которые могут принимать различные типы
</li>
</ul>
<h2>Примеры параметризованных выражений</h2>
<ul>
<li>
<code>sum(x, y) = x + y</code> - функция сложения двух чисел
</li>
<li>
<code>{'is_greater(x, y) = x > y'}</code> - предикат сравнения
</li>
<li>
<code>power(base, exp) = if exp = 0 then 1 else base × power(base, exp-1)</code> - возведение в степень
</li>
<li>
<code>{'filter(A, P) = {x ∈ A | P(x)}'}</code> - фильтрация множества по предикату
</li>
</ul>
<h2>Шаблонные параметры</h2>
<ul>
<li>
<b>R, R, ..., Rᵢ</b> - обозначения для произвольных ступеней
</li>
<li>
<b>Определение по месту</b>: типизация определяется исходя из контекста использования
</li>
<li>
<b>Универсальность</b>: шаблон может применяться к различным типам данных
</li>
<li>
<b>Проверка совместимости</b>: система проверяет корректность применения шаблона
</li>
</ul>
<h2>Типизация параметризованных выражений</h2>
<p>
Параметризованные выражения имеют типизацию вида <code>Hᵣ [H, H, ..., Hᵢ]</code>, где:
</p>
<ul>
<li>
<code>Hᵣ</code> - типизация результата
</li>
<li>
<code>H, H, ..., Hᵢ</code> - типизации аргументов
</li>
<li>
Для предикатов <code>Hᵣ = Logic</code>
</li>
<li>
Для функций <code>Hᵣ</code> определяется типом возвращаемого значения
</li>
</ul>
<h2>Применение параметров</h2>
<ul>
<li>
<b>Подстановка</b>: замена формальных параметров фактическими значениями
</li>
<li>
<b>Проверка типов</b>: проверка соответствия типов фактических параметров формальным
</li>
<li>
<b>Вычисление</b>: выполнение выражения с подставленными параметрами
</li>
<li>
<b>Результат</b>: получение результата с соответствующей типизацией
</li>
</ul>
<h2>Применение в концептуальных схемах</h2>
<p>
Параметризованные выражения используются для определения терм-функций и предикат-функций в концептуальных
схемах. Они позволяют создавать универсальные шаблоны, которые могут применяться к различным объектам предметной
области.
</p>
</div>
);
}

View File

@ -0,0 +1,96 @@
export function HelpRSLangExpressionQuantor() {
return (
<div>
<h1>Кванторные выражения</h1>
<p>
Кванторные выражения в языке родов структур позволяют формулировать утверждения о свойствах элементов множеств.
Кванторы связывают переменные и позволяют выражать логические утверждения о всех или некоторых элементах
множества.
</p>
<h2>Основные кванторы</h2>
<ul>
<li>
<b>Универсальный квантор</b>: <code>x A: P(x)</code> - "для всех x из A выполняется P(x)"
</li>
<li>
<b>Экзистенциальный квантор</b>: <code>x A: P(x)</code> - "существует x из A такой, что P(x)"
</li>
<li>
<b>Квантор единственности</b>: <code>!x A: P(x)</code> - "существует единственный x из A такой, что P(x)"
</li>
<li>
<b>Квантор существования и единственности</b>: <code>x A: P(x)</code> - альтернативная запись для !
</li>
</ul>
<h2>Связанные переменные</h2>
<ul>
<li>
<b>Связывание переменной</b>: переменная x в выражении <code>x A: P(x)</code> связана квантором
</li>
<li>
<b>Область действия квантора</b>: выражение P(x) является областью действия квантора
</li>
<li>
<b>Свободные переменные</b>: переменные, не связанные кванторами, называются свободными
</li>
</ul>
<h2>Множественные кванторы</h2>
<ul>
<li>
<b>Последовательные кванторы</b>: <code>x A y B: P(x, y)</code> - для всех x из A и всех y из B
</li>
<li>
<b>Смешанные кванторы</b>: <code>x A y B: P(x, y)</code> - для каждого x из A существует y из B
</li>
<li>
<b>Кванторы с условиями</b>: <code>x A: P(x) Q(x)</code> - для всех x из A, если P(x), то Q(x)
</li>
</ul>
<h2>Примеры кванторных выражений</h2>
<ul>
<li>
<code>x A: x B</code> - все элементы A принадлежат B
</li>
<li>
<code>{'∃x ∈ A: x > 0'}</code> - существует положительный элемент в A
</li>
<li>
<code>x A y B: x = f(y)</code> - для каждого x из A существует y из B такой, что x = f(y)
</li>
<li>
<code>!x A: P(x) Q(x)</code> - существует единственный x из A, для которого выполняются P(x) и Q(x)
</li>
</ul>
<h2>Отрицание кванторов</h2>
<ul>
<li>
<b>Отрицание универсального</b>: <code>¬(x A: P(x))</code> эквивалентно <code>x A: ¬P(x)</code>
</li>
<li>
<b>Отрицание экзистенциального</b>: <code>¬(x A: P(x))</code> эквивалентно <code>x A: ¬P(x)</code>
</li>
<li>
<b>Отрицание единственности</b>: <code>¬(!x A: P(x))</code> эквивалентно{' '}
<code>x A: ¬P(x) y A: P(y) x y</code>
</li>
</ul>
<h2>Типизация кванторных выражений</h2>
<p>
Все кванторные выражения имеют типизацию <b>Logic</b>, так как они возвращают логическое значение ИСТИНА или
ЛОЖЬ. Кванторы используются для формулировки аксиом, теорем и условий в определениях конституент.
</p>
<h2>Применение в концептуальных схемах</h2>
<p>
Кванторные выражения используются для формулировки общих свойств объектов предметной области, определения
отношений между понятиями и выражения универсальных закономерностей в рамках концептуальных схем.
</p>
</div>
);
}

View File

@ -0,0 +1,110 @@
export function HelpRSLangExpressionRecursive() {
return (
<div>
<h1>Рекурсивные выражения</h1>
<p>
Рекурсивные выражения в языке родов структур используются для определения множеств и функций через их
собственные определения. Рекурсия позволяет задавать бесконечные структуры и сложные зависимости.
</p>
<h2>Основные типы рекурсивных выражений</h2>
<ul>
<li>
<b>Рекурсивное определение множества</b>: <code>A = B f(A)</code> - множество A определяется через себя
</li>
<li>
<b>Рекурсивная функция</b>: <code>f(n) = if n = 0 then 1 else n × f(n-1)</code> - функция определяется через
себя
</li>
<li>
<b>Индуктивное определение</b>: <code>{'A = A₀ {f(x) | x ∈ A}'}</code> - множество строится индуктивно
</li>
<li>
<b>Трансфинитная рекурсия</b>: <code>{'A = {Aᵢ | i < α}'}</code> - объединение по ординалам
</li>
</ul>
<h2>Структура рекурсивных определений</h2>
<ul>
<li>
<b>Базовый случай</b>: начальное значение или базовое множество
</li>
<li>
<b>Рекурсивный случай</b>: правило построения новых элементов из существующих
</li>
<li>
<b>Условие завершения</b>: условие, обеспечивающее конечность процесса
</li>
<li>
<b>Монотонность</b>: свойство, гарантирующее корректность рекурсии
</li>
</ul>
<h2>Примеры рекурсивных выражений</h2>
<ul>
<li>
<code>{'N = {0} {n+1 | n ∈ N}'}</code> - индуктивное определение натуральных чисел
</li>
<li>
<code>fact(n) = if n = 0 then 1 else n × fact(n-1)</code> - факториал
</li>
<li>
<code>fib(n) = if n 1 then n else fib(n-1) + fib(n-2)</code> - числа Фибоначчи
</li>
<li>
<code>{'LIST = {nil} {cons(x, l) | x ∈ A, l ∈ LIST}'}</code> - список элементов из A
</li>
</ul>
<h2>Свойства рекурсивных выражений</h2>
<ul>
<li>
<b>Корректность</b>: рекурсивное определение должно быть корректным
</li>
<li>
<b>Завершаемость</b>: рекурсивный процесс должен завершаться
</li>
<li>
<b>Единственность</b>: результат должен быть однозначно определен
</li>
<li>
<b>Монотонность</b>: функция должна быть монотонной для корректности
</li>
</ul>
<h2>Принцип математической индукции</h2>
<p>Для доказательства свойств рекурсивно определенных объектов используется принцип математической индукции:</p>
<ul>
<li>
<b>База индукции</b>: доказательство свойства для базового случая
</li>
<li>
<b>Индуктивный шаг</b>: доказательство того, что если свойство выполняется для n, то оно выполняется для n+1
</li>
<li>
<b>Заключение</b>: свойство выполняется для всех объектов
</li>
</ul>
<h2>Типизация рекурсивных выражений</h2>
<p>Рекурсивные выражения могут иметь различные типизации:</p>
<ul>
<li>
Рекурсивные множества имеют типизацию <code>(H)</code>
</li>
<li>
Рекурсивные функции имеют типизацию <code>H H</code>
</li>
<li>
Рекурсивные предикаты имеют типизацию <b>Logic</b>
</li>
</ul>
<h2>Применение в концептуальных схемах</h2>
<p>
Рекурсивные выражения используются для определения сложных структур данных, бесконечных множеств и функций в
концептуальных схемах. Они позволяют описывать объекты с внутренней структурой и зависимостями.
</p>
</div>
);
}

View File

@ -0,0 +1,85 @@
export function HelpRSLangExpressionSet() {
return (
<div>
<h1>Операции с множествами</h1>
<p>
Теоретико-множественные выражения в языке родов структур позволяют создавать и манипулировать множествами.
Результатом таких выражений является множество элементов определенной ступени.
</p>
<h2>Основные операции с множествами</h2>
<ul>
<li>
<b>Объединение</b>: <code>A B</code> - множество всех элементов, принадлежащих A или B
</li>
<li>
<b>Пересечение</b>: <code>A B</code> - множество всех элементов, принадлежащих и A, и B
</li>
<li>
<b>Разность</b>: <code>A \ B</code> - множество всех элементов A, не принадлежащих B
</li>
<li>
<b>Симметрическая разность</b>: <code>A B</code> - множество элементов, принадлежащих ровно одному из A или
B
</li>
<li>
<b>Дополнение</b>: <code>A'</code> - множество всех элементов универсального множества, не принадлежащих A
</li>
</ul>
<h2>Конструкторы множеств</h2>
<ul>
<li>
<b>Перечисление</b>: <code>{'{a, b, c}'}</code> - множество из элементов a, b, c
</li>
<li>
<b>Выделение</b>: <code>{'{x ∈ A | P(x)}'}</code> - множество всех x из A, для которых выполняется P(x)
</li>
<li>
<b>Замена</b>: <code>{'{f(x) | x ∈ A}'}</code> - множество значений f(x) для всех x из A
</li>
<li>
<b>Декартово произведение</b>: <code>A × B</code> - множество всех пар (a, b), где a A, b B
</li>
<li>
<b>Множество всех подмножеств</b>: <code>(A)</code> - множество всех подмножеств A
</li>
</ul>
<h2>Специальные множества</h2>
<ul>
<li>
<b>Пустое множество</b>: <code></code> - множество, не содержащее элементов
</li>
<li>
<b>Универсальное множество</b>: <code>U</code> - множество всех элементов рассматриваемой области
</li>
<li>
<b>Синглтон</b>: <code>{'{a}'}</code> - множество, содержащее только элемент a
</li>
</ul>
<h2>Примеры выражений</h2>
<ul>
<li>
<code>A (B C)</code> - объединение A с пересечением B и C
</li>
<li>
<code>{'{x ∈ A | x > 0}'}</code> - множество всех положительных элементов из A
</li>
<li>
<code>{'{x² | x ∈ {1, 2, 3}}'}</code> - множество {'{(1, 4, 9)}'}
</li>
<li>
<code>A × B × C</code> - множество всех троек (a, b, c)
</li>
</ul>
<h2>Типизация множеств</h2>
<p>
Множество имеет типизацию <code>(H)</code>, где H - ступень элементов множества. Например, множество целых
чисел имеет типизацию <code>(Z)</code>.
</p>
</div>
);
}

View File

@ -0,0 +1,78 @@
export function HelpRSLangExpressionStructure() {
return (
<div>
<h1>Структурные выражения</h1>
<p>
Структурные выражения в языке родов структур позволяют манипулировать ступенями операндов. Эти выражения
используются для изменения структуры данных и создания новых типов на основе существующих.
</p>
<h2>Основные структурные операции</h2>
<ul>
<li>
<b>Кортеж</b>: <code>(H, H, ..., Hₙ)</code> - ступень кортежа арности n
</li>
<li>
<b>Проекция</b>: <code>π(t)</code> - извлечение i-го элемента кортежа t
</li>
<li>
<b>Конкатенация кортежей</b>: <code>t t</code> - объединение двух кортежей
</li>
<li>
<b>Структурирование</b>: <code>struct(field: H, field: H, ...)</code> - создание структуры с именованными
полями
</li>
</ul>
<h2>Операции с множествами структур</h2>
<ul>
<li>
<b>Декартово произведение ступеней</b>: <code>H × H × ... × Hₙ</code> - ступень n-арных кортежей
</li>
<li>
<b>Степень ступени</b>: <code>Hⁿ</code> - n-арное произведение ступени H на себя
</li>
<li>
<b>Множество кортежей</b>: <code>(H × H × ... × Hₙ)</code> - множество n-арных кортежей
</li>
</ul>
<h2>Примеры структурных выражений</h2>
<ul>
<li>
<code>(Z, Z)</code> - ступень пар целых чисел
</li>
<li>
<code>(Z × Z)</code> - множество пар целых чисел
</li>
<li>
<code>π((x, y))</code> - извлечение первого элемента кортежа
</li>
<li>
<code>struct(name: Z, age: Z)</code> - структура с полями name и age типа целых чисел
</li>
</ul>
<h2>Типизация структурных выражений</h2>
<p>Результат структурного выражения имеет типизацию, определяемую операцией:</p>
<ul>
<li>
Кортеж имеет типизацию <code>(H, H, ..., Hₙ)</code>
</li>
<li>
Проекция кортежа имеет типизацию <code>Hᵢ</code>
</li>
<li>
Множество кортежей имеет типизацию <code>(H × H × ... × Hₙ)</code>
</li>
</ul>
<h2>Применение в концептуальных схемах</h2>
<p>
Структурные выражения используются для определения сложных типов данных в концептуальных схемах, таких как
записи, кортежи и структурированные множества. Они позволяют создавать формальные описания сложных объектов
предметной области.
</p>
</div>
);
}

View File

@ -10,7 +10,7 @@ export function HelpRSLangInterpret() {
содержания и схемных терминов и определений. Для этого в соответствии с{' '}
<LinkTopic text='конвенциями' topic={HelpTopic.CC_CONSTITUENTA} /> вводятся списки объектов предметной области,
соответствующих неопределяемым понятиям. При этом обеспечивается корректность отношений{' '}
<LinkTopic text='типизации' topic={HelpTopic.RSL_TYPES} /> для родовых структур.
<LinkTopic text='типизации' topic={HelpTopic.RSL_TYPIFICATION} /> для родовых структур.
</p>
<p>
Интерпретация производных понятий может быть задана внешними методами либо автоматически вычислена с помощью

View File

@ -0,0 +1,63 @@
import { LinkTopic } from '../../components/link-topic';
import { HelpTopic } from '../../models/help-topic';
export function HelpRSLangLiterals() {
return (
<div>
<h1>Идентификаторы и литералы</h1>
<p>
В языке родов структур идентификаторы и литералы имеют строгие правила записи, определяющие их роль в выражениях
и обеспечивающие однозначность интерпретации.
</p>
<h2>Правила написания идентификаторов</h2>
<ul>
<li>
<b>Понятия</b> идентификаторы, начинающиеся с заглавной латинской буквы, соответствующей типу{' '}
<LinkTopic topic={HelpTopic.CC_CONSTITUENTA} text='конституенты' />: <code>X1</code>,<code>F11</code>,{' '}
<code>D24</code>.
</li>
<li>
<b>Радикалы</b> обозначения для произвольных типизаций, используемые в{' '}
<LinkTopic topic={HelpTopic.RSL_EXPRESSION_PARAMETER} text='шаблонных выражениях' /> идентификаторы,
начинающиеся с буквы R.
</li>
<li>
<b>Переменные</b> идентификаторы, начинающиеся со строчной греческой или латинской буквы, например:
<code>ξ</code>, <code>μ2</code>, <code>y1</code>.
</li>
<li>
<b>Специальные идентификаторы</b> зарезервированные слова и обозначения, имеющие фиксированное значение в
языке.
</li>
</ul>
<h2>Литералы</h2>
<p>
Литералы задают фиксированные значения в выражениях. В языке родов структур используются следующие виды
литералов:
</p>
<ul>
<li>
<b>Целые числа</b> последовательность цифр. Отрицательные числа не поддерживаются:
<code>0</code>, <code>42</code>.
</li>
<li>
<b>Множество целых чисел</b> символ <code>Z</code>.
</li>
<li>
<b>Пустое множество</b> символ <code></code>.
</li>
</ul>
<h2>Примеры</h2>
<p>
Пример использования переменной и понятия: <code>x X1</code>, где <code>x</code> переменная, а{' '}
<code>X1</code> понятие.
</p>
<p>
Пример с литералами: <code>card(X1) = 5</code>.
</p>
</div>
);
}

View File

@ -47,7 +47,7 @@ export function HelpRSLangOperations() {
</h2>
<p>
Порождение полной совокупности термов, раскрывающих структуру выбранной конституенты. Операция применима к
терм-функциям, термам и родовым структурам с <LinkTopic text='типизацией' topic={HelpTopic.RSL_TYPES} />{' '}
терм-функциям, термам и родовым структурам с <LinkTopic text='типизацией' topic={HelpTopic.RSL_TYPIFICATION} />{' '}
множество и кортеж.
<br />
<code>{'Generate(S1∈(X1×(X1))) = {Pr1(S1), Pr2(S1), red(Pr2(S1))}'}</code>

View File

@ -1,4 +1,4 @@
export function HelpRSLangTypes() {
export function HelpRSLangTypification() {
return (
<div>
<h1>Типизация</h1>

View File

@ -31,7 +31,17 @@ const labelHelpTopicRecord: Record<HelpTopic, string> = {
[HelpTopic.CC_PROPAGATION]: 'Сквозные изменения',
[HelpTopic.RSLANG]: '🚀 Экспликация',
[HelpTopic.RSL_TYPES]: 'Типизация',
[HelpTopic.RSL_LITERALS]: 'Идентификаторы',
[HelpTopic.RSL_TYPIFICATION]: 'Типизация',
[HelpTopic.RSL_EXPRESSION_LOGIC]: 'Логические выражения',
[HelpTopic.RSL_EXPRESSION_SET]: 'Операции с множествами',
[HelpTopic.RSL_EXPRESSION_STRUCTURE]: 'Структурные выражения',
[HelpTopic.RSL_EXPRESSION_ARITHMETIC]: 'Арифметика',
[HelpTopic.RSL_EXPRESSION_QUANTOR]: 'Кванторные конструкции',
[HelpTopic.RSL_EXPRESSION_DECLARATIVE]: 'Декларативные',
[HelpTopic.RSL_EXPRESSION_IMPERATIVE]: 'Императивные',
[HelpTopic.RSL_EXPRESSION_RECURSIVE]: 'Рекурсивные',
[HelpTopic.RSL_EXPRESSION_PARAMETER]: 'Параметризованные',
[HelpTopic.RSL_CORRECT]: 'Переносимость',
[HelpTopic.RSL_INTERPRET]: 'Интерпретируемость',
[HelpTopic.RSL_OPERATIONS]: 'Операции',
@ -82,7 +92,17 @@ const describeHelpTopicRecord: Record<HelpTopic, string> = {
[HelpTopic.CC_PROPAGATION]: 'сквозные изменения в ОСС',
[HelpTopic.RSLANG]: 'экспликация и язык родов структур',
[HelpTopic.RSL_TYPES]: 'система типов в <br/>родоструктурной экспликации',
[HelpTopic.RSL_LITERALS]: 'обозначения конституент,<br/>локальных переменных и литералов',
[HelpTopic.RSL_TYPIFICATION]: 'система типов в <br/>родоструктурной экспликации',
[HelpTopic.RSL_EXPRESSION_LOGIC]: 'логические выражения',
[HelpTopic.RSL_EXPRESSION_SET]: 'операции с множествами',
[HelpTopic.RSL_EXPRESSION_STRUCTURE]: 'операции со ступенями',
[HelpTopic.RSL_EXPRESSION_ARITHMETIC]: 'арифметические выражения',
[HelpTopic.RSL_EXPRESSION_QUANTOR]: 'кванторные конструкции',
[HelpTopic.RSL_EXPRESSION_DECLARATIVE]: 'декларативные выражения',
[HelpTopic.RSL_EXPRESSION_IMPERATIVE]: 'императивные выражения',
[HelpTopic.RSL_EXPRESSION_RECURSIVE]: 'рекурсивные выражения',
[HelpTopic.RSL_EXPRESSION_PARAMETER]: 'выражения с внешними параметрами',
[HelpTopic.RSL_CORRECT]: 'биективная переносимость',
[HelpTopic.RSL_INTERPRET]: 'интерпретация определений <br/>и утверждений',
[HelpTopic.RSL_OPERATIONS]: 'формальные операции',

View File

@ -32,7 +32,17 @@ export const HelpTopic = {
CC_PROPAGATION: 'concept-change-propagation',
RSLANG: 'rslang',
RSL_TYPES: 'rslang-types',
RSL_LITERALS: 'rslang-literals',
RSL_TYPIFICATION: 'rslang-typification',
RSL_EXPRESSION_LOGIC: 'rslang-expression-logic',
RSL_EXPRESSION_SET: 'rslang-expression-set',
RSL_EXPRESSION_STRUCTURE: 'rslang-expression-structure',
RSL_EXPRESSION_ARITHMETIC: 'rslang-expression-arithmetic',
RSL_EXPRESSION_QUANTOR: 'rslang-expression-quantor',
RSL_EXPRESSION_DECLARATIVE: 'rslang-expression-declarative',
RSL_EXPRESSION_IMPERATIVE: 'rslang-expression-imperative',
RSL_EXPRESSION_RECURSIVE: 'rslang-expression-recursive',
RSL_EXPRESSION_PARAMETER: 'rslang-expression-parameter',
RSL_CORRECT: 'rslang-correctness',
RSL_INTERPRET: 'rslang-interpretation',
RSL_OPERATIONS: 'rslang-operations',
@ -88,7 +98,17 @@ export const topicParent = new Map<HelpTopic, HelpTopic>([
[HelpTopic.CC_PROPAGATION, HelpTopic.CONCEPTUAL],
[HelpTopic.RSLANG, HelpTopic.RSLANG],
[HelpTopic.RSL_TYPES, HelpTopic.RSLANG],
[HelpTopic.RSL_LITERALS, HelpTopic.RSLANG],
[HelpTopic.RSL_TYPIFICATION, HelpTopic.RSLANG],
[HelpTopic.RSL_EXPRESSION_LOGIC, HelpTopic.RSLANG],
[HelpTopic.RSL_EXPRESSION_SET, HelpTopic.RSLANG],
[HelpTopic.RSL_EXPRESSION_STRUCTURE, HelpTopic.RSLANG],
[HelpTopic.RSL_EXPRESSION_ARITHMETIC, HelpTopic.RSLANG],
[HelpTopic.RSL_EXPRESSION_QUANTOR, HelpTopic.RSLANG],
[HelpTopic.RSL_EXPRESSION_DECLARATIVE, HelpTopic.RSLANG],
[HelpTopic.RSL_EXPRESSION_IMPERATIVE, HelpTopic.RSLANG],
[HelpTopic.RSL_EXPRESSION_RECURSIVE, HelpTopic.RSLANG],
[HelpTopic.RSL_EXPRESSION_PARAMETER, HelpTopic.RSLANG],
[HelpTopic.RSL_CORRECT, HelpTopic.RSLANG],
[HelpTopic.RSL_INTERPRET, HelpTopic.RSLANG],
[HelpTopic.RSL_OPERATIONS, HelpTopic.RSLANG],

View File

@ -23,10 +23,20 @@ import { HelpContributors } from '../../items/info/help-contributors';
import { HelpPrivacy } from '../../items/info/help-privacy';
import { HelpRules } from '../../items/info/help-rules';
import { HelpRSLangCorrect } from '../../items/rslang/help-rslang-correct';
import { HelpRSLangExpressionArithmetic } from '../../items/rslang/help-rslang-expression-arithmetic';
import { HelpRSLangExpressionDeclarative } from '../../items/rslang/help-rslang-expression-declarative';
import { HelpRSLangExpressionImperative } from '../../items/rslang/help-rslang-expression-imperative';
import { HelpRSLangExpressionLogic } from '../../items/rslang/help-rslang-expression-logic';
import { HelpRSLangExpressionParameter } from '../../items/rslang/help-rslang-expression-parameter';
import { HelpRSLangExpressionQuantor } from '../../items/rslang/help-rslang-expression-quantor';
import { HelpRSLangExpressionRecursive } from '../../items/rslang/help-rslang-expression-recursive';
import { HelpRSLangExpressionSet } from '../../items/rslang/help-rslang-expression-set';
import { HelpRSLangExpressionStructure } from '../../items/rslang/help-rslang-expression-structure';
import { HelpRSLangInterpret } from '../../items/rslang/help-rslang-interpret';
import { HelpRSLangLiterals } from '../../items/rslang/help-rslang-literals';
import { HelpRSLangOperations } from '../../items/rslang/help-rslang-operations';
import { HelpRSLangTemplates } from '../../items/rslang/help-rslang-templates';
import { HelpRSLangTypes } from '../../items/rslang/help-rslang-types';
import { HelpRSLangTypification } from '../../items/rslang/help-rslang-typification';
import { HelpCstClass } from '../../items/ui/help-cst-class';
import { HelpCstStatus } from '../../items/ui/help-cst-status';
import { HelpFormulaTree } from '../../items/ui/help-formula-tree';
@ -86,7 +96,17 @@ export function TopicPage({ topic }: TopicPageProps) {
if (topic === HelpTopic.CC_PROPAGATION) return <HelpConceptPropagation />;
if (topic === HelpTopic.RSLANG) return <HelpRSLang />;
if (topic === HelpTopic.RSL_TYPES) return <HelpRSLangTypes />;
if (topic === HelpTopic.RSL_LITERALS) return <HelpRSLangLiterals />;
if (topic === HelpTopic.RSL_TYPIFICATION) return <HelpRSLangTypification />;
if (topic === HelpTopic.RSL_EXPRESSION_LOGIC) return <HelpRSLangExpressionLogic />;
if (topic === HelpTopic.RSL_EXPRESSION_SET) return <HelpRSLangExpressionSet />;
if (topic === HelpTopic.RSL_EXPRESSION_STRUCTURE) return <HelpRSLangExpressionStructure />;
if (topic === HelpTopic.RSL_EXPRESSION_ARITHMETIC) return <HelpRSLangExpressionArithmetic />;
if (topic === HelpTopic.RSL_EXPRESSION_QUANTOR) return <HelpRSLangExpressionQuantor />;
if (topic === HelpTopic.RSL_EXPRESSION_DECLARATIVE) return <HelpRSLangExpressionDeclarative />;
if (topic === HelpTopic.RSL_EXPRESSION_IMPERATIVE) return <HelpRSLangExpressionImperative />;
if (topic === HelpTopic.RSL_EXPRESSION_RECURSIVE) return <HelpRSLangExpressionRecursive />;
if (topic === HelpTopic.RSL_EXPRESSION_PARAMETER) return <HelpRSLangExpressionParameter />;
if (topic === HelpTopic.RSL_CORRECT) return <HelpRSLangCorrect />;
if (topic === HelpTopic.RSL_INTERPRET) return <HelpRSLangInterpret />;
if (topic === HelpTopic.RSL_OPERATIONS) return <HelpRSLangOperations />;