Перезапись

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

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

Примеры случаев [ править ]

Логика [ править ]

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

${\ Displaystyle \ neg \ neg от А \ до А}$( исключение двойного отрицания )

${\ Displaystyle \ neg (A \ земля B) \ к \ 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))) соответственно. Следующая система переписывания терминов может затем использоваться для вычисления суммы и произведения заданных натуральных чисел. ^[6]

${\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)))),}$

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

Лингвистика [ править ]

В лингвистике , переписать правила , называемые также правила фраза структуры , используются в некоторых системах порождающей грамматики , ^[7] в качестве средства генерирования грамматически правильных предложений языка. Такое правило обычно принимает форму A → X, где A - синтаксическая метка категории , такая как именная фраза или предложение , а X - последовательность таких меток или морфем , выражающая тот факт, что A может быть заменен на X при генерации составная структура предложения. Например, правило S → NP VP означает, что предложение может состоять из именной фразы, за которой следует глагольная фраза.; дальнейшие правила будут определять, из каких подкомпонентов может состоять именная и глагольная фраза и т. д.

Системы рерайтинга абстрактных [ править ]

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

АРС это просто набор , элементы которого, как правило , называются объектами, вместе с бинарным отношением на А , традиционно обозначаемой →, и называется уменьшение соотношения , переписывают соотношение ^[10] или просто сокращения . ^[9] Эта (укоренившаяся) терминология, использующая «сокращение», немного вводит в заблуждение, потому что отношение не обязательно уменьшает некоторую меру объектов; это станет более очевидным, когда мы обсудим системы перезаписи строк далее в этой статье.

Пример 1 . Предположим, что набор объектов равен T = { a , b , c }, а бинарное отношение задано правилами a → b , b → a , a → c и b → c . Обратите внимание, что эти правила могут применяться как к a, так и к b любым способом, чтобы получить член c . Такое свойство явно важно. В некотором смысле c - это «простейший» термин в системе, поскольку к c не применимо ничего.чтобы преобразовать его дальше. Этот пример приводит нас к определению некоторых важных понятий в общем контексте ARS. Для начала нам потребуются основные понятия и обозначения. ^[11]

• ${\displaystyle {\stackrel {*}{\rightarrow }}}$является транзитивным замыканием из , где = есть тождественное соотношение , то есть имеет наименьшее предпорядок ( рефлексивный и транзитивное отношение) , содержащий . Это также называется рефлекторным транзитивное замыкание в .${\displaystyle \rightarrow \cup =}$${\displaystyle {\stackrel {*}{\rightarrow }}}$${\displaystyle \rightarrow }$${\displaystyle \rightarrow }$
• ${\displaystyle \leftrightarrow }$это , то есть объединение отношения → с его обратной связью , также известной как симметричное закрытие из .${\displaystyle \rightarrow \cup \ {\xrightarrow {-1}}}$${\displaystyle \rightarrow }$
• ${\displaystyle {\stackrel {*}{\leftrightarrow }}}$является транзитивным замыканием из , то есть наименьшее отношение эквивалентности , содержащий . Он также известен как рефлексивное транзитивное симметричное закрытие в .${\displaystyle \leftrightarrow \cup =}$${\displaystyle {\stackrel {*}{\leftrightarrow }}}$${\displaystyle \rightarrow }$${\displaystyle \rightarrow }$

Нормальные формы, возможность соединения и проблема слов [ править ]

Объект x в A называется приводимым, если существует другой y в A такой, что ; в противном случае она называется неприводимой или нормальной формой . Объект y называется нормальной формой x, если и y неприводим. Если x имеет единственную нормальную форму, то это обычно обозначается значком . В примере 1 выше c - это нормальная форма, а . Если каждый объект имеет хотя бы одну нормальную форму, ARS называется нормализующей .${\displaystyle x\rightarrow y}$${\displaystyle x{\stackrel {*}{\,\rightarrow \,}}y}$${\displaystyle x{\downarrow }}$${\displaystyle c=a{\downarrow }=b{\downarrow }}$

Родственное, но слабее , чем понятие существования нормальных форм является то , что из двух объектов будучи присоединяемым : х и у называется соединимым , если существует некоторый г со свойством . Из этого определения очевидно, что можно определить отношение соединяемости как , где - композиция отношений . Соединяемость обычно обозначается также несколько сбивчиво, но в этом обозначении стрелка вниз является бинарным отношением, то есть мы пишем, если x и y соединяются.${\displaystyle x{\stackrel {*}{\,\rightarrow \,}}z{\stackrel {*}{\,\leftarrow \,}}y}$${\displaystyle {\stackrel {*}{\,\rightarrow }}\circ {\stackrel {*}{\,\leftarrow }}}$${\displaystyle \circ }$${\displaystyle \downarrow }$${\displaystyle x\downarrow y}$

Одна из важных проблем, которые можно сформулировать в ARS, - это проблема слов : эквивалентны ли x и y при заданных x и y ? Это очень общая установка для формулировки проблемы слов для представления алгебраической структуры . Например, проблема со словом для групп - это частный случай проблемы со словом ARS. Центральным в "легком" решении проблемы слов является существование уникальных нормальных форм: в этом случае, если два объекта имеют одинаковую нормальную форму, то они эквивалентны в соответствии с . Проблема слов для ARS в целом неразрешима .${\displaystyle {\stackrel {*}{\,\leftrightarrow \,}}}$${\displaystyle {\stackrel {*}{\leftrightarrow }}}$

Собственность и слияние Черч-Россер [ править ]

Говорят, что ARS обладает свойством Черча – Россера, если это подразумевается . На словах свойство Черча – Россера означает, что любые два эквивалентных объекта соединимы. Алонзо Черч и Дж. Баркли Россер доказали в 1936 г., что лямбда-исчисление обладает этим свойством; ^[12] отсюда и название свойства. ^[13] (Это свойство лямбда-исчисления также известно как теорема Черча – Россера .) В ARS со свойством Черча – Россера проблема слов может быть сведена к поиску общего преемника. В системе Чёрча – Россера объект имеет не более одного${\displaystyle x{\stackrel {*}{\,\leftrightarrow \,}}y}$${\displaystyle x\downarrow y}$нормальная форма; то есть нормальная форма объекта уникальна, если она существует, но вполне может не существовать.

Несколько различных свойств эквивалентны свойству Черча – Россера, но может быть проще проверить в определенных условиях. В частности, слияние эквивалентно Чёрчу – Россеру. Об ARS говорится:${\displaystyle (A,\rightarrow )}$

• конфлюэнтно, если для всех w , x и y в A , следует . Грубо говоря, слияние означает, что независимо от того, насколько два пути расходятся от общего предка ( w ), пути соединяются у некоторого общего преемника. Это понятие может быть уточнено как свойство конкретного объекта w и системы, названной конфлюэнтной, если все ее элементы являются конфлюэнтными.${\displaystyle x{\stackrel {*}{\,\leftarrow \,}}w{\stackrel {*}{\,\rightarrow \,}}y}$${\displaystyle x\downarrow y}$
• локально конфлюэнтно, если для всех w , x и y в A , следует . Это свойство иногда называют слабым слиянием .${\displaystyle x\leftarrow w\rightarrow y}$${\displaystyle x\downarrow y}$

Теорема. Для ARS следующие условия эквивалентны: (i) он обладает свойством Черча – Россера, (ii) он конфлюэнтен. ^[14]

Следствие . ^[15] В сливном АРС, если тогда${\displaystyle x{\stackrel {*}{\,\leftrightarrow \,}}y}$

• Если и x, и y - нормальные формы, то x = y .
• Если y - нормальная форма, то${\displaystyle x{\stackrel {*}{\,\rightarrow \,}}y}$

Из-за этих эквивалентностей в литературе встречается немало различий в определениях. Например, в Bezem et al. 2003 г. собственность и слияние Черча-Россера определены как синонимы и идентичны приведенному здесь определению слияния; Черч – Россер, как здесь определено, остается безымянным, но дается как эквивалентное свойство; это отступление от других текстов является преднамеренным. ^[16] Из-за вышеприведенного следствия в конфлюэнтной ARS можно определить нормальную форму y для x как неприводимого y со свойством, что . Это определение, найденное в Книге и Отто, эквивалентно общепринятому определению, данному здесь в конфлюэнтной системе, но является более всеобъемлющим ^{[примечание 2]}${\displaystyle x{\stackrel {*}{\,\leftrightarrow \,}}y}$ больше в неконфлюэнтной ARS.

С другой стороны, местное слияние не эквивалентно другим понятиям слияния, приведенным в этом разделе, но оно строго слабее, чем слияние. Отношение является локально конфлюэнтным, но не конфлюэнтным, поскольку и эквивалентны, но не соединяются. ^[17]${\displaystyle a\rightarrow b,\;b\rightarrow a,\;a\rightarrow c,\;b\rightarrow d}$${\displaystyle c}$${\displaystyle d}$

Прекращение и сближение [ править ]

Абстрактная система перезаписи называется завершающей или нётеровой, если нет бесконечной цепочки . В завершающей ARS каждый объект имеет по крайней мере одну нормальную форму, поэтому он нормализуется. Обратное неверно. В примере 1, например, существует бесконечная цепочка перезаписи, а именно , даже если система нормализует. Сливающийся и завершающийся ARS называется конвергентным . В конвергентной ARS каждый объект имеет уникальную нормальную форму. ${\displaystyle x_{0}\rightarrow x_{1}\rightarrow x_{2}\rightarrow \cdots }$${\displaystyle a\rightarrow b\rightarrow a\rightarrow b\rightarrow \cdots }$

Теорема ( лемма Ньюмана ): завершающаяся ARS конфлюэнтна тогда и только тогда, когда она локально конфлюэнтна.

Системы перезаписи строк [ править ]

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

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

Понятие полусистемы Туэ по существу совпадает с представлением моноида . Поскольку является конгруэнцией, мы можем определить фактор-моноид свободного моноида с помощью сравнения Туэ обычным образом . Если моноидом является изоморфными с , то система полу-Thue называется моноидное представление о .${\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}}}$

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

Проблема слов для полутоновой системы в целом неразрешима; этот результат иногда называют теоремой Постмаркова . ^[18]

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

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

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

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

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

Формальное определение [ править ]

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

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

Например, это правило перезаписи, обычно используемое для установления нормальной формы относительно ассоциативности . Это правило может быть применено к числителю в члене с соответствующей заменой , см. Рисунок 2. ^{[примечание 5]} Применение этой замены к правой части правила дает член ( a * ( a + 1)) * ( a + 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 {\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}}}$

Прекращение действия [ править ]

Помимо раздела « Завершение и конвергенция» , следует учитывать дополнительные тонкости для систем переопределения терминов.

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

Следующая система перезаписи терминов является нормализующей, ^{[примечание 6],} но не завершающейся, ^{[примечание 7]} и не сливающейся: ^[22]

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

${\displaystyle f(x,g(x))\rightarrow b,}$

${\displaystyle h(c,x)\rightarrow f(h(x,c),h(x,x)).}$

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

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

а также

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

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

Их союз - это безостановочная система, поскольку . Этот результат опровергает гипотезу о Дершовице , ^[24] , который утверждал , что объединение двух нагрузочных долгосрочные систем перезаписи и снова завершением , если все левые стороны и правые сторон являются линейными , и нет « перекрывается » между левая и правая части . Все эти свойства подтверждаются примерами Тоямы.${\displaystyle 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 \ldots }$${\displaystyle R_{1}}$${\displaystyle R_{2}}$${\displaystyle R_{1}}$${\displaystyle R_{2}}$${\displaystyle R_{1}}$${\displaystyle R_{2}}$

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

Системы перезаписи графов [ править ]

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

Системы перезаписи трассировки [ править ]

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

Философия [ править ]

Системы перезаписи можно рассматривать как программы, которые выводят конечные эффекты из списка причинно-следственных связей. Таким образом, переписывающие системы можно рассматривать как автоматические средства доказательства причинно-следственной связи. ^{[ необходима цитата ]}

См. Также [ править ]

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

Заметки [ править ]

Ссылки [ править ]

Дальнейшее чтение [ править ]

• Баадер, Франц ; Нипков, Тобиас (1999). Переписывание сроков и все такое . Издательство Кембриджского университета. ISBN 978-0-521-77920-3.316 страниц. Учебник для студентов бакалавриата.
• Марк Безем , Ян Виллем Клоп , Роэль де Фрайер (« Терезе »), Системы перезаписи терминов («TeReSe»), Cambridge University Press, 2003, ISBN 0-521-39115-6 . Это самая последняя всеобъемлющая монография. Однако он использует изрядное количество нестандартных обозначений и определений. Например, собственность Черча – Россера определяется как тождественная слиянию. 
• Нахум Дершовиц и Жан-Пьер Жуано «Системы перезаписи » , глава 6 в Яне ван Левен (ред.), Справочник по теоретической информатике , том B: Формальные модели и семантика. , Elsevier и MIT Press, 1990, ISBN 0-444-88074-7 , стр. 243–320. Препринт этой главы находится в свободном доступе от авторов, но не хватает цифру. 
• Нахум Дершовиц и Дэвид Плейстед . «Переписывание» , глава 9 в книге Джона Алана Робинсона и Андрея Воронкова (ред.), Справочник по автоматизированному мышлению , том 1 .
• Жерар Хуэ и Дерек Оппен, Уравнения и правила перезаписи, Обзор (1980) Стэнфордская группа проверки, отчет № 15 Отчет отдела компьютерных наук № STAN-CS-80-785
• Ян Виллем Клоп . «Системы перезаписи терминов», глава 1 в Самсоне Абрамски , Дов М. Габбай и Том Майбаум (ред.), Справочник по логике в компьютерных науках , Том 2: Предпосылки: Вычислительные структуры .
• Дэвид Плейстед. «Системы рассуждений по уравнениям и переписывания терминов» , в книге Дов М. Габбей , С.Дж. Хоггер и Джон Алан Робинсон (ред.), Справочник по логике в искусственном интеллекте и логическом программировании , Том 1 .
• Юрген Авенхаус и Клаус Мадленер. «Переписывание терминов и эквациональное рассуждение». В: Ранан Б. Банерджи (ред.), Формальные методы в искусственном интеллекте: Справочник , Elsevier (1990).

Перезапись строк

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

Другой

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

Внешние ссылки [ править ]

Поищите рерайтинг в Викисловаре, бесплатном словаре.

• Rewriting Главная страница
• Рабочая группа 1.6 IFIP
• Исследователи переписывания по Аарту Middeldorp , Университет Инсбрука
• Портал прекращения действия