D: Update docs for RS language

This commit is contained in:
Ivan 2025-08-18 22:29:05 +03:00
parent 1d182f4417
commit 14cda60b0d
12 changed files with 382 additions and 638 deletions

View File

@ -193,6 +193,8 @@
"Бурбакизатор",
"Версионирование",
"Владельцом",
"генемные",
"дебуль",
"Демешко",
"Десинглетон",
"доксинг",
@ -214,6 +216,9 @@
"Кучкаров",
"Кучкарова",
"мультиграфа",
"мультииндекс",
"Мультииндексы",
"Мультифильтр",
"неинтерпретируемый",
"неитерируемого",
"Никанорова",
@ -230,6 +235,7 @@
"подпапках",
"Присакарь",
"ПРОКСИМА",
"родовидовое",
"Родоструктурная",
"родоструктурного",
"Родоструктурное",

View File

@ -2,98 +2,62 @@ export function HelpRSLangExpressionArithmetic() {
return (
<div>
<h1>Арифметические выражения</h1>
<p>
Арифметические выражения в языке родов структур позволяют выполнять математические операции над числовыми
данными. Эти выражения работают с целыми числами и возвращают числовые результаты.
</p>
<p>Арифметические выражения в языке родов структур предназначены для работы с целыми числами.</p>
<h2>Основные арифметические операции</h2>
<h2>Основные операции</h2>
<p>
Данные операции формируют теоретико-множественное выражение, которое имеет типизацию <code>Z</code> (целое
число).
</p>
<ul>
<li>
<b>Сложение</b>: <code>a + b</code> - сумма чисел a и b
<b>Сложение</b>: <code>a + b</code> сумма чисел <code>a</code> и <code>b</code>.
</li>
<li>
<b>Вычитание</b>: <code>a - b</code> - разность чисел a и b
<b>Вычитание</b>: <code>a - b</code> разность чисел <code>a</code> и <code>b</code>.
</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
<b>Умножение</b>: <code>a * b</code> произведение чисел <code>a</code> и <code>b</code>.
</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> (целые числа). Результат арифметической операции
всегда является целым числом.
Данные операции формируют логическое выражение, которое имеет типизацию <code>Logic</code>.
</p>
<ul>
<li>
<b>Меньше</b>: <code>a &lt; b</code>
</li>
<li>
<b>Меньше или равно</b>: <code>a b</code>
</li>
<li>
<b>Больше</b>: <code>a &gt; b</code>
</li>
<li>
<b>Больше или равно</b>: <code>a b</code>
</li>
</ul>
<h2>Вычисление мощности</h2>
<p>
<b>Мощность множества</b>: <code>card(X1)</code> количество элементов множества <code>X</code>. Так как на
практике используются только конечные множества, мощность всегда является целым числом.
</p>
<h2>Применение в концептуальных схемах</h2>
<p>
Арифметические выражения используются для определения числовых характеристик объектов предметной области,
вычисления количественных показателей и формулировки числовых ограничений в аксиомах и теоремах.
</p>
<h2>Примеры</h2>
<ul>
<li>
<code>(4 + 5) * 3</code>
</li>
<li>
<code>card(X1) &gt; 5</code>
</li>
<li>
<code>x y + 1</code>
</li>
</ul>
</div>
);
}

View File

@ -1,96 +1,44 @@
import { LinkTopic } from '../../components/link-topic';
import { HelpTopic } from '../../models/help-topic';
export function HelpRSLangExpressionDeclarative() {
return (
<div>
<h1>Декларативные выражения</h1>
<p>
Декларативные выражения в языке родов структур используются для определения понятий через их свойства и
характеристики. Эти выражения описывают "что есть" объект, а не "как его получить".
Декларативная конструкция, также известная как схема ограниченного выделения, в языке родов структур задает
множество через перебираемое множество и проверяемое условие. С точки зрения определения понятий такие выражения
задают родовидовое определение.
</p>
<p>
<LinkTopic topic={HelpTopic.RSL_TYPIFICATION} text='Типизация' /> конструкции совпадает с типизацией множества,
из которого происходит отбор.
</p>
<h2>Основные типы декларативных выражений</h2>
<h2>Синтаксис</h2>
<ul>
<li>
<b>Определение через свойства</b>: <code>{'A = {x | P(x)}'}</code> - A есть множество всех x, обладающих
свойством P
<code>D{'{ξ∈ТМВ | ЛВ(ξ)}'}</code>
</li>
<li>
<b>Определение через равенство</b>: <code>A = B</code> - A равно B по определению
<code>D{'{(ξ₁, ξ₂)∈ТМВ | ЛВ(ξ₁, ξ₂)}'}</code>
</li>
<li>
<b>Определение через включение</b>: <code>A B</code> - A является подмножеством B
</li>
<li>
<b>Аксиоматическое определение</b>: <code>x A: P(x)</code> - для всех x из A выполняется свойство P
Буква <code>D</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>{'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>
<h2>Семантика</h2>
<p>
Декларативные выражения используются для определения понятий в концептуальных схемах, формулировки аксиом и
теорем, а также для описания свойств объектов предметной области. Они составляют основу формального описания
концептуальных схем.
Локальные переменные перебирают свою область определения. Если для текущего значения переменной логическое
выражение справа истинно, то это значение (или кортеж значений) включается в результирующее множество.
</p>
<h2>Пример</h2>
<p>
<code>
D{'{ξ∈{1, 2, 3, 4, 5, 6} | ∃σ∈{10, 11, 12} (σ = 2 ξ)}'} = {'{5, 6}'}
</code>
</p>
</div>
);

View File

@ -1,97 +1,70 @@
import { LinkTopic } from '../../components/link-topic';
import { HelpTopic } from '../../models/help-topic';
export function HelpRSLangExpressionImperative() {
return (
<div>
<h1>Императивные выражения</h1>
<p>
Императивные выражения в языке родов структур используются для задания множеств через последовательность
действий или операций. Эти выражения описывают "как получить" объект, а не "что он есть".
Императивная конструкция в языке родов структур является теоретико-множественным выражением, построенным с
помощью блоков и правил вычисления. Она выражает конструктивные (генемные) способы определения понятий.
</p>
<p>
Императивная конструкция может быть преобразовано в эквивалентную с точки зрения теории множеств{' '}
<LinkTopic topic={HelpTopic.RSL_EXPRESSION_DECLARATIVE} text='декларативную конструкцию' />, что обосновывает ее
теоретические свойства. Однако использование императивной конструкции при экспликации отличается от
декларативной тем, что позволяет выражать другие типы определений и точно указывает способ интерпретации
понятия.
</p>
<h2>Основные императивные конструкции</h2>
<h2>Синтаксис</h2>
<ul>
<li>
<b>Последовательность операций</b>: <code>op; op; ...; opₙ</code> - выполнение операций в заданном порядке
<code>I{'{ТМВ(ξ1, ξ2) | ξ1ТМВ1; ξ2≔ТМВ2; ξkТМВk; ЛВ(ξ1,ξ2); ...}'}</code>
</li>
<li>
<b>Условные операции</b>: <code>if P then op else op</code> - условное выполнение операций
Буква <code>D</code> часть синтаксиса, а не идентификатор.
</li>
<li>
<b>Циклические операции</b>: <code>while P do op</code> - повторение операции пока выполняется условие P
Левая часть выражение <code>ТМВ(ξ1, ..., ξk)</code>, которое задаёт результирующий элемент, из которых
формируется множества.
</li>
<li>
<b>Присваивание</b>: <code>x := expr</code> - присваивание значения выражения переменной
Правая часть последовательность блоков, разделённых точкой с запятой. Блоки рассматриваются слева направо.
</li>
</ul>
<h2>Операции построения множеств</h2>
<h2>Блоки правой части</h2>
<ul>
<li>
<b>Добавление элемента</b>: <code>{'A := A {x}'}</code> - добавление элемента x к множеству A
<b>Перебор</b>
<code> </code>
объявленная переменная или кортеж переменных перебирает элементы множества.
</li>
<li>
<b>Удаление элемента</b>: <code>{'A := A {x}'}</code> - удаление элемента x из множества A
<b>Присвоение</b>
<code> </code>
объявленная переменная или кортеж переменных получает значение выражения. Значение вычисляется заново при
каждом переходе к следующему набору значений перебираемых переменных.
</li>
<li>
<b>Объединение множеств</b>: <code>A := A B</code> - объединение множеств A и B
</li>
<li>
<b>Пересечение множеств</b>: <code>A := A B</code> - пересечение множеств A и B
<b>Логическое выражение</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>
<h2>Семантика</h2>
<p>
Императивные выражения используются для определения алгоритмов построения множеств, вычисления характеристик
объектов и реализации операций над данными в концептуальных схемах. Они позволяют задавать конструктивные
способы получения объектов.
Для каждого набора значений перебираемых и определяемых переменных вычисляется значение{' '}
<code>ТМВ(ξ1, ..., ξk)</code>. Этот результат включается в итоговое множество, если все логические выражения
истинны.
</p>
<h2>Пример</h2>
<p>
<code>
I{'{(ξ1,ξ2) | ξ1∈{1, 2, 3}; ξ2≔ξ1+1; ∃σ∈{4, 5, 6} (σ=2ξ2)}'} = {'{(1, 2), (2, 3)}'}
</code>
</p>
</div>
);

View File

@ -3,79 +3,89 @@ export function HelpRSLangExpressionLogic() {
<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"
<b>Принадлежность</b>: <code>ξS</code> элемент ξ принадлежит множеству S.
</li>
<li>
<b>Непринадлежность</b>: <code>x A</code> - "x не принадлежит множеству A"
<b>Непринадлежность</b>: <code>ξS</code> элемент ξ не принадлежит множеству S.
</li>
<li>
<b>Включение</b>: <code>A B</code> - "A является подмножеством B"
<b>Равенство множеств</b>: <code>S1=S2</code>.
</li>
<li>
<b>Строгое включение</b>: <code>A B</code> - "A является собственным подмножеством B"
<b>Неравенство множеств</b>: <code>S1S2</code>.
</li>
<li>
<b>Равенство множеств</b>: <code>A = B</code> - "множества A и B равны"
<b>Включение</b>: <code>S1S2</code> S является подмножеством S.
</li>
<li>
<b>Строгое включение</b>: <code>S1S2</code>.
</li>
<li>
<b>Невключение</b>: <code>S1S2</code>.
</li>
</ul>
<h2>Примеры логических выражений</h2>
<h2>Арифметические предикаты</h2>
<ul>
<li>
<code>x A: x B</code> - "все элементы A принадлежат B"
<b>Равенство</b>: <code>2 = 4</code>.
</li>
<li>
<code>x A: P(x) Q(x)</code> - "существует элемент x из A, для которого выполняются P(x) и Q(x)"
<b>Неравенство</b>: <code>2 4</code>.
</li>
<li>
<code>A B B A A = B</code> - "если A включено в B и B включено в A, то A равно B"
<b>Меньше</b>: <code>2 &lt; 4</code>.
</li>
<li>
<b>Меньше или равно</b>: <code>2 4</code>.
</li>
<li>
<b>Больше</b>: <code>2 &gt; 4</code>.
</li>
<li>
<b>Больше или равно</b>: <code>2 4</code>.
</li>
</ul>
<h2>Типизация логических выражений</h2>
<p>
Все логические выражения имеют типизацию <b>Logic</b> и могут использоваться в качестве аксиом, теорем или
условий в определениях конституент.
</p>
<h2>Логические связки</h2>
<ul>
<li>
<b>Отрицание</b>: <code>¬A</code> истина тогда и только тогда, когда 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 (ложно только при A истинно и B ложно).
</li>
<li>
<b>Эквивалентность</b>: <code>A B</code> истина, если A и B имеют одинаковое значение истины.
</li>
</ul>
<h2>Примеры</h2>
<ul>
<li>
<code>¬αS1</code>
</li>
<li>
<code>D1S1 2+2=5</code>
</li>
<li>
<code>{`D1⊆D2 ⇔ ∀x∈D1 x∈D2`}</code>
</li>
</ul>
</div>
);
}

View File

@ -3,117 +3,53 @@ export function HelpRSLangExpressionParameter() {
<div>
<h1>Параметризованные выражения</h1>
<p>
Параметризованные выражения в языке родов структур позволяют создавать шаблоны выражений, которые могут быть
применены к различным наборам параметров. Такие выражения используются в определениях терм-функций и
предикат-функций.
Параметризованные выражения в языке родов структур образуют самостоятельный класс конструкций. Они используются
для объявления терм-функций и предикат-функций. Вызов таких функций является соответственно
теоретико-множественным выражением (ТМВ) или логическим выражением (ЛВ).
</p>
<h2>Основные типы параметризованных выражений</h2>
<h2>Объявление терм-функции</h2>
<code>F1 ::= [α1ТМВ1, α2ТМВ2(α1)] ТМВ(α1, α2)</code>
<ul>
<li>В квадратных скобках через запятую указывается упорядоченный набор объявлений параметров.</li>
<li>
<b>Параметризованная функция</b>: <code>f(x, x, ..., xₙ) = expr</code> - функция с параметрами
Объявление параметра производится с помощью предиката принадлежности <code></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>
<h2>Объявление предикат-функции</h2>
<code>P1 ::= [α1ТМВ1, α2ТМВ2(α1)] ЛВ(α1, α2)</code>
<p>Отличие от терм-функции состоит в том, что после списка параметров задаётся логическое выражение, а не ТМВ.</p>
<h2>Вызов функций</h2>
<code>F1[ξ1, S1], P1[ξ1\ξ2, ξ3]</code>
<ul>
<li>
<b>Формальные параметры</b>: параметры в определении функции или предиката
</li>
<li>
<b>Фактические параметры</b>: конкретные значения, подставляемые при вызове
</li>
<li>
<b>Типизированные параметры</b>: параметры с указанием их типизации
</li>
<li>
<b>Шаблонные параметры</b>: параметры, которые могут принимать различные типы
</li>
<li>После имени функции в квадратных скобках указываются аргументы, порядок имеет значение.</li>
<li>Проверяется соответствие типизаций аргументов типизациям параметров, указанным при объявлении.</li>
<li>Результатом вызова терм-функции является ТМВ, вызова предикат-функции ЛВ.</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>
<h2>Шаблонные выражения</h2>
<code>F2 ::= [α1R1×R2, α2R1] α2=pr1(α1)</code>
<p>
Параметризованные выражения имеют типизацию вида <code>Hᵣ [H, H, ..., Hᵢ]</code>, где:
Функции, параметры которых содержат <b>радикалы</b>, называются шаблонными. Радикал используется для обозначения
произвольной типизации в ступени аргумента функции.
</p>
<ul>
<li>
<code>Hᵣ</code> - типизация результата
При вызове функции значение радикала вычисляется из типизаций аргументов. Все вычисленные значения должны
совпадать.
</li>
<li>Радикалы с разными индексами считаются различными по типизации.</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

@ -3,94 +3,51 @@ export function HelpRSLangExpressionQuantor() {
<div>
<h1>Кванторные выражения</h1>
<p>
Кванторные выражения в языке родов структур позволяют формулировать утверждения о свойствах элементов множеств.
Кванторы связывают переменные и позволяют выражать логические утверждения о всех или некоторых элементах
множества.
Кванторные выражения в языке родов структур используются для формулировки утверждений о всех или некоторых
элементах множества.
</p>
<h2>Основные кванторы</h2>
<h2>Синтаксис</h2>
<ul>
<li>
<b>Универсальный квантор</b>: <code>x A: P(x)</code> - "для всех x из A выполняется P(x)"
<b>Всеобщность</b>: <code>ξТМВ (ЛВ(ξ))</code>
</li>
<li>
<b>Экзистенциальный квантор</b>: <code>x A: P(x)</code> - "существует x из A такой, что P(x)"
<b>Существование</b>: <code>ξТМВ (ЛВ(ξ))</code>
</li>
<li>
<b>Квантор единственности</b>: <code>!x A: P(x)</code> - "существует единственный x из A такой, что P(x)"
<code>(ξ1, ξ2)ТМВ (ЛВ(ξ1, ξ2))</code>
</li>
<li>
<b>Квантор существования и единственности</b>: <code>x A: P(x)</code> - альтернативная запись для !
<code>ξ1,ξ2ТМВ (ЛВ(ξ1, ξ2))</code>
</li>
<li>Скобки вокруг ЛВ могут быть опущены для атомарных логических выражений.</li>
</ul>
<h2>Семантика</h2>
<ul>
<li>
<b>Всеобщность</b>: выражение истинно, если для всех значений <code>ξ</code> из области определения
выполняется условие <code>ЛВ(ξ)</code>.
</li>
<li>
<b>Существование</b>: выражение истинно, если существует хотя бы одно значение <code>ξ</code> из области
определения, для которого условие <code>ЛВ(ξ)</code> выполняется.
</li>
<li>
Кортеж переменных означает объявление переменной, пробегающий значения и введение обозначений для ее проекций.
</li>
<li>
Перечисление переменных является сокращением вложенных кванторов с одним типом и одной областью определения.
</li>
</ul>
<h2>Связанные переменные</h2>
<h2>Пример</h2>
<ul>
<li>
<b>Связывание переменной</b>: переменная x в выражении <code>x A: P(x)</code> связана квантором
</li>
<li>
<b>Область действия квантора</b>: выражение P(x) является областью действия квантора
</li>
<li>
<b>Свободные переменные</b>: переменные, не связанные кванторами, называются свободными
<code>xD1 yD2 (x,y)S1 & (x,x)S1</code>
</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

@ -1,109 +1,57 @@
export function HelpRSLangExpressionRecursive() {
return (
<div>
<h1>Рекурсивные выражения</h1>
<h1>Циклические конструкции</h1>
<p>Циклическая (рекурсивная) конструкция является теоретико-множественным выражением.</p>
<h2>Синтаксис</h2>
<ul>
<li>
<code>{'R{ξ ≔ ТМВ1 | ТМВ2(ξ)}'}</code>
</li>
<li>
<code>{'R{ξ ≔ ТМВ1 | ЛВ(ξ) | ТМВ2(ξ)}'}</code>
</li>
<li>
<code>{'R{(ξ,σ) ≔ (ТМВ1,ТМВ2) | ЛВ(ξ,σ) | ТМВ3(ξ,σ)}'}</code>
</li>
<li>
Буква <code>R</code> часть синтаксиса, а не идентификатор.
</li>
</ul>
<h2>Состав конструкции</h2>
<ul>
<li>
<b>База рекурсии</b> в первом блоке оператором присваивания <code></code> задаётся начальное значение
переменной (или кортежа переменных) рекурсии.
</li>
<li>
<b>Условие продолжения</b> во втором блоке указывается логическое выражение <code>ЛВ</code>, которое
пересчитывается на каждом шаге для текущего значения переменной рекурсии. Второй блок опционален, условием
выхода по умолчанию считается повторение предыдущего значения на текущем шаге.
</li>
<li>
<b>Пересчёт</b> в третьем блоке задаётся ТМВ, вычисляемое на текущем значении переменной и дающее значение
переменной на следующем шаге.
</li>
</ul>
<h2>Порядок выполнения шага</h2>
<p>На каждом шаге сначала вычисляется условие продолжения рекурсии, затем выполняется пересчёт.</p>
<h2>Завершение и результат</h2>
<p>
Рекурсивные выражения в языке родов структур используются для определения множеств и функций через их
собственные определения. Рекурсия позволяет задавать бесконечные структуры и сложные зависимости.
Рекурсия продолжается, пока условие продолжения истинно, или до стабилизации значения переменной рекурсии
(значение на шаге <i>k</i> равно значению на шаге <i>k+1</i>). Результатом является последнее значение
переменной (или кортежа переменных) рекурсии.
</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>
<h2>Пример</h2>
<p>
Рекурсивные выражения используются для определения сложных структур данных, бесконечных множеств и функций в
концептуальных схемах. Они позволяют описывать объекты с внутренней структурой и зависимостями.
Вычисление степеней двойки:
<br />
<code>{'R{(ξ,σ) ≔ (1, 0) | σ<5 | (2ξ, σ+1)} = 32'}</code>
</p>
</div>
);

View File

@ -1,85 +1,45 @@
export function HelpRSLangExpressionSet() {
return (
<div>
<h1>Операции с множествами</h1>
<h1>Теоретико-множественные выражения</h1>
<p>
Теоретико-множественные выражения в языке родов структур позволяют создавать и манипулировать множествами.
Результатом таких выражений является множество элементов определенной ступени.
Теоретико-множественные выражения (ТМВ) в языке родов структур используются для задания и преобразования
множеств. Сложные конструкции теоретико-множественных выражений выделены в индивидуальные разделы справочника.
</p>
<p>
В данном разделе приведены классические операции над множествами, построенные на основе предикатов
принадлежности и логических связок.
</p>
<h2>Основные операции с множествами</h2>
<h2>Основные операции</h2>
<ul>
<li>
<b>Объединение</b>: <code>A B</code> - множество всех элементов, принадлежащих A или B
<b>Объединение</b>: <code>D1 D2</code> множество элементов, принадлежащих D1 или D2.
</li>
<li>
<b>Пересечение</b>: <code>A B</code> - множество всех элементов, принадлежащих и A, и B
<b>Пересечение</b>: <code>D1 D2</code> множество элементов, принадлежащих и D1, и D2.
</li>
<li>
<b>Разность</b>: <code>A \ B</code> - множество всех элементов A, не принадлежащих B
<b>Разность</b>: <code>D1 \ D2</code> множество элементов, принадлежащих D1, но не D2.
</li>
<li>
<b>Симметрическая разность</b>: <code>A B</code> - множество элементов, принадлежащих ровно одному из A или
B
</li>
<li>
<b>Дополнение</b>: <code>A'</code> - множество всех элементов универсального множества, не принадлежащих A
<b>Симметрическая разность</b>: <code>D1 D2</code> множество элементов, принадлежащих исключительно D1 или
исключительно D2.
</li>
</ul>
<h2>Конструкторы множеств</h2>
<h2>Примеры</h2>
<ul>
<li>
<b>Перечисление</b>: <code>{'{a, b, c}'}</code> - множество из элементов a, b, c
<code>{`{1,2} {2,3} = {1,2,3}`}</code>
</li>
<li>
<b>Выделение</b>: <code>{'{x ∈ A | P(x)}'}</code> - множество всех x из A, для которых выполняется P(x)
<code>{`{1,2,3} ∩ {2,3,4} = {2,3}`}</code>
</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
<code>{`{1,2,3} \\ {2} = {1,3}`}</code>
</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

@ -1,78 +1,123 @@
import { LinkTopic } from '../../components/link-topic';
import { HelpTopic } from '../../models/help-topic';
export function HelpRSLangExpressionStructure() {
return (
<div>
<h1>Структурные выражения</h1>
<p>
Структурные выражения в языке родов структур позволяют манипулировать ступенями операндов. Эти выражения
используются для изменения структуры данных и создания новых типов на основе существующих.
Структурные выражения в языке родов структур используются для преобразований, меняющий{' '}
<LinkTopic topic={HelpTopic.RSL_TYPIFICATION} text='типизацию' /> аргументов, позволяя порождать структурно
зависимые или структурно новые понятия.
</p>
<h2>Основные структурные операции</h2>
<h2>Порождение структур</h2>
<ul>
<li>
<b>Кортеж</b>: <code>(H, H, ..., Hₙ)</code> - ступень кортежа арности n
<b>Булеан / Множество подмножеств</b>: <code>(X1)</code> множество всех подмножеств <code>X1</code>.
</li>
<li>
<b>Проекция</b>: <code>π(t)</code> - извлечение i-го элемента кортежа t
<b>Декартово произведение</b>: <code>X1×X2</code> множество всех пар элементов из <code>X1</code> и{' '}
<code>X2</code>.
</li>
<li>
<b>Конкатенация кортежей</b>: <code>t t</code> - объединение двух кортежей
<b>Кортеж</b>: <code>(a, b, c)</code> упорядоченная n-ка (n 2).
</li>
<li>
<b>Структурирование</b>: <code>struct(field: H, field: H, ...)</code> - создание структуры с именованными
полями
<b>Перечисление</b>: <code>{'{a, b, c}'}</code> неупорядоченная n-ка (n 1).
</li>
<li>
<b>Синглетон / буль</b>: <code>bool(a)</code> = <code>{`{a}`}</code> множество, состоящее из одного
элемента.
</li>
</ul>
<h2>Операции с множествами структур</h2>
<h2>Производные структуры</h2>
<ul>
<li>
<b>Декартово произведение ступеней</b>: <code>H × H × ... × Hₙ</code> - ступень n-арных кортежей
<b>Множество-сумма</b>: <code>red(S1)</code> объединение элементов всех множеств в <code>S1</code>. Операция
применима только к множествам, состоящим из множеств.
</li>
<li>
<b>Степень ступени</b>: <code>Hⁿ</code> - n-арное произведение ступени H на себя
<b>Десинглетон / дебуль</b>: <code>debool({`{a}`})</code> = <code>a</code> извлечение единственного элемента
из множества. Операция применима только к множествам с одним элементом.
</li>
<li>
<b>Множество кортежей</b>: <code>(H × H × ... × Hₙ)</code> - множество n-арных кортежей
<b>Малая проекция</b>: <code>pr1((a1, , an))</code> = <code>a1</code>.
</li>
<li>
<b>Большая проекция</b>: <code>Pr1(S1)</code> множество первых компонентов всех кортежей из <code>S1</code>.
</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>
Структурные выражения используются для определения сложных типов данных в концептуальных схемах, таких как
записи, кортежи и структурированные множества. Они позволяют создавать формальные описания сложных объектов
предметной области.
Индексы у операций над кортежами для упрощения отображаются равными 1, но их можно заменить на другие
натуральные числа или их последовательность, разделенная запятой.
</p>
<h2>Мультииндексы</h2>
<p>
Вместо одного индекса можно использовать <b>мультииндекс</b> последовательность натуральных чисел через
запятую. В этом случае проекция или фильтр возвращает сразу несколько позиций кортежа.
</p>
<ul>
<li>
<code>pr1,3((a1, a2, a3, a4)) = (a1, a3)</code>
</li>
<li>
<code>Pr2,4(S1)</code> множество пар, составленных из второй и четвёртой компонент кортежей из{' '}
<code>S1</code>.
</li>
</ul>
<h2>Фильтр</h2>
<ul>
<li>
<b>Фильтр</b>: <code>Fi1[D1](S1)</code> подмножество <code>S1</code>, в котором для каждого элемента первая
проекция принадлежит <code>D1</code>.
</li>
<li>
К фильтру применим <b>мультииндексы</b>, тогда нужно указывать столько же параметров в квадратных скобках.
</li>
<li>
Допустимо использование мультииндексов в фильтре с одним параметром. Тогда проверяется принадлежность
параметру кортежа, составленного из соответствующих проекций элементов фильтруемого множества.
</li>
<li>
<b>Мультифильтр</b>: <code>Fi1,2[D1](S1)</code> отличается от фильтра с мультииндексом{' '}
<code>Fi1,2[Pr1(D1), Pr2(D2)](S1)</code> тем, что в первом случае проверяется принадлежность парам из D1, а во
втором полному декартову произведению проекций D1
</li>
</ul>
<h2>Примеры</h2>
<ul>
<li>
<code>{`(2) = {{}, {1}, {2}, {1, 2}}`}</code>
</li>
<li>
<code>(1,2,3)</code> кортеж из трёх чисел
</li>
<li>
<code>pr2((5, 4, 3, 2, 1)) = 4</code>
</li>
<li>
<code>
Pr3({`{(1, 2, 3),(4, 5, 6)}`}) = {`{3, 6}`}
</code>
</li>
<li>
<code>
red({`{{1, 2, 3},{3, 4}}`}) = {`{1, 2, 3, 4}`}
</code>
</li>
<li>
<code>bool(1) = {`{1}`}</code>, <code>debool({`{1}`}) = 1</code>
</li>
<li>
<code>{`Fi2[{2, 4}]({((1, 2), (3, 4), (5, 6))}) = {((1, 2), (3, 4))}`}</code>
</li>
</ul>
</div>
);
}

View File

@ -33,10 +33,7 @@ export function HelpRSLangLiterals() {
</ul>
<h2>Литералы</h2>
<p>
Литералы задают фиксированные значения в выражениях. В языке родов структур используются следующие виды
литералов:
</p>
<p>Литералы задают фиксированные значения в выражениях.</p>
<ul>
<li>
<b>Целые числа</b> последовательность цифр. Отрицательные числа не поддерживаются:

View File

@ -94,7 +94,7 @@ const describeHelpTopicRecord: Record<HelpTopic, string> = {
[HelpTopic.RSLANG]: 'экспликация и язык родов структур',
[HelpTopic.RSL_LITERALS]: 'обозначения конституент,<br/>локальных переменных и литералов',
[HelpTopic.RSL_TYPIFICATION]: 'система типов в <br/>родоструктурной экспликации',
[HelpTopic.RSL_EXPRESSION_LOGIC]: 'логические выражения',
[HelpTopic.RSL_EXPRESSION_LOGIC]: 'логические связывающие конструкции',
[HelpTopic.RSL_EXPRESSION_SET]: 'операции с множествами',
[HelpTopic.RSL_EXPRESSION_STRUCTURE]: 'операции со ступенями',
[HelpTopic.RSL_EXPRESSION_ARITHMETIC]: 'арифметические выражения',