自然数的表示

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

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

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.022就是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,并获得nn'的绑定的能力。
  • 根据不同的第一个参数进行不同的行为的能力。换句话说,必须使得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其实有两种情况)
  • matchcase一类的模式匹配,如上面定义的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=xn0nxy=y0xy=x\\ n \not= 0 \rightarrow nxy=y

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

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

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

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

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