Переписывание

Материал из Seo Wiki - Поисковая Оптимизация и Программирование

Перейти к: навигация, поиск

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

Содержание

Основные понятия и примеры

Основные свойства систем переписывания можно сформулировать не прибегая к конкретной реализации их в виде операций над термами. Для этого часто используется понятие Абстрактной Системы Редукций или ARS (от англ. Abstract Reduction Systems). ARS состоит из некоторого множества A и набора бинарных отношений <math>(\to_{\alpha})_{\alpha\in I}</math>, на нём, которые называются редукциями. Говорят, что a редуцируется, или переписывается в b в один шаг относительно данной ARS, если пара (a,b) принадлежит некоторому <math>\to_{\alpha}</math>. Важнейшими свойствами редукционных систем являются:

  • Конфлюентность  — если a может за некоторое число шагов редуцироваться как в b так и в c, то существует элемент d, в который могут редуцироваться оба b и c.
  • Остановочность — любая цепочка одношаговых редукций всегда конечна, то есть достигается элемент, который не может больше быть редуцирован.
  • Локальная (или слабая) конфлюентность — то же, что и конфлюентность, но при условии, что a переписывается в b и c ровно за один шаг.
  • Слабая остановочность — для каждого элемента существует, обрывающаяся цепочка его последовательных редукций.
  • Каноничность или свойство Чёрча-Россера — конфлюентность плюс остановочность.

Очевидно, конфлюентность влечёт слабую конфлюенцию, а остановочность, соответственно, слабую остановочность. Однако, конфлюентность и остановочность между собой не связанны. Например, система, состоящая из одного правила a•b → b•a конфлюентна, но не остановочна. Система, состоящая из двух правил a → b и a → c остановочна, но не конфлюентна, а все три правила вместе образуют систему, которая и не остановочна и не конфлюентна.

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

Классическая теория переписывания

Несмотря на то, что изначально понятие переписывания было введено для лямбда-исчисления, основной массив результатов и приложений в настоящее время касается переписывания первого порядка. Переписывающие системы такого рода называют Системами Переписывания Термов или TRS (от англ. Term rewriting systems).

Переписывание высших порядков

Стратегии

Обобщения

Приложения

См. также

References

  • Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite Systems (1990). Chapter 6 of Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pp.243—320.
  • Term Rewriting Systems, Terese, Cambridge Tracts in Theoretical Computer Science, 2003
  • Term Rewriting and All That, Franz Baader and Tobias Nipkow, Cambridge University Press, 1998de:Termersetzungssystem

en:Rewriting fr:Réécriture (informatique) it:Riscrittura ja:項書き換え tr:Terimi yeniden yazma

Личные инструменты

Served in 0.100 secs.