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

В математике , информатике и логике переписывание охватывает широкий спектр методов замены подтермов формулы другими терминами . Такие методы могут быть реализованы с помощью систем переписывания (также известных как системы переписывания , механизмы переписывания , ^{[1] [2]} или системы редукции ). В своей самой базовой форме они состоят из набора объектов, а также отношений о том, как преобразовывать эти объекты.

Переписывание может быть недетерминированным . Одно правило для переписывания термина может быть применено многими различными способами к этому термину, или может быть применено более одного правила. Системы переписывания тогда не предоставляют алгоритм для изменения одного термина на другой, а набор возможных применений правил. Однако в сочетании с соответствующим алгоритмом системы переписывания можно рассматривать как компьютерные программы , и несколько доказателей теорем ^[3] и декларативные языки программирования основаны на переписывании терминов. ^{[4] [5]}

В логике процедура получения конъюнктивной нормальной формы (КНФ) формулы может быть реализована как система переписывания. ^[6] Правила примера такой системы будут следующими:

${\displaystyle \neg \neg A\to A}$( устранение двойного отрицания )

${\displaystyle \neg (A\land B)\to \neg A\lor \neg B}$( Законы Де Моргана )

${\displaystyle \neg (A\or B)\to \neg A\land \neg B}$

${\displaystyle (A\land B)\lor C\to (A\lor C)\land (B\lor C)}$( распределительность )

${\displaystyle A\lor (B\land C)\to (A\lor B)\land (A\lor C),}$^{[примечание 1]}

где символ ( ) указывает, что выражение, соответствующее левой части правила, может быть переписано в выражение, образованное правой частью, а каждый символ обозначает подвыражение. В такой системе каждое правило выбирается так, чтобы левая часть была эквивалентна правой, и, следовательно, когда левая часть соответствует подвыражению, выполнение переписывания этого подвыражения слева направо сохраняет логическую последовательность и значение всего выражения.${\displaystyle \to}$

Системы переписывания терминов могут использоваться для вычисления арифметических операций над натуральными числами . Для этого каждое такое число должно быть закодировано как термин . Простейшая кодировка — та, которая используется в аксиомах Пеано , основанная на константе 0 (нуле) и функции-преемнике S. Например, числа 0, 1, 2 и 3 представлены терминами 0, S(0), S(S(0)) и S(S(S(0))), соответственно. Следующая система переписывания терминов может затем использоваться для вычисления суммы и произведения данных натуральных чисел. ^[7]

${\displaystyle {\begin{align}A+0&\to A&{\textrm {(1)}},\\A+S(B)&\to S(A+B)&{\textrm {(2)}},\\A\cdot 0&\to 0&{\textrm {(3)}},\\A\cdot S(B)&\to A+(A\cdot B)&{\textrm {(4)}}.\end{align}}}$

Например, вычисление 2+2, дающее в результате 4, можно продублировать, переписав термин следующим образом:

${\displaystyle S(S(0))+S(S(0))}$ ${\displaystyle \;\;{\stackrel {(2)}{\to }}\;\;}$ ${\displaystyle S(\;S(S(0))+S(0)\;)}$ ${\displaystyle \;\;{\stackrel {(2)}{\to }}\;\;}$ ${\displaystyle S(S(\;S(S(0))+0\;))}$ ${\displaystyle \;\;{\stackrel {(1)}{\to }}\;\;}$ ${\displaystyle S(S(S(S(0)))),}$

где номера правил указаны над стрелкой «переписать-ту» .

В качестве другого примера, вычисление 2⋅2 выглядит так:

${\displaystyle S(S(0))\cdot S(S(0))}$ ${\displaystyle \;\;{\stackrel {(4)}{\to }}\;\;}$ ${\displaystyle S(S(0))+S(S(0))\cdot S(0)}$ ${\displaystyle \;\;{\stackrel {(4)}{\to }}\;\;}$ ${\displaystyle S(S(0))+S(S(0))+S(S(0))\cdot 0}$ ${\displaystyle \;\;{\stackrel {(3)}{\to }}\;\;}$ ${\displaystyle S(S(0))+S(S(0))+0}$ ${\displaystyle \;\;{\stackrel {(1)}{\to }}\;\;}$ ${\displaystyle S(S(0))+S(S(0))}$ ${\displaystyle \;\;{\stackrel {\textrm {s.a.}}{\to }}\;\;}$ ${\displaystyle S(S(S(S(0)))),}$

где последний шаг включает в себя вычисления предыдущего примера.

В лингвистике правила структуры фраз , также называемые правилами переписывания , используются в некоторых системах генеративной грамматики [ ^8] как средство генерации грамматически правильных предложений языка. Такое правило обычно имеет вид , где A — метка синтаксической категории , такая как именная группа или предложение , а X — последовательность таких меток или морфем , выражающая тот факт, что A может быть заменено на X при генерации составной структуры предложения. Например, правило означает, что предложение может состоять из именная группа (NP), за которой следует глагольная группа (VP); дальнейшие правила будут указывать, из каких подсоставляющих могут состоять именная группа и глагольная группа, и так далее.${\displaystyle {\rm {A\rightarrow X}}}$${\displaystyle {\rm {S\rightarrow NP\ VP}}}$

Из приведенных выше примеров ясно, что мы можем думать о переписывании систем в абстрактной манере. Нам нужно указать набор объектов и правила, которые могут быть применены для их преобразования. Наиболее общая (одномерная) установка этого понятия называется абстрактной системой редукции ^[9] или абстрактной системой переписывания (сокращенно ARS ). ^[10] ARS — это просто набор A объектов вместе с бинарным отношением → на A , называемым отношением редукции , отношением переписывания ^[11] или просто редукцией . ^[9]

Многие понятия и обозначения могут быть определены в общем случае ARS. является рефлексивным транзитивным замыканием . является симметричным замыканием . является рефлексивным транзитивным симметричным замыканием . Текстовая проблема для ARS заключается в определении, при заданных x и y , является ли . Объект x в A называется приводимым , если существует некоторый другой y в A такой, что ; в противном случае он называется неприводимым или нормальной формой . Объект y называется "нормальной формой x ", если , и y неприводим. Если нормальная форма x уникальна, то это обычно обозначается как . Если каждый объект имеет хотя бы одну нормальную форму, ARS называется нормализующей . или x и y называются соединяемыми , если существует некоторый z со свойством, что . Говорят, что ARS обладает свойством Чёрча–Россера, если влечет . ARS является конфлюэнтной , если для всех w , x и y в A , влечет . ARS локально конфлюэнтна тогда и только тогда, когда для всех w , x и y в A , следует . ARS называется терминирующей или нётеровой, если нет бесконечной цепи . Конфлюэнтная и терминирующая ARS называется сходящейся или канонической .${\displaystyle {\overset {*}{\rightarrow }}}$${\displaystyle \rightarrow }$${\displaystyle \leftrightarrow }$${\displaystyle \rightarrow }$${\displaystyle {\overset {*}{\leftrightarrow }}}$${\displaystyle \rightarrow }$${\displaystyle x{\overset {*}{\leftrightarrow }}y}$${\displaystyle x\rightarrow y}$${\displaystyle x{\stackrel {*}{\rightarrow }}y}$${\displaystyle x{\downarrow }}$${\displaystyle x\downarrow y}$${\displaystyle x{\overset {*}{\rightarrow }}z{\overset {*}{\leftarrow }}y}$${\displaystyle x{\overset {*}{\leftrightarrow }}y}$${\displaystyle x\downarrow y}$${\displaystyle x{\overset {*}{\leftarrow }}w{\overset {*}{\rightarrow }}y}$${\displaystyle x\downarrow y}$${\displaystyle x\leftarrow w\rightarrow y}$${\displaystyle x{\mathbin {\downarrow }}y}$${\displaystyle x_{0}\rightarrow x_{1}\rightarrow x_{2}\rightarrow \cdots }$

Важными теоремами для абстрактных переписывающих систем являются то, что ARS является конфлюэнтной тогда и только тогда, когда она обладает свойством Чёрча–Россера, лемма Ньюмена (конечная ARS является конфлюэнтной тогда и только тогда, когда она локально конфлюэнтна), и что проблема слов для ARS в общем случае неразрешима .

Система перезаписи строк (SRS), также известная как система полу-Туэ , использует свободную моноидную структуру строк ( слов) над алфавитом для расширения отношения перезаписи, , на все строки в алфавите, которые содержат левую и, соответственно, правую части некоторых правил в качестве подстрок . Формально система полу-Туэ — это кортеж , где — (обычно конечный) алфавит, а — бинарное отношение между некоторыми (фиксированными) строками в алфавите, называемое набором правил перезаписи . Отношение перезаписи в один шаг, индуцированное на , определяется как: если есть какие-либо строки, то если существуют такие, что , и . Поскольку — отношение на , пара соответствует определению абстрактной системы перезаписи. Поскольку пустая строка находится в , — подмножество . Если отношение симметрично , то система называется системой Туэ .${\displaystyle R}$ ${\displaystyle (\Sigma ,R)}$${\displaystyle \Sigma }$${\displaystyle R}$ ${\displaystyle {\underset {R}{\rightarrow }}}$${\displaystyle R}$${\displaystyle \Sigma ^{*}}$${\displaystyle s,t\in \Sigma ^{*}}$${\displaystyle s{\underset {R}{\rightarrow }}t}$${\displaystyle x,y,u,v\in \Sigma ^{*}}$${\displaystyle s=xuy}$${\displaystyle t=xvy}$${\displaystyle uRv}$${\displaystyle {\underset {R}{\rightarrow }}}$${\displaystyle \Sigma ^{*}}$${\displaystyle (\Sigma ^{*},{\underset {R}{\rightarrow }})}$${\displaystyle \Sigma ^{*}}$${\displaystyle R}$${\displaystyle {\underset {R}{\rightarrow }}}$${\displaystyle R}$

В SRS отношение редукции совместимо с моноидной операцией, то есть подразумевает для всех строк . Аналогично, рефлексивное транзитивное симметричное замыкание , обозначаемое , является конгруэнцией , то есть это отношение эквивалентности (по определению), и оно также совместимо с конкатенацией строк. Отношение называется конгруэнцией Туэ, порожденной . В системе Туэ, то есть если симметрично, отношение перезаписи совпадает с конгруэнцией Туэ .${\displaystyle {\overset {*}{\underset {R}{\rightarrow }}}}$${\displaystyle x{\overset {*}{\underset {R}{\rightarrow }}}y}$${\displaystyle uxv{\overset {*}{\underset {R}{\rightarrow }}}uyv}$${\displaystyle x,y,u,v\in \Sigma ^{*}}$${\displaystyle {\underset {R}{\rightarrow }}}$${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$${\displaystyle R}$${\displaystyle R}$${\displaystyle {\overset {*}{\underset {R}{\rightarrow }}}}$${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$

Понятие полусистемы Туэ по сути совпадает с представлением моноида . Поскольку является конгруэнцией, мы можем определить фактормоноид свободного моноида с помощью конгруэнции Туэ. Если моноид изоморфен , то полусистема Туэ называется представлением моноида .${\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}$ ${\displaystyle {\mathcal {M}}_{R}=\Sigma ^{*}/{\overset {*}{\underset {R}{\leftrightarrow }}}}$${\displaystyle \Sigma ^{*}}$${\displaystyle {\mathcal {M}}}$${\displaystyle {\mathcal {M}}_{R}}$${\displaystyle (\Sigma ,R)}$${\displaystyle {\mathcal {M}}}$

Мы сразу же получаем некоторые очень полезные связи с другими областями алгебры. Например, алфавит с правилами , где — пустая строка , является представлением свободной группы на одном генераторе. Если вместо этого правилами являются только , то мы получаем представление бициклического моноида . Таким образом, полусистемы Туэ представляют собой естественную структуру для решения проблемы слов для моноидов и групп. Фактически, каждый моноид имеет представление в виде , т. е. он всегда может быть представлен полусистемой Туэ, возможно, над бесконечным алфавитом.${\displaystyle \{a,b\}}$${\displaystyle \{ab\rightarrow \varepsilon ,ba\rightarrow \varepsilon \}}$${\displaystyle \varepsilon }$${\displaystyle \{ab\rightarrow \varepsilon \}}$${\displaystyle (\Sigma ,R)}$

Проблема слов для полусистемы Туэ в общем случае неразрешима; этот результат иногда называют теоремой Поста–Маркова . ^[12]

Система переписывания терминов ( TRS ) — это система переписывания, объектами которой являются термины , которые являются выражениями с вложенными подвыражениями. Например, система, показанная в разделе § Логика выше, является системой переписывания терминов. Термины в этой системе состоят из бинарных операторов и и унарного оператора . В правилах также присутствуют переменные, которые представляют любой возможный термин (хотя одна переменная всегда представляет один и тот же термин в пределах одного правила).${\displaystyle (\vee )}$${\displaystyle (\wedge )}$${\displaystyle (\neg )}$

В отличие от систем переписывания строк, объектами которых являются последовательности символов, объекты системы переписывания терминов образуют алгебру терминов . Термин можно визуализировать как дерево символов, причем набор допустимых символов фиксируется заданной сигнатурой . Как формализм, системы переписывания терминов обладают полной мощью машин Тьюринга , то есть каждая вычислимая функция может быть определена системой переписывания терминов. ^[13]

Некоторые языки программирования основаны на переписывании терминов. Одним из таких примеров является Pure, функциональный язык программирования для математических приложений. ^{[14] [15]}

Правило перезаписи — это пара терминов , обычно записываемых как , для указания того, что левая часть l может быть заменена правой частью r . Система перезаписи терминов — это набор R таких правил. Правило может быть применено к термину s , если левый термин l соответствует некоторому подтерму s , то есть если существует некоторая подстановка, такая что подтерм корня в некоторой позиции p является результатом применения подстановки к термину l . Подтерм, соответствующий левой части правила, называется редексом или приводимым выражением . ^[16] Результирующий термин t применения этого правила является тогда результатом замены подтерма в позиции p в s на термин с примененной подстановкой , см. рисунок 1. В этом случае говорят, что он переписан за один шаг или переписан напрямую в системой , формально обозначаемой как , или как некоторыми авторами.${\displaystyle l\rightarrow r}$${\displaystyle l\rightarrow r}$ ${\displaystyle \sigma }$${\displaystyle s}$ ${\displaystyle \sigma }$${\displaystyle r}$${\displaystyle \sigma }$${\displaystyle s}$${\displaystyle t}$${\displaystyle R}$${\displaystyle s\rightarrow _{R}t}$${\displaystyle s{\underset {R}{\rightarrow }}t}$${\displaystyle s{\overset {R}{\rightarrow }}t}$

Если термин может быть переписан в несколько шагов в термин , то есть, если , то говорят, что термин переписан в , формально обозначаемый как . Другими словами, отношение является транзитивным замыканием отношения ; часто также нотация используется для обозначения рефлексивно-транзитивного замыкания , то есть, если или . ^[17] Переписывание термина, заданное набором правил, можно рассматривать как абстрактную систему переписывания, как определено выше, с терминами в качестве ее объектов и в качестве ее отношения переписывания.${\displaystyle t_{1}}$${\displaystyle t_{n}}$${\displaystyle t_{1}{\underset {R}{\rightarrow }}t_{2}{\underset {R}{\rightarrow }}\cdots {\underset {R}{\rightarrow }}t_{n}}$${\displaystyle t_{1}}$${\displaystyle t_{n}}$${\displaystyle t_{1}{\overset {+}{\underset {R}{\rightarrow }}}t_{n}}$${\displaystyle {\overset {+}{\underset {R}{\rightarrow }}}}$${\displaystyle {\underset {R}{\rightarrow }}}$${\displaystyle {\overset {*}{\underset {R}{\rightarrow }}}}$${\displaystyle {\underset {R}{\rightarrow }}}$${\displaystyle s{\overset {*}{\underset {R}{\rightarrow }}}t}$${\displaystyle s=t}$${\displaystyle s{\overset {+}{\underset {R}{\rightarrow }}}t}$${\displaystyle R}$${\displaystyle {\underset {R}{\rightarrow }}}$

Например, — это правило перезаписи, обычно используемое для установления нормальной формы относительно ассоциативности . Это правило можно применить к числителю в члене с соответствующей заменой , см. рисунок 2. ^{[примечание 2]} Применение этой замены к правой части правила дает член , а замена числителя этим членом дает , который является результирующим членом применения правила перезаписи. В целом, применение правила перезаписи достигло того, что называется «применением закона ассоциативности для к » в элементарной алгебре. С другой стороны, правило можно было бы применить к знаменателю исходного члена, получив .${\displaystyle x*(y*z)\rightarrow (x*y)*z}$${\displaystyle *}$${\displaystyle {\frac {a*((a+1)*(a+2))}{1*(2*3)}}}$${\displaystyle \{x\mapsto a,\;y\mapsto a+1,\;z\mapsto a+2\}}$${\displaystyle (a*(a+1))*(a+2)}$${\displaystyle {\frac {(a*(a+1))*(a+2)}{1*(2*3)}}}$${\displaystyle *}$${\displaystyle {\frac {a*((a+1)*(a+2))}{1*(2*3)}}}$${\displaystyle {\frac {a*((a+1)*(a+2))}{(1*2)*3}}}$

Вопросы завершения систем переписывания в целом рассматриваются в разделе Abstract rewriting system#Termination and convergence . Для систем переписывания терминов в частности необходимо учитывать следующие дополнительные тонкости.

Завершение даже системы, состоящей из одного правила с линейной левой частью, неразрешимо. ^{[18] [19]} Завершение также неразрешимо для систем, использующих только унарные функциональные символы; однако, оно разрешимо для конечных основных систем. ^[20]

Следующая система перезаписи терминов является нормализующей, ^{[примечание 3],} но не завершающей, ^{[примечание 4]} и не конфлюэнтной: ^[21]$${\displaystyle {\begin{aligned}f(x,x)&\rightarrow g(x),\\f(x,g(x))&\rightarrow b,\\h(c,x)&\rightarrow f(h(x,c),h(x,x)).\\\end{aligned}}}$$

Следующие два примера систем переписывания терминов, завершающих работу, принадлежат Тояме: ^[22]

${\displaystyle f(0,1,x)\rightarrow f(x,x,x)}$

и

${\displaystyle g(x,y)\rightarrow x,}$

${\displaystyle g(x,y)\rightarrow y.}$

Их союз — это непрекращающаяся система, поскольку

$${\displaystyle {\begin{aligned}&f(g(0,1),g(0,1),g(0,1))\\\rightarrow &f(0,g(0,1),g(0,1))\\\rightarrow &f(0,1,g(0,1))\\\rightarrow &f(g(0,1),g(0,1),g(0,1))\\\rightarrow &\cdots \end{aligned}}}$$Этот результат опровергает гипотезу Дершовица ^[23], который утверждал, что объединение двух терминирующих переписывающих систем и снова является терминирующим, если все левые части и правые части линейны , и нет « перекрытий » между левыми частями и правыми частями . Все эти свойства удовлетворяются примерами Тоямы.${\displaystyle R_{1}}$${\displaystyle R_{2}}$${\displaystyle R_{1}}$${\displaystyle R_{2}}$${\displaystyle R_{1}}$${\displaystyle R_{2}}$

См. разделы Порядок перезаписи и Упорядочение путей (перезапись терминов) для получения информации об отношениях упорядочения, используемых в доказательствах завершения для систем перезаписи терминов.

Системы переписывания высшего порядка являются обобщением систем переписывания терминов первого порядка до лямбда-термов , допускающих функции высшего порядка и связанные переменные. ^[24] Различные результаты о TRS первого порядка можно переформулировать и для HRS. ^[25]

Системы перезаписи графов являются еще одним обобщением систем перезаписи терминов, оперирующих графами вместо ( основных ) терминов / их соответствующего древовидного представления.

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

• Критическая пара (логика)
• Компилятор
• Алгоритм завершения Кнута-Бендикса
• L-системы определяют перезапись, которая выполняется параллельно.
• Ссылочная прозрачность в информатике
• Регулируемое переписывание
• Сети взаимодействия

• Баадер, Франц ; Нипков, Тобиас (1999). Переписывание терминов и все такое . Cambridge University Press. ISBN 978-0-521-77920-3.316 страниц.
• Marc Bezem, Jan Willem Klop , Roel de Vrijer («Terese»), Term Rewriting Systems («TeReSe»), Cambridge University Press, 2003, ISBN 0-521-39115-6 . Это самая последняя всеобъемлющая монография. Однако в ней используется довольно много еще нестандартных обозначений и определений. Например, свойство Чёрча–Россера определяется как идентичное слиянию. 
• Нахум Дершовиц и Жан-Пьер Жуанно «Системы перезаписи», Глава 6 в Jan van Leeuwen (ред.), Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics. , Elsevier и MIT Press, 1990, ISBN 0-444-88074-7 , стр. 243–320. Препринт этой главы находится в свободном доступе у авторов, но в нем отсутствуют рисунки. 
• Нахум Дершовиц и Дэвид Плейстед . «Переписывание», Глава 9 в книге Джона Алана Робинсона и Андрея Воронкова (редакторы), Справочник по автоматизированному рассуждению , Том 1 .
• Жерар Юэ и Дерек Оппен, Уравнения и правила перезаписи, Исследование (1980), Стэнфордская группа проверки, Отчет № 15, Отчет Департамента компьютерных наук № STAN-CS-80-785
• Ян Виллем Клоп . «Системы переписывания терминов», Глава 1 в книге Сэмсона Абрамски , Дова М. Габбея и Тома Майбаума (редакторы), Справочник по логике в информатике, Том 2: Предыстория: вычислительные структуры .
• Дэвид Плейстед. «Эквациональное рассуждение и системы переписывания терминов», в книге Дов М. Габбея , К. Дж. Хоггера и Джона Алана Робинсона (редакторы), Справочник по логике в области искусственного интеллекта и логического программирования, том 1 .
• Юрген Авенхаус и Клаус Мадленер. «Переписывание терминов и эквациональное рассуждение». В Ranan B. Banerji (ред.), Formal Techniques in Artificial Intelligence: A Sourcebook , Elsevier (1990).

Переписывание строк

• Рональд В. Бук и Фридрих Отто, Системы переписывания строк , Springer (1993).
• Бенджамин Беннингхофен, Сюзанна Кеммерих и Майкл М. Рихтер , Системы редукций . LNCS 277 , Springer-Verlag (1987).

Другой

• Мартин Дэвис , Рон Сигал, Элейн Дж. Вейукер , (1994) Вычислимость, сложность и языки: основы теоретической информатики – 2-е издание , Academic Press, ISBN 0-12-206382-1 . 

Поищите информацию о переписывании в Викисловаре, бесплатном словаре.

• Домашняя страница переписывания
• Рабочая группа ИФИП 1.6
• Исследователи переписывания Аарт Миддельдорп, Университет Инсбрука
• Портал прекращения
• Maude System — программная реализация системы переписывания общих терминов. ^[5]