Jump to content

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

(Перенаправлено из свойства нормализации )

В абстрактном переписывании [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]

Слабо, но не сильно нормализующая система перезаписи [9]

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

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

[ редактировать ]

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

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

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

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

[ редактировать ]

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

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

См. также

[ редактировать ]

Примечания

[ редактировать ]
  1. ^ Франц Баадер ; Тобиас Нипков (1998). Переписывание терминов и все такое . Издательство Кембриджского университета . ISBN  9780521779203 .
  2. ^ Олебуш, Энно (1998). «Теоремы Черча-Россера для абстрактной редукции по модулю отношения эквивалентности» . Техники и приложения переписывания . Конспекты лекций по информатике. Том. 1379. с. 18. дои : 10.1007/BFb0052358 . ISBN  978-3-540-64301-2 .
  3. ^ Jump up to: Перейти обратно: а б Клоп, 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 .
  9. ^ Н. Дершовиц и Ж.-П. Жуанно (1990). «Переписать системы». Ян ван Леувен (ред.). Формальные модели и семантика . Справочник по теоретической информатике. Том. Б. Эльзевир. п. 268. ИСБН  0-444-88074-7 .
  10. ^ Риоло, Рик; Ворзель, Уильям П.; Котанчек, Марк (4 июня 2015 г.). Теория и практика генетического программирования XII . Спрингер. п. 59. ИСБН  978-3-319-16030-6 . Проверено 8 сентября 2021 г.
Arc.Ask3.Ru: конец переведенного документа.
Arc.Ask3.Ru
Номер скриншота №: 79c2d867b88a540f2f8a2c4e7713ba4d__1714251540
URL1:https://arc.ask3.ru/arc/aa/79/4d/79c2d867b88a540f2f8a2c4e7713ba4d.html
Заголовок, (Title) документа по адресу, URL1:
Normal form (abstract rewriting) - Wikipedia
Данный printscreen веб страницы (снимок веб страницы, скриншот веб страницы), визуально-программная копия документа расположенного по адресу URL1 и сохраненная в файл, имеет: квалифицированную, усовершенствованную (подтверждены: метки времени, валидность сертификата), открепленную ЭЦП (приложена к данному файлу), что может быть использовано для подтверждения содержания и факта существования документа в этот момент времени. Права на данный скриншот принадлежат администрации Ask3.ru, использование в качестве доказательства только с письменного разрешения правообладателя скриншота. Администрация Ask3.ru не несет ответственности за информацию размещенную на данном скриншоте. Права на прочие зарегистрированные элементы любого права, изображенные на снимках принадлежат их владельцам. Качество перевода предоставляется как есть. Любые претензии, иски не могут быть предъявлены. Если вы не согласны с любым пунктом перечисленным выше, вы не можете использовать данный сайт и информация размещенную на нем (сайте/странице), немедленно покиньте данный сайт. В случае нарушения любого пункта перечисленного выше, штраф 55! (Пятьдесят пять факториал, Денежную единицу (имеющую самостоятельную стоимость) можете выбрать самостоятельно, выплаичвается товарами в течение 7 дней с момента нарушения.)