ГОСТ Р 59791—2021
j
interpretablename считаются именами CL. Синтаксическое соответствие CLIF следует особенностям сопоставле
ния, определенным в таблицы А.2. Обратите внимание, что синтаксис комментариев CLIF обрабатывает выраже
ния с комментариями как идентичные по значению выражениям без комментариев, поэтому комментарий можно
считать «прикрепленным» к выражению без комментария.
А.4.2 Семантическая совместимость
CLIF — это семантическое расширение CL. Чтобы подтвердить, что CLIF является семантическим расшире
нием CL, необходимо показать, что если I является интерпретацией CLIF, то должна существовать интерпретация
CL, которая приписывает одинаковое значение истинности каждому высказыванию. Это будет продемонстрирова
но путем построения J из I с использованием обозначений и соглашений, приведенных выше при описании I и в
6.2 при описании J.
J имеет тот же словарь, что и I: UD^ = URj = U,,
relj
=
relj
и
furij = furij.
Интерпретация имен interpretablename
выполняется очевидным образом:
intj(x) = int^x)
для любого interpretablename х. Поскольку имена interpretedname
словаря CLIF классифицируются как имена CL, для
intj(x)
также необходимо давать определение, если х является
interpretedname. Это делается для обеспечения соответствия первым двум записям в семантической таблице CLIF, то
есть
intj(x)
= целое число, обозначаемое х, если х является десятичным числом, и
intj(x)
= строка символов
Юникода, обозначаемая х, если х является строкой в кавычках CLIF. После этого сравнение случаев показывает, что
J (s) = I (s) для любого высказывания s CLIF. Если s представляет собой текст с именем N, списком исключе ний
L и основным текстом В, следует показать, что J(s) = true, только если [J<L](B) = true и rel(J(N)) = UR^
j
<L* (т. к. UDj
= URj). Нетрудно заметить, что это в точности эквивалентно истинности высказывания I в «соленом» пере воде
основного текста, соответствующем таблице А.2, как описано в 6.2. (При формальном доказательстве будет
выполнена структурная индукция по высказываниям основного текста.) Следовательно, для любого текста t CLIF
J(t) = Kt).
Особенность заключается не в том, что если I представляет собой любую интерпретацию CL текста t CLIF,
то должна существовать интерпретация J CLIF, в которой t будет иметь такое же значение. Поскольку имена
interpretedname CLIF обрабатываются в CL как обычные имена, J может присвоить им значение, которое несо
вместимо с их фиксированной интерпретацией в CLIF, например J(‘a string’) = 3 не исключается правилами общей
логической семантики. Это обычное явление для любого диалекта, которое связывает заранее определенные
извне значения с некоторыми категориями имен, например числами или выражениями с типом данных. Такие диа
лекты могут поддерживать выводы, которые не допускается выразить как аксиомы CL, поэтому должны классифи
цироваться как внешние семантические расширения CL. Субдиалект CLIF, который не использует цифры и строки в
кавычках, отличается полной семантической совместимостью, что можно показать, инвертировав приведенную
выше конструкцию J из I.
32