From 1d182f441770a862dfd6a66784e60342f1c95eaa Mon Sep 17 00:00:00 2001 From: Ivan <8611739+IRBorisov@users.noreply.github.com> Date: Fri, 15 Aug 2025 21:53:49 +0300 Subject: [PATCH] D: Generating help pt1 --- .../help/items/cc/help-concept-system.tsx | 4 +- .../src/features/help/items/help-rslang.tsx | 65 ++++++++-- .../features/help/items/help-thesaurus.tsx | 2 +- .../help/items/rslang/help-rslang-correct.tsx | 2 +- .../help-rslang-expression-arithmetic.tsx | 99 +++++++++++++++ .../help-rslang-expression-declarative.tsx | 97 ++++++++++++++ .../help-rslang-expression-imperative.tsx | 98 +++++++++++++++ .../rslang/help-rslang-expression-logic.tsx | 81 ++++++++++++ .../help-rslang-expression-parameter.tsx | 119 ++++++++++++++++++ .../rslang/help-rslang-expression-quantor.tsx | 96 ++++++++++++++ .../help-rslang-expression-recursive.tsx | 110 ++++++++++++++++ .../rslang/help-rslang-expression-set.tsx | 85 +++++++++++++ .../help-rslang-expression-structure.tsx | 78 ++++++++++++ .../items/rslang/help-rslang-interpret.tsx | 2 +- .../items/rslang/help-rslang-literals.tsx | 63 ++++++++++ .../items/rslang/help-rslang-operations.tsx | 2 +- ...types.tsx => help-rslang-typification.tsx} | 2 +- .../frontend/src/features/help/labels.ts | 24 +++- .../src/features/help/models/help-topic.ts | 24 +++- .../help/pages/manuals-page/topic-page.tsx | 24 +++- 20 files changed, 1053 insertions(+), 24 deletions(-) create mode 100644 rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-arithmetic.tsx create mode 100644 rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-declarative.tsx create mode 100644 rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-imperative.tsx create mode 100644 rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-logic.tsx create mode 100644 rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-parameter.tsx create mode 100644 rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-quantor.tsx create mode 100644 rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-recursive.tsx create mode 100644 rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-set.tsx create mode 100644 rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-structure.tsx create mode 100644 rsconcept/frontend/src/features/help/items/rslang/help-rslang-literals.tsx rename rsconcept/frontend/src/features/help/items/rslang/{help-rslang-types.tsx => help-rslang-typification.tsx} (98%) diff --git a/rsconcept/frontend/src/features/help/items/cc/help-concept-system.tsx b/rsconcept/frontend/src/features/help/items/cc/help-concept-system.tsx index e4279d8f..bcba80fc 100644 --- a/rsconcept/frontend/src/features/help/items/cc/help-concept-system.tsx +++ b/rsconcept/frontend/src/features/help/items/cc/help-concept-system.tsx @@ -35,8 +35,8 @@ export function HelpConceptSystem() { экспликации. Портал поддерживает . Помимо аксиом также могут приводиться дополнительные утверждения, называемые теоремами. Понятия, которым даются формальные определения называют производными. Следует отметить, что в родоструктурной экспликации - к аксиомам также относят соотношения , а к производным - понятиям, – термы, терм-функции и предикат-функции. + к аксиомам также относят соотношения , а к + производным понятиям, – термы, терм-функции и предикат-функции.

diff --git a/rsconcept/frontend/src/features/help/items/help-rslang.tsx b/rsconcept/frontend/src/features/help/items/help-rslang.tsx index 3c07bda1..2244c165 100644 --- a/rsconcept/frontend/src/features/help/items/help-rslang.tsx +++ b/rsconcept/frontend/src/features/help/items/help-rslang.tsx @@ -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 ( -

-
+

Родоструктурная экспликация

-

Формальная запись (экспликация) концептуальных схем осуществляется с помощью языка родов структур.

-

Для ознакомления с основами родов структур можно использовать следующие материалы:

-

1. Видео: Краткое введение в мат. аппарат

-

2. Текст: Учебник И. Н. Пономарева

-

3. Видео: лекции для 4 курса (второй семестр 2022-23 год)

-
-
+

+ Формальная запись (экспликация) концептуальных схем осуществляется с помощью языка родов структур (далее + – Язык). В данном разделе поясняются основные понятия и формальные конструкции Языка. В своей основе Язык + является формальной логикой первого порядка, все дополнительные обозначения основываются на предикате + принадлежности x∈y. +

+

+ Используются строгие правила написания идентификаторов для обозначений понятий, локальных переменных и + литералов. +

+

+ Элементы Языка подразделяются на теоретико-множественные выражения и логические выражения. Упрощенно говоря, + теоретико-множественное выражение возвращает элемент некоторой{' '} + , логическое выражение возвращает логическое + значение ИСТИНА или ЛОЖЬ. +

+

+ Помимо указанных выражений также допускаются параметризованные и шаблонные выражения, значения и типизация + которых зависят от вводимых параметров. Такие выражения используются в определениях{' '} + + . +

+

Выражения, позволяющие манипулировать ступенями операндов называются структурными выражениями.

+

+ Отдельно рассматриваются сложные конструкции, задающие множество через отбор элементов, императивно или + рекурсивно. +

+ + +
+

Для глубокого ознакомления с основами родов структур можно использовать следующие материалы:

+

+ 1. Видео: Краткое введение в мат. аппарат +

+

+ 2.{' '} + + Текст: Учебник И. Н. Пономарева + +

+

+ 3.{' '} + + Видео: лекции для 4 курса (второй семестр 2022-23 год) + +

+
-
); + ); } diff --git a/rsconcept/frontend/src/features/help/items/help-thesaurus.tsx b/rsconcept/frontend/src/features/help/items/help-thesaurus.tsx index fe8c504f..bc30cb8a 100644 --- a/rsconcept/frontend/src/features/help/items/help-thesaurus.tsx +++ b/rsconcept/frontend/src/features/help/items/help-thesaurus.tsx @@ -137,7 +137,7 @@ export function HelpThesaurus() { {'\u2009'}родовая структура (S#) – неопределяемое понятие, имеющее структуру, построенную на базисных множествах и константных множеств. Содержание родовой структуры формируется{' '} - , аксиомами и конвенцией. + , аксиомами и конвенцией.
  • diff --git a/rsconcept/frontend/src/features/help/items/rslang/help-rslang-correct.tsx b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-correct.tsx index 1433cf50..b323e054 100644 --- a/rsconcept/frontend/src/features/help/items/rslang/help-rslang-correct.tsx +++ b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-correct.tsx @@ -18,7 +18,7 @@ export function HelpRSLangCorrect() { Правила проверки теоретико-множественных выражений выводятся из условия биективной переносимости предиката принадлежности – элемент должен соответствовать множеству, для которого проверяется принадлежность. Необходимым условием биективной переносимости является выполнение{' '} - для всех локальных и глобальных + для всех локальных и глобальных идентификаторов.

    diff --git a/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-arithmetic.tsx b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-arithmetic.tsx new file mode 100644 index 00000000..e11078fc --- /dev/null +++ b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-arithmetic.tsx @@ -0,0 +1,99 @@ +export function HelpRSLangExpressionArithmetic() { + return ( +

    +

    Арифметические выражения

    +

    + Арифметические выражения в языке родов структур позволяют выполнять математические операции над числовыми + данными. Эти выражения работают с целыми числами и возвращают числовые результаты. +

    + +

    Основные арифметические операции

    +
      +
    • + Сложение: a + b - сумма чисел a и b +
    • +
    • + Вычитание: a - b - разность чисел a и b +
    • +
    • + Умножение: a × b или a * b - произведение чисел a и b +
    • +
    • + Деление: a ÷ b или a / b - частное от деления a на b +
    • +
    • + Остаток от деления: a mod b - остаток от деления a на b +
    • +
    • + Возведение в степень: a^b или a**b - a в степени b +
    • +
    + +

    Операции сравнения

    +
      +
    • + Равенство: a = b - a равно b +
    • +
    • + Неравенство: a ≠ b - a не равно b +
    • +
    • + Меньше: {'a < b'} - a меньше b +
    • +
    • + Меньше или равно: a ≤ b - a меньше или равно b +
    • +
    • + Больше: {'a > b'} - a больше b +
    • +
    • + Больше или равно: a ≥ b - a больше или равно b +
    • +
    + +

    Специальные функции

    +
      +
    • + Абсолютное значение: |a| - модуль числа a +
    • +
    • + Минимум: min(a, b) - минимальное из чисел a и b +
    • +
    • + Максимум: max(a, b) - максимальное из чисел a и b +
    • +
    • + Факториал: n! - факториал числа n +
    • +
    + +

    Примеры арифметических выражений

    +
      +
    • + (a + b) × c - произведение суммы a и b на c +
    • +
    • + a^2 + b^2 - сумма квадратов a и b +
    • +
    • + |x - y| - абсолютная разность x и y +
    • +
    • + min(a, b) + max(c, d) - сумма минимума a и b с максимумом c и d +
    • +
    + +

    Типизация арифметических выражений

    +

    + Все арифметические выражения имеют типизацию Z (целые числа). Результат арифметической операции + всегда является целым числом. +

    + +

    Применение в концептуальных схемах

    +

    + Арифметические выражения используются для определения числовых характеристик объектов предметной области, + вычисления количественных показателей и формулировки числовых ограничений в аксиомах и теоремах. +

    +
    + ); +} diff --git a/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-declarative.tsx b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-declarative.tsx new file mode 100644 index 00000000..6da5b126 --- /dev/null +++ b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-declarative.tsx @@ -0,0 +1,97 @@ +export function HelpRSLangExpressionDeclarative() { + return ( +
    +

    Декларативные выражения

    +

    + Декларативные выражения в языке родов структур используются для определения понятий через их свойства и + характеристики. Эти выражения описывают "что есть" объект, а не "как его получить". +

    + +

    Основные типы декларативных выражений

    +
      +
    • + Определение через свойства: {'A = {x | P(x)}'} - A есть множество всех x, обладающих + свойством P +
    • +
    • + Определение через равенство: A = B - A равно B по определению +
    • +
    • + Определение через включение: A ⊆ B - A является подмножеством B +
    • +
    • + Аксиоматическое определение: ∀x ∈ A: P(x) - для всех x из A выполняется свойство P +
    • +
    + +

    Структура декларативных определений

    +
      +
    • + Определяемый объект: понятие, которое определяется +
    • +
    • + Определяющие свойства: характеристики, которые задают определяемый объект +
    • +
    • + Область определения: множество, в рамках которого происходит определение +
    • +
    • + Условия корректности: ограничения, обеспечивающие корректность определения +
    • +
    + +

    Примеры декларативных выражений

    +
      +
    • + {'EVEN = {x ∈ Z | x mod 2 = 0}'} - четные числа есть множество целых чисел, делящихся на 2 +
    • +
    • + {'PRIME = {x ∈ N | x > 1 ∧ ∀y ∈ N: y | x → y = 1 ∨ y = x}'} - простые числа +
    • +
    • + ∀x ∈ A: x ∈ B → x ∈ C - все элементы A, принадлежащие B, принадлежат также C +
    • +
    • + {'MAX = {x ∈ A | ∀y ∈ A: y ≤ x}'} - максимум множества A +
    • +
    + +

    Свойства декларативных определений

    +
      +
    • + Ясность: определение должно однозначно определять объект +
    • +
    • + Непротиворечивость: определение не должно содержать логических противоречий +
    • +
    • + Полнота: определение должно содержать все необходимые характеристики +
    • +
    • + Минимальность: определение не должно содержать избыточных условий +
    • +
    + +

    Типизация декларативных выражений

    +

    Декларативные выражения могут иметь различные типизации в зависимости от типа определяемого объекта:

    +
      +
    • + Определения множеств имеют типизацию ℬ(H) +
    • +
    • + Определения свойств имеют типизацию Logic +
    • +
    • + Определения отношений имеют типизацию ℬ(H₁ × H₂ × ... × Hₙ) +
    • +
    + +

    Применение в концептуальных схемах

    +

    + Декларативные выражения используются для определения понятий в концептуальных схемах, формулировки аксиом и + теорем, а также для описания свойств объектов предметной области. Они составляют основу формального описания + концептуальных схем. +

    +
    + ); +} diff --git a/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-imperative.tsx b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-imperative.tsx new file mode 100644 index 00000000..16d7e96d --- /dev/null +++ b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-imperative.tsx @@ -0,0 +1,98 @@ +export function HelpRSLangExpressionImperative() { + return ( +
    +

    Императивные выражения

    +

    + Императивные выражения в языке родов структур используются для задания множеств через последовательность + действий или операций. Эти выражения описывают "как получить" объект, а не "что он есть". +

    + +

    Основные императивные конструкции

    +
      +
    • + Последовательность операций: op₁; op₂; ...; opₙ - выполнение операций в заданном порядке +
    • +
    • + Условные операции: if P then op₁ else op₂ - условное выполнение операций +
    • +
    • + Циклические операции: while P do op - повторение операции пока выполняется условие P +
    • +
    • + Присваивание: x := expr - присваивание значения выражения переменной +
    • +
    + +

    Операции построения множеств

    +
      +
    • + Добавление элемента: {'A := A ∪ {x}'} - добавление элемента x к множеству A +
    • +
    • + Удаление элемента: {'A := A {x}'} - удаление элемента x из множества A +
    • +
    • + Объединение множеств: A := A ∪ B - объединение множеств A и B +
    • +
    • + Пересечение множеств: A := A ∩ B - пересечение множеств A и B +
    • +
    + +

    Примеры императивных выражений

    +
      +
    • + {'result := ∅; for x ∈ A do if P(x) then result := result ∪ {x}'} - построение множества + элементов A, удовлетворяющих условию P +
    • +
    • + sum := 0; for x ∈ A do sum := sum + x - вычисление суммы элементов множества A +
    • +
    • + {'max := first(A); for x ∈ A do if x > max then max := x'} - поиск максимального элемента в A +
    • +
    • + {'B := ∅; while A ≠ ∅ do {x := choose(A); B := B ∪ {f(x)}; A := A {x}}'} - применение функции f + к элементам A +
    • +
    + +

    Свойства императивных выражений

    +
      +
    • + Детерминированность: результат должен быть однозначно определен +
    • +
    • + Корректность: операции должны быть корректными для заданных типов данных +
    • +
    • + Завершаемость: императивное выражение должно завершаться за конечное число шагов +
    • +
    • + Эффективность: выражение должно быть эффективным с точки зрения вычислительных ресурсов +
    • +
    + +

    Типизация императивных выражений

    +

    Императивные выражения могут иметь различные типизации в зависимости от результата выполнения:

    +
      +
    • + Построение множеств имеет типизацию ℬ(H) +
    • +
    • + Вычисление значений имеет типизацию H +
    • +
    • + Логические операции имеют типизацию Logic +
    • +
    + +

    Применение в концептуальных схемах

    +

    + Императивные выражения используются для определения алгоритмов построения множеств, вычисления характеристик + объектов и реализации операций над данными в концептуальных схемах. Они позволяют задавать конструктивные + способы получения объектов. +

    +
    + ); +} diff --git a/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-logic.tsx b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-logic.tsx new file mode 100644 index 00000000..83ff8685 --- /dev/null +++ b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-logic.tsx @@ -0,0 +1,81 @@ +export function HelpRSLangExpressionLogic() { + return ( +
    +

    Логические выражения

    +

    + Логические выражения в языке родов структур возвращают логическое значение ИСТИНА или ЛОЖЬ. Они используются для + формулировки аксиом, теорем и условий. +

    + +

    Основные логические операторы

    +
      +
    • + Отрицание: ¬P или !P - "не P" +
    • +
    • + Конъюнкция: P ∧ Q или P && Q - "P и Q" +
    • +
    • + Дизъюнкция: P ∨ Q или P || Q - "P или Q" +
    • +
    • + Импликация: P → Q или {'P => Q'} - "если P, то Q" +
    • +
    • + Эквивалентность: P ↔ Q или {'P <=> Q'} - "P эквивалентно Q" +
    • +
    + +

    Кванторы

    +
      +
    • + Универсальный квантор: ∀x ∈ A: P(x) - "для всех x из A выполняется P(x)" +
    • +
    • + Экзистенциальный квантор: ∃x ∈ A: P(x) - "существует x из A такой, что P(x)" +
    • +
    • + Единственность: ∃!x ∈ A: P(x) - "существует единственный x из A такой, что P(x)" +
    • +
    + +

    Теоретико-множественные предикаты

    +
      +
    • + Принадлежность: x ∈ A - "x принадлежит множеству A" +
    • +
    • + Непринадлежность: x ∉ A - "x не принадлежит множеству A" +
    • +
    • + Включение: A ⊆ B - "A является подмножеством B" +
    • +
    • + Строгое включение: A ⊂ B - "A является собственным подмножеством B" +
    • +
    • + Равенство множеств: A = B - "множества A и B равны" +
    • +
    + +

    Примеры логических выражений

    +
      +
    • + ∀x ∈ A: x ∈ B - "все элементы A принадлежат B" +
    • +
    • + ∃x ∈ A: P(x) ∧ Q(x) - "существует элемент x из A, для которого выполняются P(x) и Q(x)" +
    • +
    • + A ⊆ B ∧ B ⊆ A → A = B - "если A включено в B и B включено в A, то A равно B" +
    • +
    + +

    Типизация логических выражений

    +

    + Все логические выражения имеют типизацию Logic и могут использоваться в качестве аксиом, теорем или + условий в определениях конституент. +

    +
    + ); +} diff --git a/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-parameter.tsx b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-parameter.tsx new file mode 100644 index 00000000..ae3d4bf1 --- /dev/null +++ b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-parameter.tsx @@ -0,0 +1,119 @@ +export function HelpRSLangExpressionParameter() { + return ( +
    +

    Параметризованные выражения

    +

    + Параметризованные выражения в языке родов структур позволяют создавать шаблоны выражений, которые могут быть + применены к различным наборам параметров. Такие выражения используются в определениях терм-функций и + предикат-функций. +

    + +

    Основные типы параметризованных выражений

    +
      +
    • + Параметризованная функция: f(x₁, x₂, ..., xₙ) = expr - функция с параметрами +
    • +
    • + Параметризованный предикат: P(x₁, x₂, ..., xₙ) = condition - предикат с параметрами +
    • +
    • + Шаблонное выражение: template(param₁, param₂, ...) - шаблон с параметрами +
    • +
    • + Параметризованное множество: {'A(param) = {x | P(x, param)}'} - множество, зависящее от + параметра +
    • +
    + +

    Типы параметров

    +
      +
    • + Формальные параметры: параметры в определении функции или предиката +
    • +
    • + Фактические параметры: конкретные значения, подставляемые при вызове +
    • +
    • + Типизированные параметры: параметры с указанием их типизации +
    • +
    • + Шаблонные параметры: параметры, которые могут принимать различные типы +
    • +
    + +

    Примеры параметризованных выражений

    +
      +
    • + sum(x, y) = x + y - функция сложения двух чисел +
    • +
    • + {'is_greater(x, y) = x > y'} - предикат сравнения +
    • +
    • + power(base, exp) = if exp = 0 then 1 else base × power(base, exp-1) - возведение в степень +
    • +
    • + {'filter(A, P) = {x ∈ A | P(x)}'} - фильтрация множества по предикату +
    • +
    + +

    Шаблонные параметры

    +
      +
    • + R₁, R₂, ..., Rᵢ - обозначения для произвольных ступеней +
    • +
    • + Определение по месту: типизация определяется исходя из контекста использования +
    • +
    • + Универсальность: шаблон может применяться к различным типам данных +
    • +
    • + Проверка совместимости: система проверяет корректность применения шаблона +
    • +
    + +

    Типизация параметризованных выражений

    +

    + Параметризованные выражения имеют типизацию вида Hᵣ ← [H₁, H₂, ..., Hᵢ], где: +

    +
      +
    • + Hᵣ - типизация результата +
    • +
    • + H₁, H₂, ..., Hᵢ - типизации аргументов +
    • +
    • + Для предикатов Hᵣ = Logic +
    • +
    • + Для функций Hᵣ определяется типом возвращаемого значения +
    • +
    + +

    Применение параметров

    +
      +
    • + Подстановка: замена формальных параметров фактическими значениями +
    • +
    • + Проверка типов: проверка соответствия типов фактических параметров формальным +
    • +
    • + Вычисление: выполнение выражения с подставленными параметрами +
    • +
    • + Результат: получение результата с соответствующей типизацией +
    • +
    + +

    Применение в концептуальных схемах

    +

    + Параметризованные выражения используются для определения терм-функций и предикат-функций в концептуальных + схемах. Они позволяют создавать универсальные шаблоны, которые могут применяться к различным объектам предметной + области. +

    +
    + ); +} diff --git a/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-quantor.tsx b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-quantor.tsx new file mode 100644 index 00000000..74380ebe --- /dev/null +++ b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-quantor.tsx @@ -0,0 +1,96 @@ +export function HelpRSLangExpressionQuantor() { + return ( +
    +

    Кванторные выражения

    +

    + Кванторные выражения в языке родов структур позволяют формулировать утверждения о свойствах элементов множеств. + Кванторы связывают переменные и позволяют выражать логические утверждения о всех или некоторых элементах + множества. +

    + +

    Основные кванторы

    +
      +
    • + Универсальный квантор: ∀x ∈ A: P(x) - "для всех x из A выполняется P(x)" +
    • +
    • + Экзистенциальный квантор: ∃x ∈ A: P(x) - "существует x из A такой, что P(x)" +
    • +
    • + Квантор единственности: ∃!x ∈ A: P(x) - "существует единственный x из A такой, что P(x)" +
    • +
    • + Квантор существования и единственности: ∃₁x ∈ A: P(x) - альтернативная запись для ∃! +
    • +
    + +

    Связанные переменные

    +
      +
    • + Связывание переменной: переменная x в выражении ∀x ∈ A: P(x) связана квантором ∀ +
    • +
    • + Область действия квантора: выражение P(x) является областью действия квантора +
    • +
    • + Свободные переменные: переменные, не связанные кванторами, называются свободными +
    • +
    + +

    Множественные кванторы

    +
      +
    • + Последовательные кванторы: ∀x ∈ A ∀y ∈ B: P(x, y) - для всех x из A и всех y из B +
    • +
    • + Смешанные кванторы: ∀x ∈ A ∃y ∈ B: P(x, y) - для каждого x из A существует y из B +
    • +
    • + Кванторы с условиями: ∀x ∈ A: P(x) → Q(x) - для всех x из A, если P(x), то Q(x) +
    • +
    + +

    Примеры кванторных выражений

    +
      +
    • + ∀x ∈ A: x ∈ B - все элементы A принадлежат B +
    • +
    • + {'∃x ∈ A: x > 0'} - существует положительный элемент в A +
    • +
    • + ∀x ∈ A ∃y ∈ B: x = f(y) - для каждого x из A существует y из B такой, что x = f(y) +
    • +
    • + ∃!x ∈ A: P(x) ∧ Q(x) - существует единственный x из A, для которого выполняются P(x) и Q(x) +
    • +
    + +

    Отрицание кванторов

    +
      +
    • + Отрицание универсального: ¬(∀x ∈ A: P(x)) эквивалентно ∃x ∈ A: ¬P(x) +
    • +
    • + Отрицание экзистенциального: ¬(∃x ∈ A: P(x)) эквивалентно ∀x ∈ A: ¬P(x) +
    • +
    • + Отрицание единственности: ¬(∃!x ∈ A: P(x)) эквивалентно{' '} + ∀x ∈ A: ¬P(x) ∨ ∃y ∈ A: P(y) ∧ x ≠ y +
    • +
    + +

    Типизация кванторных выражений

    +

    + Все кванторные выражения имеют типизацию Logic, так как они возвращают логическое значение ИСТИНА или + ЛОЖЬ. Кванторы используются для формулировки аксиом, теорем и условий в определениях конституент. +

    + +

    Применение в концептуальных схемах

    +

    + Кванторные выражения используются для формулировки общих свойств объектов предметной области, определения + отношений между понятиями и выражения универсальных закономерностей в рамках концептуальных схем. +

    +
    + ); +} diff --git a/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-recursive.tsx b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-recursive.tsx new file mode 100644 index 00000000..30201d5f --- /dev/null +++ b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-recursive.tsx @@ -0,0 +1,110 @@ +export function HelpRSLangExpressionRecursive() { + return ( +
    +

    Рекурсивные выражения

    +

    + Рекурсивные выражения в языке родов структур используются для определения множеств и функций через их + собственные определения. Рекурсия позволяет задавать бесконечные структуры и сложные зависимости. +

    + +

    Основные типы рекурсивных выражений

    +
      +
    • + Рекурсивное определение множества: A = B ∪ f(A) - множество A определяется через себя +
    • +
    • + Рекурсивная функция: f(n) = if n = 0 then 1 else n × f(n-1) - функция определяется через + себя +
    • +
    • + Индуктивное определение: {'A = A₀ ∪ {f(x) | x ∈ A}'} - множество строится индуктивно +
    • +
    • + Трансфинитная рекурсия: {'A = ⋃{Aᵢ | i < α}'} - объединение по ординалам +
    • +
    + +

    Структура рекурсивных определений

    +
      +
    • + Базовый случай: начальное значение или базовое множество +
    • +
    • + Рекурсивный случай: правило построения новых элементов из существующих +
    • +
    • + Условие завершения: условие, обеспечивающее конечность процесса +
    • +
    • + Монотонность: свойство, гарантирующее корректность рекурсии +
    • +
    + +

    Примеры рекурсивных выражений

    +
      +
    • + {'N = {0} ∪ {n+1 | n ∈ N}'} - индуктивное определение натуральных чисел +
    • +
    • + fact(n) = if n = 0 then 1 else n × fact(n-1) - факториал +
    • +
    • + fib(n) = if n ≤ 1 then n else fib(n-1) + fib(n-2) - числа Фибоначчи +
    • +
    • + {'LIST = {nil} ∪ {cons(x, l) | x ∈ A, l ∈ LIST}'} - список элементов из A +
    • +
    + +

    Свойства рекурсивных выражений

    +
      +
    • + Корректность: рекурсивное определение должно быть корректным +
    • +
    • + Завершаемость: рекурсивный процесс должен завершаться +
    • +
    • + Единственность: результат должен быть однозначно определен +
    • +
    • + Монотонность: функция должна быть монотонной для корректности +
    • +
    + +

    Принцип математической индукции

    +

    Для доказательства свойств рекурсивно определенных объектов используется принцип математической индукции:

    +
      +
    • + База индукции: доказательство свойства для базового случая +
    • +
    • + Индуктивный шаг: доказательство того, что если свойство выполняется для n, то оно выполняется для n+1 +
    • +
    • + Заключение: свойство выполняется для всех объектов +
    • +
    + +

    Типизация рекурсивных выражений

    +

    Рекурсивные выражения могут иметь различные типизации:

    +
      +
    • + Рекурсивные множества имеют типизацию ℬ(H) +
    • +
    • + Рекурсивные функции имеют типизацию H₁ → H₂ +
    • +
    • + Рекурсивные предикаты имеют типизацию Logic +
    • +
    + +

    Применение в концептуальных схемах

    +

    + Рекурсивные выражения используются для определения сложных структур данных, бесконечных множеств и функций в + концептуальных схемах. Они позволяют описывать объекты с внутренней структурой и зависимостями. +

    +
    + ); +} diff --git a/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-set.tsx b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-set.tsx new file mode 100644 index 00000000..ecf8299f --- /dev/null +++ b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-set.tsx @@ -0,0 +1,85 @@ +export function HelpRSLangExpressionSet() { + return ( +
    +

    Операции с множествами

    +

    + Теоретико-множественные выражения в языке родов структур позволяют создавать и манипулировать множествами. + Результатом таких выражений является множество элементов определенной ступени. +

    + +

    Основные операции с множествами

    +
      +
    • + Объединение: A ∪ B - множество всех элементов, принадлежащих A или B +
    • +
    • + Пересечение: A ∩ B - множество всех элементов, принадлежащих и A, и B +
    • +
    • + Разность: A \ B - множество всех элементов A, не принадлежащих B +
    • +
    • + Симметрическая разность: A △ B - множество элементов, принадлежащих ровно одному из A или + B +
    • +
    • + Дополнение: A' - множество всех элементов универсального множества, не принадлежащих A +
    • +
    + +

    Конструкторы множеств

    +
      +
    • + Перечисление: {'{a, b, c}'} - множество из элементов a, b, c +
    • +
    • + Выделение: {'{x ∈ A | P(x)}'} - множество всех x из A, для которых выполняется P(x) +
    • +
    • + Замена: {'{f(x) | x ∈ A}'} - множество значений f(x) для всех x из A +
    • +
    • + Декартово произведение: A × B - множество всех пар (a, b), где a ∈ A, b ∈ B +
    • +
    • + Множество всех подмножеств: ℘(A) - множество всех подмножеств A +
    • +
    + +

    Специальные множества

    +
      +
    • + Пустое множество: - множество, не содержащее элементов +
    • +
    • + Универсальное множество: U - множество всех элементов рассматриваемой области +
    • +
    • + Синглтон: {'{a}'} - множество, содержащее только элемент a +
    • +
    + +

    Примеры выражений

    +
      +
    • + A ∪ (B ∩ C) - объединение A с пересечением B и C +
    • +
    • + {'{x ∈ A | x > 0}'} - множество всех положительных элементов из A +
    • +
    • + {'{x² | x ∈ {1, 2, 3}}'} - множество {'{(1, 4, 9)}'} +
    • +
    • + A × B × C - множество всех троек (a, b, c) +
    • +
    + +

    Типизация множеств

    +

    + Множество имеет типизацию ℬ(H), где H - ступень элементов множества. Например, множество целых + чисел имеет типизацию ℬ(Z). +

    +
    + ); +} diff --git a/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-structure.tsx b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-structure.tsx new file mode 100644 index 00000000..059d7341 --- /dev/null +++ b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-expression-structure.tsx @@ -0,0 +1,78 @@ +export function HelpRSLangExpressionStructure() { + return ( +
    +

    Структурные выражения

    +

    + Структурные выражения в языке родов структур позволяют манипулировать ступенями операндов. Эти выражения + используются для изменения структуры данных и создания новых типов на основе существующих. +

    + +

    Основные структурные операции

    +
      +
    • + Кортеж: (H₁, H₂, ..., Hₙ) - ступень кортежа арности n +
    • +
    • + Проекция: πᵢ(t) - извлечение i-го элемента кортежа t +
    • +
    • + Конкатенация кортежей: t₁ ⊕ t₂ - объединение двух кортежей +
    • +
    • + Структурирование: struct(field₁: H₁, field₂: H₂, ...) - создание структуры с именованными + полями +
    • +
    + +

    Операции с множествами структур

    +
      +
    • + Декартово произведение ступеней: H₁ × H₂ × ... × Hₙ - ступень n-арных кортежей +
    • +
    • + Степень ступени: Hⁿ - n-арное произведение ступени H на себя +
    • +
    • + Множество кортежей: ℬ(H₁ × H₂ × ... × Hₙ) - множество n-арных кортежей +
    • +
    + +

    Примеры структурных выражений

    +
      +
    • + (Z, Z) - ступень пар целых чисел +
    • +
    • + ℬ(Z × Z) - множество пар целых чисел +
    • +
    • + π₁((x, y)) - извлечение первого элемента кортежа +
    • +
    • + struct(name: Z, age: Z) - структура с полями name и age типа целых чисел +
    • +
    + +

    Типизация структурных выражений

    +

    Результат структурного выражения имеет типизацию, определяемую операцией:

    +
      +
    • + Кортеж имеет типизацию (H₁, H₂, ..., Hₙ) +
    • +
    • + Проекция кортежа имеет типизацию Hᵢ +
    • +
    • + Множество кортежей имеет типизацию ℬ(H₁ × H₂ × ... × Hₙ) +
    • +
    + +

    Применение в концептуальных схемах

    +

    + Структурные выражения используются для определения сложных типов данных в концептуальных схемах, таких как + записи, кортежи и структурированные множества. Они позволяют создавать формальные описания сложных объектов + предметной области. +

    +
    + ); +} diff --git a/rsconcept/frontend/src/features/help/items/rslang/help-rslang-interpret.tsx b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-interpret.tsx index 5942241e..6e3c50e8 100644 --- a/rsconcept/frontend/src/features/help/items/rslang/help-rslang-interpret.tsx +++ b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-interpret.tsx @@ -10,7 +10,7 @@ export function HelpRSLangInterpret() { содержания и схемных терминов и определений. Для этого в соответствии с{' '} вводятся списки объектов предметной области, соответствующих неопределяемым понятиям. При этом обеспечивается корректность отношений{' '} - для родовых структур. + для родовых структур.

    Интерпретация производных понятий может быть задана внешними методами либо автоматически вычислена с помощью diff --git a/rsconcept/frontend/src/features/help/items/rslang/help-rslang-literals.tsx b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-literals.tsx new file mode 100644 index 00000000..c4e53d0a --- /dev/null +++ b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-literals.tsx @@ -0,0 +1,63 @@ +import { LinkTopic } from '../../components/link-topic'; +import { HelpTopic } from '../../models/help-topic'; + +export function HelpRSLangLiterals() { + return ( +

    +

    Идентификаторы и литералы

    +

    + В языке родов структур идентификаторы и литералы имеют строгие правила записи, определяющие их роль в выражениях + и обеспечивающие однозначность интерпретации. +

    + +

    Правила написания идентификаторов

    +
      +
    • + Понятия — идентификаторы, начинающиеся с заглавной латинской буквы, соответствующей типу{' '} + : X1,F11,{' '} + D24. +
    • +
    • + Радикалы — обозначения для произвольных типизаций, используемые в{' '} + — идентификаторы, + начинающиеся с буквы R. +
    • +
    • + Переменные — идентификаторы, начинающиеся со строчной греческой или латинской буквы, например: + ξ, μ2, y1. +
    • +
    • + Специальные идентификаторы — зарезервированные слова и обозначения, имеющие фиксированное значение в + языке. +
    • +
    + +

    Литералы

    +

    + Литералы задают фиксированные значения в выражениях. В языке родов структур используются следующие виды + литералов: +

    +
      +
    • + Целые числа — последовательность цифр. Отрицательные числа не поддерживаются: + 0, 42. +
    • +
    • + Множество целых чисел — символ Z. +
    • +
    • + Пустое множество — символ . +
    • +
    + +

    Примеры

    +

    + Пример использования переменной и понятия: x ∈ X1, где x — переменная, а{' '} + X1 — понятие. +

    +

    + Пример с литералами: card(X1) = 5. +

    +
    + ); +} diff --git a/rsconcept/frontend/src/features/help/items/rslang/help-rslang-operations.tsx b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-operations.tsx index 62a78f19..ef3bd714 100644 --- a/rsconcept/frontend/src/features/help/items/rslang/help-rslang-operations.tsx +++ b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-operations.tsx @@ -47,7 +47,7 @@ export function HelpRSLangOperations() {

    Порождение полной совокупности термов, раскрывающих структуру выбранной конституенты. Операция применима к - терм-функциям, термам и родовым структурам с {' '} + терм-функциям, термам и родовым структурам с {' '} множество и кортеж.
    {'Generate(S1∈ℬ(X1×ℬ(X1))) = {Pr1(S1), Pr2(S1), red(Pr2(S1))}'} diff --git a/rsconcept/frontend/src/features/help/items/rslang/help-rslang-types.tsx b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-typification.tsx similarity index 98% rename from rsconcept/frontend/src/features/help/items/rslang/help-rslang-types.tsx rename to rsconcept/frontend/src/features/help/items/rslang/help-rslang-typification.tsx index de5db510..b5f3f437 100644 --- a/rsconcept/frontend/src/features/help/items/rslang/help-rslang-types.tsx +++ b/rsconcept/frontend/src/features/help/items/rslang/help-rslang-typification.tsx @@ -1,4 +1,4 @@ -export function HelpRSLangTypes() { +export function HelpRSLangTypification() { return (

    Типизация

    diff --git a/rsconcept/frontend/src/features/help/labels.ts b/rsconcept/frontend/src/features/help/labels.ts index f4ecc4b7..03132819 100644 --- a/rsconcept/frontend/src/features/help/labels.ts +++ b/rsconcept/frontend/src/features/help/labels.ts @@ -31,7 +31,17 @@ const labelHelpTopicRecord: Record = { [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.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]: 'формальные операции', diff --git a/rsconcept/frontend/src/features/help/models/help-topic.ts b/rsconcept/frontend/src/features/help/models/help-topic.ts index d16ace94..67f38150 100644 --- a/rsconcept/frontend/src/features/help/models/help-topic.ts +++ b/rsconcept/frontend/src/features/help/models/help-topic.ts @@ -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.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], diff --git a/rsconcept/frontend/src/features/help/pages/manuals-page/topic-page.tsx b/rsconcept/frontend/src/features/help/pages/manuals-page/topic-page.tsx index 7a1c1c4d..ca43cbdb 100644 --- a/rsconcept/frontend/src/features/help/pages/manuals-page/topic-page.tsx +++ b/rsconcept/frontend/src/features/help/pages/manuals-page/topic-page.tsx @@ -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 ; if (topic === HelpTopic.RSLANG) return ; - if (topic === HelpTopic.RSL_TYPES) return ; + if (topic === HelpTopic.RSL_LITERALS) return ; + if (topic === HelpTopic.RSL_TYPIFICATION) return ; + if (topic === HelpTopic.RSL_EXPRESSION_LOGIC) return ; + if (topic === HelpTopic.RSL_EXPRESSION_SET) return ; + if (topic === HelpTopic.RSL_EXPRESSION_STRUCTURE) return ; + if (topic === HelpTopic.RSL_EXPRESSION_ARITHMETIC) return ; + if (topic === HelpTopic.RSL_EXPRESSION_QUANTOR) return ; + if (topic === HelpTopic.RSL_EXPRESSION_DECLARATIVE) return ; + if (topic === HelpTopic.RSL_EXPRESSION_IMPERATIVE) return ; + if (topic === HelpTopic.RSL_EXPRESSION_RECURSIVE) return ; + if (topic === HelpTopic.RSL_EXPRESSION_PARAMETER) return ; if (topic === HelpTopic.RSL_CORRECT) return ; if (topic === HelpTopic.RSL_INTERPRET) return ; if (topic === HelpTopic.RSL_OPERATIONS) return ;