Теорема Чёрча — Россера — одна из основных теорем лямбда-исчисления, утверждающая что порядок применения правил редукции к термам не влияет на конечный результат.
Точнее, при наличии двух различных редукций или последовательностей редукций, которые могут быть применены к одному и тому же терму, всегда существует терм, достижимый из результатов обеих редукций применением (возможно, пустых) последовательностей дополнительных редукций. Теорема была доказана в 1936 годуАлонзо Черчем и Россером, в честь которых она названа.
Теорема Чёрча — Россера. Если для некоторого λ-терма a имеется два варианта редукции a → b и a → c, то существует некоторый λ-терм d — такой, что b → d и c → d.
Примечание. Редукции не ограничиваются только β- и δ-редукциями.
Как следствие теоремы, терм в лямбда-исчислении имеет не более одной нормальной формы, что оправдывает ссылку на «нормальную форму» данного нормализуемого терма. Если некоторый λ-терм a имеет нормальные формы d и e, то они α-эквивалентны, то есть эквивалентны с точностью до обозначения связанных переменных. Другими словами, d и e находятся в одном классе эквивалентности.Шаблон:Sfn
