lambda演算

• BNF范式
• 阿尔法规约和贝塔规约
• Y-combinator

BNF范式

 ::= 

 ::= lambda . 

 ::= ( )

lambda可以视作匿名函数，如
(lambda x y.+ x y)
如何调用上述函数？
((lambda x y.+ x y) 2 3)
可以通过语法糖的方式得到命名函数
let add = (lambda x y. x + y)
(add 2 3)

阿尔法规约和贝塔规约

Alpha转换公理：例如，“lambda x y.+ x y”转换为“lambda a b.+ a b”。换句话说，函数的参数起什么名字没有关系，可以随意替换，只要函数体里面对参数的使用的地方也同时注意相应替换掉就是了。

Beta转换公理：例如，“(lambda x y. x + y) 2 3”转换为“2 + 3”。这个就更简单了，也就是说，当把一个lambda函数用到参数身上时，只需用实际的参数来替换掉其函数体中的相应变量即可。

Y-combinator

简单起见，考虑没有终止条件的递归求阶乘函数factorial
伪代码

factorial (n)
  return n * factorial(n - 1);

翻译成lambda，可以发现匿名函数中无法调用自己

lambda n.* n (<???> (- n 1))

为了解决这个问题，考虑加一个参数，并采用语法糖

let factorial = lambda n f.* n (f f (- n 1))  // 注意如何进一步递归时需要两个参数
(factorial factorial 5)                       // 也就是 factorial（factorial，5）

一个重要性质：函数即数据

现在引入不动点的概念

假设，我们已经构造出了一个完美的factorial，它可以以常规的方式递归自己(实际上lambda系统中无法定义出此函数)
let perfect_factorial = lambda n.* n (perfect_factorial (- n 1))
此外，定义出P函数，一个伪递归（注意进一步递归的时候不需要两个参数）
let F = lambda n f.* n (f (- n 1))
我们可以先给出F的f参数(perfect_factorial)，得到一个新的lambda函数
let new_F = lambda n.* n (perfect_factorial (- n 1))
那么，可以发现，new_F 和 perfect_factorial 没有区别，二者等价
即(F perfect_factorial) = perfect_factorial

那么对于P来说，perfect_factorial就是它的不动点
直观的说如果f(x) = x，x就是f的不动点

通过不动点的概念，我们可以推理出，对于任意的伪递归F
let F = lambda n f.* n (f (- n 1))
必然存在一个完美的f，使得(F f) = f

假设存在一个神奇的Y-combinator，当它作用于伪递归F时，可以求出P对应的完美的函数f
即Y(F) = f,结合上文中的F(f) = f,我们可以得到
Y(F) = f = F(f) = F(Y(F))
即Y(F) = F(Y(F))

显然

let Y = lambda F.

let f_gen = lambda self. F(self(self))

return f_gen(f_gen)