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 $\lambda x.xxx$ . Ĝi havas la sekvan reverkregulon: Por iu termo t,

(\mathbf {\lambda } x.xxx)t\rightarrow ttt

Sed konsideru tion, kio okazas kiam ni aplikas $\lambda x.xxx$ al ĝi mem:

$(\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)$
	$\ldots \,$

Pro tio la termo $(\lambda x.xxx)(\lambda x.xxx)$ ne estas forte normiga.

Diversaj sistemoj de la tiphava lambda kalkulo, inkluzive la simple tiphavan lambdan kalkulon, la sistemon F de Jean-Yves Girard, kaj la 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ŭ