原始再帰関数

数理論理学において、原始再帰関数は原始再帰関数を高次の型理論に一般化したものである。原始再帰関数は、すべての純粋な有限型の関数の集合から構成される。

原始再帰関数は証明理論と構成的数学において重要であり、クルト・ゲーデルによって開発された直観主義算術の弁証法の解釈の中心的部分です。

再帰理論では、原始再帰関数はチューリング計算可能性の例であるのと同様に、原始再帰関数は高次型計算可能性の例です。

すべての原始的な再帰関数には型があり、型はどのような入力を受け取り、どのような出力を生成するかを示します。型 0 のオブジェクトは単なる自然数です。また、入力を受け取らずに自然数のセットNの出力を返す定数関数と見なすこともできます。

任意の 2 つの型 σ と τ について、型 σ→τ は、型 σ の入力を受け取り、型 τ の出力を返す関数を表します。したがって、関数f ( n ) = n +1 は型 0→0 です。型 (0→0)→0 と 0→(0→0) は異なります。慣例により、表記 0→0→0 は 0→(0→0) を指します。型理論の専門用語では、型 0→0 のオブジェクトは関数と呼ばれ、0 以外の型の入力を受け取るオブジェクトは関数と呼ばれます。

任意の 2 つの型 σ と τ について、型 σ×τ は順序付きペアを表します。このペアの最初の要素は型 σ を持ち、2 番目の要素は型 τ を持ちます。たとえば、関数A がNからNへの関数fと自然数nを入力として受け取り、f ( n ) を返すとします。この場合、A の型は (0 × (0→0))→0 です。この型は、カリー化によって 0→(0→0)→0 と記述することもできます。

(純粋な)有限型の集合は、0 を含み、× と → の演算に対して閉じている型の最小の集合です。上付き文字は、変数x ^{τ が}特定の型 τ を持つと想定されることを示すために使用されます。型が文脈から明らかな場合は、上付き文字を省略できます。

原始再帰関数は、次のような有限型のオブジェクトの最小の集合です。

• 定数関数f ( n ) = 0は原始的な再帰関数である。
• 後継関数g ( n ) = n + 1は原始再帰関数である。
• 任意の型σ×τに対して、関数K( x ^σ , y ^τ ) = xは原始再帰関数である。
• 任意の型 ρ、σ、τ に対して、関数

  S( r ^ρ→σ→τ , s ^ρ→σ , t ^ρ ) = ( r ( t ))( s ( t ))

  原始的な再帰関数である

• 任意の型τ、型τのf、および型0→τ→τの任意のgに対して、関数R ( f , g ) ^0→τは次のように再帰的に定義される。

  R ( f , g )(0) = f ,

  R ( f , g )( n +1) = g ( n , R ( f , g )( n ))

  原始的な再帰関数である

• 弁証法の解釈
• 高階関数
• 原始再帰関数
• 単純な型付けのラムダ計算

• Jeremy AvigadとSolomon Feferman (1999)。ゲーデルの機能的 (「弁証法」) 解釈(PDF)。S. Buss 編『証明理論ハンドブック』、North-Holland。pp. 337–405。