追加がプリミティブ再帰的であることを示すには？

Question

どのようにして、追加がプリミティブ再帰的であるかを数字で示すとどうなりますか？

私はそれが原始的な再帰的な証明である理由を理解していますが、数字で再帰的にプリミティブがどのように機能するのか想像できません。

Answer 1

関数φがプリミティブ再帰的であることを示すには、定数、後続および射影関数で始まり、各関数が以前の関数から構図で構成されるように終わるφで終わる有限の反復関数のシーケンスを提供すれば十分です。原始的な再帰。原始再帰的加算機能は、P[m/n]がn >= 1とn <= mためにそのn番目の引数を返すm進投影関数である

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

定義されます。 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] 

それはあなたが求めているものを正確には不明だので、私はほかの原始再帰的定義の一般的な概要、さらには原始的であることの証明を与えました再帰的であり、計算例を提供しています。あなたがまだ不明な場合は、小さな値のプリミティブ再帰関数で計算を実行すると便利です。