Система перезаписи абстрактных

редактировать

В математической логике и теоретической информатике, реферат система(также (абстрактная) система сокращенияили абстрактная система перезаписи; сокращенно ARS) - это формализм, который фиксирует наиболее существенное понятие и свойства переписывающих систем. В своей простейшей форме ARS представляет собой просто набор («объектов») вместе с бинарным отношением, традиционно обозначаемым $→ {\ displaystyle \ rightarrow}$ $\ rightarrow$ ; это определение может быть дополнительно уточнено, если мы проиндексируем (пометим) подмножества бинарного отношения. Несмотря на свою простоту, ARS достаточно для описания важных свойств переписывающих систем, таких как нормальные формы, завершение и различные понятия слияния.

Исторически сложилось так, что было несколько формализации переписывания в абстрактной обстановке, каждая со своими особенностями. Частично это связано с тем, что некоторые понятия эквивалентны, см. Ниже в этой статье. Формализация, которая чаще всего встречается в монографиях и учебниках и которой здесь обычно следуют, принадлежит Gérard Huet (1980).

Содержание

1 Определение
2 Пример 1
3 Основные понятия
4 Нормальные формы и проблема слов
5 Присоединяемость и свойство Черча – Россера
6 Понятия слияния
7 Прекращение и конвергенция
8 Примечания
9 Далее чтение

Определение

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

ARS - это набор A, элементы которого обычно называются объектами вместе с бинарное отношение на A, традиционно обозначаемое → и называемое отношением редукции, отношением перезаписиили просто редукцией. Эта (укоренившаяся) терминология с использованием «редукции» немного вводит в заблуждение, потому что отношение не обязательно уменьшает некоторую меру объектов.

В некоторых контекстах может быть полезно различать некоторые подмножества правил, то есть некоторые подмножества редукционного отношения →, например все отношение редукции может состоять из правил ассоциативности и коммутативности. Следовательно, некоторые авторы определяют отношение редукции → как индексированное объединение некоторых отношений; например, если $→ 1 ∪ → 2 = → {\ displaystyle {\ rightarrow _ {1} \ cup \ rightarrow _ {2}} = {\ rightarrow}}$ ${\ displaystyle {\ rightarrow _ {1} \ cup \ rightarrow _ {2}} = {\ rightarrow}}$ , используется обозначение ( A, → 1 , → 2 ).

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

Пример 1

Предположим, что набор объектов равен T = {a, b, c}, а бинарное отношение задано правилами a → b, b → a, a → c и b → c. Обратите внимание, что эти правила могут применяться как к a, так и к b, чтобы получить c. Более того, к c ничего нельзя применить, чтобы преобразовать его дальше. Такое свойство явно важно.

Основные понятия

Пример 1 приводит нас к определению некоторых важных понятий в общей настройке ARS. Для начала нам понадобятся некоторые основные понятия и обозначения.

$→ ∗ {\ displaystyle {\ stackrel {*} {\ rightarrow}}}$ ${\ stackrel {*} {\ rightarrow}}$ - это транзитивное замыкание элемента $( →) ∪ (=) {\ displaystyle (\ rightarrow) \ cup (=)}$ ${\ displaystyle (\ rightarrow) \ cup (=)}$ , где = - отношение идентичности, то есть $→ ∗ {\ displaystyle {\ stackrel {*} {\ rightarrow}}}$ ${\ stackrel {*} {\ rightarrow}}$ - наименьший предпорядок (рефлексивное и транзитивное отношение), содержащий $→ { \ Displaystyle \ rightarrow}$ $\ rightarrow$ . В качестве альтернативы, $→ ∗ {\ displaystyle {\ stackrel {*} {\ rightarrow}}}$ ${\ stackrel {*} {\ rightarrow}}$ - это рефлексивное переходное замыкание из $→ {\ displaystyle \ rightarrow}$ $\ rightarrow$ .
$↔ {\ displaystyle \ leftrightarrow}$ $\ leftrightarrow$ равно $(→) ∪ (→) - 1 {\ displaystyle (\ rightarrow) \ cup {(\ rightarrow) ^ {- 1}}}$ ${\ displaystyle (\ rightarrow) \ cup {(\ rightarrow) ^ {- 1}}}$ , то есть объединение отношения → с его обратным отношением, также известное как симметричное замыкание элемента $→ {\ displaystyle \ rightarrow}$ $\ rightarrow$ .
$↔ ∗ {\ displaystyle {\ stackrel {*} {\ leftrightarrow}}}$ ${\ stackrel {*} {\ leftrightarrow}}$ - это переходное замыкание из $(↔) ∪ (=) {\ displaystyle (\ leftrightarrow) \ cup (=)}$ ${\ displaystyle (\ leftrightarrow) \ cup (=)}$ , то есть $↔ ∗ {\ displaystyle {\ stackrel {*} {\ leftrightarrow}}}$ ${\ stackrel {*} {\ leftrightarrow}}$ наименьшее отношение эквивалентности, содержащее $→ {\ displaystyle \ rightarrow}$ $\ rightarrow$ . Точно так же $↔ ∗ {\ displaystyle {\ stackrel {*} {\ leftrightarrow}}}$ ${\ stackrel {*} {\ leftrightarrow}}$ - это рефлексивное транзитивное симметричное замыкание из $→ {\ displaystyle \ rightarrow }$ $\ rightarrow$ .

Нормальные формы и проблема со словами

Решение проблемы со словами: определение того,

x ↔ ∗ y {\ displaystyle x {\ stackrel {*} {\ leftrightarrow}} y}

x {\ stackrel {*} {\ leftrightarrow}} y

обычно требует эвристического поиска (красный, зеленый), тогда как решение

x ↓ = y ↓ {\ displaystyle x \ downarrow = y \ downarrow}

x \ downarrow = y \ downarrow

является простым (серый). Для систем перезаписи терминов алгоритм завершения Кнута-Бендикса увеличивает

→ {\ displaystyle \ rightarrow}

\ rightarrow

, чтобы установить уникальные нормальные формы, если это возможно.

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

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

Соединяемость и свойство Черча – Россера

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

Считается, что ARS обладает свойством Черча-Россератогда и только тогда, когда $x ↔ ∗ y {\ displaystyle x {\ stackrel {*} {\ leftrightarrow}} y }$ $x {\ stackrel {*} {\ leftrightarrow}} y$ подразумевает $x ↓ y {\ displaystyle x {\ mathbin {\ downarrow}} y}$ $x {\ mathbin {\ downarrow}} y$ для всех объектов x, y. Эквивалентно свойство Черча-Россера означает, что рефлексивное транзитивное симметричное замыкание содержится в отношении соединяемости. Алонсо Черч и Дж. Баркли Россер доказал в 1936 году, что лямбда-исчисление обладает этим свойством; отсюда и название собственности. (Тот факт, что лямбда-исчисление обладает этим свойством, также известен как теорема Черча-Россера.) В ARS со свойством Черча-Россера проблема слов может быть сведена к поиску общего преемника. В системе Чёрча-Россера объект имеет не более одной нормальной формы; то есть нормальная форма объекта уникальна, если она существует, но вполне может не существовать. В лямбда-исчислении, например, выражение (λx.xx) (λx.xx) не имеет нормальной формы, поскольку существует бесконечная последовательность бета-редукций (λx.xx) (λx.xx) → (λx.xx) (λx.xx) →...

Понятия слияния

Ему эквивалентны различные свойства, более простые, чем Черч-Россер. Существование этих эквивалентных свойств позволяет доказать, что система является системой Чёрча-Россера с меньшими усилиями. Более того, понятия слияния могут быть определены как свойства определенного объекта, что для Черча-Россера невозможно. ARS $(A, →) {\ displaystyle (A, \ rightarrow)}$ $(A, \ rightarrow)$ называется

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

Пример локально-конфлюэнтной системы перезаписи, не имеющей свойства Черча-Россера

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

Следствие. В конфлюэнтной ARS, если $x ↔ ∗ y {\ displaystyle x {\ stackrel {*} {\ leftrightarrow}} y}$ $x {\ stackrel {*} {\ leftrightarrow}} y$ , то

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

Из-за этих эквивалентностей a в литературе встречается немало различий в определениях. Например, в Терезе свойство Черча-Россера и слияние определены как синонимы и идентичны приведенному здесь определению слияния; Черч-Россер, как здесь определено, остается безымянным, но предоставляется как эквивалентное свойство; это отступление от других текстов является преднамеренным. Из-за приведенного выше следствия можно определить нормальную форму y числа x как неприводимое y со свойством, что $x ↔ ∗ y {\ displaystyle x {\ stackrel {*} {\ leftrightarrow}} y}$ $x {\ stackrel {*} {\ leftrightarrow}} y$ . Это определение, найденное в Книге и Отто, эквивалентно общему определению, данному здесь для конфлюэнтной системы, но оно более инклюзивное в неконфлюэнтной ARS.

С другой стороны, местное слияние не эквивалентно другим понятиям слияния, приведенным в этом разделе, но оно строго слабее, чем слияние. Типичный контрпример: ${b → c, c → b, b → a, c → d} {\ displaystyle \ {b \ rightarrow c, c \ rightarrow b, b \ rightarrow a, c \ rightarrow d \} }$ ${\ displaystyle \ {b \ rightarrow c, c \ rightarrow b, b \ rightarrow a , c \ rightarrow d \}}$ , который локально сливается, но не сливается (см. Рисунок).

Завершение и конвергенция

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

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

Первоначальное доказательство этого результата Ньюманом в 1942 г. было довольно сложным. Только в 1980 году Хуэ опубликовал гораздо более простое доказательство, основанное на том факте, что, когда $→ {\ displaystyle \ rightarrow}$ $\ rightarrow$ завершается, мы можем применить хорошо обоснованную индукцию.

Дополнительная литература

Баадер, Франц ; Нипков, Тобиас (1998). Изменение сроков и все такое. Издательство Кембриджского университета. ISBN 9780521779203. CS1 maint: ref = harv (ссылка ) Учебник для студентов.
Нахум Дершовиц и Жан-Пьер Жуано Системы перезаписи, глава 6 в Ян ван Левен (ред.), Справочник по теоретической информатике, том B: Формальные модели и семантика., Elsevier and MIT Press, 1990, ISBN 0-444-88074-7, стр. 243–320. Препринт этой главы находится в свободном доступе у авторов, но в нем отсутствуют рисунки.
Рональд В. Книга и Фридрих Отто, String-rewriting Systems, Springer (1993). Глава 1, «Системы абстрактной редукции»
, Ян Виллем Клоп, («Тереза»), Системы переписывания терминов, Cambridge University Press, 2003, ISBN 0-521 -39115-6, Глава 1. Это обширная монография. Однако он использует изрядное количество обозначений и определений, которые обычно не встречаются в других местах. Например, свойство Черча – Россера идентично слиянию.
Джон Харрисон, Справочник по практической логике и автоматизированному мышлению, Cambridge University Press, 2009, ISBN 978-0-521-89957-4, глава 4 «Равенство». Переписывание абстрактных текстов с практической точки зрения решения задач в эквациональной логике.
Жерар Юэ, Конфлюэнтные редукции: абстрактные свойства и приложения к системам перезаписи терминов, Журнал ACM (JACM ), Октябрь 1980 г., том 27, выпуск 4, стр. 797–821. В статье Хюэ установлены многие современные концепции, результаты и обозначения.
Sinyor, J.; «Задача 3x + 1 как система перезаписи строк» , Международный журнал математики и математических наук, том 2010 (2010), идентификатор статьи 458563, 6 страниц.