Переписать заказ
В теоретической информатике , в частности в автоматизированных рассуждениях о формальных уравнениях, порядок сокращения используется для предотвращения бесконечных циклов . Порядки перезаписи и, в свою очередь, отношения перезаписи являются обобщениями этой концепции, оказавшимися полезными в теоретических исследованиях.
Мотивация
[ редактировать ]Интуитивно понятно, что порядок приведения R связывает два термина s и t, если t в некотором смысле «простее», чем s .
Например, упрощение терминов может быть частью программы компьютерной алгебры и может осуществляться с использованием набора правил { x +0 → x , 0+ x → x , x *0 → 0, 0* x → 0, x * 1 → х , 1* х → х }. Чтобы доказать невозможность бесконечных циклов при упрощении термина с использованием этих правил, порядок сокращения, определяемый « 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 ]
- Обратным порядку перезаписи снова является порядок перезаписи.
- Хотя существуют заказы на перезапись, которые являются полными для набора основных терминов (для краткости «основной итог»), ни один заказ на перезапись не может быть полным для набора всех терминов . [ примечание 3 ] [ 5 ]
- Система переписывания терминов { l 1 ::= r 1 ,..., l n ::= r n , ...} завершается , если ее правила являются подмножеством редукционного порядка. [ примечание 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). «Переписать системы». Ян ван Леувен (ред.). Формальные модели и семантика . Справочник по теоретической информатике. Том. Б. Эльзевир. стр. 243–320. дои : 10.1016/B978-0-444-88074-1.50011-1 . ISBN 9780444880741 .
- ^ Перейти обратно: а б Дершовиц, Жуанно (1990), разд.2.1, стр.251
- ^ Перейти обратно: а б с Дершовиц, Жуанно (1990), разд.5.1, стр.270
- ^ Дершовиц, Жуанно (1990), раздел 2.2, стр.252
- ^ Перейти обратно: а б Дершовиц, Жуанно (1990), разд.5.2, стр.274
- ^ Перейти обратно: а б Дершовиц, Жуанно (1990), разд.5.1, стр.272
- ^ Перейти обратно: а б Дершовиц, Жуанно (1990), разд.5.1, стр.271
- ^ Дэвид А. Плейстед (1978). Рекурсивно определенный порядок доказательства прекращения действия систем переписывания терминов (технический отчет). унив. штата Иллинойс, Департамент Comp. наук. п. 52. Р-78-943.
- ^ Н. Дершовиц (1982). «Заказы на системы переписывания терминов» (PDF) . Теория. Вычислить. Наука . 17 (3): 279–301. дои : 10.1016/0304-3975(82)90026-3 . S2CID 6070052 . Здесь: стр.287; понятия называются немного по-другому.