Vikipedio:Projekto matematiko/Normaliga propraĵo (lambda-kalkulo)

El Vikipedio

Ĉi tiu artikolo montras stilajn aŭ/kaj gramatikajn aŭ/kaj strukturajn problemojn kaj bezonas poluradon por konformi al pli bona nivelo de kvalito. Post plibonigo movu la artikolon al
Normiga eco (lambda-kalkulo)
(eble la nomo mem bezonas korekton) Se la ligo estas ruĝa, vi povas movi la artikolon. Se la ligo estas blua, la alia artikolo pri la temo jam ekzistas kaj tiun kaj ĉi tiun artikolon necasas kunigi.

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 eble finiĝas je termo en norma formo.

La pura tiphava lambda kalkulo ne estas forte normiga. Konsideru la termon $λ x . x x x$ . Ĝi havas la sekvan reverkregulon: Por iu termo t,

$(\mathbf{\lambda} x . x x x) t \rightarrow t t t$

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

$(\mathbf{\lambda} x . x x x) (\lambda x . x x x)$	$\rightarrow (\mathbf{\lambda} x . x x x) (\lambda x . x x x) (\lambda x . x x x)$
	$\rightarrow (\mathbf{\lambda} x . x x x) (\lambda x . x x x) (\lambda x . x x x) (\lambda x . x x x)$
	$\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)$
	$\ldots\,$

Pro tio la termo $(λ x . x x x)(λ x . x x x)$ 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.