Переписывание — широкий спектр техник, методов и теоретических результатов, связанных с процедурами последовательной замены частей формул или термов формального языка по заданной схеме — системе переписывающих правил. В наиболее общей форме речь идёт о совокупности некоторого набора объектов и правил — отношений между этими объектами, которые указывают как преобразовать этот набор.
Переписывание может быть недетерминированным. Например, система переписывающих правил может включать в себя правило, которое может быть применено к одному и тому же терму несколькими разными способами, но не содержать, при этом, указания на то, какой конкретно способ нужно применить в том или ином случае. Если система переписывания, всё же, оформлена в качестве однозначно понимаемого алгоритма, она может рассматриваться как компьютерная программа. На техниках переписывания основан ряд систем интерактивного доказательства теорем[1] и декларативных языков программирования[2][3].
Основные понятия и примеры
Основные свойства систем переписывания можно сформулировать, не прибегая к конкретной реализации их в виде операций над термами. Для этого часто используется понятие Абстрактной Системы Редукций или ARS (от англ. Abstract Reduction Systems). ARS состоит из некоторого множества A и набора бинарных отношений на нём, которые называются редукциями. Говорят, что a редуцируется или переписывается в b в один шаг относительно данной ARS, если пара (a,b) принадлежит некоторому . Важнейшими свойствами редукционных систем являются:
- Конфлюентность — если a может за некоторое число шагов редуцироваться как в b, так и в c, то существует элемент d, в который могут редуцироваться оба b и c.
- Остановочность — любая цепочка одношаговых редукций всегда конечна, то есть, достигается элемент, который не может больше быть редуцирован.
- Локальная (или слабая) конфлюентность — то же, что и конфлюентность, но при условии, что a переписывается в b и c ровно за один шаг.
- Слабая остановочность — для каждого элемента существует обрывающаяся цепочка его последовательных редукций.
- Каноничность или свойство Чёрча-Россера — конфлюентность плюс остановочность.
Очевидно, конфлюентность влечёт слабую конфлюенцию, а остановочность, соответственно, слабую остановочность. Однако, конфлюентность и остановочность между собой не связаны. Например, система, состоящая из одного правила a•b → b•a конфлюентна, но не остановочна. Система, состоящая из двух правил a → b и a → c остановочна, но не конфлюентна, а все три правила вместе образуют систему, которая и не остановочна и не конфлюентна.
Остановочность редукционной системы позволяет сопоставить каждому элементу его нормальную форму — элемент, в который его можно редуцировать, но который сам уже больше не редуцируется. Если вдобавок соблюдается конфлюентность, то такая нормальная форма всегда будет единственной, или канонической. В связи с этим, особо ценным является свойство Чёрча-Россера, так как позволяет быстро и эффективно решать проблему равенства двух элементов a и b относительно системы равенств, соответствующей множеству редукций без учёта направления. Для этого достаточно вычислить нормальные формы обоих элементов. Поскольку в этом случае нормальная форма будет также канонической, элементы будут равны, тогда и только тогда, когда результаты совпадут.
Классическая теория переписывания
Несмотря на то, что изначально понятие переписывания было введено для лямбда-исчисления, основной массив результатов и приложений в настоящее время касается переписывания первого порядка. Переписывающие системы такого рода называют Системами Переписывания Термов или TRS (от англ. Term rewriting systems).
Переписывание высших порядков
Системы переписывания высших порядков являются обобщением систем переписывания термов первого порядка на лямбда-термы, позволяя функции высших порядков и связанные переменные.[4] Различные результаты о системах переписывания термов первого порядка также могут быть переформулированы для высших порядков.[5]
См. также
- Алгоритм Кнута — Бендикса
- Лямбда-исчисление
- Переписывающая система
- Представление группы
- L-система
- Рефал
Примечания
- ↑ Jieh Hsiang, Hélène Kirchner, Pierre Lescanne, Michaël Rusinowitch. The term rewriting approach to automated theorem proving (англ.) // The Journal of Logic Programming. — 1992-10-01. — Vol. 14, iss. 1. — P. 71–99. — ISSN 0743-1066. — doi:10.1016/0743-1066(92)90047-7. Архивировано 6 мая 2021 года.
- ↑ Theory and practice of constraint handling rules (англ.) // The Journal of Logic Programming. — 1998-10-01. — Vol. 37, iss. 1—3. — P. 95–138. — ISSN 0743-1066. — doi:10.1016/S0743-1066(98)10005-5. Архивировано 5 июля 2022 года.
- ↑ Maude: specification and programming in rewriting logic (англ.) // Theoretical Computer Science. — 2002-08-28. — Vol. 285, iss. 2. — P. 187–243. — ISSN 0304-3975. — doi:10.1016/S0304-3975(01)00359-0. Архивировано 7 марта 2022 года.
- ↑ Wolfram, D. A. The Clausal Theory of Types. — Cambridge University Press, 1993. — P. 47–50. — ISBN 9780521395380. — doi:10.1017/CBO9780511569906.
- ↑ Nipkow, Tobias. Higher-Order Rewriting and Equational Reasoning // Automated Deduction - A Basis for Applications. Volume I: Foundations / Tobias Nipkow, Christian Prehofer. — Kluwer, 1998. — P. 399–430.
Литература
- Term Rewriting Systems, Terese, Cambridge Tracts in Theoretical Computer Science, 2003
- Term Rewriting and All That, Franz Baader and Tobias Nipkow, Cambridge University Press, 1998
Ссылки
- nLab authors rewriting. nLab (July 2023).
 | |
|---|---|
| В библиографических каталогах |
Эта страница в последний раз была отредактирована 9 января 2024 в 02:21.
Обычно почти сразу, изредка в течении часа.