知识/定理
丘奇（1936）λ 演算：以函数抽象/应用定义可计算函数；丘奇-图灵论题——一切直觉可计算函数等价于图灵可计算。
公式
λ 演算：$\lambda x.e$ 抽象、$MN$ 应用；$\beta$-归约。
证明思路
（等价性）证明 λ 演算、图灵机、递归函数（哥德尔-埃尔布朗）三者计算能力相同。
应用/例子
函数式编程语言（Lisp、Haskell）、类型论、证明助手。
意义/影响
「可计算」的精确定义（论题而非定理）；函数式编程与程序语言的哲学源头。
DOXA · 数学编年史 · 知识详情
1936 ｜ 丘奇 ｜ 逻辑 ｜ 概念
丘奇（1936）λ 演算：以函数抽象/应用定义可计算函数；丘奇-图灵论题——一切直觉可计算函数等价于图灵可计算。
λ 演算：$\lambda x.e$ 抽象、$MN$ 应用；$\beta$-归约。
（等价性）证明 λ 演算、图灵机、递归函数（哥德尔-埃尔布朗）三者计算能力相同。
函数式编程语言（Lisp、Haskell）、类型论、证明助手。
「可计算」的精确定义（论题而非定理）；函数式编程与程序语言的哲学源头。