Check our new puzzle game!关于游戏functional is a puzzle game about math and abstraction. Solve problems and reuse your solutions to write ever-more-complex
我能想明白的一种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))
最后