λ 演算

背景

• 1874 年，德国数学家格奥尔格·康托尔创立集合论后，在审视数集时对极限的概念提出质疑，引起数学界的争论；德国数学家戴维·希尔伯特支持康托尔的质疑，并和其他形式主义者一样，希望基于集合论创立一套更正式、更严谨的数学证明体系；
• 1910-1913 年，英国数学家伯兰特·罗素和其老师阿尔弗雷德·怀特海合著发表《数学原理》，在书中发明了一套形式证明系统，用于描述逻辑和数学命题；
• 1928 年，希尔伯特在一次会议上提出了三大问题，并相信答案是肯定的：
  1. 数学是否完备：在一个形式系统中，任意公式都能从该系统中得出（即任意公式都为该系统的定理）则称该系统具有完备性；
  2. 数学是否自洽：系统不产生悖论则称该系统具有自洽性；
  3. 数学是否可判定：对任意一条命题，存在一种算法，可以判定该命题是否可以从公理推导出来，则称该系统具有可判定性；
• 1931 年，美籍奥地利数学家库尔特·哥德尔发表论文，证明了任何蕴含了基础算术公理的基本数学系统都是不完备的，称为哥德尔不完备第一定理；接着又证明了数学里任何自洽的形式系统都无法证明其自洽性，称为哥德尔不完备第二定理；
• 1936 年，英国数学家艾伦·图灵为解决判定性问题，提出一种基于状态的抽象计算模型——图灵机，用于模拟数学运算的过程，并提出停机问题，从而证明了数学系统不可判定；
• 同一时期，图灵提出的图灵机引起了他博士生导师——美国数学家阿隆佐·邱奇的注意，并用 λ 演算描述了计算的基本函数式概念，最终发现图灵机与 λ 演算等价，任一图灵机中的程序都可以转化为一个等价的 λ 演算程序，反之亦然，以此提出邱奇-图灵猜想；

定义

expression  ::=  name | function | application
function    ::=  "λ" name "." expression
application ::=  expression expression

• 标识符：x

  • 用于表示变量的任意名字；
  • 名字没有任何含义，仅区分不同变量，名字相同代表变量相同；
  • 分类：
    • 约束变量：在函数头中出现的变量（即参数），如λx.y中的x；
    • 自由变量：未在函数头中出现的变量，如λx.y中的y；

• 函数：λx.x+1

  • 字母λ无实际意义，仅标识一个函数的开始；
  • λ之后.之前称为函数头，放置变量（即参数）；
  • .表示将name绑定/约束于该函数体expression；
  • .之后称为函数体，可放置表达式；
    • 函数体不作任何计算，只作解析，解析完成则函数应用完成；
    • 函数体尽可能向右扩展，即λx.M N等价于λx.(M N)，而非(λx.M) N；

• 应用：(λx.x+1) a

  • 传入后一个表达式，调用前一个表达式；
  • 默认为左结合，即从左向右执行，则有M N P等价于(M N) P；
  • 应用函数后根据运算法则进行演算；

• 表达式：(λx.(λy.x y)) (λi.i)

  • 一行符号称为表达式；
  • 允许使用括号组织表达式，改变优先级；

  注意

  在 λ 演算的世界中，只存在上述的标识符、函数和应用三种语法，此处的+仅为方便表示抽象的“相加”函数操作，不表示实际表达式内容。λ 演算中加法的实际定义见后文。

柯里化

• 柯里化：

  • 以美国逻辑学家哈斯克尔·柯里的名字命名的一种技术，最先由乌克兰裔俄罗斯学者 Moses Schönfinkel 发现；
  • 根据上述定义，一个函数只接受一个参数，通过柯里化技术可以实现多个参数的接受；

• 实现：一个函数的输入和输出都可以是函数，因此可以先接受一个参数，再返回接受余下参数的新函数；

  备注

  假设要实现一个函数，该函数接受两个参数并返回两参数之和，则λx y.x+y可以写作λx.(λy.x+y)，当传入第一个参数a时，该函数返回另一个函数λy.a+y，并继续接受第二个参数。

• 因为函数体是向右扩展的，因此λx.λy.M等价于λx.(λy.(M))，这种柯里化的函数可简记为多参数的形式λxy.M（假设所有变量都为单字母）；

• 柯里化是闭包的鼻祖；

运算法则

• λ 演算在应用函数时只有三条运算法则：Alpha 转换、Beta 归约和Eta 转换；

Alpha 转换

alpha[x/y]

• Alpha 转换：即约束变量重命名；

  • 在 λ 演算中，变量的名字并不重要，因此在为函数体中的约束变量重命名之后，函数在重命名前与重命名后是等价的；
  • Alpha 转换可记为alpha[x/y]，表示x变为y；

• 命名冲突：当对约束变量进行 Alpha 转换时，可能会与自由变量发生命名冲突，此时函数重命名前后不等价；

  alpha[a/b] (λa.a+b) -> (λb.b+b)
  

• 某些编译器在编译时会包括 Alpha 转换阶段，对程序中的所有变量进行重命名，使变量唯一；

Beta 归约

[x:=y]

• Beta 归约：

  • 当应用函数时，用后一个表达式替换函数体中的相关约束变量；
  • Beta 归约可记为[x:=y]，表示用y替换x；
  • 可理解为用实参替换形参的过程；
  • 根据 Beta 归约，可得结果：

  (λx.M) y ≡ M[x:=y]
  

• Alpha 转换：在进行 Beta 归约之前，首先要保证约束变量和自由变量不发生冲突，因此有时有必要首先进行 Alpha 转换；

  备注

  有函数λz.(λx.x+z)，若应用于表达式x+2，则根据 Beta 归约，应用的结果为λx.x+x+2，此时第一个x原为约束变量，第二个x原为自由变量，但 Beta 归约后自由变量与函数进行了绑定，发生命名冲突。

Eta 转换

• Eta 转换：在等价表达式之间转换；

• 等价：若有两个函数，对于相同输入产生了相同输出，则称这两个函数等价；

• 分类：

  • Eta 归约：当两个表达式等价时，将更复杂的表达式归约为更简洁的表达式；

    备注

    有函数λx.M x，则表达式(λx.M x) a有结果M a，因此可得λx.M x ≡ M，进行 Eta 归约后，λx.M x归约为M。

  • Eta 抽象/扩展：当两个表达式等价时，将更简洁的表达式扩展为更复杂的表达式；

• Eta 转换有利于无值编程，某些编译器在编译时会进行 Eta 转换；

编码

• 邱奇-图灵猜想：所有计算或算法都可以由一台图灵机来执行，以任何常规编程语言编写的计算机程序都可以翻译成一台图灵机；
• 由于 λ 演算是图灵机的等价形式，因此该猜想同样适用于 λ 演算；
• 在 λ 演算的世界中只存在函数，不存在非函数的数据类型（如数字、布尔值等），但λ演算可以通过函数对其他数据类型进行编码；

算术运算

自然数

• 思路：定义自然数首先从0开始，然后使用后继函数得到其余所有自然数；

• 0：

  0 = λx.(λy.y)
  

• 后继函数：

  SUCC = λa.(λb.(λc.b (a b c)))
  

  • 因为1定义为0的后继，则1可以表示为：

       SUCC 0
    -> (λa.(λb.(λc.b (a b c)))) 0
    -> λb.(λc.b (0 b c))
    -> λb.(λc.b ((λx.(λy.y)) b c))
    -> λb.(λc.b c)
    -> alpha[b c/x y] λb.(λc.b c)
    -> λx.(λy.x y)
    

  • 因为2定义为1的后继，则2可以表示为：

       SUCC 1
    -> λa.(λb.(λc.b (a b c))) 1
    -> λb.(λc.b (1 b c))
    -> λb.(λc.b ((λx.(λy.x y)) b c))
    -> λb.(λc.b (b c))
    -> alpha[b c/x y] λb.(λc.b (b c))
    -> λx.(λy.x (x y))
    

• 自然数：其余自然数只是在0的基础上不断叠加应用x；

  0 = λx.(λy.y)
  1 = λx.(λy.x y)
  2 = λx.(λy.x (x y))
  3 = λx.(λy.x (x (x y)))
  4 = λx.(λy.x (x (x (x y))))
  ...
  

  备注

  虽然用这种方法表示数字很奇怪，但是从数学角度上看两种表示方式并无差别，都是人为定义的符号。

加法

x SUCC y

• 思路：当一个自然数接受第一个参数时，该参数会重复该自然数的次数，且每次都对第二个参数进行应用，因此将后继函数传入自然数中，后继函数就会对第二个参数重复应用相等次数；

   3 + 5
-> 3 SUCC 5
-> λx.(λy.x (x (x y))) SUCC 5
-> SUCC (SUCC (SUCC 5))
-> λx.(λy.x (x (x (x (x (x (x (x y))))))))
-> 8

乘法

MULTIPLY = λa.(λb.(λc.a (b c)))

• 思路：将c传入自然数b后，得到b个c，再将结果传入自然数a，得到a个“b个c”；

   2 * 3
-> MULTIPLY 2 3
-> λc.2 (3 c)
-> λc.(λy.(3 c) ((3 c) y))
使 ((3 c) y) = (c (c (c y))) = a
-> λc.(λy.3 c a)
-> λc.(λy.c (c (c a)))
-> λc.(λy.c (c (c (c (c (c y))))))
-> 6

减法

• 前趋函数：减法作为加法的对立，可以通过构造一个前趋函数来实现；

• 思路：

  • 一个自然数从0构造而来，其自身等价于x SUCC 0，若能够将x-1次（即倒数第一次，或前一次）计算的结果保留，则可以实现这个前趋函数；
  • 一个自然数无法达到目的，但可以通过构造用两个自然数构成的数对来达成；
  • 有数对(a,b)，可以用数对的第一个成员保存调用后继函数后的结果，用第二个成员保存调用后继函数前的原值，这种方式可以获取前一次的计算结果；
  • 设应用后继函数的次数为n，则为了获取n-1的值，可以从(0,-1)或(0,0)开始计算，这样n次后可得数对(n,n-1)，此时获取第二个成员则达到目的；
  • 因为数对(a,b)的第二个成员始终会被舍弃，因此从(0,0)开始与从(0,-1)开始并无差别；

• 实现：

  • 因为要获取第二个成员（通过λx.(λy.y)获取），所以可定义数对(a,b)为下述形式，则最小数对为λp.p 0 0：

    PAIR = λp.p a b
    

  • 将数对的第一个成员取出，获取应用后继函数前的原值：

    PAIR 1 -> (λp.p a b) 1 -> λx.(λy.x) a b -> a
    

  • 通过后继函数获得a+1：SUCC (PAIR 1)；

  • 因此，下述函数可以通过(a,b)得到新数对(a+1,a)，该函数接受一个数对作为参数；

    NEXTPAIR = λx.(λy.y (SUCC (x 1)) (x 1))
             = λx.(λy.y (SUCC (x (λx.(λy.x)))) (x (λx.(λy.x))))
    

       NEXTPAIR (2,3)
    -> λy.y (SUCC ((2,3) 1)) ((2,3) 1)
    -> λy.y (SUCC ((λp.p 2 3) 1)) ((λp.p 2 3) 1)
    -> λy.y (SUCC 2) 2
    -> λy.y 3 2
    -> (3,2)
    

  • 将该函数对数对(a,b)应用n次，可以得到新数对(a+n,a+n-1)，则当a等于0时，可得(n,n-1)；

    2 NEXTPAIR (0,0) -> NEXTPAIR (1,0) -> (2,1)
    

  • 构造函数，取出数对中的第二个成员，即可得到前趋函数：

    PRED = λn.(n NEXTPAIR λp.p 0 0) λi.(λj.j)
    

• 结果：前趋函数接受一个自然数作为参数；

  NEXTPAIR = λx.(λy.y (SUCC (x (λx.(λy.x)))) (x (λx.(λy.x))))
  PRED     = λn.(n NEXTPAIR λp.p 0 0) λx.(λy.y)
  

• 减法：与加法同理：

  x PRED y
  

逻辑运算

布尔值

TRUE  = λx.(λy.x)
FALSE = λx.(λy.y)

• 真值：定义为函数，该函数传入两个参数，始终返回前一个参数；

• 假值：定义为函数，该函数传入两个参数，始终返回后一个参数；

  备注

  假值FALSE的定义与0相同，约束变量均被丢弃，返回后一个值。

逻辑否

NOT = λb.b FALSE TRUE

• 逻辑否可定义为以上形式，接受一个布尔值作为参数，返回一个布尔值；

   NOT TRUE
-> (λb.b FALSE TRUE) TRUE
-> TRUE FALSE TRUE
-> (λx.(λy.x)) FALSE TRUE
-> FALSE

逻辑与

AND = λb1.(λb2.b1 b2 FALSE)

• 逻辑与可定义为以上形式，接受两个布尔值作为参数，返回一个布尔值；

   AND TRUE TRUE
-> (λb1.(b2.b1 b2 FALSE)) TRUE TRUE
-> TRUE TRUE FALSE
-> (λx.(λy.x)) TRUE FALSE
-> TRUE

   AND TRUE FALSE
-> (λb1.(b2.b1 b2 FALSE)) TRUE FALSE
-> TRUE FALSE FALSE
-> FALSE

逻辑或

OR = λb1.(λb2.b1 TRUE b2)

• 逻辑或可定义为以上形式，接受两个布尔值作为参数，返回一个布尔值；

   OR TRUE FALSE
-> λb1.(λb2.b1 TRUE b2) TRUE FALSE
-> TRUE TRUE FALSE
-> TRUE

   OR FALSE TRUE
-> λb1.(λb2.b1 TRUE b2) FALSE TRUE
-> FALSE TRUE TRUE
-> TRUE

条件

IF = λx.(x FALSE NOT FALSE)

• IF函数接受一个自然数作为参数，若为0，则返回TRUE，否则返回FALSE；

   IF 0
-> (λx.(x FALSE NOT FALSE)) 0
-> (λx.(λy.y)) FALSE NOT FALSE
-> NOT FALSE
-> TRUE

   IF 2
-> λx.(x FALSE NOT FALSE) 2
-> 2 FALSE NOT FALSE
-> (λx.(λy.x (x y))) FALSE NOT FALSE
-> FALSE (FALSE NOT) FALSE
-> FALSE

比较

• 大于等于：

  GE = λx.(λy.IF (x PRED y))
  

  • 思路：对y调用x次PRED，若为零则说明两者相等或x大于y；

     GE 3 4
  -> (λx.(λy.IF (x PRED y))) 3 4
  -> IF (3 PRED 4)
  -> IF 1
  -> FALSE
  

     GE 5 2
  -> (λx.(λy.IF (x PRED y))) 5 2
  -> IF (5 PRED 2)
  -> IF 0
  -> TRUE
  

• 等于：

  EQUAL = λx.(λy.AND (GE x y) (GE y x))
  

  • 思路：当GE x y为真且GE y x为真时，可以确定相等关系；

     EQUAL 3 3
  -> AND (GE 3 3) (GE 3 3)
  -> AND TRUE TRUE
  -> TRUE
  

     EQUAL 4 3
  -> AND (GE 4 3) (GE 3 4)
  -> AND TRUE FALSE
  -> FALSE
  

递归（Y 组合子）

Y = λf.(λx.f (x x)) (λx.f (x x))

• 不动点：一个由函数f映射到其自身的值，即f x -> x中，x为函数f的不动点；

• Y 组合子：由哈斯克尔·柯里定义，用于计算高阶函数的不动点，使得 λ 演算可以在不支持递归的场合中实现递归；

• 思路：

  • 递归即自己定义自己，一个最简单的递归：

    LOOP = LOOP
    

  • 在构造函数时，函数至少接受一个参数，因此该参数可以设定为该函数本身，即函数g有g g，称为自我应用；

  • 通过模仿最外层g g的结构，可以构造出函数g的函数体，该函数无论如何，得到的结构始终是g g；

    LOOP = (λx.x x) (λx.x x)
    

  • 若要得到函数f，使其满足f a -> a，则修改函数g的内部结构，可得：

    f (x x) -> (x x)
    

  • 因此Y组合子为：

    Y = λf.(λx.f (x x)) (λx.f (x x))
    

   Y a
-> (λf.(λx.f (x x)) (λx.f (x x))) a
-> (λx.a (x x)) (λx.a (x x))
-> a ((λx.a (x x)) (λx.a (x x)))
-> a (Y a)
-> a (a (Y a))
...