一句话:从丘奇数与Kleene表示出发,系统推导出更小、更快、更精确的前驱函数表示。
λ演算自始以迭代应用表示自然数:后继增加一次应用,前驱则需“撤销”应用,这长期被视为困难,连Church也认为不可能。Kleene曾以迂回视角找到一种相关表示,使前驱更易定义。本文用现代视角重审这一经典问题,梳理系统化推导方法,从丘奇数及其变体生成更多前驱函数表示,并比较其大小、速度与精确性,同时保持正确性与基本性质。结果是一组可系统推导、简洁性与性能各异的前驱实现,揭示了表示选择对λ演算数值编码的影响。
Abstract From the outset, lambda calculus represented natural numbers through iterated application. The successor hence adds one more application, and the predecessor removes. In effect, the predecessor un-applies a term—which seemed impossible, even to Church. It took Kleene a rather oblique glance to sight a related representation of numbers, with an easier predecessor. Let us see what we can do if we look at this old problem with today’s eyes. We discern the systematic ways to derive more predecessors—smaller, faster, and sharper—while keeping all teeth.