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

В абстрактном переписывании ^[1] объект находится в нормальной форме , если его нельзя переписать дальше, т. е. он неприводим. В зависимости от системы перезаписи объект может переписываться в несколько нормальных форм или вообще не переписываться. Многие свойства систем переписывания относятся к нормальным формам.

Определения

Формально, если ( A ,→) — абстрактная система переписывания , x ∈ A находится в нормальной форме , если не существует y ∈ A такого, что x → y , т. е. x — неприводимый термин.

Объект a является слабо нормализуемым, если существует хотя бы одна конкретная последовательность перезаписей, начиная с a , которая в конечном итоге приводит к нормальной форме. Система перезаписи обладает свойством слабой нормализации или является (слабо) нормализуемой (WN), если каждый объект слабо нормализуется. Объект a является сильно нормализующим, если каждая последовательность перезаписей, начиная с a, в конечном итоге заканчивается нормальной формой. Абстрактная система переписывания является сильно нормализуемой , завершающей , нетеровой или обладает свойством (сильной) нормализации (SN), если каждый из ее объектов является сильно нормализующим. ^[2]

Система перезаписи обладает свойством нормальной формы (НФ), если для всех объектов a и нормальных форм b , b может быть получено из a серией перезаписей и обратных перезаписей, только если a сводится к b . Система перезаписи обладает уникальным свойством нормальной формы (UN), если для всех нормальных форм a , b ∈ S , a может быть достигнута из b серией перезаписей и обратных перезаписей, только если a равно b . Система перезаписи обладает уникальным свойством нормальной формы относительно редукции (UN ^→), если для каждого члена, приводящего к нормальным формам a и b , a равно b . ^[3]

Результаты

В этом разделе представлены некоторые хорошо известные результаты. Во-первых, SN подразумевает WN. ^[4]

Слияние (сокращенно CR) подразумевает, что NF подразумевает UN, подразумевает UN ^→. ^[3] Обратные последствия обычно не имеют места. {a→b,a→c,c→c,d→c,d→e} – это UN ^→ но не UN, поскольку b=e и b,e — нормальные формы. {a→b,a→c,b→b} — это UN, но не NF, поскольку b=c, c — нормальная форма и b не сводится к c. {a→b,a→c,b→b,c→c} является NF, поскольку нет нормальных форм, но не CR, поскольку a сводится к b и c, а b,c не имеют общей редукции.

ВН и ООН ^→ подразумевают слияние. Отсюда CR, NF, ООН и ООН. ^→ совпадают, если выполнено WN. ^[5]

Примеры

Одним из примеров является то, что упрощение арифметических выражений дает число — в арифметике все числа являются нормальными формами. Примечательным фактом является то, что все арифметические выражения имеют уникальное значение, поэтому система перезаписи является строго нормализуемой и конфлюэнтной: ^[6]

(3 + 5) * (1 + 2) ⇒ 8 * (1 + 2) ⇒ 8 * 3 ⇒ 24

(3 + 5) * (1 + 2) ⇒ (3 + 5) * 3 ⇒ 3*3 + 5*3 ⇒ 9 + 5*3 ⇒ 9 + 15 ⇒ 24

Примеры ненормализующих систем (не слабо и не сильно) включают счет до бесконечности (1 ⇒ 2 ⇒ 3 ⇒ ...) и петли, такие как функция преобразования гипотезы Коллатца (1 ⇒ 2 ⇒ 4 ⇒ 1 ⇒ ...) , то вопрос о наличии других петель преобразования Коллатца остается открытым). ^[7] Другим примером является система с одним правилом { r ( x , y ) → r ( y , x ) }, которая не имеет нормализующих свойств, поскольку с любого терма, например r (4,2), начинается одна последовательность перезаписи, а именно. r (4,2) → r (2,4) → r (4,2) → r (2,4) → ..., что бесконечно долго. Это приводит к идее переписать «по модулю коммутативности », где термин находится в нормальной форме, если не применяются никакие правила, кроме коммутативности. ^[8]

Система { b → a , b → c , c → b , c → d } (на фото) является примером слабо нормализующей, но не сильно нормализующей системы. a и d — нормальные формы, а b и c можно свести к a или d , но бесконечное сокращение b → c → b → c → ... означает, что ни b, ни c не являются сильно нормализующими.

Нетипизированное лямбда-исчисление

Чистое нетипизированное лямбда-исчисление не удовлетворяет свойству сильной нормализации и даже свойству слабой нормализации. Рассмотрим термин $\lambda x.xxx$ (приложение остается ассоциативным ). Он имеет следующее правило перезаписи: для любого термина $t$ ,

(\mathbf {\lambda } x.xxx)t\rightarrow ttt

Но подумайте, что происходит, когда мы подаем заявку $\lambda x.xxx$ себе:

{\begin{aligned}(\mathbf {\lambda } x.xxx)(\lambda x.xxx)&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow \ \cdots \,\end{aligned}}

Следовательно, термин $(\lambda x.xxx)(\lambda x.xxx)$ не является сильно нормализующим. И это единственная редуцирующая последовательность, а значит, она тоже не является слабо нормирующей.

Типизированное лямбда-исчисление

Различные системы типизированного лямбда-исчисления, включая просто типизированное лямбда-исчисление , Жана-Ива Жирара и система F исчисление Тьерри Коканда являются конструкций строго нормализующими.

Систему лямбда-исчисления со свойством нормализации можно рассматривать как язык программирования, обладающий свойством завершать каждую программу . Хотя это очень полезное свойство, у него есть недостаток: язык программирования со свойством нормализации не может быть полным по Тьюрингу , иначе можно было бы решить проблему остановки, посмотрев, проверяется ли тип программы. Это означает, что существуют вычислимые функции, которые не могут быть определены в просто типизированном лямбда-исчислении, а также в исчислении конструкций и системе F. Типичным примером является самоинтерпретатор общего языка программирования . ^[10]

См. также

Примечания

Ссылки

^ Франц Баадер ; Тобиас Нипков (1998). Переписывание терминов и все такое . Издательство Кембриджского университета . ISBN 9780521779203 .
^ Олебуш, Энно (1998). «Теоремы Черча-Россера для абстрактной редукции по модулю отношения эквивалентности» . Техники и приложения переписывания . Конспекты лекций по информатике. Том. 1379. с. 18. дои : 10.1007/BFb0052358 . ISBN 978-3-540-64301-2 .
^ Перейти обратно: ^а ^б Клоп, JW; де Вриер, RC (февраль 1989 г.). «Уникальные нормальные формы лямбда-исчисления с сюръективным спариванием» . Информация и вычисления . 80 (2): 97–113. дои : 10.1016/0890-5401(89)90014-X .
^ «логика. В чем разница между сильной нормализацией и слабой нормализацией в контексте систем перезаписи?» . Обмен стеками в области компьютерных наук . Проверено 12 сентября 2021 г.
^ Олебуш, Энно (17 апреля 2013 г.). Расширенные темы по переписыванию терминов . Springer Science & Business Media. стр. 13–14. ISBN 978-1-4757-3661-8 .
^ Тереза (2003). Системы переписывания терминов . Кембридж, Великобритания: Издательство Кембриджского университета. п. 1. ISBN 0-521-39115-6 .
^ Тереза (2003). Системы переписывания терминов . Кембридж, Великобритания: Издательство Кембриджского университета. п. 2. ISBN 0-521-39115-6 .
^ Дершовиц, Нахум; Жуанно, Жан-Пьер (1990). «6. Переписать системы». Ян ван Леувен (ред.). Справочник по теоретической информатике . Том. Б. Эльзевир. стр. 9–10. CiteSeerX 10.1.1.64.3114 . ISBN 0-444-88074-7 .
^ Н. Дершовиц и Ж.-П. Жуанно (1990). «Переписать системы». Ян ван Леувен (ред.). Формальные модели и семантика . Справочник по теоретической информатике. Том. Б. Эльзевир. п. 268. ИСБН 0-444-88074-7 .
^ Риоло, Рик; Ворзель, Уильям П.; Котанчек, Марк (4 июня 2015 г.). Теория и практика генетического программирования XII . Спрингер. п. 59. ИСБН 978-3-319-16030-6 . Проверено 8 сентября 2021 г.

[1] Франц Баадер ; Тобиас Нипков (1998). Переписывание терминов и все такое . Издательство Кембриджского университета . ISBN 9780521779203 .

[2] Олебуш, Энно (1998). «Теоремы Черча-Россера для абстрактной редукции по модулю отношения эквивалентности» . Техники и приложения переписывания . Конспекты лекций по информатике. Том. 1379. с. 18. дои : 10.1007/BFb0052358 . ISBN 978-3-540-64301-2 .

[NF-3] Перейти обратно: ^а ^б Клоп, JW; де Вриер, RC (февраль 1989 г.). «Уникальные нормальные формы лямбда-исчисления с сюръективным спариванием» . Информация и вычисления . 80 (2): 97–113. дои : 10.1016/0890-5401(89)90014-X .

[4] «логика. В чем разница между сильной нормализацией и слабой нормализацией в контексте систем перезаписи?» . Обмен стеками в области компьютерных наук . Проверено 12 сентября 2021 г.

[5] Олебуш, Энно (17 апреля 2013 г.). Расширенные темы по переписыванию терминов . Springer Science & Business Media. стр. 13–14. ISBN 978-1-4757-3661-8 .

[6] Тереза (2003). Системы переписывания терминов . Кембридж, Великобритания: Издательство Кембриджского университета. п. 1. ISBN 0-521-39115-6 .

[7] Тереза (2003). Системы переписывания терминов . Кембридж, Великобритания: Издательство Кембриджского университета. п. 2. ISBN 0-521-39115-6 .

[8] Дершовиц, Нахум; Жуанно, Жан-Пьер (1990). «6. Переписать системы». Ян ван Леувен (ред.). Справочник по теоретической информатике . Том. Б. Эльзевир. стр. 9–10. CiteSeerX 10.1.1.64.3114 . ISBN 0-444-88074-7 .

[Dershowitz.Jouannaud.1990.Fig2-9] Н. Дершовиц и Ж.-П. Жуанно (1990). «Переписать системы». Ян ван Леувен (ред.). Формальные модели и семантика . Справочник по теоретической информатике. Том. Б. Эльзевир. п. 268. ИСБН 0-444-88074-7 .

[10] Риоло, Рик; Ворзель, Уильям П.; Котанчек, Марк (4 июня 2015 г.). Теория и практика генетического программирования XII . Спрингер. п. 59. ИСБН 978-3-319-16030-6 . Проверено 8 сентября 2021 г.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

v т и Нормальные формы в логике
Пропозициональная логика	Нормальная форма отрицания Конъюнктивная нормальная форма Дизъюнктивная нормальная форма Алгебраическая нормальная форма ( полином Жегалкина ) Каноническая форма Блейка Каноническая нормальная форма Оговорка о роге
Логика предикатов	Шолем нормальная форма Гербрандизация Пренекс нормальная форма
Другой	Бета-нормальная форма Модальная клаузальная форма Нормальная форма (естественная дедукция)