帰納的再帰

直観主義型理論（ITT）は数理論理学の一分野であり、帰納再帰は型とその型に対する関数を同時に宣言するための機能である。これにより、帰納型よりも大きな型、例えば宇宙などを作成することが可能となる。作成された型は、ITT内では依然として述語的である。

帰納的定義は、ある型の要素を生成するための規則によって与えられます。そして、その型の要素が生成される方法について帰納的に定義することで、その型の関数を定義することができます。帰納的再帰は、この状況を一般化します。なぜなら、型の要素を生成するための規則が関数を参照することが許されているため、型と関数を同時に定義できるからです。 ^{[ 1 ]}

帰納的再帰を用いることで、様々な宇宙構造を含む大規模な型を定義することができる。これは型理論の証明論的な強度を大幅に高める。しかしながら、帰納的再帰による定義は依然として述語的であるとみなされる。

帰納的再帰は、マルティン＝レーフの直観主義型理論の規則に関する研究から生まれた。この型理論には多数の「型形成子」があり、それぞれに4種類の規則がある。マルティン＝レーフは、各型形成子の規則がパターンに従っており、それが型理論の特性（例えば、強い正規化、述語性）を保持していることを示唆していた。研究者たちは、このパターンの最も一般的な記述を探し始めた。なぜなら、それが型理論を拡張するためにどのような種類の型形成子を追加できるか（あるいは追加できないか）を教えてくれるからである。

「宇宙」型の定義が最も興味深かった。なぜなら、規則を「タルスキ流」に記述すると、「宇宙型」と、それに対して作用する関数が同時に定義されるからである。これが最終的にディビャーを帰納的再帰へと導いた。

Dybjer の最初の論文では、帰納的再帰を規則の「スキーマ」と呼んでいました。それは、どのような型フォーマーを型理論に追加できるかを述べていました。後に、彼と Setzer は、型理論内で新しい帰納的再帰的定義を作成できる規則を備えた新しい型フォーマーを作成しました。^{[ 2 ]}これは、Half証明支援システム( Alfの変種) に追加されました。

帰納的再帰型について説明する前に、より単純なケースである帰納型について説明します。帰納型のコンストラクタは自己参照できますが、制限があります。コンストラクタのパラメータは「正」でなければなりません。

• 定義中の型を参照しない
• 定義される型と完全に一致するか、
• 定義対象の型を返す関数であること。

帰納型では、パラメータの型は先行するパラメータに依存することができますが、定義中の型のパラメータを参照することはできません。帰納再帰型はさらに進んで、パラメータの型は、定義中の型を使用する先行するパラメータを参照することができます。これらのパラメータは「半正」でなければなりません。

• 定義中の関数に前のパラメータがラップされている場合、そのパラメータに依存する関数となる。

だから、もし${\displaystyle D}$定義されている型であり、${\displaystyle f}$関数が（同時に）定義されている場合、これらのパラメータ宣言は正です。

• ${\displaystyle a:A}$
• ${\displaystyle d:D}$
• ${\displaystyle g:A\to {\mathsf {Type}}}$
• ${\displaystyle h:A\to D}$
• ${\displaystyle i:A\to B\to D}$
• ${\displaystyle j:g\ a}$ （以前のパラメータに依存しますが、そのどれも型ではありません）${\displaystyle D}$）

これは半分肯定的な結果です。

• ${\displaystyle k:(f\ d)\to D}$ （パラメータによって異なります）${\displaystyle d}$タイプの${\displaystyle D}$しかし、電話を通じてのみ${\displaystyle f}$）

これらは肯定的でも半肯定的でもない。

• ${\displaystyle k:D\to A}$ （${\displaystyle D}$（これは関数の引数です。）
• ${\displaystyle l:(A\to D)\to A}$ （このパラメータは、${\displaystyle D}$しかし、${\displaystyle A}$自体。）
• ${\displaystyle m:z\ d}$ （${\displaystyle d}$タイプの${\displaystyle D}$しかし、その機能を通してではない${\displaystyle f}$）

簡単な一般的な例としては、タルスキ流の宇宙の型フォーマーが挙げられます。これは型で構成されています。${\displaystyle U}$そして関数${\displaystyle T:U\to {\mathsf {Type}}}$要素がある${\displaystyle U}$型理論のすべての型について（ただし${\displaystyle U}$それ自体！）、そして関数${\displaystyle T}$要素をマッピングします${\displaystyle U}$関連する型に。

タイプ${\displaystyle U}$型理論における各型形成型に対して、コンストラクタ（または導入規則）が存在する。依存関数に対するコンストラクタは次のようになる。

${\displaystyle {\mathsf {constructor}}_{\Pi }(u:U)(u':T(u)\to U):U}$

つまり、要素を取る${\displaystyle u}$タイプの${\displaystyle U}$パラメータの型にマッピングされる関数${\displaystyle u'}$すべての値に対して${\displaystyle x:T(u)}$、${\displaystyle u'(x)}$関数の戻り値の型にマッピングされます（これはパラメーターの値に依存します）。${\displaystyle x}$（最終版）${\displaystyle :U}$コンストラクタの結果は、型の要素であると述べています。${\displaystyle U}$）

還元（または計算規則）によれば、${\displaystyle T({\mathsf {constructor}}_{\Pi }(u,u'))}$に縮小${\displaystyle \prod _{x:T(u)}T(u'(x))}$。

縮小後、関数${\displaystyle T}$入力のより小さな部分で動作している。それが成り立つ場合${\displaystyle T}$任意のコンストラクタに適用すると、${\displaystyle T}$必ず終了します。

帰納的再帰はAgdaとIdrisで実装されています。^{[ 3 ]}

• 帰納法- 型と型のファミリーを同時に定義するさらなる作業

• ピーター・ディビャーの帰納法および帰納再帰に関する出版物一覧
• 帰納法と再帰、およびその派生概念を扱ったスライド