λ演算

  • 更新时间: 2018-05-11
  • 来源: 原创或网络
  • 浏览数: 7次
  • 字数: 33812
  • 发表评论

λ演算(lambda calculus,λ-calculus)是一套从数学逻辑中发展,以变量绑定和替换的规则,来研究函数如何抽象化定义、函数如何被应用以及递归的形式系统。它由数学家阿隆佐·邱奇在20世纪30年代首次发表。Lambda演算作为一种广泛用途的计算模型,可以清晰地定义什么是一个可计算函数,而任何可计算函数都能以这种形式表达和求值,它能模拟单一磁带图灵机的计算过程;尽管如此,Lambda演算强调的是变换规则的运用,而非实现它们的具体机器。

Lambda演算可比拟是最根本的编程语言,它包括了一条变换规则(变量替换)和一条将函数抽象化定义的方式。因此普遍公认是一种更接近软件而非硬件的方式。对函数式编程语言造成很大影响,比如Lisp、ML语言和Haskell语言。在1936年邱奇利用λ演算给出了对于判定性问题(Entscheidungsproblem)的否定:关于两个lambda表达式是否等价的命题,无法由一个“通用的算法”判断,这是不可判定性能够证明的头一个问题,甚至还在停机问题之先。

Lambda演算包括了建构lambda项,和对lambda项运行归约的操作。在最简单的lambda演算中,只使用以下的规则来建构lambda项:

语法 名称 描述
a 变量 表示参数或数学/逻辑值的字符或字符串
(λx.M) 抽象化 函数定义(M是一个lambda项)。变量x在表达式中已被绑定。
(M N) 应用 将函数应用于参数。 M 和 N 是 lambda 项。

产生了诸如:(λx.λy.(λz.(λx.zx)(λy.zy))(x y)的表达式。如果表达式是明确而没有歧义的,则括号可以省略。对于某些应用,其中可能包括了逻辑和数学的常量以及相关操作。

本文讨论的是邱奇的“无类型lambda演算”,此后,已经研究出来了一些有类型lambda演算。


1 历史

最开始,邱奇试图创制一套完整的形式系统作为数学的基础,当他发现这个系统易受罗素悖论的影响时,就把lambda演算单独分离出来,用于研究可计算性,最终导致了他对判定性问题的否定回答。

2 非形式化的直觉描述

在λ演算中,每个表达式都代表一个函数,这个函数有一个参数,并且会返回一个值。不论是参数和返回值,也都是一个单参的函数。可以这么说,λ演算中只有一种“类型”,那就是这种单参函数。函数是通过λ表达式匿名地定义的,这个表达式说明了此函数将对其参数进行什么操作。

例如,“加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演算这样表达:一个单一参数的函数,它的返回值又是一个单一参数的函数(参见柯里化)。例如,函数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表达式,就得到了组合子逻辑。

动机

在数学和计算机科学中,“可计算的”函数是基础观念。对于所谓的可计算性,λ-演算提供了一个简单明确的语义,使计算的性质可以被形式化研究。λ-演算结合了两种简化方式,使得这个语义变得简单。第一种简化是不给予函数一个确定名称,而“匿名”地对待它们。例如,两数的平方和函数

square_sum⁡(x,y)=x2+y2

可以用匿名的形式重新写为:

(x,y)↦x2+y2(理解成一包含xy的数组被映射到x2+y2

同样地,

id⁡(x)=x

可以用匿名的形式重新写为:

x↦x(即输入是直接对应到它本身。)

第二个简化是λ演算只使用单一个参数输入的函数。如果普通函数需要两个参数,例如square_sum函数,可转成接受单一参数,传给另一个函数中介,而中介函数也只接受一个参数,最后输出结果。例如,

(x,y)↦x2+y2

可以重新写成:

x↦(y↦x2+y2)

这是称为柯里化的方法,将多参数的函数转换成为多个中介函数的复合链,每个中介函数都只接受一个参数。 将square_sum函数应用于参数(5,2),直接产生结果

((x,y)↦x2+y2)(5,2)=52+22=29,

而对于柯里化转换版的评估,需要再多一步:

((x↦(y↦x2+y2))(5))(2)=(y↦52+y2)(2) //在内层表达式中x的定义为5,这就像β-归约一样。
=52+22 //y的定义为2,再次如同β-归约。=29

得出相同结果。

lambda演算

lambda演算是由特定形式语法所组成的一种语言,一组转换规则可操作其中的lambda项。这些转换规则被看作是一个等式理论或者一个操作定义。如上节所述,lambda演算中的所有函数都是匿名的,它们没有名称,它们只接受一个输入变量,柯里化用于实现有多个输入变量的函数。

Lambda项

lambda演算的语法将一些表达式定义为有效的lambda演算式,而某一些表达式无效,就像C编程语言中有些字符串有效,有些则不是。有效的lambda演算式称为“lambda项”。

以下三个规则给出了语法上有效的lambda项,如何建构的归纳定义:

  • 变量x本身就是一个有效的lambda项
  • 如果t是一个lambda项,而x是一个变量,则(λx.t) 是一个lambda项(称为lambda抽象);
  • 如果ts是lambda项,那么(ts)是一个lambda项(称为应用)。

其它的都不是lambda项。因此,lambda项当且仅当可重复应用这三个规则获取时,才是有效的。一些括号根据某些规则可以省略。例如,最外面的括号通常不会写入。

“lambda抽象”是指一个匿名函数的定义,它将单一输入的λx.t替换成t的表达式,所以产生了一个匿名函数,它采用x的值并返回t。例如,λx.x2+2是表示使用函数f(x)=x2+2作为t项的一个lambda抽象。lambda抽象只是先“设置”了函数定义,还没使用它。这个抽象在t项中绑定了变量x。一个应用ts表示将函数t应用在输入s,亦即对输入s使用函数t产生t(s)

lambda演算中并没有变量声明的概念。如λx.x+y(即f(x)=x+y)的定义中,lambda演算将y当作尚未定义的变量。lambda抽象λx.x+y在语法上是有效的,并表示将其输入添加到未知y的函数。

可用圆括弧对来消除歧义。例如,λx.((λx.x)x)(λx.(λx.x))x表示不同的项(尽管它们刚好化简到相同值)。这里第一个例子定义了一个包含子函数的抽象,并将子函数应用于x(先应用后传回)的结果;而第二个例子定义了一个传回任何输入的函数,然后在应用过程中传回对输入为x的应用(返回函数然后应用)。

操作函数的函数

在lambda演算中,函数被认为是第一类对象,因此函数可以当作输入,或作为其它函数的输出返回。

例如,λx.x表示映射到本身的函数,x↦x(λx.x)y表示将这个函数应用于y。此外,(λx.y)则表示无论输入为何,始终返回y值的常量函数x↦y。lambda演算中的函数应用是左结合的,因此stx表示(st)x

有几个“等价”和“化简”的概念,允许将各个lambda项“缩减”为“相同”的lambda项。

α-等价

对于lambda项,等价的基本形式定义,是α-等价。它捕捉了直觉概念,在lambda抽象中一个绑定变量的特别选择(通常)并不重要。 比如,λx.xλy.yα-等价的lambda项,它们都表示相同的函数(自映射函数);但如xy项则不是α-等价的,因为它们并非以lambda抽象方式绑定的。 在许多演示中,通常会确定α-等价的lambda项。

为了能够定义β-归约,需要以下定义:

自由变量

所谓的自由变量是那些在lambda抽象不受到绑定的变量。表达式中的一组自由变量定义归纳如下:

  • x的自由变量就只是x
  • λx.t的自由变量集合,是在t中移除了x的自由变量集合。
  • ts的自由变量是t的一组自由变量,与s的一组自由变量,这两项变量的并集。

例如,代表映射自身的λx.x,其中的lambda项没有自由变量,但是在函数λx.yx中的lambda项,有一个自由变量y

避免捕获的替换记法

假设tsr是lambda项,而xy是变量。如果写成t[x:=r]是一种避免被捕获的记法方式,表示在t这个lambda项中,以r来替换x变量的值。这定义为:

  • x[x:=r]=r
  • y[x:=r]=y,如果x≠y
  • (ts)[x:=r]=(t[x:=r])(s[x:=r])
  • (λx.t)[x:=r]=λx.t
  • 如果x≠y而且y不在lambda项r的自由变量中,则(λy.t)[x:=r]=λy.(t[x:=r])。对于lambda项r,变量y被称为是“新鲜”的。

例如,(λx.x)[y:=y]=λx.(x[y:=y])=λx.x((λx.y)x)[x:=y]=((λx.y)[x:=y])(x[x:=y])=(λx.y)y

新鲜度条件(要求y不在lambda项r中的自由变量中)对于确保替换不会改变函数的意义很重要。例如,忽视新鲜度条件的替代:(λx.y)[y:=x]=λx.(y[y:=x])=λx.x。此替换会将原本意义为常量函数的λx.y,转换成意义为映射自身函数的λx.x

一般来说,在无法满足新鲜度条件的情况,可利用α-重命名使用一个合适的新变量来补救,切换回正确的替换概念;比如在(λx.y)[y:=x]中,使用一个新变量z重命名这个lambda抽象,获取(λz.y)[y:=x]=λz.(y[y:=x])=λz.x,则替换就能保留原本函数的义涵。

β-归约

β-归约规定了形式如(λx.t)s的应用,可以化简成t[x:=s]项。符号记法(λx.t)s→t[x:=s]用于表示(λx.t)s 经过β-归约转换为t[x:=s]。例如,对于每个s,可转换为(λx.x)s→x[x:=s]=s。这表明λx.x实际上的应用是映射自身函数。同样地,(λx.y)s→y[x:=s]=y,表明了λx.y是一个常量函数。

lambda演算可视为函数式编程语言的理想化版本,如Haskell或ML语言。在这种观点下,β-归约对应于一组计算步骤。 这个步骤重复应用β-转换,一直到没有东西能再被化简。在无类型lambda演算中,如本文所述,这个归约过程可能无法终止, 比如Ω=(λx.xx)(λx.xx),是个特殊的lambda项。这里 (λx.xx)(λx.xx)→(xx)[x:=λx.xx]=(x[x:=λx.xx])(x[x:=λx.xx])=(λx.xx)(λx.xx)也就是说,该lambda项在一次β-归约中化简到本身,因此归约过程将永远不会终止。

无类型lambda演算的另一方面是它并不区分不同种类的数据。例如,需要编写只针对数字操作的功能。然而,在无类型的lambda演算中,没有办法避免函数被应用于真值、字符串或其它非数字对象。

3 形式化定义


本条目包含过多行话或专业术语,可能需要简化或提出进一步解释。
请在讨论页中发表对于本议题的看法,并移除或解释本条目中的行话。

形式化地,我们从一个标识符(identifier)的可数无穷集合开始,比如{a, b, c, ..., x, y, z, x1, x2, ...},则所有的lambda表达式可以通过下述以BNF范式表达的上下文无关文法描述:

  1. <表达式> ::= <标识符>
  2. <表达式> ::= (λ<标识符>.<表达式>)
  3. <表达式> ::= (<表达式> <表达式>)

头两条规则用来生成函数,而第三条描述了函数是如何作用在参数上的。通常,lambda抽象(规则2)和函数作用(规则3)中的括弧在不会产生歧义的情况下可以省略。如下假定保证了不会产生歧义:(1)函数的作用是左结合的,和(2)lambda操作符被绑定到它后面的整个表达式。例如,表达式 (λx.x x)(λy.y) 可以简写成λ(x.x x) λy.y 。

类似λx.(x y)这样的lambda表达式并未定义一个函数,因为变量y的出现是自由的,即它并没有被绑定到表达式中的任何一个λ上。一个lambda表达式的自由变量的集合是通过下述规则(基于lambda表达式的结构归纳地)定义的:

  1. 在表达式V中,V是变量,则这个表达式里自由变量的集合只有V。
  2. 在表达式λV .E中(V是变量,E是另一个表达式),自由变量的集合是E中自由变量的集合减去变量V。因而,E中那些V被称为绑定在λ上。
  3. 在表达式 (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-归约规则”。

4 归约


本条目包含过多行话或专业术语,可能需要简化或提出进一步解释。
请在讨论页中发表对于本议题的看法,并移除或解释本条目中的行话。

归约的操作包括:

操作 名称 描述
(λx.M[x]) → (λy.M[y]) α-转换 重命名表达式中的绑定(形式)变量。用于避免名称冲突。
((λx.M) E) → (M[x:=E]) β-归约 在抽象化的函数定义体中,以参数表达式代替绑定变量。

α-变换

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-变换也是有效的。

5 数据类型的编码

基本的lambda算法可用于建构布尔值,算术,数据结构和递归的模型,如以下各小节所述。

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等于在零的基础上m次加n。另一种方式是

    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一个元素和一个更小的列表。

6 附加的编程技术

lambda演算出现在相当大量的编程习惯用法中,其中许多编程语言最初以lambda演算作为语义基础,在此背景下开发的;有效地利用lambda演算作为基底。因为几个编程语言部分含括了lambda演算(或者非常相似的东西),所以这些技术也可以在实际的编程中见到,但有可能被认为是模糊或外来的。

命名常量

在lambda演算中,库将采用预先定义好的函数集合,其中lambda项仅仅是特定的常量。纯粹的lambda算法并不具有命名常量的概念,因为所有的原子λ项都是变量;但是在程序主体中,我们可将一个变量当成常量的名称,利用lambda抽象把这个变量绑定,并将该lambda抽象应用于预期的定义,来模拟命名常量的作法。因此在N(“主程序”的另一个lambda项)中,要以f来表示M(一些明确的lambda项),则写成如下:

f.N)M

作者经常引入类似如let的语法糖,允许以更直观的次序撰写上述内容:

let f =M inN

通过等号链接这个命名常量,即可将lambda演算“编程”的一个lambda项,写为零或多个函数的定义,而使用构成程序主体的那些函数。这个let显著的限制,是在M中并没有定义f名称,因为M不在绑定f的lambda抽象范畴之内;这意味着递归函数定义不能以let来使用M。更进步的letrec语法糖允许以直觉的方式编写递归函数定义,而不需用到不动点组合子。

递归与不动点

递归是使用函数自身的函数定义;在表面上,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项有普遍接受的名称:

.λ))

其中有几个在“消除lambda抽象”中有直接的应用,将lambda项变为组合演算的术语。

消除lambda抽象

如果N是一个没有λ-抽象的lambda项,但可能包含了命名常量(组合子),则存在一个lambda项T(x,N),这相同于一个缺少λ-抽象(除了作为命名常量的一部分,如果这些被认为是非原子的)的λx.N;也可以被视为匿名变量,就如同T(x,N)从N之中删除所有出现的x,同时仍然允许在N包含x的位置替换参数值。

转换函数T可由下式定义:

, )

在这两种情况下,形式T(x,N)P可借由使初始的组合子IKS获取参数P而化简, 就像(λx.N)P经过β-归约一样。I返回那个参数。K则将参数抛弃,就像(λx.N),如果xN中不是以自由变量出现。S将参数传递给应用程序的两个子句,然后将第一个结果应用到第二个的结果之上。

组合子BC类似于S,但把参数传递给应用的一个子项(B传给“参数”子项,而C传给“函数”子项),如果子项中没有出现x,则保存后续的K。与BC相比,S组合子实际上混合了两个功能: 重新排列参数,并复制一个参数,以便它可以在两个地方使用。W组合子只做后者,产生了SKI组合子演算的B,C,K,W系统。

7 可计算函数和lambda演算

自然数的函数F: N
    I := λx.x
    K := λx.λy.x
    S := λx.λy.λz.x z (y z)
    B := λx.λy.λz.x (y z)
    C := λx.λy.λz.x z y
    W := λx.λy.x y y
    U := λx.λy.y (x x y)
    ω := λx.x x
    Ω := ω ω
    Y := λg.(λx.g (x x)) (λx.g (x x))
N是可计算函数,当且仅当存在着一个lambda表达式f,使得对于N中的每对x, y都有F(x)= y当且仅当f x == y,这里的x和y分别是对应于x和y的邱奇数。这是定义可计算性的多种方式之一;关于其他方式和它们的等价者的讨论请参见邱奇-图灵论题。
    T(x, x) := I
    T(x, N) := K N if x is not free in N.
    T(x, M N) := S T(x, M) T(x, N) 
我来评分 :6
0

转载注明:转自5lulu技术库

本站遵循:署名-非商业性使用-禁止演绎 3.0 共享协议