В математической логике и теоретической информатике , в абстрактной системе переписывания (также (система абстрактного) уменьшения или системы абстрактных переписывают ; сокращенное АРС ) является формализмом , который захватывает квинтэссенцию понятия и свойство переписывания систем. В своей простейшей форме ARS - это просто набор («объектов») вместе с бинарным отношением , традиционно обозначаемый; это определение может быть дополнительно уточнено, если мы проиндексируем (пометим) подмножества бинарного отношения. Несмотря на свою простоту, ARS достаточно для описания важных свойств переписывающих систем, таких как нормальные формы , завершение и различные понятия слияния .
Исторически сложилось так, что существовало несколько формализованных форм переписывания в абстрактной обстановке, каждая со своими особенностями. Частично это связано с тем, что некоторые понятия эквивалентны, см. Ниже в этой статье. Формализация, которая чаще всего встречается в монографиях и учебниках и которой здесь обычно следуют, принадлежит Gérard Huet (1980). [1]
Определение
Абстрактная восстановительная система ( АРС ) является наиболее общим (одномерным) понятием о задании множества объектов и правил , которые могут быть применены к их трансформации. В последнее время авторы также используют термин « абстрактная система переписывания» . [2] (Предпочтение здесь слова «сокращение» вместо «переписывание» представляет собой отход от единообразного использования слова «переписывание» в названиях систем, которые являются конкретизацией ARS. Поскольку слово «сокращение» не встречается в названия более специализированных систем, в старых текстах сокращение system является синонимом ARS). [3]
АРС представляет собой набор , элементы которого, как правило , называются объектами, вместе с бинарным отношением на А , традиционно обозначаемой →, и называется уменьшение соотношения , переписывают соотношением [2] или только сокращения . [3] Эта (укоренившаяся) терминология, использующая «сокращение», немного вводит в заблуждение, потому что отношение не обязательно уменьшает некоторую меру объектов.
В некоторых контекстах может быть полезно различать некоторые подмножества правил, то есть некоторые подмножества отношения редукции →, например, все отношение редукции может состоять из правил ассоциативности и коммутативности . Следовательно, некоторые авторы определяют отношение редукции → как индексированное объединение некоторых отношений; например, еслииспользуются обозначения (A, → 1 , → 2 ).
Как математический объект, ARS - это то же самое, что и немаркированная система перехода состояний , и если отношение рассматривается как индексированное объединение, то ARS - это то же самое, что и маркированная система перехода состояний с индексами, являющимися метками. Однако фокус исследования и терминология различаются. В системе перехода состояний каждый заинтересован в интерпретации меток как действий, тогда как в ARS основное внимание уделяется тому, как объекты могут быть преобразованы (переписаны) в другие. [4]
Пример 1
Предположим, что набор объектов равен T = { a , b , c }, а бинарное отношение задано правилами a → b , b → a , a → c и b → c . Обратите внимание, что эти правила могут применяться как к a, так и к b, чтобы получить c . Более того, к c ничего нельзя применить для его дальнейшего преобразования. Такое свойство явно важно.
Основные понятия
Пример 1 приводит нас к определению некоторых важных понятий в общем контексте ARS. Для начала нам потребуются основные понятия и обозначения. [5]
- является транзитивным замыканием из, где = - тождественное отношение , т. е.- наименьший предпорядок ( рефлексивное и транзитивное отношение), содержащий. В качестве альтернативы,является рефлексивным транзитивным замыканием в.
- является , То есть объединение отношения → с его обратной связью , также известное как симметричное закрытие из.
- является транзитивным замыканием из, это наименьшее отношение эквивалентности, содержащее. Эквивалентно,является рефлексивным транзитивен симметричным замыканием из.
Нормальные формы и проблема слова
Объект x в A называется приводимым, если в A существует какой-либо другой y и; в противном случае она называется неприводимой или нормальной формой . Объект y называется нормальной формой x, еслии y неприводимо. Если x имеет единственную нормальную форму, то это обычно обозначается как. В примере 1 выше c - это нормальная форма, а. Если каждый объект имеет хотя бы одну нормальную форму, ARS называется нормализующей .
Одной из важных проблем, которые можно сформулировать в ARS, является проблема слов : при заданных x и y они эквивалентны при? Это очень общая установка для формулировки проблемы слов для представления алгебраической структуры . Например, проблема со словом для групп - это частный случай проблемы со словом ARS. Центральным элементом "простого" решения проблемы слов является существование уникальных нормальных форм: в этом случае два объекта эквивалентны в соответствии стогда и только тогда, когда они имеют одинаковую нормальную форму. Проблема слов для ARS в целом неразрешима .
Присоединяемость и свойство Чёрча – Россера
Родственное, но слабее , чем понятие существования нормальных форм является то , что из двух объектов будучи присоединяемым : х и у называется соединимым , если существует некоторый г со свойством. Из этого определения очевидно, что можно определить отношение соединяемости как, где это композиция отношений . Присоединяемость обычно обозначается, несколько сбивчиво, также с помощью, но в этих обозначениях стрелка вниз является бинарным отношением, т. е. мы пишем если x и y соединимы.
Говорят, что ARS обладает свойством Черча-Россера тогда и только тогда, когда подразумевает для всех объектов x , y . Эквивалентно свойство Черча-Россера означает, что рефлексивное транзитивное симметричное замыкание содержится в отношении соединяемости. Алонзо Черч и Дж. Баркли Россер доказали в 1936 г., что лямбда-исчисление обладает этим свойством; [6] отсюда и название собственности. [7] (Тот факт, что лямбда-исчисление обладает этим свойством, также известен как теорема Черча-Россера .) В ARS со свойством Черча-Россера проблема слов может быть сведена к поиску общего преемника. В системе Чёрча-Россера объект имеет не более одной нормальной формы; то есть нормальная форма объекта уникальна, если она существует, но вполне может не существовать. Например, в лямбда-исчислении выражение (λx.xx) (λx.xx) не имеет нормальной формы, потому что существует бесконечная последовательность бета-редукций (λx.xx) (λx.xx) → (λx.xx) ( λx.xx) → ... [8]
Понятия слияния
Ему эквивалентны различные свойства, более простые, чем Черч-Россер. Существование этих эквивалентных свойств позволяет доказать, что система является системой Чёрча-Россера, с меньшими затратами времени. Более того, понятия слияния можно определить как свойства определенного объекта, что для Черча-Россера невозможно. ARS как говорят,
- сливаться тогда и только тогда, когда для всех w , x и y в A , подразумевает . Грубо говоря, слияние означает, что независимо от того, насколько два пути расходятся от общего предка ( w ), пути соединяются у некоторого общего преемника. Это понятие может быть уточнено как свойство конкретного объекта w и системы, названной конфлюэнтной, если все ее элементы являются конфлюэнтными.
- полуконфлюэнтно тогда и только тогда, когда для всех w , x и y в A , подразумевает . Это отличается от слияния одноступенчатым уменьшением от w до x .
- локально конфлюэнтно тогда и только тогда, когда для всех w , x и y в A , подразумевает . Это свойство иногда называют слабым слиянием .
Теорема. Для ARS следующие три условия эквивалентны: (i) он обладает свойством Черча-Россера, (ii) он конфлюэнтен, (iii) он полуконфлюэнтен. [9]
Следствие . [10] В сливном ОРС, если тогда
- Если и x, и y - нормальные формы, то x = y .
- Если y - нормальная форма, то
Из-за этих эквивалентностей в литературе встречается немало различий в определениях. Например, в Терезе свойство Черча-Россера и слияние определены как синонимы и идентичны приведенному здесь определению слияния; Черч-Россер, как здесь определено, остается безымянным, но дается как эквивалентное свойство; это отступление от других текстов является преднамеренным. [11] Из-за приведенного выше следствия можно определить нормальную форму y для x как неприводимое y со свойством, что. Это определение, данное в Книге и Отто, эквивалентно общему определению, данному здесь для конфлюэнтной системы, но оно более инклюзивное в неконфлюэнтной ARS.
С другой стороны, местное слияние не эквивалентно другим понятиям слияния, приведенным в этом разделе, но оно строго слабее, чем слияние. Типичный контрпример:, которая локально сливается, но не сливается (см. рисунок).
Прекращение и сближение
Абстрактная система перезаписи называется завершающей или нётеровой, если не существует бесконечной цепочки.. (Это просто означает, что отношение перезаписи является нётеровым .) В завершающей ARS каждый объект имеет по крайней мере одну нормальную форму, таким образом, он нормализуется. Обратное неверно. Например, в примере 1 существует бесконечная цепочка перезаписи, а именно, хотя система нормализуется. Сливающийся и согласующие АРС называется канонической , [12] или сходится . В конвергентной ARS каждый объект имеет уникальную нормальную форму. Но достаточно, чтобы система была конфлюэнтной и нормализуемой, чтобы существовала уникальная нормаль для каждого элемента, как показано в примере 1.
Теорема ( лемма Ньюмана ): завершающаяся ARS конфлюэнтна тогда и только тогда, когда она локально конфлюэнтна.
Первоначальное доказательство этого результата Ньюманом в 1942 г. было довольно сложным. Только в 1980 году Хуэ опубликовал гораздо более простое доказательство, основанное на том факте, что когдазавершается, мы можем применить хорошо обоснованную индукцию . [13]
Заметки
- ^ Книга и Отто, стр. 9
- ^ a b Тереза, стр. 7,
- ^ a b Книга и Отто, стр. 10
- ^ Тереза, стр. 7-8
- ^ Баадер и Нипкова, стр. 8-9
- ^ Алонзо Черч и Дж. Баркли Россер. Некоторые свойства преобразования. Пер. AMS, 39: 472-482, 1936.
- ^ Баадер и Нипков, стр. 9
- ^ С.Б. Купер, Теория вычислимости , стр. 184
- ^ Баадер и Нипков, стр. 11
- ^ Баадер и Нипков, стр. 12
- ^ Тереза стр.11
- ^ Дэвид А. Даффи (1991). Принципы автоматизированного доказательства теорем . Вайли. Здесь: раздел 7.2.1, с.153
- ^ Харрисон, стр. 260
дальнейшее чтение
- Баадер, Франц ; Нипков, Тобиас (1998). Перезапись терминов и все такое . Издательство Кембриджского университета. ISBN 9780521779203. Учебник для студентов бакалавриата.
- Нахум Дершовиц и Жан-Пьер Жуано переписывают системы , глава 6 в книге Яна ван Леувена (ред.), Справочник по теоретической информатике, том B: Формальные модели и семантика. , Elsevier и MIT Press, 1990 г., ISBN 0-444-88074-7 , стр. 243–320. Препринт этой главы находится в свободном доступе от авторов, но он пропускает цифру.
- Рональд В. Бук и Фридрих Отто, Системы перезаписи строк , 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 страниц.