Lambda calculus with types (Perspectives in Logic)
Lambda calculus with types (Perspectives in Logic)
复制标题
具有类型的 Lambda 演算（逻辑视角）
DOI：
10.1112/blms/bdu053
复制
发表时间：
2014
影响因子：
0.9
通讯作者：
J. Hindley
中科院分区：
文献类型：
--
作者：
J. Hindley
Lambda演算是一种形式语言，结合了计算规则，由美国逻辑学家阿朗佐·丘奇（Alonzo Church）在1928年左右发明。它描述了函数行为的一些非常原始的特征，如今在计算机科学中作为高阶语言的基础，其中程序可以作用于或修改其他程序。丘奇把它设计成一个框架，在这个框架上建立所有逻辑的基础。（这是在Gödel的不完备性定理被完全理解之前！）他的大系统被证明是不一致的，但它的看似微不足道的λ核心却有它自己的兴趣：当自然数被适当地用λ语言编码后，所有被认为是可计算的函数都可以在λ微积分中定义。这使得丘奇在1935年解决了希尔伯特存在了30年的判定问题，通过证明没有算法可以决定一阶谓词逻辑的哪些公式是有效的。（图灵在一年后提出了这个问题的著名解决方案。）
Lambda calculus is a formal language, combined with computation rules, that was invented in about 1928 by an American logician, Alonzo Church. It describes some very primitive features of function behaviour, and nowadays serves in computer science as a basis for languages that are higher-order, in which programs may act on and modify other programs. Church devised it as a framework on which to build a foundation for all of logic.(This was before Gödel’s incompletability theorems were fully understood!) His grand system turned out inconsistent, but its apparently trivial λ-core was found to have interest of its own: after the natural numbers were suitably encoded in λ-language, all functions then regarded as computable could be defined in λ-calculus. This led Church in 1935 to solve Hilbert’s 30-year-old Entscheidungsproblem, by showing there is no algorithm that decides which formulas of first-order predicate logic are valid.(Turing’s well-known solution of this problem came a year later.)