如何发现Y组合子

我能想明白的一种Y组合子（游戏第4章“递归”第1题）的发现过程。 记号 本指南使用与游戏中略有不同的λ演算语法：将游戏中的“变量:”替换为“λ变量.”。 1、2、3、ZERO、MUL、PRE等记号与游戏第5章“数字”引入的同名记号含义相同。 记号“:=”表示将其右侧的表达式作为左侧记号的定义；“=>”表示其左侧的表达式可规约为其右侧的表达式。 动机 仿照一般编程语言，可以写出“递归”的阶乘函数： FACTO_1 := λn.ZERO n 1 (MUL n (FACTO_1 (PRE n)))但λ演算中实际上并没有声明、定义一个符号的操作，诸如ZERO、1等记号只是一种类似C语言中宏的语法糖，所以无法这样实现递归函数。 为了在函数中调用自己，它需要有个名字。我们可以给它增加一个参数表示函数本身，这样就可以用参数名代替函数名，递归调用自己了： FACTO_2 := λf. // 新增一个参数f表示函数本身 λn. ZERO n 1 (MUL n ( f f // 因为新增了参数，所以调用时也要传递进去 (PRE n) )) 调用该函数时，要像这样： FACTO_2 FACTO_2 2 但是这太丑了，在调用时要写两遍函数名，函数体内也要写两个f。但是，理想中的写法 FACTO := λf. λn. ZERO n 1 (MUL n ( f // 只写一个 f (PRE n) ))传入参数的个数不正确，根本是算不出预期结果的。由此想到，是否可以用某个高阶函数 Y “修饰”一下 FACTO，让 Y FACTO 变成一个递归函数呢？ 发现 Y 组合子 在之前定义的函数 FACTO_2 中，通过将函数自身传递给自身作为参数，实现了递归的功能。FACTO 与 FACTO_2 的唯一不同，即是将定义中的两个 f 替换成了一个 f。利用高阶函数 Y，将传递给 FACTO 的第一个参数 f 变成两个 FACTO，能否正确地实现递归呢？令 Y_0 := λf.计算3的阶乘： Y_0 FACTO 3 => FACTO (FACTO FACTO) 3 // 在这里调用形式是 FACTO (FACTO FACTO) n => MUL 3 (FACTO FACTO 2) // 在这里调用形式是 FACTO FACTO n => MUL 3 (MUL 2 (FACTO 1)) // 在这里调用形式是 FACTO n => 错误从中发现，随着“递归”的进行，FACTO的第一个参数f变得越来越“短”：只要f是有限个FACTO，这样的“递归”总会在充分大的次数后停止。因此，f应该能够自我复制，这样无论进行多少次规约，总还有新的f被传入FACTO。 考虑函数 t := λx. x x则 t t => (λx. x x) t => t t => ...t具有自己复制自己的功能。要让f能够自我复制，它应该像这样被调用：f f => FACTO (f f)。因为f与FACTO有关，所以f是某个高阶函数g对FACTO进行修饰后的结果，也就是f = g FACTO。将上式的f做替换可得：g FACTO (g FACTO) => FACTO (g FACTO (g FACTO))。写到这里，实际上我们已经找到了g。如果你没有注意到，直接把g的定义写出来就非常显然了：g := λr. λx. r (x x)。根据g的定义，我们可以写出Y，一个接受“递归”函数r做参数的高阶函数。Y的作用是将我们找到的自复制函数f f，也就是g r (g r)作为参数传递给r：Y := λr. r (g r (g r))。利用g的定义，可以写出等价的定义：Y := λr.对这个式子中的两个gr各规约一步，即可得到我们最熟知的Y组合子的形式： Y := λr.gr(gr) =>λr.(λx.r(xx))(λx.r(xx)) =>λf.(λx.f(xx))(λx.f(xx)) 最后