Print4D

从λ演算开始

19 Jun 2015

为了实践一次惰性求值,也顺带学习一下 Java 8 带来的函数式支持,所以用 Java 写了一个λ演算的解释器,lambda-interp

关于λ演算,维基百科上有很好的解释。


零,lambda-interp

lambda-interp 使用 % 表示 lambda 符号 λ。这里是 β-归约 的一个例子:

> (%s.s s) %x.x %y.y
Result: %y.y

虽然λ演算中 lambda 表达式不支持多参数,但 lambda-interp 中可以定义多参数的表达式。这仅仅是一个语法糖,转换成 AST 之后,所有的 lambda 表达式依然是单参数的。

> %x y z.x y z
Result: %x.%y.%z.((x y) z)

这样做的好处,一是保持核心语言简单;二是天然地支持了柯里化

另外,lambda-interp 中除了 lambda 表达式之外,没有数字,字符串,布尔值等等任何其它数据类型。因为λ演算中没有这些东西,而且这些确实也不是必须的。

lambda-interp 由 4 部分构成:词法分析、语法分析、解语法糖和求值。

因为λ演算如此简陋,所以词法分析也挺粗暴的。4 个符号 %.() 被切分成 Key;任何有数字和字母组成的串切分成 Id;除此之外任何其他符号都为非法字符。也就是说,用数字作为标识符也是有效的。比如可以这样写:

> (%0.0) %x.x
Result: %x.x

求值采用的惰性求值(call by name),即表达式仅仅在被需要的时候才会进行求值。使用值传递(call by value)会更简单,但它在某些特殊情况中会产生问题。

后面会提到关于这样实现的更多细节。


一,从λ演算开始

lambda-interp 提供的这些功能丝毫看不出它有什么用处,确实它太简单了。放在现下的程序语言中看,它只是它们中三个(还是受限的)功能:

不过,只这三个功能就足够了,从它开始,就足以构造出一个完整的程序语言。

想象一下,假如 scheme 没有提供像 pair 和 list 这样的复合类型,那能不能通过其他方式实现。从使用者的角度看,pair 就是通过 cons 将两个值保存在一个地方,再配合 car 和 cdr 分别获取这两个值。闭包也可以将参数保存起来,那么自然地,实现一个接受两个参数的函数 my-cons,其返回一个新的函数(闭包)。再实现 my-car 和 my-cdr 两个函数,接受 my-cons 返回的函数作为参数,最后分别返回原来的两个参数就可以了。代码非常简单:

(define my-cons
  (lambda (x y)
    (lambda (b)
      (if b x y))))

(define my-car
  (lambda (p)
    (p #t)))

(define my-cdr
  (lambda (p)
    (p #f)))

使用起来和原生的 pair 一模一样的。my-cons、my-car 和 my-cdr 对数据的类型也是透明的,所以它同样对任意数据类型(甚至它自身)都有效。

(define p (my-cons 1 2))
(my-car p)    ;; 1
(my-cdr p)    ;; 2

这基本就是使用λ演算构造一个完整语言的思路了。


布尔值

首先从布尔值开始,其实就是构造 true 和 false。但应该先考察一下究竟什么是 true 和 false。单独看 true 和 false,它们仅仅只表示真和假,但真假又有什么用呢。确实,如果离开了 if,true 和 false 没有任何用处。倒是可以 print 出来给程序员看,可计算机是看不懂的。也就是说,布尔值一定得和 if 语句放在一起,它才有意义。在任何编程语言中,我们定义的所有布尔值,无论传来传去经过多少层函数,最后它必定会被 if 处理,否则就是多余的。

所以我们应该从 if 入手,来构造布尔值。完全可以把 if 看成是一个函数:它接受三个参数,第一个参数为 true,返回第二个参数,否则返回第三个参数。

if(test, conseq, alt)

但问题是函数内部如何判断参数 test 是否为 true,莫非继续调用 if?这样当然是不行的。问题的关键不在于如何判断 test,这样想的话还是把布尔值作为一种具有特定的值看待了。在这里布尔值其实没有什么特别的表示,仅仅和 if 之间具有一种约定关系。或许 if 函数应该这样表达才不至于引起误解:

if(p, x, y)

由于λ演算中没有多参数的表达式,所以这个 if 应用最终会被翻译成如下格式:

if(p)(x)(y)

if 函数接受一个参数,返回一个接受一个参数的新函数,这个新函数又返回一个新函数。由于 p 作为布尔值有两种取值,所以 if 函数返回的函数就可能有两个,记作 f1 和 f2:

f1(x)(y) # x
f2(x)(y) # y

f1(x)(y) 返回 xf2(x)(y) 返回 y。这样好像还是挺不直观的,那就将 f1f2 变回多参数的形式:

f1(x, y) # x
f2(x, y) # y

变换之后 f1f2 所对应的 lambda 表达式就显而易见了:

# f1
%x y.x

# f2
%x y.y

这样我们只需要构造出一个 lambda 表达式(if),被一个 lambda 表达式(true)应用之后得到 %x y.x,被另一个 lambda 表达式(true)应用之后得到 %x y.y。这三个表达式构造的方式很多,我们使用最简单的一种,if 为一个原样返回的表达式 %p.p;true 为 %x y.x; false 为 %x y.y。最后再将 if 改为 3 个参数,让应用发生在 if 内部:

if:    %p x y.p x y
true:  %x y.x
false: %x y.y

布尔值的构造就完成了,在 lambda-interp 中试一下:

# (if            true     (%a.a) (%b.b))
> (%p x y.p x y) (%x y.x) (%a.a) (%b.b)
Result: %a.a

# (if            false    (%a.a) (%b.b))
> (%p x y.p x y) (%x y.y) (%a.a) (%b.b)
Result: %b.b

在 scheme 中试验一下:

(define my-if
  (lambda (p x y)
  (p x y)))

(define my-true
  (lambda (x y) x))

(define my-false
  (lambda (x y) y))

(my-if my-true #t #f)   ;; #t
(my-if my-false #t #f)  ;; #f

之所以在 scheme 中试验一下,原因是这样构造的 my-if 函数存在参数传递上的一个问题。my-if 只是 scheme 中的一个普通函数,那么函数应用时必然遵从 scheme 的求值规则。同大多数程序语言一样,scheme 使用值传递的方式,所有的参数会在函数应用之前被求值。无论是否会被用到,my-if 所有参数都会被求值。下面这个 my-if 函数应用会引起无限循环,if 则不会。

(define p
  (lambda ()
    (p)))

(if #t #t (p))             ;; #t
(my-if my-true #t (p))     ;; 无限循环

从这个例子也可以看出 scheme 中的 if 并不是看起来的那样是一个普通的函数。甚至在大部分语言中,if 都是需要在解释器中单独处理的。那么这些语言中,要使用 my-if 需要用一点延迟求值的技巧,将参数放入函数中,这样解释器就不会对函数体求值了。

((my-if my-true
        (lambda (x) #t)
        (lambda (x) (p))) "anything")

正是由于这个原因,lambda-interp 使用了惰性求值的实现方式。lambda 表达式被应用的时候,参数不会被求值,只有当参数被需要的时候,参数才被求值。

# 只有被需要时,((%b.b b) %b.b b) 才会被求值

# (if            true     (%a.a) ((%b.b b) %b.b b))
> (%p x y.p x y) (%x y.x) (%a.a) ((%b.b b) %b.b b)
Result: %a.a

# (if            false    (%a.a) ((%b.b b) %b.b b))
> (%p x y.p x y) (%x y.y) (%a.a) ((%b.b b) %b.b b)
# 无限循环,堆栈溢出


复合数据结构

作为一种容器式的数据结构 pair,其实前面已经实现了。很容易将 my-consmy-carmy-cdr 变为 lambda 表达式:

cons: %x y f.f x y
car:  %p.p true
cdr:  %x y.false

相应地,list 的表示也很容易,只是需要约定一下非空表与空表各自的形式。一般地,使用 (false, (x, y)) 来表示非空表,使用 (true, true) 表示空表。

nil:  %z.z
list: %x y.cons false (cons x y)
null: car                           # 判断是否为 nil
head: %z.car (cdr z)
tail: %z.cdr (cdr z)


数字

样布尔值一样,true 和 false 只有在 if 中才有意义。数字也不是孤立存在的,数字也只有在特定的函数(四则运算、指数运算、比较)里才有含义。之所以用阿拉伯数字表示 0,1,2,3,……,仅仅是因为方便。如果用 “*” 的个数来表示数字也是完全可行的,只要这些方法可以处理。但无论如果表示,一定得体现出自然数的依次等量的增长,也就是后继的含义。比如用 “*” 表示 1,“**” 表示 2,就不能用 “****” 表示 3,“***” 表示 4。这其实也是自然数的定义(这里把 0 看作自然数):

使用λ演算来表示的话,似乎可以完全自由的定义一套规则来表达自然数。

0: %x.x
1: %x.%x.x
2: %x.%x.%x.x
3: %x.%x.%x.%x.x

这样表达是有一个确定的后继的,不难推出后继(suc)的表达式为 %y.%x.y。如果可以定义加法、乘法、比较等表达式的话,那这套表示法就是完全可行的。不过这非常困难,这些自然数都表示为 lambda 表达式,只有 body 不同,要使不同的自然数产生不同的效果,一定要应用自然数的表达式使 body 产生作用。即使调用形式如同 (add 1 2),最后在 add 内也一定是 (1 add^ 2) 这样的形式。然而这些 lambda 表达式(除了 0)的第一个 x 和后面的 x 不是同一个变量,而且没有被用到。也就是说无论是 (1 add^ 2) 还是 (1 mult^ 2),结果都是一样的,因为参数 x 都会被丢弃。另外,第二个问题是,自然数的 lambda 表达式通常应该接受两个参数,一个表示操作,一个表示其他的自然数。所以自然数的 lambda 表示至少应该接受两个参数,f 和 x。

0:   %f x.x
1:   %f x.f x
2:   %f x.f (f x)
3:   %f x.f (f (f x))
suc: %n f x.n f (f x)

这是λ演算作者 Alonzo Church 的自然数编码,我认为是最为优雅的。我无法推测出它背后的直觉是什么,不知道 Church 是如果编码出来的。但也不难看出它背后的含义,一个自然数就是一个算子(x),它将一个操作(f)应用 n 次。比如加法,可以这样简单的实现,(2 suc 3),它的含义简单直观,就是在 3 之上应用两次后继(suc)函数,第一次得到 4,第二次得到 5,就是最后的结果。不过它的应用方式不太直观,而且有点低效。

稍微改造过后的加法是这样的:

add: %m n f x.m f (n f x)

它将应用方式变为了 (add 2 3),而且避免了 n 次应用。加法的定义利用了 一个恒等式。

乘法背后的恒等式为 。不太严格的表达,就是在 (mult 2 3) 中,将 3 作为 2 的 f 参数传入,这样 2 中的每一个 f 都被替换为了 3 中的 3 个 f,最后的结果就是 2 * 3 = 6 个 f。

mult: %m n f.m (n f)

减法通过前驱(pre,和后继相反)函数来定义。减法类似加法最初的定义:%m n.n pre m,意思也很好理解,计算 m 的前驱 n 次。只是 pre 的定义就稍微复杂了一点,它通过一个初始的 pair (x . x)(pre 3)(x . x) 应用 3 次,依次得到 (fx . x)(f (fx) . fx)(f (f (fx)) . f (f x)),再取出 pair 中的第二个元素即为 3 的前驱。

prefn: %f p.cons (f (car p)) (car p)
pre:   %n f x.cdr (n (prefn f) (cons x x))
sub:   %m n.n pre m

关于除法、指数、负数、小数的表示,可以参见维基百科上相应的说明。


流程控制

流程控制已经有了条件判断(if),还需要一个可以表达循环的方法。但λ演算因为没有状态,写不出退出循环的条件,所以这里使用递归来代替循环。

然而λ演算中表达式没有名字,无法在表达式中来调用自身。关于这个问题, Y组合已经解决过了。这里直接套用公式就行。

Y: %f.(%x.f (x x)) (%x.f (x x))
f: Y(f^)

因为惰性求值,所以不用担心 Y(f^) 会陷入无限循环。


二,合在一起

一个完整的程序语言的基本要素似乎齐备了。这里尝试使用 lambda-interp 写一个阶乘函数。为了简单而且直观,lambda-interp 提供了一个关键字 define 用于创建函数(给 lambda 表达式一个名字),不过这并不是必须的。

define true  = %x y.x
define false = %x y.y
define if    = %p x y. p x y

define cons = %x y f.f x y
define car = %p.p true
define cdr = %p.p false

值得注意的是,环境会和相应的 lambda 表达式绑定在一起(闭包),lambda 表达式中的自由变量无论是标识符还是函数名,都会在环境中查找。这和 Lua 创建函数时的行为是一致的,如果 car 在 true 之前创建,那么在调用 car 时会抛出无法找到 true 的错误。

fact: Y (%g n. if (iszero n) 1 (mult n (g (pre n))))

fact 就是一个计算阶乘的函数,它真的是可以工作的。lambda-interp 已经在 PreDefinition.java 预定义了一些常用的函数,所以可以直接尝试对 fact 3 求值。求值的结果看起来会很复杂,这是因为其中包含无限递归无法归约的关系。被应用到其他表达式时,它和 %f x.f (f (fx)) 其实是等价的,可以通过下面的方式来验证。

> iszero (sub 6 (fact 3))
Result: (%x.(%y.x))   # true

> iszero (sub 7 (fact 3))
Result: (%x.(%y.y))   # fasle

这种以λ演算来编码数据的方式效率非常低下,几乎从来不会有一个严肃的程序语言这样子来实现。但理解λ演算至少可以对函数式语言有更深的理解,甚至对所有编程语言,因为无论是数值还是逻辑运算,不就是一套按照规则变换的形式系统么。

(完)

参考资料: