Vidi fonton por Normaliga propraĵo (lambda-kalkulo)

En [[matematika logiko]] kaj teoria komputiko, reverka sistemo havas la '''normigan econ''' se ĉiu termo estas ''forte normiga''; tio estas, se ĉiu vico de reverkoj finiĝas je termo en [[norma formo]].

La ''pura'' maltiphava [[lambda kalkulo]] ne estas forte normiga. Konsideru la termon <math>\lambda x . x x x</math>. Ĝi havas la sekvan reverkregulon: Por iu termo ''t'',

: <math>(\mathbf{\lambda} x . x x x) t \rightarrow t t t</math>

Sed konsideru tion, kio okazas kiam ni aplikas <math>\lambda x . x x x</math> al ĝi mem:
{|
| <math>(\mathbf{\lambda} x . x x x) (\lambda x . x x x)</math>
| <math> \rightarrow (\mathbf{\lambda} x . x x x) (\lambda x . x x x) (\lambda x . x x x)</math>
|-
|
| <math> \rightarrow (\mathbf{\lambda} x . x x x) (\lambda x . x x x) (\lambda x . x x x) (\lambda x . x x x)</math>
|-
|
| <math> \rightarrow (\mathbf{\lambda} x . x x x) (\lambda x . x x x) (\lambda x . x x x) (\lambda x . x x x) (\lambda x . x x x)</math>
|-
|
| <math>\ldots\,</math>
|}

Pro tio la termo <math>(\lambda x . x x x) (\lambda x . x x x)</math> ne estas forte normiga.

Diversaj sistemoj de la '''tiphava lambda kalkulo''', inkluzive la [[tiphava lambda kalkulo|simple tiphavan lambdan kalkulon]], la [[sistemo F|sistemon F]] de Jean-Yves Girard, kaj la [[kalkulo de konstruoj|kalkulon de konstruoj]] de Thierry Coquand, havas la '''normaligan econ'''.

Lambda kalkula sistemo kun la '''normiga eco''' povas esti vidata kiel programlingvo kun la eco, ke ĉiu programo finiĝas. Kvankam ĉi tio estas tre utila eco, ĝi havas malavantaĝon: programlingvo kun la normiga eco ne povas esti kompleta laŭ Turing. Tio signifas, ke ekzistas komputeblaj funkcioj, kiuj ne povas esti difinitaj en la simple tiphava lambda kalkulo (kaj simile ekzistas komputeblaj funkcioj, kiuj ne povas esti difinitaj aŭ en la kalkulo de konstruoj aŭ en la sistemo F).  Ekzemple, ne eblas difini la normigajn algoritmojn de iuj de la supre citataj kalkuloj en tiu sama kalkulo.

== Vidu ankaŭ ==

* [[Lambda kalkulo]]
* [[Tiphava lambda kalkulo]]
* [[Reverkado]]
* [[Kalkulo de konstruoj]]

[[Kategorio:Lambda-kalkulo]]
[[Kategorio:Logiko en komputiko]]