Church-Rosserov teorem
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 s 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
Izvori 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.
