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

Формальная система для транскрипции выражений в эквивалентные термины

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

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

Определение

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

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

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

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

Пример 1

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

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

Сначала определим некоторые основные понятия и обозначения. ^[5]

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

Нормальные формы

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

Соединяемость

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

Свойство Чёрча-Россера и понятия слияния

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

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

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

Пример локально конфлюэнтной системы переписывания, не обладающей свойством Чёрча–Россера

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

Следствие . ^[9] В конфлюэнтной АРС, если тогда ${\displaystyle x{\stackrel {*}{\leftrightarrow }}y}$

• Если и x, и y являются нормальными формами, то x = y .
• Если y — нормальная форма, то . ${\displaystyle x{\stackrel {*}{\rightarrow }}y}$

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

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

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

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

Теорема ( лемма Ньюмена ): Конечная ARS конфлюэнтна тогда и только тогда, когда она локально конфлюэнтна.

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

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

• Текстовая задача (математика) — в частности, раздел об абстрактных системах переписывания

Примечания

1. Бук и Отто 1993, стр. 9
2. Terese 2003, стр. 7
3. Book & Otto 1993, стр. 10
4. Тереза ​​2003, стр. 7–8
5. Баадер и Нипков 1998, стр. 8–9.
6. Чёрч и Россер 1936
7. Баадер и Нипков 1998, стр. 9
8. Баадер и Нипков 1998, стр. 11
9. Баадер и Нипков 1998, стр. 12
10. Тереза ​​2003, стр. 11
11. Даффи 1991, стр. 153, раздел 7.2.1
12. Харрисон 2009, стр. 260

Ссылки

• Баадер, Франц ; Нипков, Тобиас (1998). Переписывание терминов и все такое. Cambridge University Press. ISBN 9780521779203.Учебник, подходящий для студентов бакалавриата.
• Nachum Dershowitz и Jean-Pierre Jouannaud Rewrite Systems, Глава 6 в Jan van Leeuwen (Ed.), Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics , Elsevier и MIT Press, 1990, ISBN 0-444-88074-7 , стр. 243–320. Препринт этой главы находится в свободном доступе у авторов, но в нем отсутствуют рисунки. 
• Книга, Рональд В .; Отто, Фридрих (1993). "1, "Абстрактные системы редукции"". Системы переписывания строк . Springer. ISBN 0-387-97965-4.
• Марк Безем; Ян Виллем Клоп ; Роэль де Вриер; Тереза ​​(2003). «1». Системы переписывания терминов . Издательство Кембриджского университета. ISBN 0-521-39115-6.Это всеобъемлющая монография. Однако она использует довольно много обозначений и определений, которые нечасто встречаются в других источниках. Например, свойство Чёрча–Россера определяется как тождественное слиянию.
• Харрисон, Джон (2009). "4 "Равенство"". Справочник по практической логике и автоматизированному рассуждению Издательство Кембриджского университета . ISBN 978-0-521-89957-4.Переписывание аннотации с практической точки зрения решения задач по эквациональной логике .
• Жерар Юэ , Конфлюэнтные редукции: абстрактные свойства и приложения к системам переписывания терминов , Журнал ACM ( JACM ), октябрь 1980 г., том 27, выпуск 4, стр. 797–821. В статье Юэ были установлены многие современные концепции, результаты и обозначения.
• Синьор, Дж.; «Проблема 3x+1 как система переписывания строк», Международный журнал математики и математических наук , том 2010 (2010), идентификатор статьи 458563, 6 страниц.
• Даффи, Дэвид А. (1991). Принципы автоматического доказательства теорем . Wiley.
• Чёрч, Алонзо; Россер, Дж. Б. (1936). «Некоторые свойства преобразования». Труды Американского математического общества . 39 (3): 472–482. doi : 10.2307/1989762 . ISSN  0002-9947. JSTOR  1989762.