λ演算
(lambda calculus
)是一套用于研究函数
定义、函数应用和递归
的形式系统
。它由阿隆佐·邱奇
和他的学生斯蒂芬·科尔·克莱尼
在20世纪
30年代
引入。邱奇运用λ演算在1936年
给出判定性问题
(Entscheidungsproblem)的一个否定的答案。这种演算可以用来清晰地定义什么是一个可计算函数
。关于两个lambda演算表达式是否等价的命题无法通过一个“通用的算法”来解决,这是不可判定性能够证明的头一个问题,甚至还在停机问题
之先。Lambda演算对函数式编程语言
有巨大的影响,比如Lisp语言
、ML语言
和Haskell语言
。
Lambda演算可以被称为最小的通用程序设计语言。它包括一条变换规则(变量替换)和一条函数定义方式,Lambda演算之通用在于,任何一个可计算函数都能用这种形式来表达和求值。因而,它是等价于图灵机
的。尽管如此,Lambda演算强调的是变换规则的运用,而非实现它们的具体机器。可以认为这是一种更接近软件而非硬件的方式。
本文讨论的是邱奇的“无类型lambda演算”,此后,已经研究出来了一些有类型lambda演算
。
[编辑
]
历史
最开始,邱奇试图创制一套完整的形式系统作为数学的基础,当他发现这个系统易受罗素悖论
的影响时,就把lambda演算单独分离出来,用于研究可计算性
,最终导致了他对判定性问题
的否定回答。
[编辑
]
非形式化的描述
在lambda演算中,每个表达式都代表一个只有单独参数的函数,这个函数的参数本身也是一个只有单一参数的函数,同时,函数的值是又一个只有单一
参数的函数。函数是通过lambda表达式匿名地定义的,这个表达式说明了此函数将对其参数进行什么操作。例如,“加2”函数f(x)= x +
2可以用lambda演算表示为λx.x + 2 (或者λy.y + 2,参数的取名无关紧要)而f(3)的值可以写作(λx.x + 2)
3。函数的应用(application)是左结合
的:f x y =(f x) y。考虑这么一个函数:它把一个函数作为参数,这个函数将被作用在3上:λf.f 3。如果把这个(用函数作参数的)函数作用于我们先前的“加2”函数上:(λf.f 3)(λx.x+2),则明显地,下述三个表达式:
(λf.f 3)(λx.x+2)与 (λx.x + 2) 3与3 + 2
是等价的。有两个参数的函数可以通过lambda演算这么表达:一个单一参数的函数的返回值又是一个单一参数函数的参数(参见Currying
)。例如,函数f(x, y) = x - y可以写作λx.λy.x - y。下述三个表达式:
(λx.λy.x - y) 7 2与 (λy.7 - y) 2与7 - 2
也是等价的。然而这种lambda表达式之间的等价性无法找到一个通用的函数来判定。
并非所有的lambda表达式都可以规约至上述那样的确定值,考虑
(λx.x x)(λx.x x)
或
(λx.x x x)(λx.x x x)
然后试图把第一个函数作用在它的参数上。 (λx.x x)被称为ω 组合子
,((λx.x x)(λx.x x))被称为Ω,而((λx.x x x) (λx.x x x))被称为Ω2
,以此类推。
若仅形式化函数作用的概念而不允许lambda表达式,就得到了组合子逻辑
。
[编辑
]
形式化定义
形式化地,我们从一个标识符(identifier)的可数无穷
集合
开始,比如{a, b, c, ..., x, y, z, x1
, x2
, ...},则所有的lambda表达式可以通过下述以BNF
范式表达的上下文无关文法
描述:
- <expr> ::= <identifier>
- <expr> ::=(λ<identifier> .<expr>)
- <expr> ::=(<expr> <expr>)
头两条规则用来生成函数,而第三条描述了函数是如何作用在参数上的。通常,lambda抽象(规则2)和函数作用(规则3)中的括号在不会产生歧义
的情况下可以省略。如下假定保证了不会产生歧义:(1)函数的作用是左结合的,和(2)lambda操作符被绑定到它后面的整个表达式。例如,表达式
(λx.x x)(λy.y) 可以简写成λ(x.x x) λy.y 。
类似λx.(x y)这样的lambda表达式并未定义一个函数,因为变量y的出现是自由的
,即它并没有被绑定到表达式中的任何一个λ上。变量出现次数的绑定是通过下述规则(基于lambda表达式的结构归纳
地)定义的:
- 在表达式V中,V是变量,则这个表达式里变量V只有一次自由出现。
- 在表达式λV .E中(V是变量,E是另一个表达式),变量自由出现的次数是E中变量自由出现的次数,减去E中V自由出现的次数。因而,E中那些V被称为绑定在λ上。
- 在表达式 (E E')中,变量自由出现的次数是E和E'中变量自由出现次数之和。
在lambda表达式的集合上定义了一个等价关系
(在此用==标注),“两个表达式其实表示的是同一个函数”这样的直觉性判断即由此表述,这种等价关系是通过所谓的“alpha-变换规则”和“beta-归约规则”。
[编辑
]
归约
[编辑
]
α-变换
Alpha-变换规则表达的是,被绑定变量的名称是不重要的。比如说λx.x和λy.y是同一个函数。尽管如此,这条规则并非像它看起来这么简单,关于被绑定的变量能否由另一个替换有一系列的限制。
Alpha-变换规则陈述的是,若V与W均为变量,E是一个lambda表达式,同时E[V:=W]是指把表达式E中的所有的V的自由出现都替换为W,那么在W不是 E中的一个自由出现,且如果W替换了V,W不会被E中的λ绑定的情况下,有
λV.E == λW.E[V:=W]
这条规则告诉我们,例如λx.(λx.x) x这样的表达式和λy.(λx.x) y是一样的。
[编辑
]
β-归约
Beta-归约规则表达的是函数作用的概念。它陈述了若所有的E'的自由出现在E [V:=E']中仍然是自由的情况下,有
((λV.E) E') == E [V:=E']
成立。
==关系被定义为满足上述两条规则的最小等价关系(即在这个等价关系中减去任何一个映射,它将不再是一个等价关系)。
对上述等价关系的一个更具操作性的定义可以这样获得:只允许从左至右来应用规则。不允许任何beta归约的lambda表达式被称为Beta范式
。
并非所有的lambda表达式都存在与之等价的范式,若存在,则对于相同的形式参数命名而言是唯一的。此外,有一个算法用户计算范式,不断地把最左边的形
式参数替换为实际参数,直到无法再作任何可能的规约为止。这个算法当且仅当lambda表达式存在一个范式时才会停止。Church-Rosser定理
说明了,当且仅当两个表达式等价时,它们会在形式参数换名后得到同一个范式。
[编辑
]
η-变换
前两条规则之后,还可以加入第三条规则,eta-变换,来形成一个新的等价关系。Eta-变换表达的是外延性
的概念,在这里外延性指的是,两个函数对于所有的参数得到的结果都一致,当且仅当它们是同一个函数。Eta-变换可以令λx .f x和f相互转换,只要x不是f中的自由出现。下面说明了为何这条规则和外延性是等价的:
若f与g外延地等价,即,f a == g a对所有的lambda表达式a成立,则当取a为在f中不是自由出现的变量x时,我们有f x == g
x,因此λx .f x == λx .g x,由eta-变换f == g。所以只要eta-变换是有效的,会得到外延性也是有效的。
相反地,若外延性是有效的,则由beta-归约,对所有的y有(λx .f x) y == f y,可得λx .f x == f,即eta-变换也是有效的。
[编辑
]
lambda演算中的算术
在lambda演算中有许多方式都可以定义自然数
,但最常见的还是邱奇数
,下面是它们的定义:
0 = λf.λx.x
1 = λf.λx.f x
2 = λf.λx.f (f x)
3 = λf.λx.f (f (f x))以此类推。直观地说,lambda演算中的数字n就是一个把函数f作为参数并以f的n次幂为返回值的函数。换句话说,邱奇整数是一个高阶函数
-- 以单一参数函数f为参数,返回另一个单一参数的函数。
(注意在邱奇原来的lambda演算中,lambda表达式的形式参数在函数体中至少出现一次,这使得我们无法像上面那样定义0)在邱奇整数定义的基础上,我们可以定义一个后继函数,它以n为参数,返回n + 1:
SUCC = λn.λf.λx.f(n f x)
加法是这样定义的:
PLUS = λm.λn.λf.λx.m f (n f x)
PLUS可以被看作以两个自然数为参数的函数,它返回的也是一个自然数。你可以试试验证
PLUS 2 3 与 5
是否等价。乘法可以这样定义:
MULT = λm.λn.m(PLUS n)0,
即m乘以n等于在零的基础上n次加m。另一种方式是
MULT = λm.λn.λf.m(n f)
正整数n的前驱元(predecessesor)PRED n = n - 1要复杂一些:
PRED = λn.λf.λx.n(λg.λh.h(g f))(λu.x)(λu.u)
或者
PRED = λn.n(λg.λk.(g 1)(λu.PLUS(g k) 1) k)(λl.0) 0
注意(g 1)(λu.PLUS(g k) 1) k表示的是,当g(1)是零时,表达式的值是k,否则是g(k)+ 1。
[编辑
]
逻辑与谓词
习惯上,下述两个定义(称为邱奇布尔值)被用作TRUE
和FALSE
这样的布尔值:
TRUE := λx y.x
FALSE := λx y.y
(注意FALSE
等价于前面定义邱奇数零)
接着,通过这两个λ-项,我们可以定义一些逻辑运算:
AND := λp q.p q FALSE
OR := λp q.p TRUE q
NOT := λp.p FALSE TRUE
IFTHENELSE := λp x y.p x y
我们现在可以计算一些逻辑函数,比如:
AND TRUE FALSE
≡(λp q.p q FALSE) TRUE FALSE →β
TRUE FALSE FALSE
≡(λx y.x) FALSE FALSE →β
FALSE
我们见到AND TRUE FALSE
等价于FALSE
。
“谓词”是指返回布尔值的函数。最基本的一个谓词是ISZERO
,当且仅当其参数为零时返回真,否则返回假:
ISZERO := λn.n(λx.FALSE) TRUE
运用谓词与上述TRUE
和FALSE
的定义,使得"if-then-else"这类语句很容易用lambda演算写出。
[编辑
]
有序对
有序对(2-元组)数据类型可以用TRUE
、FALSE
和IF
来定义。
CONS := λx y.λp.IF p x y
CAR := λx.x TRUE
CDR := λx.x FALSE
链表数据类型可以定义为,要么是为空列表保留的值(e.g.FALSE
),要么是CONS
一个元素和一个更小的列表。
[编辑
]
递归
递归
是使用函数自身的函数定义;在表面上,lambda演算不允许这样。但是这种印象是误解。考虑个例子,阶乘
函数f(n)
递归的定义为
f(n):= if n = 0 then 1 else n·f(n-1)
。
在lambda演算中,你不能定义包含自身的函数。要避免这样,你可以开始于定义一个函数,这里叫g
,它接受一个函数f
作为参数并返回接受n
作为参数的另一个函数:
g := λf n.(if n = 0 then 1 else n·f(n-1))
。
函数g
返回要么常量1
,要么函数f
对n-1
的n次应用。使用ISZERO
谓词,和上面描述的布尔和代数定义,函数g
可以用lambda演算来定义。
但是,g
自身仍然不是递归的;为了使用g
来建立递归函数,作为参数传递给g
的f
函数必须有特殊的性质。也就是说,作为参数传递的f
函数必须展开为调用带有一个参数的函数g
-- 并且这个参数必须再次f
函数!
换句话说,f
必须展开为g(f)
。这个到g
的调用将接着展开为上面的阶乘函数并计算下至另一层递归。在这个展开中函数f
将再次出现,并将被再次展开为g(f)
并继续递归。这种函数,这里的f = g(f)
,叫做g
的不动点,并且它可以在lambda演算中使用叫做悖论算子
或不动点算子
来实现,它被表示为Y
-- Y组合子
:
Y = λg.(λx.g(x x))(λx.g(x x))
在lambda演算中,Y g
是g
的不动点,因为它展开为g(Y g)
。现在,要完成我们对阶乘函数的递归调用,我们可以简单的调用 g(Y g)n
,这里的n是我们要计算它的阶乘的数。
比如假定n = 5,它展开为:
(λn.(if n = 0 then 1 else n·((Y g)(n-1)))) 5
if 5 = 0 then 1 else 5·(g(Y g,5-1))
5·(g(Y g)4)
5·(λn.(if n = 0 then 1 else n·((Y g)(n-1))) 4)
5·(if 4 = 0 then 1 else 4·(g(Y g,4-1)))
5·(4·(g(Y g)3))
5·(4·(λn.(if n = 0 then 1 else n·((Y g)(n-1))) 3))
5·(4·(if 3 = 0 then 1 else 3·(g(Y g,3-1))))
5·(4·(3·(g(Y g)2)))
...
等等,递归的求值算法的结构。所有递归定义的函数都可以看作某个其他适当的函数的不动点,因此,使用Y
所有递归定义的函数都可以表达为lambda表达式。特别是,我们现在可以明晰的递归定义自然数的减法、乘法和比较谓词。
[编辑
]
可计算函数和lambda演算
自然数
的函数F: N
→ N
是可计算函数
,当且仅当
存在着一个lambda表达式f
,使得对于N
中的每对x, y都有F(
x)
= y当且仅当f x == y
,这里的x
和y
分别是对应于x和y的邱奇数
。这是定义可计算性的多种方式之一;关于其他方式很它们的等价者的讨论请参见邱奇-图灵论题
。
[编辑
]
参见
[编辑
]
外部链接
相关推荐
《λ演算的语法和语义》是由荷兰学者H.P.巴伦德莱赫特编写的教材,专注于探讨计算理论中的核心概念——λ演算。λ演算是函数式编程的基础,也是理论计算机科学中极其重要的一部分。这本书深入浅出地阐述了λ演算的...
λ-演算的语法和语义
### 编程语言与λ演算:核心概念与模型 #### 概述 《编程语言与λ演算》是一份详尽的学术资料,由Matthias Felleisen和Matthew Flatt共同撰写,旨在深入探讨编程语言理论及其与λ演算的关系。这份资料主要聚焦于...
λ演算,这是一种于1930年代由阿隆佐·邱奇提出的计算模型,是函数式编程的理论基础,并对计算机科学的多个领域产生了深远的影响。它的核心概念是函数的抽象化,即一个函数可以接受另一个函数作为参数或返回另一个...
λ演算的完备性(Church-Turing Thesis)表明,任何可以用λ演算表示的计算都可以通过图灵机来完成,这为现代计算机科学奠定了理论基础。此外,λ演算中的类型系统,如简单类型λ演算,有助于防止类型错误,并为程序...
《mikrokosmos:(λ)教育性λ演算解释器》 λ演算是计算机科学中的一个基础理论,由Alonzo Church在20世纪30年代提出,用于研究函数计算的本质。λ演算的核心是λ表达式,它是一种表示函数的方法,通过抽象和应用...
**λ演算**是计算机科学和数学中的一个基础理论,它是函数编程语言的理论基石,对理解编程语言的性质和行为至关重要。λ演算由美国数学家阿隆佐·邱奇在20世纪30年代提出,用于研究计算的本质。在λ演算中,计算被...
λ演算解释器 如所述的lambda演算的解释器 语法 : <λexp>::= |(λ <λexp>) |(<λexp> <λexp>) 例子: >> (lambda x x) λx. x >> (lambda x y) λx. y >> x x >> 5 5 >> ((lambda x 5)...
λ演算(lambda calculus)是一套用于研究函数定义、函数应用和递归的形式系统。它由阿隆佐·邱奇和他的学生斯蒂芬·科尔·克莱尼在20世纪30年代发明的。 λ演算可以被称为最小的通用程序设计语言。它包括一条变换...