В абстрактном переписывании [ 1] объект находится в нормальной форме , если его нельзя переписать дальше, т. е. он неприводим. В зависимости от системы переписывания объект может переписываться в несколько нормальных форм или ни в одну. Многие свойства систем переписывания связаны с нормальными формами.
Формально это можно выразить так: если ( A ,→) — абстрактная система переписывания , то x ∈ A находится в нормальной форме , если не существует y ∈ A такого, что x → y , т. е. x — неприводимый терм.
Объект a является слабо нормализующим, если существует хотя бы одна конкретная последовательность переписываний, начинающаяся с a , которая в конечном итоге приводит к нормальной форме. Система переписывания обладает свойством слабой нормализации или является (слабо) нормализующей (WN), если каждый объект является слабо нормализующим. Объект a является сильно нормализующим , если каждая последовательность переписываний, начинающаяся с a, в конечном итоге заканчивается нормальной формой. Абстрактная система переписывания является сильно нормализующей , завершающей , нётеровой или обладает свойством (сильной) нормализации (SN), если каждый из ее объектов является сильно нормализующим. [2]
Система переписывания имеет свойство нормальной формы (NF), если для всех объектов a и нормальных форм b , b может быть достигнута из a серией переписываний и обратных переписываний, только если a сводится к b . Система переписывания имеет свойство уникальной нормальной формы (UN), если для всех нормальных форм a , b ∈ S , a может быть достигнута из b серией переписываний и обратных переписываний, только если a равно b . Система переписывания имеет свойство уникальной нормальной формы относительно редукции (UN → ), если для каждого члена, сводящегося к нормальным формам a и b , a равно b . [3]
В этом разделе представлены некоторые известные результаты. Во-первых, SN подразумевает WN. [4]
Confluence (сокращенно 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 не имеют общего сведения.
WN и UN → подразумевают слияние. Следовательно, CR, NF, UN и UN → совпадают, если выполняется WN. [5]
Одним из примеров является то, что упрощение арифметических выражений дает число - в арифметике все числа являются нормальными формами. Примечательным фактом является то, что все арифметические выражения имеют уникальное значение, поэтому система переписывания является строго нормализующей и конфлюэнтной: [6]
Примерами ненормализующихся систем (не слабо и не сильно) являются счет до бесконечности (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]
