В математике , информатике и логике , переписывание охватывает широкий спектр (потенциально недетерминированной ) методы замены подтермов из формулы с другими терминами. Объекты фокуса для этой статьи включают системы подстановок (также известные как систему перезаписи , перезаписи двигатели [1] или систему снижения ). В своей самой основной форме они состоят из набора объектов плюс отношения о том, как преобразовать эти объекты.
Перезапись может быть недетерминированной . Одно правило переписывания термина может применяться к этому термину разными способами, или может применяться более одного правила. Таким образом, системы перезаписи не предоставляют алгоритм для замены одного термина на другой, а предоставляют набор возможных применений правил. Однако в сочетании с соответствующим алгоритмом системы перезаписи можно рассматривать как компьютерные программы , а некоторые средства доказательства теорем [2] и декларативные языки программирования основаны на перезаписи терминов. [3] [4]
Примеры случаев
Логика
В логике процедура получения конъюнктивной нормальной формы (КНФ) формулы может быть реализована как система перезаписи. [5] Правила примера такой системы:
где символ () указывает, что выражение, соответствующее левой части правила, может быть переписано в выражение, образованное правой частью, и каждый символ обозначает подвыражение. В такой системе каждое правило выбирается так, чтобы левая часть была эквивалентна правой части, и, следовательно, когда левая часть соответствует подвыражению, выполнение перезаписи этого подвыражения слева направо поддерживает логическую согласованность и значение всего выражения. .
Арифметика
Системы перезаписи терминов могут использоваться для вычисления арифметических операций с натуральными числами . Для этого каждое такое число необходимо закодировать как термин . Простой метод кодирование является той , которая используется в аксиомах Пеаны , на основании константы 0 (ноль) и функция преемника S . например, числа 0, 1, 2 и 3 представлены терминами 0, S (0), S (S (0)) и S (S (S (0))) соответственно. Следующая система переписывания терминов может затем использоваться для вычисления суммы и произведения заданных натуральных чисел. [6]
Например, вычисление 2 + 2 для получения 4 можно продублировать, переписав термы следующим образом:
где номера правил указаны над стрелкой перезаписи .
В качестве другого примера вычисление 2⋅2 выглядит так:
где последний шаг включает вычисление из предыдущего примера.
Лингвистика
В лингвистике , переписать правила , называемые также правила фраза структуры , используются в некоторых системах порождающей грамматики , [7] в качестве средства генерирования грамматически правильных предложений языка. Такое правило обычно принимает форму A → X, где A - синтаксическая метка категории , такая как именная фраза или предложение , а X - последовательность таких меток или морфем , выражающая тот факт, что A может быть заменен на X при генерации составная структура предложения. Например, правило S → NP VP означает, что предложение может состоять из именной фразы, за которой следует глагольная фраза ; дальнейшие правила будут определять, из каких подкомпонентов может состоять именная и глагольная фраза и т. д.
Системы рерайтинга абстрактных текстов
Из приведенных выше примеров ясно, что мы можем думать о переписывании систем абстрактным образом. Нам нужно указать набор объектов и правила, которые можно применить для их преобразования. Наиболее общая (одномерная) установка этого понятия называется системой абстрактной редукции (сокращенно ARS ), хотя в последнее время авторы также используют абстрактную систему переписывания . [8] (Предпочтение здесь слова «сокращение» вместо «переписывание» представляет собой отход от единообразного использования слова «переписывание» в названиях систем, которые являются конкретизацией ARS. Поскольку слово «сокращение» не встречается в названия более специализированных систем, в старых текстах сокращение system является синонимом ARS). [9]
АРС это просто набор , элементы которого, как правило , называются объектами, вместе с бинарным отношением на А , традиционно обозначаемой →, и называется уменьшение соотношения , переписывают соотношение [10] или просто сокращения . [9] Эта (укоренившаяся) терминология, использующая «сокращение», немного вводит в заблуждение, потому что отношение не обязательно уменьшает некоторую меру объектов; это станет более очевидным, когда мы обсудим системы перезаписи строк далее в этой статье.
Пример 1 . Предположим, что набор объектов равен T = { a , b , c }, а бинарное отношение задано правилами a → b , b → a , a → c и b → c . Обратите внимание, что эти правила могут применяться как к a, так и к b любым способом, чтобы получить член c . Такое свойство явно важно. В некотором смысле c - это «простейший» термин в системе, поскольку к c нельзя применить никакие дальнейшие преобразования. Этот пример приводит нас к определению некоторых важных понятий в общем контексте ARS. Для начала нам потребуются основные понятия и обозначения. [11]
- является транзитивным замыканием из, где = - тождественное отношение , т. е.- наименьший предпорядок ( рефлексивное и транзитивное отношение), содержащий. Он также называется рефлексивным транзитивным замыканием из.
- является , То есть объединение отношения → с его обратной связью , также известное как симметричное закрытие из.
- является транзитивным замыканием из, это наименьшее отношение эквивалентности, содержащее. Он также известен как рефлексивное переходное симметричное замыкание на.
Нормальные формы, возможность соединения и проблема слова
Объект x в A называется приводимым, если существует другой y в A такой, что; в противном случае она называется неприводимой или нормальной формой . Объект y называется нормальной формой x, если, а y неприводимо. Если x имеет единственную нормальную форму, то это обычно обозначается как. В примере 1 выше c - это нормальная форма, а. Если каждый объект имеет хотя бы одну нормальную форму, ARS называется нормализующей .
Родственное, но слабее , чем понятие существования нормальных форм является то , что из двух объектов будучи присоединяемым : х и у называется соединимым , если существует некоторый г со свойством. Из этого определения очевидно, что можно определить отношение соединяемости как, где это композиция отношений . Присоединяемость обычно обозначается, несколько сбивчиво, также с помощью, но в этих обозначениях стрелка вниз является бинарным отношением, т. е. мы пишем если x и y соединимы.
Одной из важных проблем, которые можно сформулировать в ARS, является проблема слов : если x и y , эквивалентны ли они при? Это очень общая установка для формулировки проблемы слов для представления алгебраической структуры . Например, проблема со словом для групп - это частный случай проблемы со словом ARS. Центральным элементом "простого" решения проблемы слов является существование уникальных нормальных форм: в этом случае, если два объекта имеют одинаковую нормальную форму, то они эквивалентны при. Проблема слов для ARS в целом неразрешима .
Собственность и слияние церкви и Россера
Говорят, что ARS обладает собственностью Черча – Россера, если подразумевает . На словах свойство Черча – Россера означает, что любые два эквивалентных объекта соединимы. Алонзо Черч и Дж. Баркли Россер доказали в 1936 г., что лямбда-исчисление обладает этим свойством; [12] отсюда и название свойства. [13] (Это свойство лямбда-исчисления также известно как теорема Черча – Россера .) В ARS со свойством Черча – Россера проблема слов может быть сведена к поиску общего преемника. В системе Чёрча – Россера объект имеет не более одной нормальной формы; то есть нормальная форма объекта уникальна, если она существует, но вполне может не существовать.
Несколько различных свойств эквивалентны свойству Черча – Россера, но может быть проще проверить в определенных условиях. В частности, слияние эквивалентно Чёрчу – Россеру. ARS говорят:
- сливной, если для всех w , x и y в A , подразумевает . Грубо говоря, слияние означает, что независимо от того, насколько два пути расходятся от общего предка ( w ), пути соединяются у некоторого общего преемника. Это понятие может быть уточнено как свойство конкретного объекта w и системы, названной конфлюэнтной, если все ее элементы являются конфлюэнтными.
- локально конфлюэнтно, если для всех w , x и y в A , подразумевает . Это свойство иногда называют слабым слиянием .
Теорема. Для ARS следующие условия эквивалентны: (i) он обладает свойством Черча – Россера, (ii) он конфлюэнтен. [14]
Следствие . [15] В сливном ОРС, если тогда
- Если и x, и y - нормальные формы, то x = y .
- Если y - нормальная форма, то
Из-за этих эквивалентностей в литературе встречается немало различий в определениях. Например, в Bezem et al. 2003 г. собственность и слияние Черча-Россера определены как синонимы и идентичны приведенному здесь определению слияния; Черч – Россер, как здесь определено, остается безымянным, но дается как эквивалентное свойство; это отступление от других текстов является преднамеренным. [16] Из-за приведенного выше следствия в конфлюэнтной ARS можно определить нормальную форму y для x как неприводимого y со свойством, что. Это определение, найденное в Книге и Отто, эквивалентно общему определению, данному здесь для конфлюэнтной системы, но оно более инклюзивное [примечание 2] больше в неконфлюэнтной ARS.
С другой стороны, местное слияние не эквивалентно другим понятиям слияния, приведенным в этом разделе, но оно строго слабее, чем слияние. Соотношение локально сливается, но не сливается, так как а также эквивалентны, но не могут быть соединены. [17]
Прекращение и сближение
Абстрактная система перезаписи называется завершающей или нётеровой, если не существует бесконечной цепочки.. В завершающей ARS каждый объект имеет по крайней мере одну нормальную форму, поэтому он нормализуется. Обратное неверно. Например, в примере 1 существует бесконечная цепочка перезаписи, а именно, хотя система нормализуется. Сливающийся и завершающийся ARS называется конвергентным . В конвергентной ARS каждый объект имеет уникальную нормальную форму.
Теорема ( лемма Ньюмана ): завершающаяся ARS конфлюэнтна тогда и только тогда, когда она локально конфлюэнтна.
Системы перезаписи строк
Система перезаписи строк (SRS), также известная как система полутуэ , использует свободную моноидную структуру строк (слов) по алфавиту для расширения отношения перезаписи,, ко всем строкам в алфавите, которые содержат левую и, соответственно, правую части некоторых правил в качестве подстрок . Формально система полутуэ - это кортеж где является (обычно конечным) алфавитом, и представляет собой бинарную связь между некоторыми (фиксированными) строками в алфавите, называемую правилами перезаписи . Один шаг переписывание отношение отношение индуцированный на определяется как: для любых строк тогда и только тогда, когда существуют такой, что , , а также . С это отношение на , пара соответствует определению абстрактной системы перезаписи. Очевидно это подмножество . Если отношениеявляется симметричным , то система называется системой Туэ- .
В SRS редукционное отношение совместим с операцией моноида, что означает, что подразумевает для всех струн . Аналогично рефлексивное транзитивное симметричное замыкание, обозначенный , является конгруэнцией , что означает, что это отношение эквивалентности (по определению), и оно также совместимо с конкатенацией строк. Соотношениеназывается сравнением Туэ, порожденным. В системе Туэ, т. Е. Если симметрично, соотношение перезаписи совпадает с конгруэнцией Туэ .
Понятие полусистемы Туэ по существу совпадает с представлением моноида . Сявляется конгруэнцией, мы можем определить фактор-моноид свободного моноида путем сравнения Туэ обычным способом . Если моноидявляется изоморфными с, то система полутуэ называется моноид представление о.
Мы сразу получаем очень полезные связи с другими областями алгебры. Например, алфавит { a , b } с правилами { ab → ε, ba → ε}, где ε - пустая строка , представляет собой представление свободной группы на одном образующем. Если вместо этого правила просто { ab → ε}, то мы получаем представление бициклического моноида . Таким образом, системы полу-Туэ составляют естественную основу для решения проблемы слов для моноидов и групп. Фактически, каждый моноид имеет представление в виде, т. е. он всегда может быть представлен полу-системой Туэ, возможно, по бесконечному алфавиту.
Проблема слов для полутоновой системы в целом неразрешима; этот результат иногда называют теоремой Постмаркова . [18]
Системы перезаписи терминов
Система перезаписи терминов ( TRS ) - это система перезаписи, объектами которой являются термины , которые представляют собой выражения с вложенными подвыражениями. Например, система, показанная в разделе «Логика» выше, является системой переписывания терминов. Термины в этой системе состоят из бинарных операторов а также и унарный оператор . Также в правилах присутствуют переменные, которые представляют любой возможный термин (хотя одна переменная всегда представляет один и тот же термин в рамках одного правила).
В отличие от систем перезаписи строк, объектами которых являются последовательности символов, объекты системы перезаписи терминов образуют алгебру терминов . Термин можно представить в виде дерева символов, набор допустимых символов фиксируется данной сигнатурой .
Формальное определение
Термин правило перезаписи представляет собой пару терминов , обычно записывается в виде, чтобы указать, что левую часть l можно заменить правой частью r . Система перезаписи терминов - это набор R таких правил. Правиломогут быть применены к сроку с , если левый термин л соответствует некоторый подтерм из S , то есть, еслидля некоторой позиции p в s и некоторой подстановки . [примечание 3] Результирующий член t этого применения правила затем получается как; [примечание 4] см. рисунок 1. В этом случаесчитается, что он переписывается за один шаг или переписывается напрямую , чтобы по системе , формально обозначаемый как , , или как некоторыми авторами.
Если срок можно за несколько шагов переписать в термин , то есть если , термин как говорят, переписан на, формально обозначаемый как . Другими словами, отношениеявляется транзитивным замыканием отношения; часто также обозначениеиспользуется для обозначения окончания рефлексивно-транзитивное из, это, если s = t или. [19] Перезапись терминов, заданная наборомправил можно рассматривать как абстрактную систему переписывания, как определено выше , с терминами как ее объектами и как его отношение переписывания.
Например, это правило перезаписи, обычно используемое для установления нормальной формы относительно ассоциативности . Это правило можно применить к числителю в члене с соответствующей заменой , см. рисунок 2. [примечание 5] Применение этой подстановки к правой части правила дает член ( a * ( a + 1)) * ( a +2) , а замена числителя этим термином дает, который является результатом применения правила перезаписи. В целом, применение правила перезаписи привело к так называемому «применению закона ассоциативности для к "в элементарной алгебре. В качестве альтернативы правило можно было бы применить к знаменателю исходного члена, получив .
Прекращение
Помимо раздела « Завершение и конвергенция» , следует учитывать дополнительные тонкости для систем переопределения терминов.
Прекращение даже системы, состоящей из одного правила с линейной левой частью, неразрешимо. [20] Завершение также неразрешимо для систем, использующих только унарные функциональные символы; однако он разрешим для конечных наземных систем. [21]
Следующая система перезаписи терминов является нормализующей, [примечание 6], но не завершающейся, [примечание 7] и не сливающейся: [22]
Следующие два примера систем перезаписи терминирующих терминов принадлежат Тояме: [23]
а также
Их объединение - это безостановочная система, поскольку . Этот результат опровергает гипотезу Дершовица , [24] , который утверждал , что объединение двух систем прекращения термина перезаписи а также снова завершается, если все левые части и правые части являются линейными , и нет « перекрывается » между левой стороной и правые части . Все эти свойства подтверждаются примерами Тоямы.
См. Раздел « Порядок перезаписи» и « Порядок пути (перезапись терминов)» для получения информации об отношениях упорядочения, используемых в доказательствах завершения для систем перезаписи терминов.
Системы перезаписи графов
Обобщением систем перезаписи терминов являются системы перезаписи графов , работающие на графах вместо ( основных ) терминов / их соответствующего древовидного представления.
Системы перезаписи трассировки
Теория трассировки предоставляет средства для обсуждения многопроцессорной в более формальной точки зрения, например, с помощью трассировки моноиде и истории моноиде . Перезапись также может выполняться в системах трассировки.
Философия
Системы перезаписи можно рассматривать как программы, которые выводят конечные эффекты из списка причинно-следственных связей. Таким образом, переписывающие системы можно рассматривать как автоматические средства доказательства причинно-следственной связи. [ необходима цитата ]
Смотрите также
- Критическая пара (логика)
- Алгоритм завершения Кнута – Бендикса
- L-системы определяют перезапись, которая выполняется параллельно.
- Ссылочная прозрачность в информатике
- Регулируемая перезапись
- Rho исчисление
Заметки
- ^ Этот вариант предыдущего правила необходим, поскольку коммутативный закон A ∨ B = B ∨ A нельзя превратить в правило перезаписи. Такое правило, как A ∨ B → B ∨ A, приведет к тому, что система перезаписи не будет завершаться.
- ^ т.е. он рассматривает больше объектов как нормальную форму x, чем наше определение
- ^ здесь, обозначает подтермин с корнем в позиции p , аобозначает результат применения подстановки к сроку 1
- ^ здесь,обозначает результат замены подтерма в позиции p в s термином
- ^ так как применяя эту замену к левой части правила дает числитель
- ^ т.е. для каждого члена существует некоторая нормальная форма, например, h ( c , c ) имеет нормальные формы b и g ( b ), так как h ( c , c ) → f ( h ( c , c ), h ( c , c )) → f ( h ( c , c ), f ( h ( c , c ), h ( c , c ))) → f ( h ( c , c ), g ( h ( c , c ))) → b , и h ( c , c ) → f ( h ( c , c ), h ( c , c )) → g ( h ( c , c ), h ( c , c )) → ... → g ( б ); ни b, ни g ( b ) нельзя переписать дальше, поэтому система не является конфлюэнтной
- ^ т.е. существует бесконечное количество производных, например h ( c , c ) → f ( h ( c , c ), h ( c , c )) → f ( f ( h ( c , c ), h ( c , c ) ), h ( c , c )) → f ( f ( f ( h ( c , c ), h ( c , c )), h ( c , c )), h ( c , c )) → ...
Рекомендации
- ^ Скалторп, Нил; Фрисби, Николас; Гилл, Энди (2014). «Механизм перезаписи Университета Канзаса» (PDF) . Журнал функционального программирования . 24 (4): 434–473. DOI : 10.1017 / S0956796814000185 . ISSN 0956-7968 .
- ^ Сян, Цзе; Киршнер, Элен; Лесканн, Пьер; Русинович, Михаэль (1992). «Подход переписывания терминов к автоматическому доказательству теорем». Журнал логического программирования . 14 (1-2): 71–99. DOI : 10.1016 / 0743-1066 (92) 90047-7 .
- ^ Фрювирт, Том (1998). «Теория и практика правил обработки ограничений». Журнал логического программирования . 37 (1–3): 95–138. DOI : 10.1016 / S0743-1066 (98) 10005-5 .
- ^ Clavel, M .; Durán, F .; Eker, S .; Lincoln, P .; Martí-Oliet, N .; Meseguer, J .; Кесада, JF (2002). «Мод: Спецификация и программирование в переписывающей логике». Теоретическая информатика . 285 (2): 187–243. DOI : 10.1016 / S0304-3975 (01) 00359-0 .
- ^ Ким Марриотт; Питер Дж. Стаки (1998). Программирование с ограничениями: введение . MIT Press. С. 436–. ISBN 978-0-262-13341-8.
- ^ Юрген Авенхаус; Клаус Мадленер (1990). «Переписывание терминов и логическое обоснование». В RB Banerji (ред.). Формальные методы в искусственном интеллекте . Справочник. Эльзевир. С. 1–43. Здесь: Пример в разделе 4.1, стр.24.
- ^ Роберт Фрейдин (1992). Основы генеративного синтаксиса . MIT Press. ISBN 978-0-262-06144-5.
- ^ Bezem et al., Стр. 7,
- ^ a b Книга и Отто, стр. 10
- ^ Bezem et al., Стр. 7
- ^ Баадер и Нипкова, стр. 8-9
- ^ Алонзо Черч и Дж. Баркли Россер. «Некоторые свойства преобразования». Пер. АМС , 39: 472–482, 1936.
- ^ Баадер и Нипков, стр. 9
- ^ Баадер и Нипков, стр. 11
- ^ Баадер и Нипков, стр. 12
- ^ Bezemдр., С.11
- ^ MHA Neumann (1942). «О теориях с комбинаторным определением эквивалентности ». Анналы математики . 42 (2): 223–243. DOI : 10.2307 / 1968867 . JSTOR 1968867 .
- ^ Мартин Дэвис и др. 1994, стр. 178
- ^ Н. Дершовиц, Ж.-П. Жуанно (1990). Ян ван Леувен (ред.). Системы перезаписи . Справочник по теоретической информатике. B . Эльзевир. С. 243–320.; здесь: разд. 2.3
- ^ М. Даше (1989). "Моделирование машин Тьюринга леволинейным правилом перезаписи". Proc. 3-й RTA . LNCS. 355 . Springer LNCS. С. 109–120.
- ^ Джерард Хуэт, DS Lankford (март 1978 г.). On the Uniform Halting Problem for Term Rewriting Systems (PDF) (Технический отчет). ИРИЯ. п. 8. 283 . Проверено 16 июня 2013 года .
- ^ Бернхард Грамлих (июнь 1993 г.). «Относительно внутреннего, слабого, единообразного и модульного завершения систем перезаписи терминов» . В Воронков, Андрей (ред.). Proc. Международная конференция по логическому программированию и автоматическому мышлению (LPAR) . LNAI. 624 . Springer. С. 285–296. Здесь: Пример 3.3
- ^ Ёсихито Тояма (1987). «Контрпримеры к прекращению действия прямой суммы систем перезаписи терминов» (PDF) . Инф. Процесс. Lett . 25 (3): 141–143. DOI : 10.1016 / 0020-0190 (87) 90122-0 . hdl : 2433/99946 .
- ^ Н. Дершовиц (1985). «Прекращение действия» (PDF) . В Жан-Пьера Жуано (ред.). Proc. RTA . LNCS. 220 . Springer. С. 180–224.; здесь: стр.210
дальнейшее чтение
- Баадер, Франц ; Нипков, Тобиас (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 , Университет Инсбрука
- Портал прекращения действия