Church-Rosserov teorem: razlika između inačica
Bot: Automatski unos stranica |
m bnz |
||
| Redak 1: | Redak 1: | ||
'''Church-Rosserov teorem''' kaže da ako postoje dvije različite redukcije koje počinju od istog termina u [[lambda račun]]u, tada postoji termin koji je dohvatljiv (moguće praznim) slijedom redukcija iz oba redukta. Kao posljedica, termin u [[lambda račun]]u ima najviše jednan [[beta normalni oblik|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 [[Gordon Plotkin|Gordona Plotkina]]. Plotkin je također rabio Church-Rosserov teorem za dokaz da je evaluacija funkcijskih prorama (i za [[lijena evaluacija|lijenu evaluaciju]] i za [[striktna evaluacija|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 [[imperativno programiranje|imperativnih programskih jezika]]. | 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 [[Gordon Plotkin|Gordona Plotkina]]. Plotkin je također rabio Church-Rosserov teorem za dokaz da je evaluacija funkcijskih prorama (i za [[lijena evaluacija|lijenu evaluaciju]] i za [[striktna evaluacija|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 [[imperativno programiranje|imperativnih programskih jezika]]. | ||
Posljednja izmjena od 8. svibanj 2022. u 15:45
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š
Izvori
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.
Pogreška pri izradbi sličice:
Nedovršeni članak Church-Rosserov teorem koji govori o računarstvu treba dopuniti. Dopunite ga prema pravilima uređivanja Hrvatske internetske enciklopedije.
