Church-Rosserův teorém je jedním z hlavních teorémů lambda počtu , který říká, že pořadí, ve kterém jsou redukční pravidla aplikována na členy , neovlivňuje konečný výsledek.
Přesněji řečeno, vzhledem ke dvěma různým redukcím nebo sekvencím redukcí, které lze aplikovat na stejný člen, vždy existuje člen dosažitelný z výsledků obou redukcí aplikací (případně prázdných) sekvencí dalších redukcí. Tato věta byla prokázána v roce 1936 Alonzem Churchem a Rosserem , po kterém je pojmenována.
Churchova-Rosserova věta. Jestliže pro nějaký λ-člen a existují dvě verze redukce a → b a a → c, pak existuje nějaký λ-člen d takový, že b → d a c → d.
Poznámka. Redukce nejsou omezeny na β- a δ-redukce.
Důsledkem věty je, že termín v počtu lambda má nanejvýš jednu normální formu, která ospravedlňuje odkazování na „normální formu“ daného normalizovatelného termínu. Jestliže nějaký λ-člen a má normální tvary d a e, pak jsou α-ekvivalentní , tedy ekvivalentní až do zápisu vázaných proměnných. Jinými slovy, d a e jsou ve stejné třídě ekvivalence . [jeden]