Критическая пара (переписывание термина)

Критическая пара возникает в системе переписывания терминов , когда два правила переписывания перекрываются, образуя два разных термина. Более подробно, ( t ₁ , t ₂ ) является критической парой, если существует термин t, для которого два разных применения правила перезаписи (либо одно и то же правило, применяемое по-разному, либо два разных правила) дают термины t ₁ и t ₂ .

Определения

Фактическое определение критической пары немного сложнее, поскольку оно исключает пары, которые можно получить из критических пар путем замены, и ориентирует пару на основе перекрытия. В частности, для пары перекрывающихся правил $\rho _{0}:l_{0}\to r_{0}$ и $\rho _{1}:l_{1}\to r_{1}$ , при этом перекрытие заключается в том, что $l_{0}=D[s]$ для некоторого непустого контекста $D[\;]$ и термин $s$ (это не переменная) соответствует $l_{1}$ при некоторых заменах $s\sigma =l_{1}\tau$ которые являются наиболее общими, критическая пара — это $(D\sigma [r_{1}\tau ],r_{0}\sigma )$ . ^{[ 1 ]}

Когда обе части критической пары можно свести к одному и тому же члену, критическая пара называется сходящейся . Если одна сторона критической пары идентична другой, критическая пара называется тривиальной .

Примеры

Например, в термине «система переписывания с правилами»

ж ( г ( Икс , у ), z )	→ г ( Икс , z )
г ( х , у )	→ х ,

единственная критическая пара - это ⟨ g ( x , z ), f ( x , z )⟩. Оба эти термина могут быть получены из термина f ( g ( x , y ), z ) путем применения одного правила перезаписи.

В качестве другого примера рассмотрим систему переписывания терминов с единственным правилом.

е ( х , у )

→ х .

Применяя это правило двумя разными способами к термину f ( f ( x , x ), x ), мы видим, что ( f ( x , x ), f ( x , x )) является (тривиальной) критической парой.

Лемма о критической паре

Слияние явно подразумевает сходящиеся критические пары: если возникает какая-либо критическая пара ⟨ a , b ⟩, то a и b имеют общую редукцию и, следовательно, критическая пара сходится. Если система переписывания терминов не является слиянием , критическая пара может не сходиться, поэтому критические пары являются потенциальными источниками, где слияние не удастся.

Лемма о критической паре утверждает, что система переписывания терминов слабо (т.е. локально) конфлюэнтна тогда и только тогда, когда все критические пары сходятся. Таким образом, чтобы выяснить, является ли система переписывания терминов слабо конфлюэнтной, достаточно протестировать все критические пары и посмотреть, сходятся ли они. Это позволяет алгоритмически выяснить, является ли система переписывания терминов слабо конфлюэнтной или нет, учитывая, что можно алгоритмически проверить, сходятся ли два термина.

См. также

Завершение Кнута – Бендикса , алгоритм, основанный на критических парах для вычисления сливающейся и завершающей системы переписывания терминов, эквивалентной заданной.

Внешние ссылки

Вайсштейн, Эрик В. «Критическая пара» . Математический мир .

Ссылки

^ Тереза (2003). Системы переписывания терминов . Кембридж, Великобритания: Издательство Кембриджского университета. п. 53. ИСБН 0-521-39115-6 .

Франц Баадер и Тобиас Нипков , «Переписывание терминов и все такое» , Cambridge University Press, 1998 (ссылка на книгу)

[1] Тереза (2003). Системы переписывания терминов . Кембридж, Великобритания: Издательство Кембриджского университета. п. 53. ИСБН 0-521-39115-6 .

[ 1 ]