ГОСТ Р 56271-2014
Приложение J
(обязательное)
Семантика шаблона
J.1 Правило переписывания
Нижеследующее определение взято дословно из определений 3.1 и 3.3 работы [22]. Изначально они пред
ставлены вработе [23]. где система переписывания паттерна (формы представления) называется системой пере
писывания высокого порядка.
Член t типа к в ^-нормальной форме называется паттерном (высокого порядка), если каждое свободное
использование переменной F является подчленом Р{йп)для I, гак что йп является rj-эквивапентом списка четко
выраженных связанных переменных.
Правило переписывания — это пара А.-членов / => г. таких, что / не является свободной переменной. / и
г имеют одинаковый базовый тип и fv(l) э МО- Правило переписывания паттерна — это правило переписы
вания. где I — это паттерн. Система переписывания паттерна (PRS) — это множество правил переписывания
паттернов.
При м е ча н и е - Указанные определения являются очень общими:
- элементы первого порядка N{x, у....), являющиеся левыми частями определений шаблонов, фактически
являются паттернами (в этом случав список аргументов й0пустой);
- если N{x. у....) ♦—о определение шаблона, то N{x. у. г) =>
0
— это правило переписывания паттерна.
Указанные определения использованы вместо стандартных понятий переписывания первого порядка.
Это гарантирует, что использование кванторов тела определения шаблона не нанесет вреда. Они также обе
спечат достаточно общие рамки рассмотрения в том случае, когда механизм шаблона потребуется
расширить в будущем.
J.2 Система переписывания паттернов, соответствующая множеству шаблонов
-
0
Система переписывания паттернов R(S). соответствующая множеству шаблонов S — это множество всех
правил N{x.y. z) =>р для всех N(x, у, z) *-* р e S.
Нижеследующая лемма гарантирует, что если учащается появление шаблонов в какой-либо заданной фор
муле. то;
а) в конечном счете, этот процесс прекращается, то есть зацикливания не происходит. Можно последова
тельно расширять шаблоны до тех пор. пока из них не получится формула, не имеющая к шаблонам никакого
отношения;
б) если эта формула и содержит ссылки на шаблоны, то. в конечном счете, все равно, в каком порядке про
исходит расширение, так как результат такого последовательного расширения всегда один и тот же.
Лемма 1 Форма представления R(S)является конечной и конфлюэнтной для любого множества логиче
ских шаблонов S.
Доказательство:Длядоказательства конечностисначала определяется порядок на множестве i
0
_>names(S)
для всех базовых символов и названий шаблонов. Пусть N> 0А если и только если существует определение ша
блона W(...)*-*pe S. такое что А появляется в & >-—это транзитивное замыкание, еслиопределено. Конструкция
множества логических шаблонов гарантирует, что > фактически является порядком, так как
>0
не может иметь
циклов. Кроме того, вследствие индуктивного характера определения множеств логических шаблонов понятие .-
хорошо обосновано. Это означает, что расширение мультимножества > для >----это задание хорошо обоснованно
го порядка на мультимножествах символов.
Теперь пусть р(
0
) — это мультимножество базовых символов и названий шаблонов в р. В частности, если
символ появляется несколько раз в . то он должен появиться в р($) такое же количество раз. Если однократное
использование шаблона N в р расширено по определению до о’, то в’появляется в N на один раз меньше р. не
считая дополнительных появлений символов в теле определения шаблона, что меньше N по отношению кПо
определению расширения мультимножества в процессе упорядочивания, это означает, что р($)> д(Р). Так как >-
вполне обосновано, тосразу следует, что расширение шаблона конечно.
Для доказательства конфлюэнтности. рассмотрим лемму «критической пары» для системы переписывания
паттернов. Это теорема 4.7 в работе [22]. Покажем, что все критические пары в R(S) сходятся к одной точке. Это
тривиальный случай, так какв R(S) критических пар нет: никаких символов не появляется в более чем одной левой
части правила в R(S). Что и требовалось доказать.
Этим можно воспользоваться для определения семантики шаблонов просто как окончательного резуль
тата последовательного расширения. Данная лемма гарантирует, что полученное определение будет пра
вильным.
88