Теорема Чёрча — Россера

Теорема Чёрча — Россера — одна из основных теорем лямбда-исчисления, утверждающая что порядок применения правил редукции к термам не влияет на конечный результат.

Точнее, при наличии двух различных редукций или последовательностей редукций, которые могут быть применены к одному и тому же терму, всегда существует терм, достижимый из результатов обеих редукций применением (возможно, пустых) последовательностей дополнительных редукций. Теорема была доказана в 1936 году Алонзо Черчем и Россером, в честь которых она названа.

Стандартная формулировка

Диаграмма редукций

Теорема Чёрча — Россера. Если для некоторого λ-терма a имеется два варианта редукции a → b и a → c, то существует некоторый λ-терм d — такой, что b → d и c → d.

Примечание. Редукции не ограничиваются только β- и δ-редукциями.

Как следствие теоремы, терм в лямбда-исчислении имеет не более одной нормальной формы, что оправдывает ссылку на «нормальную форму» данного нормализуемого терма. Если некоторый λ-терм a имеет нормальные формы d и e, то они α-эквивалентны, то есть эквивалентны с точностью до обозначения связанных переменных. Другими словами, d и e находятся в одном классе эквивалентности.

Пример редукций

Литература

• Филд А., Харрисон П. Функциональное программирование = Functional Programming. — М.: Мир, 1993. — 637 с. — ISBN 5-03-001870-0.
• Душкин Р. В. 5.3. λ-исчисление как теоретическая основа ФП // Функциональное программирование на языке Haskell / Гл. ред. Д. А. Мовчан;. — М.: ДМК Пресс,, 2008. — С. 305—306. — 544 с., ил. с. — 1500 экз. — ISBN 5-94074-335-8.