A Church-Rosser-tétel a lambda-számítás egyik fő tétele , amely kimondja, hogy a redukciós szabályok kifejezésekre való alkalmazásának sorrendje nem befolyásolja a végeredményt.
Pontosabban, adott két különböző redukció vagy redukciós sorozat, amelyek ugyanarra a tagra vonatkoztathatók, mindig létezik egy kifejezés, amely mindkét csökkentés eredményéből elérhető további redukciók (esetleg üres) sorozatainak alkalmazásával. A tételt 1936 -ban bizonyította Alonzo Church és Rosser , akiről el is nevezték.
Church-Rosser tétel. Ha valamely a λ-tagra az a → b és a → c redukciónak két változata van, akkor létezik olyan d λ-tag, hogy b → d és c → d.
Jegyzet. A redukciók nem korlátozódnak a β- és δ-csökkentésekre.
A tétel következményeként a lambda-számításban egy tagnak legfeljebb egy normálalakja van, ami indokolja az adott normalizálható tag "normálformájára" való hivatkozást. Ha valamelyik a λ-tagnak d és e normálalakja van, akkor ezek α-ekvivalensek , azaz ekvivalensek a kötött változók jelöléséig. Más szavakkal, d és e ugyanabban az ekvivalencia osztályban vannak . [egy]