Порядок перезаписи

Переписываем s в t по правилу l :: = r . Если l и r связаны отношением перезаписи , то s и t тоже . Упорядочение simplifcation всегда относится л и S , а так же г и т .

В теоретической информатике , в частности, в автоматизированных рассуждениях о формальных уравнениях, порядок сокращения используется для предотвращения бесконечных циклов . Порядки перезаписи и, в свою очередь, соотношения перезаписи являются обобщениями этой концепции, которые оказались полезными в теоретических исследованиях.

Мотивация

Интуитивно, порядок сокращения R связывает два формальных выражения s и t, если t в некотором смысле «проще», чем s .

Например, упрощение терминов может быть частью программы компьютерной алгебры и может использовать набор правил { x +0 → x , 0+ x → x , x * 0 → 0, 0 * x → 0, x * 1 → x , 1 * x → x }. Чтобы доказать невозможность бесконечных циклов при упрощении термина, можно использовать порядок сокращения, определенный « sRt, если выражение t короче, чем выражение s »; применение любого правила из набора всегда правильно сокращает срок.

Напротив, чтобы установить прекращение «раздачи» с использованием правила x * ( y + z ) → x * y + x * z , потребуется более сложный порядок сокращения, поскольку это правило может увеличить размер срока к дублированию x . Теория заказов на перезапись направлена на то, чтобы помочь обеспечить соответствующий порядок в таких случаях.

Формальные определения

Формально бинарное отношение (→) на множестве терминов называется отношением перезаписи, если оно закрыто при контекстном вложении и при создании экземпляра ; формально: если l → r влечет u [ l σ ] _p → u [ r σ] _p для всех членов l , r , u , каждого пути p из u и каждой подстановки σ. Если (→) также иррефлексивно итранзитивным , то это называется порядок перезаписи , ^[1] или переписывания предзаказ . В последнем случае (→), кроме того , хорошо основана , это называется упорядочение сокращения , ^[2] или предпорядок сокращения . Учитывая бинарное отношение R , его переписывают замыкание является наименьшим переписывают отношение , содержащее R . ^[3] Транзитивное и рефлексивное отношение перезаписи, которое содержит подчлененный порядок, называется упорядочением упрощения . ^[4]

Обзор отношений перезаписи ^{[примечание 1]}
	переписать отношение	переписать заказ	порядок уменьшения	порядок упрощения
замкнутый в контексте x R y влечет u [ x ] _p R u [ y ] _p	да	да	да	да
замкнутый относительно экземпляра x R y влечет x σ R y σ	да	да	да	да
содержит подтермы отношения у подтерм из й влекут е R Y				да
рефлексивный всегда x R x		(Нет)	(Нет)	да
иррефлексивный никогда x R x		да	да	(Нет)
из транзитивных x R y и y R z следует x R z		да	да	да
обоснованная не бесконечная цепочка x ₁ R x ₂ R x ₃ R ...^{[примечание 2]}			да	(Да)

Характеристики

Обратное , то симметричное замыкание , то рефлексивное замыкание , и транзитивное замыкание из переписывания связи снова переписывание отношения, как и объединение и пересечение двух отношений перезаписи. ^[1]
Обратным порядком перезаписи снова является порядок перезаписи.
Несмотря на то, что существуют заказы на перезапись, которые являются суммарными по набору основных терминов (для краткости, «общая сумма»), ни один порядок перезаписи не может быть полным по набору всех терминов . ^{[примечание 3]}^[5]
Термин переписывания система ${л 1 :: = г 1, ..., л п :: = г п, ...}$ является завершение , если ее правила являются подмножеством упорядочения восстановления. ^{[примечание 4]}^[2]
И наоборот, для каждой системы перезаписи завершающих термов транзитивное замыкание (:: =) является упорядочением редукции ^[2], которое, однако, не обязательно может быть расширено до полного. Например, система переписывания основного члена { f ( a ) :: = f ( b ), g ( b ) :: = g ( a )} завершается, но может быть показана таким образом, используя порядок сокращения, только если константы a и b несравнимы. ^{[примечание 5]}^[6]
Общий и хорошо обоснованный порядок перезаписи ^{[примечание 6]} обязательно содержит правильное отношение подтермина на основных условиях. ^{[примечание 7]}
И наоборот, порядок перезаписи, который содержит отношение подтермина ^{[примечание 8]} , обязательно является хорошо обоснованным, когда набор функциональных символов конечен. ^[5]^{[примечание 9]}
Система переписывания конечных членов ${l 1 :: = r 1, ..., l n :: = r n, ...}$ завершается, если ее правила являются подмножеством строгой части упорядочения упрощения. ^[4]^[8]

Примечания

^ Записи в скобках указывают на предполагаемые свойства, которые не являются частью определения. Например, иррефлексивное отношение не может быть рефлексивным (на непустом множестве областей).
^ за исключением того, что все x _i равны для всех i за пределами некоторого n , для рефлексивного отношения
^ Так как x < y влечет y < x , поскольку последнее является примером первого для переменных x , y .
^ т.е. если $l i > r i$ для всех i , где (>) - порядок редукции; система не обязательно должна иметь конечное количество правил
^ Так как, например, $a > b$ подразумевает $g (a)> g (b)$ , это означает, что второе правило перезаписи не уменьшается.
^ т. е. общий порядок сокращения
^ Иначе, т | _p > t для некоторого члена t и позиции p , что подразумевает бесконечную убывающую цепочку t > t [ t ]_p > t [ t [ t ]_p ]_p > ...^[6]^[7]
^ т.е. упорядочение упрощения
^ Доказательство этого свойства основано на лемме Хигмана или, в более общем смысле, теореме Крускала о дереве .

использованная литература

Нахум Дершовиц ; Жан-Пьер Жуанно (1990). «Системы перезаписи». В Яне ван Леувене (ред.). Формальные модели и семантика . Справочник по теоретической информатике. B . Эльзевир. С. 243–320. DOI : 10.1016 / B978-0-444-88074-1.50011-1 . ISBN 9780444880741.

^ a b Дершовиц, Жуанно (1990), раздел 2.1, стр.251
^ a b c Dershowitz, Jouannaud (1990), раздел 5.1, стр.270
^ Дершоуиц, Jouannaud (1990), sect.2.2, с.252
^ a b Дершовиц, Жуанно (1990), раздел 5.2, стр.274
^ a b Дершовиц, Жуанно (1990), раздел 5.1, стр.272
^ a b Дершовиц, Жуанно (1990), раздел 5.1, стр.271
^ Дэвид А. Плейстед (1978). Рекурсивно определенный порядок доказывания прекращения системы перезаписи терминов (Технический отчет). Univ. Иллинойса, Департамент Comp. Sc. п. 52. Р-78-943.
^ Н. Дершовиц (1982). "Заказы для систем перезаписи терминов" (PDF) . Теорет. Comput. Sci . 17 (3): 279–301. DOI : 10.1016 / 0304-3975 (82) 90026-3 . S2CID 6070052 . Здесь: с.287; понятия названы несколько иначе.

[5] Записи в скобках указывают на предполагаемые свойства, которые не являются частью определения. Например, иррефлексивное отношение не может быть рефлексивным (на непустом множестве областей).

[6] за исключением того, что все x _i равны для всех i за пределами некоторого n , для рефлексивного отношения

[7] Так как x < y влечет y < x , поскольку последнее является примером первого для переменных x , y .

[9] т.е. если $l i > r i$ для всех i , где (>) - порядок редукции; система не обязательно должна иметь конечное количество правил

[10] Так как, например, $a > b$ подразумевает $g (a)> g (b)$ , это означает, что второе правило перезаписи не уменьшается.

[12] т. е. общий порядок сокращения

[14] Иначе, т | _p > t для некоторого члена t и позиции p , что подразумевает бесконечную убывающую цепочку t > t [ t ]_p > t [ t [ t ]_p ]_p > ...^[6]^[7]

[15] т.е. упорядочение упрощения

[16] Доказательство этого свойства основано на лемме Хигмана или, в более общем смысле, теореме Крускала о дереве .

[DJ90:251-1] Дершовиц, Жуанно (1990), раздел 2.1, стр.251

[DJ90:270-2] Dershowitz, Jouannaud (1990), раздел 5.1, стр.270

[DJ90:252-3] Дершоуиц, Jouannaud (1990), sect.2.2, с.252

[DJ90:274-4] Дершовиц, Жуанно (1990), раздел 5.2, стр.274

[DJ90:272-8] Дершовиц, Жуанно (1990), раздел 5.1, стр.272

[DJ90:271-11] Дершовиц, Жуанно (1990), раздел 5.1, стр.271

[13] Дэвид А. Плейстед (1978). Рекурсивно определенный порядок доказывания прекращения системы перезаписи терминов (Технический отчет). Univ. Иллинойса, Департамент Comp. Sc. п. 52. Р-78-943.

[17] Н. Дершовиц (1982). "Заказы для систем перезаписи терминов" (PDF) . Теорет. Comput. Sci . 17 (3): 279–301. DOI : 10.1016 / 0304-3975 (82) 90026-3 . S2CID 6070052 . Здесь: с.287; понятия названы несколько иначе.

[1]