Нормальная форма (абстрактное переписывание)
В абстрактном переписывании [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 подразумевает ООН, подразумевает ООН. → . [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 не являются сильно нормализующими.
Нетипизированное лямбда-исчисление
[ редактировать ]Чистое нетипизированное лямбда-исчисление не удовлетворяет свойству сильной нормализации и даже свойству слабой нормализации. Рассмотрим термин (приложение остается ассоциативным ). Он имеет следующее правило перезаписи: для любого термина ,
Но подумайте, что происходит, когда мы подаем заявку себе:
Следовательно, термин не является сильно нормализующим. И это единственная редуцирующая последовательность, а значит, она тоже не является слабо нормирующей.
Типизированное лямбда-исчисление
[ редактировать ]Различные системы типизированного лямбда-исчисления, включая просто типизированное лямбда-исчисление , Жана-Ива Жирара и система F исчисление Тьерри Коканда являются конструкций строго нормализующими.
Систему лямбда-исчисления со свойством нормализации можно рассматривать как язык программирования, обладающий свойством завершать каждую программу . Хотя это очень полезное свойство, у него есть недостаток: язык программирования со свойством нормализации не может быть полным по Тьюрингу , иначе можно было бы решить проблему остановки, посмотрев, проверяется ли тип программы. Это означает, что существуют вычислимые функции, которые не могут быть определены в просто типизированном лямбда-исчислении, а также в исчислении конструкций и системе F. Типичным примером является самоинтерпретатор общего языка программирования . [10]
См. также
[ редактировать ]- Каноническая форма
- Типизированное лямбда-исчисление
- Переписывание
- Полное функциональное программирование
- Гипотеза Барендрегта–Геверса–Клопа
- Лемма Ньюмана
- Нормализация путем оценки
Примечания
[ редактировать ]Ссылки
[ редактировать ]- ^ Франц Баадер ; Тобиас Нипков (1998). Переписывание терминов и все такое . Издательство Кембриджского университета . ISBN 9780521779203 .
- ^ Олебуш, Энно (1998). «Теоремы Черча-Россера для абстрактной редукции по модулю отношения эквивалентности» . Техники и приложения переписывания . Конспекты лекций по информатике. Том. 1379. с. 18. дои : 10.1007/BFb0052358 . ISBN 978-3-540-64301-2 .
- ^ Jump up to: Перейти обратно: а б Клоп, 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 г.