如何证明加法是原始递归的？

Question

我如何在一个例子中显示加法是原始递归的。

我通过证明理解为什么它是原始递归的，但我无法想象它是如何以原始递归方式处理数字的。

Answer 1

为了证明一个函数?是原始递归的，提供一个有限的原始递归函数序列就足够了，这些原始递归函数以常量函数、后继函数和投影函数开始，并以?这样的方式结束，每个函数都是通过组合和原始递归从先验函数构造出来的。定义了原始递归加法函数

add(0,x)     = ?(x)
add(n + 1,x) = ?(n,x,add(n,x))
  where ? = P[1/1]
        ? = S ? P[3/3]

其中P[m/n]是m进制投影函数返回其n用于个参数n >= 1和n <= m。为了证明这add是原始递归，我们必须从基本函数构造?和?：

1. P[1/1]                [Axiom]
2. P[3/3]                [Axiom]
3. S                     [Axiom]
4. S ? P[3/3]            [1,3 Composition]
6. PR(P[1/1],S ? P[3/3]) [1,4 Primitive Recursion]

该函数?由原始递归函数的公理提供。该函数?由原始递归函数S和P[3/3]步骤（4）的组合构成。最后，该函数add是通过原始递归从步骤 (6)?和?在步骤 (6) 中构造的。要了解如何通过原始递归函数（例如 ）计算值add，只需在适当的情况下系统地替换函数定义的右侧，然后进行简化即可。我在以下示例中折叠了替换和简化组合：

add(2,3) = S(P[3/3](1,3,add(1,3)))                 [Def. ?]
         = S(P[3/3](1,3,S(P[3/3](0,3,add(0,3)))))  [Def. ?]
         = S(P[3/3](1,3,S(P[3/3](0,3,P[1/1](3))))) [Def. ?]
         = S(P[3/3](1,3,S(P[3/3](0,3,3))))         [Def. P[1/1]]
         = S(P[3/3](1,3,S(3)))                     [Def. P[3/3]]
         = S(P[3/3](1,3,4))                        [Def. S]
         = S(4)                                    [Def. P[3/3]]
         = 5                                       [Def. S]

不清楚你在问什么，所以我对加法的原始递归定义进行了一般概述，证明了加法是原始递归的，并提供了一个示例计算。如果您仍然不清楚，对原始递归函数的小值执行计算可能会有所帮助。