Church-Rosserov teorem

Izvor: Wikipedija
Skoči na: orijentacija, traži

Church-Rosserov teorem kaže da ako postoje dvije različite redukcije koje počinju od istog termina u lambda računu, tada postoji termin koji je dohvatljiv (moguće praznim) slijedom redukcija iz oba redukta. Kao posljedica, termin u lambda računu ima najviše jednan normalni oblik. Stoga Church-Rosserov teorem opravdava referiranje na "normalni oblik" određenog termina. Teorem su prvi dokazali 1936. Alonzo Church i J. Barkley Rosser.

Church-Rosserov teorem također vrijedi za mnoge varijante lambda računa, kao što je jednostavno tipizirani lambda račun, mnogi računi sa naprednijim sustavima tipova, te račun beta-vrijednosti Gordona Plotkina. Plotkin je također rabio Church-Rosserov teorem za dokaz da je evaluacija funkcijskih prorama (i za lijenu evaluaciju i za striktnu evaluaciju) funkcija iz programa u vrijednosti (podskup lambda termina). 1980-ih je Church-Rosserov teorem etabliran za proširenje lambda računa svojstvima iz imperativnih programskih jezika.

Vidi još[uredi VE | uredi]

Izvori[uredi VE | uredi]

Alonzo Church i J. Barkley Rosser. Some properties of conversion. Transactions of the American Mathematical Society, vol. 39, No. 3. (May 1936), pp. 472-482.


Computer-aj aj ashton 01.svg Nedovršeni članak Church-Rosserov teorem koji govori o računarstvu treba dopuniti. Dopunite ga prema pravilima Wikipedije.