ГОСТ Р 59791—2021
6.1.1.20 Нерегулярные высказывания в конкретном синтаксисе разделяются в абстрактный син
таксис как предложения (т. е. нульарные атомарные высказывания) с новым именем предиката. Та ким
образом, нерегулярные высказывания могут быть вложены в тексты, утверждения и (в остальном)
обычные составные высказывания, а семантика таких выражений определяется, как правило, на осно ве
таблицы 2.
6.1.1.21 Комментарий — это объект данных. К правильно построенным выражениям, которые
являются текстами, утверждениями, высказываниями или функциональными терминами, можно доба
вить любое количество комментариев. Тем не менее, это не относится к именам и маркерам последо
вательности и другим комментариям. Особые ограничения относительно характера комментариев CL
отсутствуют. В частности, комментарий может быть текстом CL. В некоторых диалектах могут действо
вать определенные ограничения на форму комментариев.
В 6.1 приведено полное описание абстрактной синтаксической структуры CL. Все полностью со
вместимые диалекты CL должны обеспечивать однозначное синтаксическое представление каждого из
вышеуказанных типов правильно построенных выражений.
Типы высказываний обычно обозначают включением явных текстовых строк, таких как «forall» для
универсального высказывания и «and» для конъюнкции. Однако ограничения относительно того, как
различные синтаксические категории могут быть представлены в поверхностных формах диалекта, от
сутствуют. В частности, выражения на диалекте не обязательно должны состоять из символьных строк.
6.1.2 Метамодель абстрактного синтаксиса общей логики
6.1.2.1 Имена и маркеры последовательности
Классы имен и маркеров последовательности в языке CL получены из строк с использованием
следующих операторов:
-
Voc : String
—>
V;
- Seqmark
:
String —>Smark;
- Titling
:
String —> Ttl;
- Binder =V(J Smark.
6.1.2.2 Термины и последовательности терминов
Класс терминов в языке CL — это класс Term, который включает в себя все имена из V и все
функциональные термины. Класс функциональных терминов в языке CL — это класс FunctionalTerm,
создаваемый за счет рекурсивного применения оператора
Func1)
к парам, состоящим из одного тер
мина и одной последовательности терминов. Класс последовательностей терминов в языке CL — это
класс TermSequence, который включает все конечные последовательности терминов и/или маркеров
последовательности.
-
Func Term
х
TermSequence
—>
FunctionalTerm;
- Term = V
и
FunctionalTerm;
- TSeq:\Term
и
Smark)
x ... x
{Term
U
Smark) —> TermSequence.
6.1.2.3 Высказывания
Класс высказывания в языке CL — это класс Sentence, который включает в себя все простые
высказывания (включая уравнения, если таковые имеются), сформированные путем применения ато
марных (и Id) операций из правильно построенных терминов и последовательностей терминов, а также
всех составных высказываний, образованных путем рекурсивного применения набора операций Neg,
Conj, Disj, Cond, BiCond, EQuant и UQuant, которые отвечают следующим условиям:
- каждая операция взаимно однозначна;
►
►
- наборы операций отделены попарно и не пересекаются с множеством терминов Л:
-
Atomic-Term
х
TermSequence
—>
Sentence;
- Id: Term
x
Term
—>
Sentence;
- Neg-.Sentence
—>
Sentence;
- Conj: Sentence
x... x
Sentence
—»
Sentence;
- Disj: Sentence
x ... x
Sentence —*■Sentence; -
Cond: Sentence
x
Sentence
—>
Sentence;
- BiCond-.Sentence
x
Sentence
—
Sentence;
- EQuant-.Binder x...
x
Binder
x
Sentence
—
Sentence, n >
0;
-
UQuant.Binder x
... x
Binder x Sentence
—>
Sentence, n > 0.
1)
Здесь и далее по тексту названия классов, терминов, операций приведены сзаглавной буквы курсивом.
7