在定义自然数之前，我们要理解数学上的自然数是怎么定义的

皮亚诺公理 Peano Axioms

这个公理经常被营销号拿来作秀，即为什么$1+1=2$的问题

皮亚诺公理体系 Peano Axioms针对于一个给定的三元组$(A,0,(.)^)$ 其中的集合$A$是待检验的自然数集合，$0$是$A$中的一个元素，$(.)$代表后计算符，表示$A\rightarrow{A}$的映射

  • Axiom 1 : 0是自然数 ($0 \in A$)
  • Axiom 2 : 如果$n$是自然数，则它有一个后继$n^*$，且后继也为自然数
  • Axiom 3 : 0不是任何自然数的后继 ($\forall n \in A\ :\ n^*\neq 0$)
  • Axiom 4 : $n\mapsto n^$是单射 ($\forall n,m\in A:n\neq m \Rightarrow n^\neq m^*$)
  • Axiom 5 : 对于命题$P$，若$P$对$0$成立，且$P$对$n$成立蕴涵$P$对$n^*$成立，则$P$对任意自然数皆成立
  • 其中公理1,2确定了取自然数的方法
  • 公理3,4,5分别确保了“0前面无自然数”，“一个自然数后面只有唯一的一个自然数”，“没有孤岛，闭环存在”。
  • 另外，仔细看，公理五其实类似于第一类数学归纳法，即对$0$成立 / 若$n$成立，则$n^*$也成立，则命题对所有自然数均成立

邱奇数 Church numeral

你会发现，你很难在Lambda演算的体系中去定义一个数字，所以这里我们引入邱奇数 Church Numeral

我们假设$0$，即起点为$A$，后继函数为$f(n)$，也就有$0=0$，$1=f(0)$，$2=f(f(0))$……
当然，这里的$0$我们更应该理解为一个变量，即$x$ 我们可以规定$x$为$0$，此时的三元组即为$(A,x,f)$，那么自然数$n$就可以表示为 \(n=f^n(x)\)

[!attention] 再次强调 这些自然数实际上是函数！他们接收两个值，即表示$0$的$x$和后继函数$f$，即 \(n\equiv(\lambda{fx}.(f^n\ x))\) 所以自然数的作用实际上是将$f$应用于$x$n次! 另外，先不要管$f^n$要如何表示，我们先利用自然数函数解决下面的问题

后继函数 Succession Function

这样就很轻松的定义了自然数——即一个后继函数 succession function$f$的调用次数 但这也引出了一个新的问题——后继函数 succession function是什么呢？

不妨类比一下现存的自然数体系，我们把后继运算符$()^*$具象化为一个函数$succ(n)$，既有 \(succ(n)=n+1\)

那么在Lambda演算中，我们定义的后继函数需要接受一个函数，并返回一个对这个函数运用了一次后继函数之后的函数

  1. 接收一个数字 $(\lambda n.(\ ))$
  2. 返回一个数字 $(\lambda n.(\lambda{fx}.\ )$
  3. 思考一下，我们返回的数字应当是n+1，所以有 $(\lambda n.(\lambda{fx}.(f\ (n\ f\ x)))$

这样，我们就得到了后继函数$succ(n)\equiv (\lambda n.(\lambda{fx}.(f\ (n\ f\ x)))$

后继类运算的定义

[!attention] 再次注意 四则运算的结果也是自然数函数，所以它的返回理所应当的也应该是一个接收f和x的函数!

当我说后继，我指的是自然数不断增大的计算，这是非常好理解的，毕竟皮亚诺定理做的也是单射，即$x\mapsto x*$，但是并没有内置的前驱函数。这个我们在之后解决，先来解决好解决的后继问题

加法
  1. 接收两个数字 $(\lambda mn. )$
  2. 思考，要计算$m+1$实际上等价于$succ(m)$，所以$m+n$等价于$succ^n(m)$
  3. 易知有 $(\lambda mn. (n\ succ\ m))$
  4. 进一步思考，我们意识到这等同于 $(\lambda mn. (m\ succ\ n))$，于是得到加法交换律

所以加法的式子为 \((\lambda mn. (n\ succ\ m))\) 可以化简为 \((\lambda{mn.}(\lambda{fx.(m\ f\ (n\ f\ x))}))\)

[!tip] 理解一下，$(n\ f\ x)$相当于$n$的定义，所以下一层就有$(m\ f\ n)$，即，将$f$应用于$n$ $m$次，也就有了$m+n$

乘法

有了加法，乘法也很好理解了 \((\lambda mn. (\lambda fx.(m\ (n f)\ x)))\) 就是m次将n次f应用于x，也就是m*n。现在我们对其进行柯里化和η等价，有 \(\lambda mnf. (m\ (n f))\)

幂运算

\(λmn.(λfx.((n\ m\ f)\ x))\) 幂运算出人意料的简介，不过仔细思考，这是合理的

  • 自然数函数接收两个值，即$f$与$x$，这里$n$接收$m$和$f$。
  • 光一次$m$应用于$f$即为$f^m$，那么$n$次的将$m$应用于$f$，即为$f^{m^n}$

[!danger] 关于η等价的注意事项 之所以幂函数的$f$能被等价，而上面的乘法不能被等价，是因为$f$在这里是作为单独一个函数存在的，而乘法中的f和n被绑在了一起，作为一个全新函数出现

前驱类运算的定义 / 减法的定义

这里说的前驱类运算单指减法，除法更加棘手 由于没有内置的前驱函数，我们需要手动定义一个。当然这并不像链表一样用一个下标访问前驱地址就行了。在这里，如果我们要“访问”前驱，就得重新模拟一遍加法的过程，直到当前数的前一个数。

前驱拓展

要做到这一点，我们需要在计算时同时记录当前数和前一个数，由此，我们相当可以创建一个数据类型，即$pair$数对，如果需要其中的任何一个值，只需要使用选择器即可 \(pair := (\lambda abz.(z\ a\ b))\) 这里的$z$就是选择器，你需要“手动填入”的只是$a$和$b$，输入$TRUE$和$FALSE$即可，我们大可再定义两个函数$fst$和$snd$，这里的$p$就代表一个$pair$类型 \(\displaylines{ fst = \lambda p.(p\ TRUE)\\ snd= \lambda p.(p\ FALSE) }\)

接下来，我们要将数对作为新的基底去运算，即一个新的后继函数$\varphi(p)$，应当做到输入$(prev,curr)$返回$(prev+1,curr+1)$，即$(curr,curr+1)$ \(\varphi:=\lambda p.(pair\ (snd\ p)\ (succ\ (snd\ p)))\) 那么就会有， \((\varphi\ (pair\ 0\ 0)) = (0,1)\) 因为“新的数对的前者”取的是“旧数对的后者”，所以0也就留了下来，这样，在$\varphi$对$(pair\ 0\ 0)$进行$n$次运算后，也就得到了$(n-1,n)$

前驱函数

不妨令前驱函数为$pred$，则有 \(pred :=\lambda n. (fst\ (n\ \varphi\ (pair\ 0\ 0)))\) 这样，我们就得到了减法函数，虽然无法得到负数 \(\lambda mn.(n\ pred\ m)\)