现代魔法构成论:多变量不动点组合子

Belleve Invis · 2014-05-18

对函数式语言理论了解者很多都知道著名的不动点组合子:

Y = lambda f. ~ f ~ (Y ~ f)Y=λf.f(Yf)

使用它,我们可以定义递归函数:

fib rm = Y ~ (lambda f . ~ lambda x . ~ if rm ~ (x > 0) ~ (x times (f ~ (x - 1))) ~ (1))fib=Y(λf.λx.if(x>0)(x×(f(x1)))(1))

当然你们也看到了,YY 组合子并不支持间接递归。但是这并不代表间接递归是不可实现的。考虑下面的式子:

odd rm_r odd{r} = = lambda x . ~ (x = 1) vee (even rm ~ (x - 1)) λx.(x=1)(even(x1))
even rm_r even{r} = = lambda x . ~ (x = 0) vee (odd rm ~ (x - 1))λx.(x=0)(odd(x1))

套用在上面 fib rmfib 里相似的技术,我们有:

odd rm _ i odd{i} = = lambda o. ~lambda e. ~lambda x . ~ (x = 1) vee (e ~ (x - 1)) λo.λe.λx.(x=1)(e(x1))
even rm _ i even{i} = = lambda o. ~ lambda e. ~lambda x . ~ (x = 0) vee (o ~ (x - 1)) λo.λe.λx.(x=0)(o(x1))
odd rm odd = = Y^2_1 ~ odd rm _ i ~ even rm _ i Y{21}odd{i}even{i}
even rm even = = Y^2_2 ~ odd rm _ i ~ even rm _ iY{22}odd{i}even{i}

在这里,odd rm _iodd{i}even rm _ ieven{i} 是「不完整」的两个函数,Y^2_{{1, 2} set}Y{2{1,2}} 则构造出两个完整的递归函数出来。显而易见,Y^2Y{2}要满足:

Y^2_1 ~ f ~ g Y{21}fg = = f ~ (Y_1^2 ~ f ~ g) ~ (Y_2^2 ~ f ~ g) f(Y{21}fg)(Y{22}fg)
Y^2_2 ~ f ~ g Y{22}fg = = g ~ (Y_1^2 ~ f ~ g) ~ (Y_2^2 ~ f ~ g)g(Y{21}fg)(Y{22}fg)

故而:

odd rm odd = = Y^2_1 ~ odd rm _ i ~ even rm _ iY{21}odd{i}even{i}

对于有 nn 个函数的一般情形,Y^n_mY{nm} 的定义是:

Y^n_m Y{nm} = = lambda f_1 . ~ lambda f_2 . ~ ... lambda f_n . ~f_m ~ (Y^n_1 ~ f_1 ~ ... ~ f_n) ~ (Y^n_2 ~ f_1 ~ ... ~ f_n) ~ ... ~ (Y^n_n ~ f_1 ~ ... ~ f_n)λf{1}.λf{2}....λf{n}.f{m}(Y{n1}f{1}...f{n})(Y{n2}f{1}...f{n})...(Y{nn}f{1}...f{n})

如果 Y^nY{n} 的传入参数换成一个列表(当然「未完成」函数也改为 (lambda phi . ~ ...)(λφ....) 这种形式,其中 phiφ 是参与间接递归的函数列表),则可以写出一个「泛用」的不动点函数:

Y^{*} Y{} = = lambda psi . ~ map rm ~ psi ~ (lambda f . ~ f ~ ("map-index" rm ~ psi ~ (lambda i . ~ (Y^{*} ~ psi)_i ))) λψ.mapψ(λf.f(map-indexψ(λi.(Y{}ψ){i})))
= = Y ~ (lambda y^{*}.~ lambda psi . ~ map rm ~ psi ~ (lambda f . ~ f ~ ("map-index" rm ~ psi ~ (lambda i . ~ (y^{*} ~ psi)_i )))) Y(λy{}.λψ.mapψ(λf.f(map-indexψ(λi.(y{}ψ){i}))))
= = (lambda f . ~ (lambda x . ~ f ~ (x ~ x)) ~ (lambda x . ~ f ~ (x ~ x)))(lambda y^{*}.~ lambda psi . ~ map rm ~ psi ~ (lambda f . ~ f ~ ("map-index" rm ~ psi ~ (lambda i . ~ (y^{*} ~ psi)_i ))))(λf.(λx.f(xx))(λx.f(xx)))(λy{}.λψ.mapψ(λf.f(map-indexψ(λi.(y{}ψ){i}))))

Y^{*}Y{} 的加持下,实现间接递归就简单多了:

odd rm _ i odd{i} = = lambda (o, e). ~lambda x . ~ (x = 1) vee (e ~ (x - 1)) λ(o,e).λx.(x=1)(e(x1))
even rm _ i even{i} = = lambda (o, e). ~lambda x . ~ (x = 0) vee (o ~ (x - 1)) λ(o,e).λx.(x=0)(o(x1))
(odd rm, even rm) (odd,even) = = Y^{*} ~ (odd rm _ i, even rm _ i)Y{}(odd{i},even{i})