自然数的表示

理论上来说，任何可以『数出来』的东西，都可以用来表示自然数。当然，给『数出来』找一个严格的说法恐怕是很困难，甚至是『不可能解决』的问题。

这样看来，能够编码自然数的结构实在是太多太多了，数学家们喜欢用集合来编码，比如说：

0=∅S(n)={n}0 = \emptyset \\ S(n) = \{ n \}

这样一来11就是{∅}\{ \emptyset \}，22 就是 {{∅}}\{ \{ \emptyset \} \}，很显然地，这种结构形成了一个不断增长的{}\{ \}，可以表征自然数。

如果不用集合，也可以模仿小学时候的数数，用序列来定义自然数：

0=0S(n)=0.n0=0 \\ S(n)=0.n

这样一来，11就是0.00.0，22就是0.0.00.0.0。

用生成文法的角度去看，上面的两种定义都定义了一个『递归』的文法。其中第一种是『树形递归』，是『上下文无关文法』，第二种则是『线形递归』，是『正则文法』。如果仔细考察一下会发现：

  • 线形递归和自然数是等价的
  • 树形递归中包含线形递归

这样一来，只要一个（满足某种条件，如不能有歧义的）文法是递归的，那么它就可以编码自然数。

用于计算的自然数

回到本文的主题–邱奇数–上来，我们可以仿照上面的定义，给出一种『朴素』的λ\lambda表达式定义：

0=λx.xS(n)=λx.n0=\lambda{x}.x \\ S(n)=\lambda{x}.n

这样定义的自然数数11是λx.λx.x\lambda x.\lambda x.x.

不熟悉邱奇数的读者可能会产生疑惑：这个定义毫无疑问地编码了自然数，为什么邱奇不用这个定义而要用邱奇数呢？

简单来说，这样的定义是无法定义加法的，考虑加法的一般定义：

0+m=mS(n)+m=S(n+m)0 + m=m \\ S(n)+m = S(n + m)

要定义加法，需要两种能力：

  • 把一个数nn拆成(Sn′)=n(S n')=n，并获得n′n'的绑定的能力。
  • 根据不同的第一个参数进行不同的行为的能力。换句话说，必须使得00和其他自然数有『本质区别』，使得它可以被模式匹配地处理。

『朴素λ\lambda自然数』具有第一个能力，因为可以定义predpred：

pred(n)=nnpred(n)=nn

但是，『朴素λ\lambda自然数』不具有第二个能力。为什么呢？要回答这个问题，需要考察一下在普通的编程语言中是如何赋予自然数第二个能力的：

例如说，在Haskell中定义自然数：

data Nat = Zero | S Nat
  deriving (Show)

nAdd :: Nat -> Nat -> Nat
nAdd (S n) m = S (nAdd n m)
nAdd Zero m = m

注意到这两个nAdd ，它们是相同的函数，但却对不同的输入有不同的处理方式。

这样的需求在编程语言中被实现为

  • test指令，汇编语言
  • if，函数式与命令式语言（当然，if其实有两种情况）
  • match，case一类的模式匹配，如上面定义的nAdd，本质上就是模式匹配

考察纯λ\lambda表达式的特点，我们会发现，模式匹配的实现并不平凡。例如说，在λ\lambda表达式中实现if，可以这样写（注意，这样写并不完全正确）：

true=λxy.xfalse=λxy.yif=λxyz.xyztrue=\lambda xy.x \\ false = \lambda xy.y \\ if = \lambda xyz.x y z

结合上面的『朴素λ\lambda自然数』，可以发现：这种实现风格最大的特点是把计算的逻辑编码进数据中。这样实现出来的的数据可以叫做『函数式数据』。比如说这里的truetrue就是一个函数式数据，它和那种『头等（primitive）』的数据不同，头等数据本身并不具有计算能力，需要用一些操作头等数据的函数进行计算。比如scheme中的bool值：

> #t
#t
> #f
#f
> (if #t 1 2)
1
> (if #f 1 2)
2

这里的#t，#f都是头等数据，要用if这个操作符（或者说函数）来进行操作，本身并不编码任何计算逻辑。

所以，如果把『朴素λ\lambda自然数』当成一种头等数据，那么它确实具有第二个能力。但是，在λ\lambda表达式中不存在任何『头等数据』。所以，『朴素λ\lambda自然数』必须完全地视作一种函数式数据。如此一来，这种模式匹配的能力必须由它自己给出，或者说必须编码在它自己的结构之中。

为了完成这样的任务，自然会想到引入一个新的参数。不仅如此，还需要设计一套逻辑，使得为00的时候可以得到第一个参数的值，为其他的时候可以得到第二个参数的值。这里说的『得到』是严格的语句，它对应于『通过β\beta-规约，或者说函数调用得到』：

0xy=xn≠0→nxy=y0xy=x\\ n \not= 0 \rightarrow nxy=y

这和邱奇数已经比较接近了，但这个目标是很难做到的，因为我们还要同时保证结构的增长。

邱奇解决这个问题的办法是：

  • (λxy.y)x′y′(\lambda xy.y)x'y'显然是y′y'
  • (λxy.xy)(λx.x′)y′(\lambda xy.xy)(\lambda x.x')y' 显然是x′x'

这样一来，如果使得xx增长，换句话说就是构造xnyx^n y的结构，λxy.xny\lambda xy.x^ny就满足了前面所要求的性质（的一种变种）。

邱奇数不是唯一一种能够编码自然数的λ\lambda表达式结构，但它也许是最简单、最直接的正确结构。然而这种结构大部分人恐怕绝对不会喜欢，可见λ\lambda表达式这种『函数式数据』不是什么特别好的设计。当然，它是证明λ\lambda表达式潜力无穷的有力武器，但在现实世界中实在是难堪大用。也许，scheme的日渐式微也与此有关吧～