由一段垃圾代码想到的λ演算应用

发表于 | |

很久前看javascript函数式编程时，作者提到一段垃圾代码:

1
2
3
4
5
var f = function (f1) {
  return f2(function (x) {
     return f1(x);
  });
}

当时看到这段代码时，以为很高级，用到了高阶函数。其实不然，这是一段很经典的垃圾代码，因为经过一步步规约最后结果是f = f2。事实上，初学者很容易写出这样的代码，当时也不是很明白，直到最近看到λ演算中η-变换才豁然开朗。
首先介绍一下λ演算中η-变换规则:λx.f x -> f,用js描述就是var func = x => f(x),很明显可以得到func = f,同理可以对上面那段代码进行η-变换规约。其等价λ演算
λf1.f2 (λx.f1 x),利用η-变换进行规约如下:

1
2
3
4
5
6
7
λf1.f2 (λx.f1 x)
=> λf1.f2 f1
=> f2
// 还原成es6箭头函数
var f = f1 => f2(x => f1(x))
      =>f1 => f2(f1)
      =>f2

由此可知，了解λ演算，对于书写良好的函数式代码有一定用处，因为λ演算是函数式编程最重要的基石。假设你有js基础,下面介绍一下λ演算比较重要的基础知识点，以方便大家入门学习。
a.λ演算公式规则
形式化定义 所有的lambda表达式可以通过下述以BNF范式表达的上下文无关文法描述：

1
2
3
<expr> ::= <identifier>
<expr> ::= (λ<identifier> .<expr>)
<expr> ::= (<expr> <expr>)

规则说明:

  1. 函数的作用是左结合的
  2. λ操作符被绑定到它后面的整个表达式。举例说明一下:
    λf1.f2 (λx.f1 x) 和es6箭头函数的等价形式 f1 => f2(x => f1(x))
    对于规则1，如果知道lisp的话，就知道函数调用方式如(func . params)等价于js里的func(...params)也就不难理解了

b.自由变量和绑定变量
如果一个变量x没有在λ表达式中被绑定,比如λy . f x y，x和f是自由的，y被绑定的，在嵌套λ表达式中，相当于每一层形成一个闭包,内层自由变量可能被外层绑定而成为绑定变量。

c.α变换、β规约和η-变换

  1. α变换 名称不那么重要，如λx.f x <=> λy.f y
  2. β规约 λx.M)N -> M[x/N] 如果N中所有变量的自由出现都在M[x/N]中保持自由出现,比如(lx.ly.y x)(lz.u) -> ly.y(lz.u)
  3. η变换 比如f(x) = g(x)，也就是 f = (x => g(x)) = g，相反过程称为η展开

另外λ演算还可以用来描述其它比如自然数，逻辑运算等(邱奇编码)，这里不详细展开，因为有很多我也没看懂，有兴趣可以自己搜索看一下。