[摘录] 图灵机与lambda演算的关系

在阅读函数式编程相关资料时，看到如下一段话。感觉说的很好，可以帮助我这种学渣一点点的建立起整个知识体系。

以下片段，摘抄自豆瓣网友 赛义甫 的豆列 “逻辑与计算” 中的一段介绍。

莱布尼兹曾经有两个梦想： 
1. 创建一种“普遍语言”（universal language）使得任何问题都可以用这种语言表述； 
2. 找到一种"判定方法"（decision method）以解决所有可以在“普遍语言”中所表述的问题。 
这两个问题是上百年来数理逻辑、数学哲学和数学基础问题的核心、实质。对前一个问题的回答就是自弗雷格、罗素开始，经公理集合论运动的最终结果：
以一阶谓词逻辑为语言所形式化阐述的集合论，现在已经成为数学的普遍语言，现代逻辑学、特别是将符号逻辑应用于数学领域所产生的数理逻辑，
其最重要的目标就是为整个数学提供一个严格精确的语言。这是我们在学习数理逻辑时应当把握的方向。 
而第二个问题则是现代哲学和计算机科学最关注的问题之一：是否可以解决用这个“普遍语言”所形式化描述的所有问题？
这个问题就是所谓“可判定性问题”（Entscheidungsproblem，decision problem）。对这个问题的研究最终导致了理论计算机科学的诞生：
阿隆佐·丘奇和阿兰·图灵分别以各自的方式对这个问题做出了否定的回答。他们在研究这个问题时首先对“可判定的”（decidable）这个直觉概念进行了深入研究并给出了形式化定义和解释，
进一步把这个问题归结成“可计算的”（computable）问题，并最终将其定义为“可计算函数”（computable function）问题的研究。为此，丘奇和图灵分别提出了关于可计算函数的模型。
图灵的模型就是著名的图灵机，它已经成为现代计算机科学的理论基础；而丘奇的模型则是lambda演算，这成为后来计算机语言Lisp和现代函数式程序语言的理论基础。
其后图灵证明了这两个模型其实定义了同一类别的可计算函数。
可以说，丘奇和图灵对数理逻辑的研究是从传统的解决数学基础问题出发开创了一个崭新的领域：计算科学。 

赛义甫的个人主页：http://id.sciencenet.cn/index.php?s=/Index/index/user/saif