stringtranslate.com

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

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

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

Определение

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

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

В некоторых контекстах может быть полезно различать некоторые подмножества правил, то есть некоторые подмножества отношения редукции →, например, все отношение редукции может состоять из правил ассоциативности и коммутативности . Следовательно, некоторые авторы определяют отношение редукции → как индексированное объединение некоторых отношений; например, если , то используется обозначение (A, → 1 , → 2 ).

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

Пример 1

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

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

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

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

Объект x в A называется приводимым , если существуют некоторые другие y в A и ; в противном случае он называется неприводимым или нормальной формой . Объект y называется нормальной формой x , если и y неприводим. Если x имеет уникальную нормальную форму, то это обычно обозначается . В примере 1 выше c является нормальной формой, а . Если каждый объект имеет по крайней мере одну нормальную форму, ARS называется нормализующей .

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

Связанное, но более слабое понятие, чем существование нормальных форм, заключается в том, что два объекта являются соединяемыми : x и y называются соединяемыми, если существует некоторый z со свойством . Из этого определения очевидно, что можно определить отношение соединяемости как , где — композиция отношений . Соединяемость обычно обозначается, что несколько сбивает с толку, также с помощью , но в этой нотации стрелка вниз является бинарным отношением, т. е. мы пишем, если x и y соединяемы.

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

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

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

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

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

Следствие . [9] В конфлюэнтной АРС, если тогда

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

С другой стороны, локальное слияние не эквивалентно другим понятиям слияния, данным в этом разделе, но оно строго слабее слияния. Типичным контрпримером является , которое локально сливающееся, но не сливающееся (ср. рисунок).

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

Абстрактная система переписывания называется завершающей или нётеровой , если нет бесконечной цепи . (Это просто означает, что отношение переписывания является нётеровым отношением .) В завершающей ARS каждый объект имеет по крайней мере одну нормальную форму, поэтому она является нормализующей. Обратное неверно. Например, в примере 1 существует бесконечная цепочка переписывания, а именно , даже если система является нормализующей. Сходящаяся и завершающая ARS называется канонической , [11] или сходящейся . В сходящейся ARS каждый объект имеет уникальную нормальную форму. Но для того, чтобы система была сходящейся и нормализующей, достаточно, чтобы существовала уникальная нормаль для каждого элемента, как показано в примере 1.

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

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

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

Примечания

  1. ^ Бук и Отто 1993, стр. 9
  2. ^ ab Terese 2003, стр. 7
  3. ^ ab 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

Ссылки