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

Замена подтерма в формуле другим термином

В математике , информатике и логике переписывание охватывает широкий спектр методов замены подтермов формулы другими терминами . Такие методы могут быть реализованы с помощью систем переписывания (также известных как системы переписывания , механизмы переписывания , ^{[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\lor 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{aligned}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{aligned}}}$

Например, вычисление 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]

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

Рис.1: Схематическая треугольная диаграмма применения правила перезаписи в позиции в термине с соответствующей заменой ${\displaystyle l\longrightarrow r}$ ${\displaystyle p}$ ${\displaystyle \sigma }$

Рис.2: Правило левого термина, совпадающего с термином ${\displaystyle x*(y*z)}$ ${\displaystyle {\frac {a*((a+1)*(a+2))}{1*(2*3)}}}$

Система переписывания терминов ( 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-системы определяют перезапись, которая выполняется параллельно.
• Ссылочная прозрачность в информатике
• Регулируемое переписывание
• Сети взаимодействия

Примечания

1. Этот вариант предыдущего правила необходим, поскольку коммутативный закон A ∨ B = B ∨ A не может быть преобразован в правило перезаписи. Правило типа A ∨ B → B ∨ A сделало бы систему перезаписи незавершающейся.
2. поскольку применение этой замены к левой части правила дает числитель ${\displaystyle x*(y*z)}$ ${\displaystyle a*((a+1)*(a+2))}$
3. т.е. для каждого члена существует некоторая нормальная форма, например, h ( c , c ) имеет нормальные формы b и g ( b ), так как h ( c , c ) → f ( h ( c , c ), h ( c , c )) → f ( h ( c , c ), f ( h ( c , c ), h ( c , c ))) → f ( h ( c , c ), g ( h ( c , c ))) → b , и h ( c , c ) → f ( h ( c , c ), h ( c , c )) → g ( h ( c , c )) → ... → g ( b ); ни b, ни g ( b ) не могут быть переписаны дальше, поэтому система не является конфлюэнтной
4. т.е. существует бесконечное множество выводов, например h ( c , c ) → f ( h ( c , c ), h ( c , c )) → f ( f ( h ( c , c ), h ( c , c ) ) , h ( c , c ) ) → f ( f ( f ( h ( c , c ) , h ( c , c ) ) , h ( c , c ) ) → ...

Дальнейшее чтение

• Баадер, Франц ; Нипков, Тобиас (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]

Ссылки

1. Жозеф Гоген «Доказательство и переписывание» Международная конференция по алгебраическому и логическому программированию, 1990 Нанси, Франция, стр. 1-24
2. Sculthorpe, Neil; Frisby, Nicolas; Gill, Andy (2014). "The Kansas University rewrite engine" (PDF) . Journal of Functional Programming . 24 (4): 434–473. doi :10.1017/S0956796814000185. ISSN  0956-7968. S2CID  16807490. Архивировано (PDF) из оригинала 22.09.2017 . Получено 12.02.2019 .
3. Hsiang, Jieh; Kirchner, Hélène; Lescanne, Pierre; Rusinowitch, Michaël (1992). «Подход к автоматическому доказательству теорем с помощью переписывания терминов». The Journal of Logic Programming . 14 (1–2): 71–99. doi : 10.1016/0743-1066(92)90047-7 .
4. Frühwirth, Thom (1998). «Теория и практика правил обработки ограничений». Журнал логического программирования . 37 (1–3): 95–138. doi : 10.1016/S0743-1066(98)10005-5 .
5. Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Quesada, JF (2002). "Maude: Спецификация и программирование в переписывании логики". Теоретическая информатика . 285 (2): 187–243. doi : 10.1016/S0304-3975(01)00359-0 .
6. Ким Марриотт; Питер Дж. Стаки (1998). Программирование с ограничениями: Введение. MIT Press. С. 436–. ISBN 978-0-262-13341-8.
7. Юрген Авенхаус; Клаус Мадленер (1990). «Переписывание терминов и эквациональное рассуждение». В RB Banerji (ред.). Формальные методы в искусственном интеллекте . Справочник. Elsevier. С. 1–43.Здесь: Пример в разделе 4.1, стр.24.
8. Роберт Фрейдин (1992). Основы генеративного синтаксиса. МТИ Пресс. ISBN 978-0-262-06144-5.
9. Book и Отто, стр. 10
10. Безем и др., стр. 7,
11. Безем и др., стр. 7
12. Мартин Дэвис и др. 1994, с. 178
13. Дершовиц, Жуанно (1990), раздел 1, стр.245
14. Альберт, Грэф (2009). «Обработка сигналов на чистом языке программирования». Аудиоконференция Linux .
15. Рипе, фон Михаэль (18 ноября 2009 г.). «Чистый – eine einfache funktionale Sprache». Архивировано из оригинала 19 марта 2011 года.
16. Klop, JW "Term Rewriting Systems" (PDF) . Статьи Нахума Дершовица и студентов . Тель-Авивский университет. стр. 12. Архивировано (PDF) из оригинала 15 августа 2021 г. . Получено 14 августа 2021 г. .
17. N. Dershowitz, J.-P. Jouannaud (1990). Jan van Leeuwen (ред.). Rewrite Systems . Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 243–320.; здесь: Раздел 2.3
18. Макс Доше (1989). «Моделирование машин Тьюринга с помощью леволинейного правила перезаписи». Труды 3-й Международной конференции по методам перезаписи и их применению . LNCS. Том 355. Springer. С. 109–120.
19. Макс Доше (сентябрь 1992 г.). «Моделирование машин Тьюринга с помощью регулярного правила перезаписи». Теоретическая информатика . 103 (2): 409–420. doi : 10.1016/0304-3975(92)90022-8 .
20. Gerard Huet, DS Lankford (март 1978 г.). On the Uniform Halting Problem for Term Rewriting Systems (PDF) (Технический отчет). IRIA. стр. 8. 283. Получено 16 июня 2013 г.
21. Бернхард Грамлих (июнь 1993 г.). «Связь внутренних, слабых, однородных и модульных терминаций систем переписывания терминов». В Воронков, Андрей (ред.). Proc. Международная конференция по логическому программированию и автоматизированному рассуждению (LPAR) . LNAI. Том 624. Springer. стр. 285–296. Архивировано из оригинала 2016-03-04 . Получено 2014-06-19 .Здесь: Пример 3.3
22. Ёсихито Тояма (1987). «Контрпримеры к завершению для прямой суммы систем переписывания терминов» (PDF) . Inf. Process. Lett . 25 (3): 141–143. doi :10.1016/0020-0190(87)90122-0. hdl : 2433/99946 . Архивировано (PDF) из оригинала 2019-11-13 . Получено 2019-11-13 .
23. N. Dershowitz (1985). "Termination" (PDF) . В Jean-Pierre Jouannaud (ed.). Proc. RTA . LNCS. Vol. 220. Springer. pp. 180–224. Архивировано (PDF) из оригинала 2013-11-12 . Получено 2013-06-16 .; здесь: стр.210
24. Вольфрам, DA (1993). Теория Клауса типов . Cambridge University Press. стр. 47–50. doi :10.1017/CBO9780511569906. ISBN 9780521395380. S2CID  42331173.
25. Нипков, Тобиас; Прехофер, Кристиан (1998). «Переписывание высшего порядка и эквациональное рассуждение». В Bibel, W.; Schmitt, P. (ред.). Автоматизированная дедукция — основа для приложений. Том I: Основы . Kluwer. стр. 399–430. Архивировано из оригинала 2021-08-16 . Получено 2021-08-16 .