Порядок охвата

s ≤ t если подтерм t , является замены s экземпляром .

Свойства [ править ]

Охватывание — это предварительный порядок , то есть рефлексивный и транзитивный , но не антисимметричный . ^{[примечание 1]} ни всего ^{[примечание 2]}
Соответствующее отношение эквивалентности , определяемое формулой s ~ t, если s ⩽ t ⩽ s , представляет собой равенство по модулю переименования .
s ≤ t всякий раз, s является подчленом t когда .
s ≤ t всякий раз, когда является экземпляром замены s t .
Объединение любого обоснованного порядка перезаписи R ^{[примечание 3]} с (<) является обоснованным , где (<) обозначает иррефлексивное ядро (≤). ^[3] В частности, (<) само по себе вполне обосновано.

^ поскольку и f ( x ) ≤ f ( y ) и f ( y ) ≤ f ( x ) для переменных символов x , y и функционального символа f
^ поскольку ни a ≤ b, ни b ≤ a для различных константных символов a , b
^ т.е. иррефлексивное, транзитивное и хорошо обоснованное бинарное отношение R такое, что sRt влечет u [ s σ ] _p R u [ t σ] _p всех термов s , t , u , каждого пути p u для и каждой замены σ

^ Жерар Юэ (1981). «Полное доказательство корректности алгоритма завершения Кнута – Бендикса» . Дж. Компьютер. Сист. Наука . 23 (1): 11–21. дои : 10.1016/0022-0000(81)90002-7 .
^ Н. Дершовиц, Ж.-П. Жуанно (1990). Ян ван Леувен (ред.). Переписать системы . Справочник по теоретической информатике. Том. Б. Эльзевир. стр. 243–320. Здесь: разд.2.1, с. 250
^ Дершовиц, Жуанно (1990), раздел 5.4, с. 278; несколько небрежно, R здесь должен быть «завершающим отношением перезаписи».

Эта по информатике статья незавершена . Вы можете помочь Википедии, расширив ее .