Система рерайтинга тезисов - Abstract rewriting system

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

Исторически сложилось так, что было несколько формализованных форм переписывания в абстрактной обстановке, каждая со своими особенностями. Частично это связано с тем, что некоторые понятия эквивалентны, см. Ниже в этой статье. Формализация, которая чаще всего встречается в монографиях и учебниках и которой здесь обычно следуют, связана с Жерар Юэ (1980).^[1]

Определение

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

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

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

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

Пример 1

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

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

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

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

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

Решение проблемы со словом: решаем, если ${\displaystyle x{\stackrel {*}{\leftrightarrow }}y}$ обычно требует эвристического поиска (красный, зеленый), решая ${\displaystyle x\downarrow =y\downarrow }$ просто (серый). Для систем перезаписи терминов Алгоритм завершения Кнута-Бендикса увеличивает ${\displaystyle \rightarrow }$ по возможности установить уникальные нормальные формы.

Основная статья: Нормальная форма (реферат)

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

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

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

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

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

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

Смотрите также: Confluence (абстрактное переписывание)

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

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

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

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

Следствие.^[10] В сливном ОРС, если ${\displaystyle x{\stackrel {*}{\leftrightarrow }}y}$ тогда

• Если оба Икс и у нормальные формы, то Икс = у.
• Если у нормальная форма, то ${\displaystyle x{\stackrel {*}{\rightarrow }}y}$

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

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

Прекращение и сближение

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

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

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

Примечания

1. Книга и Отто, стр. 9
2. Тереза, стр. 7,
3. Книга и Отто, стр. 10
4. Тереза, стр. 7-8
5. Баадер и Нипков, стр. 8-9.
6. Алонзо Черч и Дж. Баркли Россер. Некоторые свойства преобразования. Пер. АМС, 39: 472-482, 1936.
7. Баадер и Нипков, стр. 9
8. С.Б. Купер, Теория вычислимости, п. 184
9. Баадер и Нипков, стр. 11
10. Баадер и Нипков, стр. 12
11. Тереза ​​стр.11
12. Дэвид А. Даффи (1991). Принципы автоматизированного доказательства теорем. Вайли. Здесь: раздел 7.2.1, с.153
13. Харрисон, стр. 260

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

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