递归和定点
纯λ演算的一大特色是可以通过使用一种自应用技巧来书写递归函数。
f(n) = if n = 0 then 1 else n*f(n-1)
f = λn.if n = 0 then 1 else n*f(n-1)
把f移到等式的后面,得到函数G
G = λf.λn.if n = 0 then 1 else n*f(n-1)
很显然有:
f = G(f)
这表明递归声明涉及找出定点。 函数G的定点是指满足f=G(f)的f的值。在λ演算中,定点由定点操作符Y来定义。 具体的推导过程可以参考我的上一篇文章Y-Combinator的推导。
Y = λf.(λx.f(x x))(λx.f(x x))
Ruby 版本
def y(&gen)
lambda {|g| g[g] }.call(lambda{|f| lambda {|*args| gen[f[f]][*args] }})
end
factorial = y do |recurse|
lambda do |x|
x.zero? ? 1 : x * recurse[x-1]
end
end
puts factorial.call(10)
Python 版本
def y_combinator(gen):
return (lambda g: g(g))(lambda f: (lambda *args: (gen(f(f)))(*args)))
ret = y_combinator(lambda fab: lambda n: 1 if n < 2 else n * fab(n - 1))(10)
print(ret)
JavaScript 版本
function y(gen) {
return (function(g) {
return g(g);
})(function(f) {
return function(args){
return gen(f(f))(args);
};
});
}
var fact = y(function (fac) {
return function (n) {
return n <= 2 ? n : n * fac(n - 1);
};
});
console.log(fac(5));
Clojure 版本
(defn Y [gen]
((fn [g] (g g))
(fn [f]
(fn [n] ((gen (f f)) n)))))
(defn fac-gen [f] (fn [n] (if (<= n 0) 1 (* n (f (dec n))))))
(assert (= ((Y fac-gen) 5) 120))