Корисник:Огњензивановиц/превод2

У апстрактном преписивању,^[1] објекат је у нормалном облику ако се не може даље писати, односно несводив је. У зависности од система преписивања, објекат може преписати у неколико нормалних облика или уопште ниједну. Многа својства система преписивања односе се на нормалне форме.

Дефиниције

Формално речено, ако је (A,→) систем апстрактног преписивања, x∈A је у нормалном облику ако не постоји y∈A тако да је x→y тј. x је несводљив термин.

Објекат а је слабо нормализован ако постоји бар један одређени низ преписа који почиње од а који на крају даје нормалан облик. Систем за поновно писање има својство слабе нормализације или (слабо) нормализује (WN) ако је сваки објекат слабо нормализован. Објекат а се снажно нормализује ако се сваки низ преписа који почиње од а на крају завршава нормалним обликом. Систем апстрактног поновног писања је снажно нормализован, завршавајући, нетеровски или има (јако) својство нормализације (SN), ако је сваки од његових објеката снажно нормализован.^[2]

Систем поновног писања има својство нормалног облика (NF) ако се за све објекте а и нормалне форме б, б може доћи из а низом поновних писања и инверзних преписа само ако се а своди на б. Систем поновног писања има јединствено својство нормалног облика (UN) ако за све нормалне облике а, b ∈ S, а може да се достигне из б низом преписивања и инверзних преписивања само ако је а једнако б. Систем преписивања има јединствено својство нормалног облика у односу на редукцију (UN^→) ако је за сваки термин који се своди на нормалне облике а и б, а једнако б.^[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 немају заједнички редукт.

WN и UN^→ имплицирају конфлуенцију. Отуда се CR, NF, UN, и UN^→ поклапају ако важи WN.

Примери

Један пример је да поједностављивање аритметичких израза производи број – у аритметици, сви бројеви су нормални облици. Изванредна чињеница је да сви аритметички изрази имају јединствену вредност, тако да је систем поновног писања снажно нормализован и конфлуентан:^[5]

(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 ⇒ ..., отворен је проблем да ли постоје још неке петље Колацове трансформације). Још један пример је систем са једним правилом { r(x,y) → r(y,x) }, који нема нормализујућа својства пошто из било ког појма, нпр. r(4,2) почиње једна секвенца поновног писања, тј. r(4,2) → r(2,4) → r(4,2) → r(2,4) → ..., која је бесконачно дуга. Ово доводи до идеје да се препише "модуло комутативности" где је термин у нормалном облику ако се не примењују никаква правила осим комутативности. ^[6]

Слабо, али не и снажно нормализујући систем преписивања^[7]

Систем {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)$ није снажно нормализован. И ово је једини редослед редукције, стога није ни слабо нормализован.

Типски ламбда рачун

Различити системи типског ламбда рачуна укључујући једноставно откуцани ламбда рачун, Систем Ф Жан-Ива Жирара и рачун конструкција Тијерија Кокванда снажно се нормализују.

Систем ламбда рачуна са својством нормализације може се посматрати као програмски језик са својством да сваки програм завршава. Иако је ово веома корисно својство, оно има недостатак: програмски језик са својством нормализације не може бити Тјуринг потпун, иначе би се халтинг проблем могао решити тако што ћемо видети да ли програм проверава типове. То значи да постоје израчунљиве функције које се не могу дефинисати у једноставном типском ламбда рачуну, и слично за рачун конструкција, и Систем Ф. Типичан пример је само-тумач у тоталном програмском језику.

Референце

↑ Franz Baader; Tobias Nipkow (1998). Term Rewriting and All That. Cambridge University Press. ISBN 9780521779203.
↑ Ohlebusch, Enno (1998). „Church-Rosser theorems for abstract reduction modulo an equivalence relation“. Rewriting Techniques and Applications. Lecture Notes in Computer Science. 1379. стр. 18. Грешка: Bad DOI specified. ISBN 978-3-540-64301-2.
↑ ^3,0 ^3,1 Шаблон:Cite journal
↑ „logic - What is the difference between strong normalization and weak normalization in the context of rewrite systems?“.
↑ Terese (2003). Term rewriting systems. Cambridge, UK: Cambridge University Press. стр. 1. ISBN 0-521-39115-6.
↑ Dershowitz, Nachum; Jouannaud, Jean-Pierre (1990). „6. Rewrite Systems“. In Jan van Leeuwen. Handbook of Theoretical Computer Science. B. Elsevier. стр. 9–10. ISBN 0-444-88074-7.
↑ N. Dershowitz and J.-P. Jouannaud (1990). „Rewrite Systems“. In Jan van Leeuwen. Formal Models and Semantics. Handbook of Theoretical Computer Science. B. Elsevier. стр. 268. ISBN 0-444-88074-7.

[1] Franz Baader; Tobias Nipkow (1998). Term Rewriting and All That. Cambridge University Press. ISBN 9780521779203.

[2] Ohlebusch, Enno (1998). „Church-Rosser theorems for abstract reduction modulo an equivalence relation“. Rewriting Techniques and Applications. Lecture Notes in Computer Science. 1379. стр. 18. Грешка: Bad DOI specified. ISBN 978-3-540-64301-2.

[NF-3] 3,0 ^3,1 Шаблон:Cite journal

[4] „logic - What is the difference between strong normalization and weak normalization in the context of rewrite systems?“.

[5] Terese (2003). Term rewriting systems. Cambridge, UK: Cambridge University Press. стр. 1. ISBN 0-521-39115-6.

[6] Dershowitz, Nachum; Jouannaud, Jean-Pierre (1990). „6. Rewrite Systems“. In Jan van Leeuwen. Handbook of Theoretical Computer Science. B. Elsevier. стр. 9–10. ISBN 0-444-88074-7.

[Dershowitz.Jouannaud.1990.Fig2-7] N. Dershowitz and J.-P. Jouannaud (1990). „Rewrite Systems“. In Jan van Leeuwen. Formal Models and Semantics. Handbook of Theoretical Computer Science. B. Elsevier. стр. 268. ISBN 0-444-88074-7.

[1]

[2]

[3]

[4]

[5]

[6]

[7]