Church-Rosser-satsen är en av huvudsatserna i lambdakalkylen , som säger att ordningen i vilken reduktionsreglerna tillämpas på termer inte påverkar det slutliga resultatet.
Mer exakt, givet två olika reduktioner eller sekvenser av reduktioner som kan tillämpas på samma term, finns det alltid en term som kan nås från resultaten av båda reduktionerna genom att tillämpa (eventuellt tomma) sekvenser av ytterligare reduktioner. Teoremet bevisades 1936 av Alonzo Church och Rosser , efter vilken den är uppkallad.
Church-Rosser sats. Om det för någon λ-term a finns två versioner av reduktion a → b och a → c, så finns det någon λ-term d så att b → d och c → d.
Notera. Reduktioner är inte begränsade till p- och 5-reduktioner.
Som en följd av satsen har en term i lambdakalkylen högst en normalform, vilket motiverar att man refererar till "normalformen" av en given normaliserbar term. Om någon λ-term a har normala former d och e, så är de α-ekvivalenta , det vill säga ekvivalenta upp till notationen av bundna variabler. Med andra ord är d och e i samma ekvivalensklass . [ett]