Λ演算查看源代码讨论查看历史
| Λ演算 |
λ演算（英语：lambda calculus，λ-calculus）是一套从数学逻辑中发展，以变量绑定和替换的规则，来研究函数如何抽象化定义、函数如何被应用以及递归的形式系统。它由数学家阿隆佐·邱奇在20世纪30年代首次发表。lambda演算作为一种广泛用途的计算模型，可以清晰地定义什么是一个可计算函数，而任何可计算函数都能以这种形式表达和求值，它能模拟单一磁带图灵机的计算过程；尽管如此，lambda演算强调的是变换规则的运用，而非实现它们的具体机器。
简介
λ演算（英语：lambda calculus，λ-calculus）是一套从数学逻辑中发展，以变量绑定和替换的规则，来研究函数如何抽象化定义、函数如何被应用以及递归的形式系统。它由数学家阿隆佐·邱奇在20世纪30年代首次发表。lambda演算作为一种广泛用途的计算模型，可以清晰地定义什么是一个可计算函数，而任何可计算函数都能以这种形式表达和求值，它能模拟单一磁带图灵机的计算过程；尽管如此，lambda演算强调的是变换规则的运用，而非实现它们的具体机器。lambda演算可比拟是最根本的编程语言，它包括了一条变换规则（变量替换）和一条将函数抽象化定义的方式。因此普遍公认是一种更接近软件而非硬件的方式。对函数式编程语言造成很大影响，比如Lisp、ML语言和Haskell语言。在1936年邱奇利用λ演算给出了对于判定性问题（Entscheidungsproblem）的否定：关于两个lambda表达式是否等价的命题，无法由一个“通用的算法”判断，这是不可判定性能够证明的头一个问题，甚至还在停机问题之先。
评价
头两条规则用来生成函数，而第三条描述了函数是如何作用在参数上的。通常，lambda抽象（规则2）和函数作用（规则3）中的括弧在不会产生歧义的情况下可以省略。如下假定保证了不会产生歧义：（1）函数的作用是左结合的，和（2）lambda操作符被绑定到它后面的整个表达式。例如，表达式 (λx.x x)(λy.y) 可以简写成λ(x.x x) λy.y 。类似λx.(x y)这样的lambda表达式并未定义一个函数，因为变量y的出现是自由的，即它并没有被绑定到表达式中的任何一个λ上。一个lambda表达式的自由变量的集合是通过下述规则（基于lambda表达式的结构归纳地）定义的：在表达式V中，V是变量，则这个表达式里自由变量的集合只有V。在表达式λV .E中（V是变量，E是另一个表达式），自由变量的集合是E中自由变量的集合减去变量V。因而，E中那些V被称为绑定在λ上。在表达式 (E E')中，自由变量的集合是E和E'中自由变量集合的并集。例，对于表达式λx.x（我们将第一个x视作变量，第二个x视作表达式），其中表达式x中，由1，它的自由变量集合是x，又由2，表达式λx.x的自由变量的集合是表达式x的自由变量集合减去变量x。所以对于表达式λx.x，它的自由变量集合是空。例，对于表达式λx.x x由形式化描述的第3点，我们把它看作((λx.x)(x))，(λx.x)和(x)分别为表达式，由上一例知道(λx.x)的自由变量集合为空，表达式(x)的变量集合为变量x，所以对于λx.x x，它的自由变量集合为x与空的并，即x。在lambda表达式的集合上定义了一个等价关系(在此用==标注)，“两个表达式其实表示的是同一个函数”这样的直觉性判断即由此表述，这种等价关系是通过所谓的“alpha-变换规则”和“beta-归约规则”。。[1]