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

Чтобы узнать о других значениях, см. Переписывание (значения) .

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

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

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

Логика

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

$\neg \neg A\to A$ ( исключение двойного отрицания )

$\neg (A\land B)\to \neg A\lor \neg B$ ( законы де Моргана )

$\neg (A\lor B)\to \neg A\land \neg B$

$(A\land B)\lor C\to (A\lor C)\land (B\lor C)$ ( дистрибутивность )

$A\lor (B\land C)\to (A\lor B)\land (A\lor C),$

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

Арифметика

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

${\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, можно продублировать, переписав термин следующим образом:

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

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

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

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

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

Лингвистика

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

Абстрактные системы переписывания

Основная статья: Абстрактная система переписывания

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

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

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

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

Основная статья: Система переписывания строк

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

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

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

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

Проблема слов для системы полуТуэ, вообще говоря, неразрешима; этот результат иногда называют теоремой Поста-Маркова .

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

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

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

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

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

Формальное определение

«Редекс» перенаправляется сюда. Чтобы узнать о лекарстве, см. Тадалафил .

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

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

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

Прекращение действия

Проблемы завершения систем перезаписи в целом рассматриваются в разделе Абстрактная система перезаписи#Завершение и конвергенция . В частности, для систем переписывания терминов необходимо учитывать следующие дополнительные тонкости.

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

Следующая система перезаписи терминов нормализуется, но не прекращается, и не сливаются: $${\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}}$$

Следующие два примера прекращения работы систем перезаписи терминов принадлежат Тояме:

$f(0,1,x)\rightarrow f(x,x,x)$

и

$g(x,y)\rightarrow x,$

$g(x,y)\rightarrow y.$

Их объединение представляет собой незавершающуюся систему, поскольку

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

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

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

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

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

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

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

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

См. также

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

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

• Баадер, Франц ; Нипков, Тобиас (1999). Переписывание сроков и все такое . Издательство Кембриджского университета. ISBN  978-0-521-77920-3 . 316 страниц.
• Марк Безем , Ян Виллем Клоп , Роэль де Вриер («Тереза»), Term Rewriting Systems («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 .

Внешние ссылки

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