阿隆佐·丘奇

生平

阿隆佐·丘奇(Alonzo Church,1903-1995)是美国数学家、逻辑学家,长期任教于普林斯顿大学,晚年转至加州大学洛杉矶分校。他是可计算性理论的奠基人之一,指导过包括 Alan Turing、Stephen Kleene、John Barkley Rosser 在内的多位重要学者。

主要贡献

丘奇在 20 世纪 30 年代创立 λ 演算,以纯函数抽象刻画计算;1936 年他证明一阶逻辑的判定问题不可解(丘奇定理),与图灵同年独立解决了希尔伯特的判定问题。"任何可有效计算的函数都可用 λ 演算(或等价的图灵机)表达"这一论断后来被称为丘奇-图灵论题。

影响

λ 演算成为函数式编程语言的直接理论来源,Lisp、ML、Haskell 均建立在其之上;丘奇编码、简单类型 λ 演算等工作也深刻影响了类型理论与程序语言语义研究。他长期主编《Journal of Symbolic Logic》,对数理逻辑学科建设贡献卓著。