WikiSysop: bnz

2022-05-08T15:45:42Z

bnz

←Starija inačica		Inačica od 8. svibanj 2022. u 15:45
Redak 1:		Redak 1:
	~~<!--'''Church-Rosserov teorem'''-->~~'''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''' 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]].

WikiSysop: Bot: Automatski unos stranica

2021-08-23T03:03:39Z

Bot: Automatski unos stranica

Nova stranica

'''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]].

== Vidi još ==

*[[Konfluencija (prepisivanje termina)]]

== Izvori ==
Alonzo Church i J. Barkley Rosser. [http://links.jstor.org/sici?sici=0002-9947%28193605%2939%3A3%3C472%3ASPOC%3E2.0.CO%3B2-Q Some properties of conversion]. Transactions of the American Mathematical Society, vol. 39, No. 3. (May 1936), pp. 472-482.

{{Mrva-rač}}
[[Kategorija:Lambda račun]]

Church-Rosserov teorem - Povijest promjena

WikiSysop: bnz

WikiSysop: Bot: Automatski unos stranica