Переписывание (Hyjyhnvdfguny)

Перейти к навигации Перейти к поиску

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

Переписывание может быть недетерминированным. Например, система переписывающих правил может включать в себя правило, которое может быть применено к одному и тому же терму несколькими разными способами, но не содержать, при этом, указания на то, какой конкретно способ нужно применить в том или ином случае. Если система переписывания, всё же, оформлена в качестве однозначно понимаемого алгоритма, она может рассматриваться как компьютерная программа. На техниках переписывания основан ряд систем интерактивного доказательства теорем[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]

Примечания

[править | править код]
  1. 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 года.
  2. 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 года.
  3. 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 года.
  4. Wolfram, D. A. The Clausal Theory of Types. — Cambridge University Press, 1993. — P. 47–50. — ISBN 9780521395380. — doi:10.1017/CBO9780511569906.
  5. 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).