Lambda 演算

Lambda 演算#

相信点开这篇文章的您或多或少地听说过函数式编程这个名词。在摩尔定律失效的今天，对多核处理器的充分利用成为了一种越发重要的程序优化方法，而函数式编程也因为其并行运算亲和的特点在大众视野中越发频繁地出现。究其原因，离不开它从其理论上的祖先之一 - lambda演算那里所继承的特征。

而lambda演算这一起源于20世纪30年代，出自图灵导师阿隆佐·邱奇之手的形式系统如今已经发展成了蔚为大观的一个大家族，本文将展示其中最基础的一种：无类型lambda演算(这也是最早阿隆佐·邱奇提出的那种)

无类型lambda演算的基本规则#

无类型lambda演算中能做的事情只有定义lambda(经常称为Abstraction)和调用lambda(经常称为Application)，它们也是lambda演算中的基础表达式。

由于函数式编程范式对主流编程语言的影响，大多数程序员对lambda表达式这个名字已经不会感到陌生了，不过，无类型lambda演算中的lambda要比主流编程语言简单一些。一个lambda通常看起来就像这样：λx.x x, 其中x是它的参数(每个lambda只能有一个参数)，.是分隔参数与表达式具体定义的分隔符，后面的x x便是它的定义了。

备注

也有些材料的记法不写空格，上面的例子要改写成λx.xx

上面的x x如果换成x(x), 可能更符合我们在一般语言中见到的函数调用。但在lambda演算较常见的写法中，调用一个lambda只需要在它和它的参数中间写个空格。此处我们调用x所给出的参数就是x自己。

以上两种表达式和定义lambda时引入的变量加在一起合称lambda项，我们在MoonBit里用一个enum类型来表示它：

enum Term {
  Var(String) // 变量
  Abs(String, Term) // 定义lambda，变量用字符串表示
  App(Term, Term) // 调用lambda
}

我们在日常编程中所接触的概念诸如布尔值，if表达式，自然数算术乃至递归都可以通过lambda表达式实现，但这并非本文内容的重心所在。

参见

有兴趣的读者可以参阅Programming with Nothing这篇博客。

要实现一个无类型lambda演算的解释器，我们所需要了解的基本就只有两条规则：Alpha转换与Beta规约。

Alpha转换所描述的事实是，lambda的结构是重点，变量名叫什么没那么重要。λx.x和λfoo.foo可以互相替换。对于某些有重复变量名的嵌套lambda例如λx.(λx.x) x，重命名时不能把内层的变量也重命名了，例如上面的例子可以通过Alpha转换写成λy.(λx.x) y。

Beta规约则专注于处理lambda的调用，还是举一个例子：

(λx.(λy.x)) (λs.(λz.z))

在无类型lambda演算中，调用lambda之后所需要作的事情仅仅是对参数进行替换(substitution)，上面这个例子里就需要把变量x替换成(λs.(λz.z))，得到的结果是

(λy.(λs.(λz.z)))

自由变量与变量捕获#

一个lambda项中的变量如果在它所处的上下文中没有定义，那么我们叫它自由变量。例如(λx.(λy.fgv h))这个lambda项中变量fgv和h就没有对应的lambda定义.

在进行Beta规约时，如果用于替换变量的那个lambda项中含有自由变量，可能会导致一种被称为“变量捕获”的行为

(λx.(λy.x)) (λz.y)

上面这个表达式在替换后会变成

λy.λz.y

λz.y中的自由变量被当成了某个lambda的参数，这显然不是我们想要的。

变量捕获问题在编写解释器时的常见解决方案是在替换前遍历表达式得到一个自由变量的集合, 做替换时遇到内层lambda就判断一下变量名在不在这个自由变量集合里面

// (λx.E) T => E.subst(x, T)
fn subst(self : Term, var : String, term : Term) -> Term {
  let freeVars : Set[String] = term.get_free_vars()
  match self {
    Abs(variable, body) => {
      if freeVars.contains(variable) {
        //自由变量集合中有当前这个内层lambda的参数名，即会发生变量捕获
        abort("subst(): error while encountering \{variable}")
      } else {
        ...
      }
    }
    ...
  }
}

此处我们介绍一种较少见但具有一定便利性的方法：德布朗指数（de Bruijn index）。

德布朗指数#

德布朗指数是一种用整数表示lambda项中变量的技术，具体地说，它用变量所在位置和原先引入它的位置中间有几层lambda来替换特定变量。

λx.(λy.x (λz.z z))

λ.(λ.1 (λ.0 0))

上面的例子中，变量x和引入它的地方λx中间有一个λy, 于是将x替换为1，而z和定义它的位置中间没有夹杂其他的lambda，于是直接用0替换。某种程度上说，德布朗指数的值描述的是变量与对应lambda的相对距离，此处的距离衡量标注就是中间嵌套的lambda层数。

备注

同一个变量在不同的地方可能会用不同的整数来替换。

我们定义一个新类型TermDBI来表示使用德布朗指数的lambda项：

enum TermDBI {
  Var(String, Int)
  Abs(String, TermDBI)
  App(TermDBI, TermDBI)
}

不过直接编写以及阅读德布朗指数形式的lambda很痛苦，所以我们需要编写一个将Term转换成TermDBI的函数debruijn() - 这也是TermDBI类型定义中仍有String的原因，保留原变量名可用于它的Show的实现，这样就可以方便地用println打印求值结果查看了。

impl Show for TermDBI with output(self : TermDBI, logger) -> Unit {
  match self {
    Var(name, _) => logger.write_string(name)
    Abs(name, body) => logger.write_string("(\\\{name}.\{body})")
    App(t1, t2) => logger.write_string("\{t1} \{t2}")
  }
}

为了简化实现，如果输入的Term中含有自由变量，debruijn()函数会直接报错。MoonBit中一般用Result[V, E]类型表示可能会出错的计算, 它有Ok(V)和Err(E)两个值构造子，分别代表计算成功与失败。

提示

使用过Rust语言的读者应该会感到熟悉。

fn bruijn(self : Term) -> Result[TermDBI, String]

我们采取一种笨办法来保存变量名与相关联的嵌套深度，首先定义Index类型

struct Index {
  name : String
  depth : Int
}

然后写一个从@immut/list.T[Index]中根据特定name查找对应depth的辅助函数

// Find the depth corresponding to the first varname in the environment
fn find(map : @immut/list.T[Index], varname : String) -> Result[Int, String] {
  match map {
    Nil => Err(varname)
    Cons(i, rest) =>
      if i.name == varname {
        Ok(i.depth)
      } else {
        find(rest, varname)
      }
  }
}

现在可以补全debruijn()函数了。

  • Var的处理最简单，只需要查表寻找对应depth即可。

  • Abs稍微复杂一点，首先对列表中所有index的depth加一(因为lambda嵌套加深了一层)，然后在列表的开头加上{ name : varname, depth : 0 }。

  • App在两个子项都能转换时成功，否则返回一个Err

fn go(m : @immut/list.T[Index], t : Term) -> Result[TermDBI, String] {
  match t {
    Var(name) => {
      let idx = find(m, name)
      match idx {
        Err(name) => Err(name)
        Ok(idx) => Ok(Var(name, idx))
      }
    }
    Abs(varname, body) => {
      let m = @immut/list.Cons(
        { name: varname, depth: 0 },
        m.map(fn(index) { { name: index.name, depth: index.depth + 1 } }),
      )
      let res = go(m, body)
      match res {
        Err(name) => Err(name)
        Ok(term) => Ok(Abs(varname, term))
      }
    }
    App(e1, e2) =>
      match (go(m, e1), go(m, e2)) {
        (Ok(e1), Ok(e2)) => Ok(App(e1, e2))
        (Err(name), _) => Err(name)
        (_, Err(name)) => Err(name)
      }
  }
}

go(Nil, self)

在TermDBI上做规约#

规约主要处理的是App，即调用：

fn eval(self : TermDBI) -> TermDBI {
  match self {
    App(t1, t2) =>
      match (eval(t1), eval(t2)) {
        (Abs(_, t1), t2) => eval(subst(t1, t2))
        (t1, t2) => App(t1, t2)
      }
    Abs(_) => self
    // Eval应该不会遇到自由变量才对
    _ => panic()
  }
}

首先对两个子项尝试规约，然后看eval(t1)得到的是否是一个lambda，如果是，就执行一步变量替换(通过subst函数)然后继续化简。对于lambda(即Abs), 直接原样返回即可。

subst函数的实现在不用考虑自由变量的情况下简单了许多, 只要记录递归到当前位置的深度并且与遇到的变量进行比对，大小相等就是需要替换的目标变量。

fn subst(t1 : TermDBI, t2 : TermDBI) -> TermDBI {
  fn go(t1 : TermDBI, t2 : TermDBI, depth : Int) -> TermDBI {
    match t1 {
      Var(_, d) => if d == depth { t2 } else { t1 }
      Abs(name, t) => Abs(name, go(t, t2, depth + 1))
      App(tl, tr) => App(go(tl, t2, depth), go(tr, t2, depth))
    }
  }

  go(t1, t2, 0)
}

完整代码请查看 GitHub 代码仓库。

改进#

笔者在保存变量名到索引的对应关系时使用了@immut/list.T[Index]类型，并且在每增加一层lambda时更新整个列表，但是这其实是个很笨的办法。相信聪明且注意力集中的读者很快就能发现，其实只需要保存一个@immut/list.T[String]就够了，有兴趣的读者可以自己试着做一做。

目录