哲学之光数学之美程序员

λ演算(Lambda Calculus)入门基础(一):定义与归

2018-05-20  本文已影响16人  SK木眠

此系列文章是自己的lambda演算入门总结与复习,着重于探讨“为什么(Why)”与“怎么做(How)”,也希望能对看到它的人学习了解这个形式系统有些微帮助。由于之前看了不少wiki、tutorial、introduce之流,但绝大多数读过之后仅知其然而不知其所以然,因此才有了这个系列,试图将我的浅薄理解稍作阐释梳理,知之尚浅,如有错漏不妥之处请不吝指出,欢迎交流讨论批评建议。

部分参考:
Wikipedia
SEP(Stanford Encyclopedia of Philosophy)
blogs:
一个入门教程,有中文翻译版,也值得一览:[翻译] [原文]
一个侧重举例的简单教程

NOTE: 在lambda演算中,函数是一等公民。即对函数做一般的基本操作都是合法的,比如把函数作为参数传入或返回,赋给一个变量等等。


lambda | λ 定义

要描述一个形式系统,我们首先需要约定用到的基本符号,对于本系列所介绍的lambda演算,其符号集包括λ . ()和变量名(x, y, z, etc.)。

1. λ 表达式/项

在lambda演算中只有三种合法表达式(也可以称之为项:λ-expression or λ-term)存在:

这时候可能就有人纳闷儿了,(λx.x) y意义很明确,但λy.xy为什么代表函数抽象而不是将函数λy.x应用于y的函数应用呢?为了消除类似的表达式歧义,可以多使用小括号,也有以下几个消歧约定可以参考:

  • 一个函数抽象的函数体将尽最大可能向右扩展,即:λx.M N代表的是一个函数抽象λx.(M N)而非函数应用(λx.M) N
  • 函数应用是左结合的,即:M N P意为(M N) P而非M (N P)

2. 自由变量和绑定变量

前面提到在函数抽象中,形参绑定于函数体,即形参是绑定变量,相对应地,不是绑定变量的自然就是自由变量。咱们来通过几个例子来理解这个关系:

由于每个lambda函数都只有一个参数,因此也只有一个绑定变量,这个绑定变量随着形参的变化而变化。
我们用FV来表示一个lambda表达式中所有自由变量的集合,如:

FV(λx.xy) = {y}
FV((λy.y)(λx.xy)) = FV(λy.y) ∪ FV(λx.xy) = {y}
FV(λx.(λy.xyz)) = FV(λy.xyz) \ x = {x,z} \ x = {z}

3. 柯里化(Currying)

有时候我们的函数需要有多个参数,这太正常不过了,但是lambda函数只能有一个参数怎么办?解决这个问题的方法就是柯里化(Currying)。
柯里化是用于处理多参数输入情况的方法,我们已经知道一个lambda函数的输入和输出也可以是函数,那么基于它,可以把多参数函数和单参数函数做以下转换:
λx y.x = λx.(λy.xy)
外层函数接受一个参数x返回一个函数λy.xy,这个返回函数(内层函数)又接受一个参数y返回xy,x绑定于外层函数,y绑定于内层函数,这样我们就在满足lambda函数只接受一个参数的约束下实现了多参数函数的功能,这就是柯里化,而λx y.x称为λx.(λy.xy)的缩写,为了方便表达,后续会常常出现λx y.x这样的书写方式,需要谨记它只是缩写写法。


lambda | λ 归约

我们已经知道了lambda表达式的基本定义与语法,下面将介绍如何对一个lambda表达式进行归约(reduction)

1. beta | β 归约

对于一个函数应用(λx.x) y,它意为将函数应用λx.x应用于y,等价于x[x:=y],即结果是y。在这个过程中,(λx.x) y ≡ x[x:=y]一步就叫做beta归约x[x:=y] ≡ y一步称作替换(substitution)[x:=y]意为将表达式中的自由变量x替换为y

x[x := N]       ≡ N
y[x := N]       ≡ y //注意 x ≠ y
(M1 M2)[x := N] ≡ (M1[x := N]) (M2[x := N])
(λx.M)[x := N]  ≡ λx.M //注意 x 是绑定变量无法替换
(λy.M)[x := N]  ≡ λy.(M[x := N]) //注意 x ≠ y, 且表达式N的自由变量中不包含 y 即 y ∉ FV(N)

细心的话可以注意到,替换规则中特别标注了一些x ≠ y或者y ∉ FV(N)等约束条件,它们的意义在于防止lambda表达式的归约过程中出现歧义。
比如以下过程:

(λx.(λy.xy)) y
= (λy.xy)[x:=y] //beta归约:注意 y ∈ FV(y) 不满足替换的约束条件
= λy.yy //替换:绑定变量y与自由变量y同名出现了冲突

可以看出在不满足约束条件的情况强行替换造成了错误的结果,那么对于这种情况该如何处理呢?那就需要alpha转换啦。

2. alpha | α 转换

这条规则就是说,一个lambda函数抽象在更名绑定变量前后是等价的,即:
λx.x ≡ λy.y
其作用就是解决绑定变量与自由变量间的同名冲突问题。
那么对于上面的那个错误归约过程就可以纠正一下了:

(λx.(λy.xy))y
= (λy.xy)[x:=y] //beta归约:注意 y ∈ FV(y) 不满足替换的约束条件
= (λz.xz)[x:=y] //alpha转换:因为绑定变量y将与自由变量x(将被替换为y)冲突,所以更名为z
= λz.yz

Perfect!这样对于lambda演算最基础的定义与归约规则已经介绍完毕了,虽然内容很简单,但是却很容易眼高手低,要试着练习喔。
下一篇将介绍丘奇编码(Church Encoding),体验lambda演算中万物皆函数的美妙哲学!

上一篇 下一篇

猜你喜欢

热点阅读