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

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-ary 投影函数，为n >= 1 和n <= m 返回其nth 参数。为了证明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]

函数φ 由原始递归函数的公理提供。函数ψ是由步骤（4）中的原始递归函数S和P[3/3]组合而成的。最后，函数add是由步骤（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]

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