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

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

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

Определение

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

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

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

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

Пример 1

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

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

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

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

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

Основная статья: Нормальная форма (абстрактное переписывание)

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

Возможность соединения

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

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

Основная статья: Confluence (абстрактный переписывание)

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

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

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

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

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

Следствие . При конфлюэнтном ОРС, если $x{\stackrel {*}{\leftrightarrow }}y$ затем

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

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

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

Прекращение и конвергенция

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

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

Первоначальное доказательство этого результата Ньюмана в 1942 году было довольно сложным. Лишь в 1980 году Юэ опубликовал гораздо более простое доказательство, использующее тот факт, что когда $\rightarrow$ завершается, мы можем применить обоснованную индукцию .

См. также

• Словесная задача (математика) - особенно раздел, посвященный абстрактным системам переписывания.

Ссылки

• Баадер, Франц ; Нипков, Тобиас (1998). Переписывание терминов и все такое . Издательство Кембриджского университета. ISBN  9780521779203 . Учебник, подходящий для студентов старших курсов.
• Нахум Дершовиц и Жан-Пьер Жуанно переписывают системы , глава 6 в книге Яна ван Леувена (ред.), Справочник по теоретической информатике, том B: формальные модели и семантика , Elsevier и MIT Press, 1990, ISBN   0-444-88074-7 , стр. 243–320. Препринт . этой главы находится в свободном доступе у авторов, но в нем отсутствуют рисунки
• Книга, Рональд В .; Отто, Фридрих (1993). «1, «Абстрактные системы редукции» ». Системы перезаписи строк . Спрингер. 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). Принципы автоматического доказательства теорем . Уайли.
• Черч, Алонсо; Россер, Дж. Б. (1936). «Некоторые свойства конверсии» . Труды Американского математического общества . 39 (3): 472–482. дои : 10.2307/1989762 . ISSN   0002-9947 . JSTOR   1989762 .