Перезапись

В математике , информатике и логике , переписывание охватывает широкий спектр (потенциально недетерминированной ) методы замены подтермов из формулы с другими терминами. Объекты фокуса для этой статьи включают системы подстановок (также известные как систему перезаписи , перезаписи двигатели ^[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 (А \ земля В) \ лор С \ к (А \ лор С) \ земля (В \ лор С)}$( распределенность )

${\ Displaystyle А \ лор (В \ земля С) \ к (А \ лор В) \ земля (А \ лор С),}$^{[примечание 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 , Университет Инсбрука
• Портал прекращения действия