从鳄鱼蛋看 λ 演算

这篇文章是 Bret Victor 所著 《Alligator Eggs!》 的中文译文,已联系原作者取得授权。Bret Victor 在 2007 到 2011 年期间在苹果负责人机界面开发,参与设计了最初的 iPad,他的个人网站非常精美,文章也及其友好。更多关于他的信息可以参考维基百科上 Bret Victor 的词条

This Article is the Chinese translation for Alligator Eggs! (Written by Bret Victor).

准备材料

  • 第一步:将这个 PDF 文件 打印到六种不同颜色上。
  • 第二步:将这个 PDF 文件 打印到几张白纸上。
  • 第三步:把这些鳄鱼和鳄鱼蛋剪下来!

零件

下面这些是 饥饿的鳄鱼(彩色的):

饥饿的鳄鱼 需要进食。它们会吃掉任何在它们面前的东西!但是它们同时也是 负责任的 鳄鱼,所以它们还需要守护自己的家庭。

这些是 老鳄鱼

老鳄鱼们并不需要进食,它们已经吃饱了,而它们生活的唯一目标就是保卫自己的家庭。

这些是

蛋会孵化出新的鳄鱼家庭!

家庭

这是一个小家庭:

一条绿色的鳄鱼守护着她绿色的蛋。

这是一个稍大的家庭:

一条绿鳄鱼和一条红鳄鱼在一起保护着一个绿色的鳄鱼蛋和一个红色的鳄鱼蛋。或者,你也可以这么理解:一条绿色的鳄鱼正在保护着一条红色的鳄鱼,而这条红色的鳄鱼正在看护着这些蛋。

这是一个大家庭!

我们可以看到,各有一条黄色、绿色和红色的鳄鱼在守卫着这个家庭。它们守护着三个东西:一个绿色的鳄鱼蛋,一条老鳄鱼,以及一个红色的鳄鱼蛋。这条老鳄鱼还保护着一个黄色的鳄鱼蛋和一个绿色的鳄鱼蛋。
注意!鳄鱼蛋必须和它们保护者的颜色一致。换句话说,如果有一个蓝色的鳄鱼蛋,那就必须有一条蓝色的鳄鱼守护着它。

进食

现在事情开始变得复杂起来了。这是紧挨着的两个家庭:

毫无疑问,绿色的鳄鱼正处于饥饿状态。无独有偶,有一个黄色的鳄鱼家庭就在她面前。看起来似乎很好吃!

我想你已经知道马上会发生什么事。

不幸的是,绿色的鳄鱼有些高估自己的能力了。她吃得太多了!

这条绿色的鳄鱼去了鳄鱼天堂。但是,故事仍在继续。绿色鳄鱼死了之后,她所看护的绿色鳄鱼蛋开始孵化……

太神奇了,这个绿色鳄鱼蛋竟然孵化成了绿色鳄鱼刚刚吃掉的东西。这是生命的奇迹!

现在,它们又变成了一个家庭。这个家庭中有一条红鳄鱼守卫着一条黄鳄鱼和一个红鳄鱼蛋,而这条黄鳄鱼则守护着她的黄色鳄鱼蛋。

这条黄色鳄鱼当然也需要进食,何况她的面前恰好有一个美味的红色鳄鱼蛋。让我们再重复一次……

可怜的鳄鱼。对她的食量来说,即便是一个鳄鱼蛋也难以消化!

这条黄色的鳄鱼死了…… 但是同时,黄色的鳄鱼蛋也开始孵化……

黄色的鳄鱼蛋孵化出了黄色鳄鱼吃掉的东西。

现在已经没有任何鳄鱼有机会进食了,所以这个故事到这里可以停止了。

进食规则

上面所述的故事是这个游戏的第一条规则:进食规则

进食规则指的是,如果有一些紧挨着的家庭……

那么最左上角的鳄鱼会吃掉她右侧的整个鳄鱼家庭。

之后,进食的这条鳄鱼会死掉。但如果这条鳄鱼正在守卫着任何和她颜色相同的鳄鱼蛋,那么 每个 这样的鳄鱼蛋(与死去的鳄鱼颜色相同且被其守卫的)都会孵化出这条死去的鳄鱼刚刚吃过的东西。

颜色规则

继续上面的例子,橘黄色的鳄鱼吃掉了黄色的鳄鱼家庭,情况变成下面这样:

现在,左上角的绿色鳄鱼想要吃掉她右侧的鳄鱼家庭。但是在此之前,我们得检查一下这是否符合 颜色规则

颜色规则说的是,如果一条鳄鱼准备吃掉一个鳄鱼家庭,并且有一种颜色在 两个家庭(进食的鳄鱼所属的家庭和将要被吃掉的家庭) 中都出现了,我们就需要将其中一个家庭的这种颜色替换为其它颜色。

上面的图片中,绿色和红色同时出现在第一、第二个家庭中。因此,我们将第二个家庭中所有的绿色替换为浅蓝色,所有的红色替换为黄色。

现在各个家庭间没有相同的颜色了,鳄鱼们已经饥渴难耐!动嘴吧!

还可以吃!

继续!

直到没有东西可以被吃掉。

老鳄鱼

这个游戏还有一条与 老鳄鱼 有关的额外规则:

左上角的老鳄鱼并不会感到饥饿,她不需要吃任何东西,她的生命只会奉献给她的家庭。那么这个游戏该怎么继续下去呢?

当需要守护的东西只剩最后一样的时候,老鳄鱼会撒手鳄寰。现在,左上角的老鳄鱼同时看护着一个绿色的家庭和一个红色的家庭,这些家庭还需要她去照顾。但是现在,绿色的鳄鱼需要进食了,于是它吃掉了右侧的红色家庭……

现在,老鳄鱼只看护着一个家庭。这个家庭可以照顾自己了,老鳄鱼失去了存在的意义,所以她很快离去。

这就是 老龄规则。当一条老鳄鱼只看管着(直接看管)一样东西时,她就该离开这个世界了。

最后,红色的鳄鱼吃掉了黄色的家庭。

游戏

游戏包含一系列谜题,目标是让玩家设计一个家庭,使这个家庭在进食 X 后能够产出 Y。举个例子:

这是两个家庭,我们将左侧的家庭命名为 “True”,将右侧的家庭命名为 “False”:

这是一个名为 “Not” 的家庭:

当 “Not” 吃掉 “True” 的时候会产生 “False”,同样的,当 “Not” 吃掉 “False” 的时候会产生 “True”。那么,“Not” 中最底部的两个鳄鱼蛋应该是什么颜色呢?

(我们需要完善一下颜色规则:如果两个家庭颜色不同,但具有相同的模式,即相同位置的鳄鱼/蛋在两个家庭中的颜色能够建立起一一映射,就认为这两个家庭是等价的。)

这些谜题可以嵌入一些故事中。玩家必须依次解决谜题才能看到故事的发展。或者,这些谜题可以做成棋盘游戏。每个玩家通过选择鳄鱼死亡来解决到达目的地等问题。

理论

这个游戏实际表示了 无类型的 λ 演算饥饿的鳄鱼 是 λ 表示的抽象函数,老鳄鱼 是括号,鳄鱼蛋 是变量。进食规则 对应着 β-规约,颜色规则 对应着 α-变换。老龄规则 指的是,如果一对括号仅仅包含着单个不可分割表达式,那这对括号就可以被去除。

变换

奥利弗·斯蒂尔(Oliver Steele)指出,家庭角色对孩子的影响非常重要,这个游戏中的物品可以进一步变化为祖父母鳄鱼、鳄鱼家长和婴儿(蛋)等等。目前,变量名称是通过颜色表示的。这两者都是任意的,所以需要重命名/染色的规则去避免冲突。可以采用类似布鲁恩指数的替代方案,从而能够反应出生顺序和家庭关系。

奥利弗还建议,孩子们也许不会喜欢家长去世这一说法,所以鳄鱼的死亡可以解释为离开。

通过改变游戏规则,让饥饿的鳄鱼变得 贪婪,并吃掉一切在它们右侧的东西,我们就可以表示 右结合 的 λ 演算。和丘奇数、Y 组合子等相比,这种表示方法似乎去掉了许多老鳄鱼(括号)。不幸的是,这意味着当鳄鱼吃掉不止一样东西时,必须有老鳄鱼出生,同时也会产生一些其他问题。我仍然想找到一种让丘奇数(重复施用)看起来不那么丑陋的表示方法。

示意图

我发现 “鳄鱼演算” 的原理比手动计算 λ 表达式来的更容易。我们将 λ 画做一条带嘴的直线。括号是一条不带嘴的直线。这是恒等(identity)函数:

这是一些丘奇数:

这是布尔型操作 AND 和 OR:

Y 组合子:

我不知道它们 起来是不是比标准符号更容易些,但我发现在有纸笔的情况下它们确实更容易 处理 。想象一下,一个表达式吃掉另一个并将它在底部孵化。我不会再在一长串符号中迷失,忘掉该把哪个 λ 应用到哪个 λ 上。


英文原文链接: Alligator Eggs! (Written by Bret Victor)

原创作品,允许转载,转载时无需告知,但请务必以超链接形式标明文章原始出处(http://blog.forec.cn/2017/03/21/AlligatorEggs/) 、作者信息(Forec)和本声明。

分享到