Перезапись

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

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

Примеры случаев

Логика

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

${\ 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))) соответственно. Следующая система переписывания терминов может затем использоваться для вычисления суммы и произведения заданных натуральных чисел. ^[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 - последовательность таких меток или морфем , выражающая тот факт, что A может быть заменен на X при генерации составная структура предложения. Например, правило S → NP VP означает, что предложение может состоять из именной фразы, за которой следует глагольная фраза.; дальнейшие правила будут определять, из каких подкомпонентов может состоять именная и глагольная фраза и т. д.

Системы рерайтинга абстрактных текстов

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

Многие понятия и обозначения могут быть определены в общих настройках ARS. является рефлексивным транзитивным замыканием в . это симметричное замыкание на . является рефлексивным транзитивен симметричным замыканием на . Слово проблема для АПС заключается в определении, данные х и у , то ли . Объект x в A называется приводимым, если существует другой y в A такой, что ; в противном случае она называется неприводимой или нормальной формой${\displaystyle {\stackrel {*}{\rightarrow }}}$${\displaystyle \rightarrow }$${\displaystyle \leftrightarrow }$${\displaystyle \rightarrow }$${\displaystyle {\stackrel {*}{\,\leftrightarrow \,}}}$${\displaystyle \rightarrow }$${\displaystyle x{\stackrel {*}{\,\leftrightarrow \,}}y}$${\displaystyle x\rightarrow y}$. Объект y называется «нормальной формой x », если и y неприводим. Если нормальная форма x уникальна, то это обычно обозначается значком . Если каждый объект имеет хотя бы одну нормальную форму, ARS называется нормализующей . или x и y называются соединяемыми, если существует некоторый z со свойством that . Говорят, что ARS обладает свойством Черча – Россера, если это подразумевается . ARS является конфлюэнтным, если для всех w , x и y${\displaystyle x{\stackrel {*}{\,\rightarrow \,}}y}$${\displaystyle x{\downarrow }}$${\displaystyle x\downarrow y}$${\displaystyle x{\stackrel {*}{\,\rightarrow \,}}z{\stackrel {*}{\,\leftarrow \,}}y}$${\displaystyle x{\stackrel {*}{\,\leftrightarrow \,}}y}$${\displaystyle x\downarrow y}$в A , влечет . АРС является локально конфлюэнтны , если и только если для всех ш , х и у в А , предполагает . ARS называется завершающим или нётеровым, если нет бесконечной цепи . Сливающийся и завершающийся ARS называется конвергентным или каноническим .${\displaystyle x{\stackrel {*}{\,\leftarrow \,}}w{\stackrel {*}{\,\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 является сливающийся тогда и только тогда , когда оно локально сливающиеся, и что слово проблема для АПС является неразрешимой В основном.

Системы перезаписи строк

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

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

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

Рис.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 , то есть, если есть замена такой , что подтермы с корнем в некоторой позиции р является результатом применения подстановки к термину л${\displaystyle l\rightarrow r}$${\displaystyle l\rightarrow r}$ ${\displaystyle \sigma }$${\displaystyle s}$ ${\displaystyle \sigma }$. Подтермин, соответствующий левой части правила, называется редексом или сокращаемым выражением . ^[13] Результирующий член t этого применения правила является результатом замены подтерма в позиции p в s термином с примененной заменой , см. Рисунок 1. В этом случае говорят, что он был переписан за один шаг , или переписано непосредственно к системе , формально обозначаются как , или , как некоторые авторы.${\displaystyle r}$${\displaystyle \sigma }$${\displaystyle s}$${\displaystyle t}$${\displaystyle R}$${\displaystyle s\rightarrow _{R}t}$${\displaystyle s\,{\xrightarrow[{R}]{}}\,t}$${\displaystyle s\,{\xrightarrow {R}}\,t}$

Если термин можно переписать в несколько этапов в срок , то есть, если этот термин называется переписано в формально обозначается как . Другими словами, отношение - это транзитивное закрытие отношения ; часто также обозначение используется для обозначения рефлексивного-транзитивного замыкания на , то есть, если s = т или . ^[14] Перезапись терминов, заданная набором правил, может рассматриваться как абстрактная система перезаписи, как определено выше , с терминами как ее объектами и как ее отношение перезаписи.${\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. ^{[примечание 2]} Применение этой замены к правой части правила дает член ( 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}}}$

Прекращение

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

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

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

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

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

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

а также

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

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

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

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

Системы перезаписи высшего порядка

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

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

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

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

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

Философия

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

Смотрите также

• Критическая пара (логика)
• Компилятор
• Алгоритм завершения Кнута – Бендикса
• 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 , Университет Инсбрука
• Портал прекращения действия