帰納構造と帰納原理

「帰納的型とリカーサー」と「帰納原理を完全に書き下す」において、自然数上の帰納原理について述べました。自然数に限らない一般的な帰納構造に対する帰納原理について述べます。帰納原理を確認したい動機は、形式体系の健全性〈soundness〉を証明するときの基盤となるからです。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\msf}[1]{\mathsf{#1}}
\newcommand{\twoto}{\Rightarrow }
%\newcommand{\thrto}{\Rrightarrow }
\newcommand{\In}{\text{ in }}
\newcommand{\op}{\mathrm{op}}
%\newcommand{\id}{\mathrm{id}}
\newcommand{\u}[1]{\underline{#1}}
\newcommand{\o}[1]{\overline{#1}}
%\newcommand{\hyp}{ \text{－} }
%\newcommand{\Iff}{ \Leftrightarrow }
\newcommand{\Imp}{ \Rightarrow }
\newcommand{\parto}{ \supset\!\to }
\newcommand{\def}{ \mathrm{def} }
\newcommand{\img}{ \mathrm{img} }
`$

内容：

• 記法の約束
• 部分関数
• 帰納構造
• 帰納閉包
• 実例： ツリー達の集合
• 演繹系から作る帰納構造
• 帰納的部分集合
• モーティブ
• リカーサー
• おわりに

記法の約束

$`X`$ を集合、$`F`$ を $`X`$ 上のファミリー〈インデックス付き集合族〉とします。このとき、シグマ型とパイ型は次のように書きます。

$`\quad \sum(X \mid F) = \sum(x\in X \mid F(x))`$
$`\quad \prod(X \mid F) = \prod(x\in X \mid F(x))`$

ファミリー〈族〉の合併も同様な書き方をします。

$`\quad \bigcup(X \mid F) = \bigcup(x\in X \mid F(x) )`$

ファミリー自体は次のように書きます。

$`\quad F = (x\in X\mid F(x))`$

これは、次のラムダ記法とまったく同じです。

$`\quad F = \lambda\, x\in X. F(x)`$

下付きを使って書いてもかまいません。

$`\quad \sum(X \mid F) = \sum_{x\in X} F(x)`$
$`\quad \prod(X \mid F) = \prod_{x\in X} F(x)`$
$`\quad \bigcup(X \mid F) = \bigcup_{x\in X} F(x)`$
$`\quad F = (F(x))_{x\in X}`$

集合 $`A, B`$ に対する関数集合〈関数空間型〉は次のいずれかで書きます。

$`\quad \mrm{Map}(A, B) = [A, B] = B^A`$

部分関数

部分関数〈部分写像〉 $`f`$ は、集合達と部分関数達の圏 $`\mbf{Partial}`$ の射です。

$`\quad f: A \to B \In \mbf{Partial}`$

部分関数を集合圏内で表現するときは、次の図式を使います。

$`\quad A \hookleftarrow \def(f) \overset{\u{f}}{\to} B \In \mbf{Set}`$

ここで、$`\def(f)`$ は部分関数 $`f`$ の定義域、矢印 $`\hookleftarrow`$ は部分集合の包含写像です。上記の $`\u{f}`$ は全域関数、つまり集合圏の射です。上記図式の略記（$`\def(f)`$ の情報は省略）として以下の記法も使います。

$`\quad f: A \parto B \In \mbf{Set}`$

以下の3つは、書き方が違うだけで完全に同義です。

1. $`f: A \to B \In \mbf{Partial}`$
2. $`A \hookleftarrow \def(f) \overset{\u{f}}{\to} B \In \mbf{Set}`$
3. $`f: A \parto B \In \mbf{Set}`$

$`f: A \parto B`$ に対して、全域関数と同様に、部分集合の像〈image of a subset〉を定義できます。

$`\text{For }f : A \parto B \In \mbf{Set}\\
\text{For }S \subseteq A\\
\quad f_*(S) :=
\{y\in B \mid \exists x\in A.\, x\in S \land x\in \def(f)\land y = f(x)\}
`$

$`f`$ が部分関数であったとしても、$`f_*`$ は以下のような関数〈全域関数〉になります。

$`\quad f_* : \mrm{Pow}(A) \to \mrm{Pow}(B) \In \mbf{Set}`$

部分関数 $`f`$ と全域関数 $`f_*`$ をオーバーロードすると分かりにくくなるので、部分集合にその像を対応させる関数は必ず下付きアスタリスクを付けることにします。

部分関数 $`f: A\parto B`$ の像〈image of $`f`$〉は次のように定義します。

$`\quad \img(f) := f_*(\def(f))`$

記法を揃えるために、$`S\subseteq A`$ に対しても：

$`\quad \img(f, S) := f_*(\def(f)\cap S) = f_*(S)`$

次の関係があります。

$`\quad \img(f) = \img(f, A) = f_*(A)`$

帰納構造

構造帰納法〈structural induction〉を遂行する舞台となる構造を帰納構造と呼ぶことにします。帰納構造〈{induction | inductive} structure〉は次の構成素を持ちます。

$`\quad (X, I, n, (C_i)_{i\in I}, X_0)`$

ここで：

1. $`X\in |\mbf{Set}|`$ は台集合〈underlying set〉
2. $`I\in |\mbf{Set}|`$ はインデキシング集合〈indexing set〉
3. $`n : I \to \mbf{N}`$ はアリティ関数〈arity function〉
4. $`(C_i)_{i\in I}`$ は構文的コンストラクタ達のファミリー〈family of syntactic constructors〉（後述）
5. $`X_0\subseteq X`$ はベース集合

帰納構造の条件として、$`X, I, X_0`$ はどれも空ではないとします*1。

1. $`X \ne \emptyset`$
2. $`X_0 \ne \emptyset`$
3. $`I \ne \emptyset`$

$`C_i`$ は次のような部分関数です。$`n(i)`$ は $`C_i`$ の引数の項数〈アリティ〉を与えます。

$`\quad C_i : X^{n(i)} \parto X \In \mbf{Set}`$

この関数を構文的コンストラクタ〈syntactic constructor〉と呼びます。帰納構造は公理的に定義されるので、構文的コンストラクタが構文とは何の関係もなくても別にかまいませんが、多くの実例では構文に関係します。

構文的コンストラクタに要求される条件は以下です。

1. $`\def(C) \ne \emptyset`$
2. $`\def(C) \cap \img(C) = \emptyset`$

構文的コンストラクタ達のファミリーの条件は以下です。

• $`\forall i, j\in I. i \ne j \Imp \img(C_i)\cap \img(C_j) = \emptyset`$

これで、帰納構造の定義は済みました。

帰納閉包

順序数 $`\theta`$ を固定します（順序数については「順序数と集合圏」参照）。帰納構造 $`(X, I, n, (C_i)_{i\in I}, X_0)`$ に対して、集合 $`\o{X_0}^\theta`$ を定義します。

まず、$`\theta`$ の要素でインデックス付けられた部分集合達の族 $`D`$ を定義します。$`\xi \in \theta`$ に対する $`D_\xi`$ は：

• $`\xi = 0`$ のとき： $`D_\xi = D_0 := X_0`$
• $`\xi = \chi + 1`$ のとき： $`D_\xi := D_\chi \cup \bigcup(i\in I\mid \img(C_i, {D_\chi}^{n(i)} ))`$
• $`\xi`$ が極限順序数のとき： $`D_\xi := \bigcup(\chi \in \xi \mid D_\chi)`$

構文的コンストラクタの条件から、二番目の定義に出てくる合併は直和とみなせます。直和（足し算）を使って書くと分かりやすいかもしれません。

$`\quad D_{\chi + 1} := D_\chi + \sum_{i\in I} {C_i}_*({D_\chi}, \cdots , {D_\chi})`$

上記の定義により、$`D: \theta \to \mrm{Pow}(X)`$ が決まります。$`\o{X_0}^\theta`$ は、$`\theta`$ が後者順序数か極限順序数かに関係なく以下のように定義します。

$`\quad \o{X_0}^\theta := \bigcup(\xi \in \theta \mid D_\xi)`$

もっともよく使うのは $`\theta = \omega`$ の場合です。この場合、$`\omega`$ の要素〈自然数〉は $`0`$ 以外すべて後者順序数なので、定義は次のようになります。

• $`D_0 := X_0`$
• $`D_{\nu + 1} := D_\nu \cup \bigcup(i\in I\mid \img(C_i, {D_\nu}^{n(i)} ))`$
• $`\o{X_0}^\omega := \bigcup(\nu \in \omega \mid D_\nu)`$

集合 $`\o{X_0}^\theta`$ を、帰納構造の$`\theta`$-帰納閉包〈$`\theta`$-inductive closure〉と呼びましょう。帰納構造の$`\theta`$-帰納閉包 $`\o{X_0}^\theta`$ は、ステップ数が $`\theta`$ 未満の帰納的構成で構成可能〈到達可能〉な要素達の集合です。$`\theta \gt \omega`$ のときは、超限帰納法を使うことになります。とある $`\theta`$ に対して、$`\o{X_0}^\theta = X`$ となることはありますが、特定の $`\theta`$ に対して $`\o{X_0}^\theta = X`$ というたぐいの条件を（帰納構造に対して）要求はしません。

実例： ツリー達の集合

分岐ノードが二分岐または分岐しないタイプのツリーを考えます。そのようなツリーの全体を $`X`$ とします。$`X`$ の定義（通常の帰納的定義）は：

• 空でない集合 $`A`$ の要素は $`X`$ の要素である。
• $`t`$ が $`X`$ の要素なら、$`\msf{u}(t)`$ は $`X`$ の要素である。
• $`t_1, t_2`$ が $`X`$ の要素なら、$`\msf{b}(t_1, t_2)`$ は $`X`$ の要素である。
• 以上で定義される要素だけが $`X`$ の要素である。

ここで注意すべきは、$`\msf{u}, \msf{b}`$ が単なる記号であることです。$`\msf{u}(t)`$ は形が関数呼び出しですが、何らかの関数を評価した結果ではなくて、それ自体で記号的実体です。

インデキシング集合は $`I := \{1, 2\}`$ として、アリティ関数 $`n`$ と構文的コンストラクタ $`C_1, C_2`$ は次のように定義します。

• $`n(1) = 1, n(2) = 2`$
• $`C_1`$ は、$`t \mapsto \msf{u}(t)`$ という関数（全域関数）
• $`C_2`$ は、$`(t_1, t_2) \mapsto \msf{b}(t_1, t_2)`$ という関数（全域関数）

$`X_0 := A`$ と定義します。これで、帰納構造が定義できました。

上記の帰納構造の台集合 $`X`$ 上に高さ関数 $`\mrm{height}`$ を定義できます。

• $`x\in A`$ なら、$`\mrm{height}(x) := 0`$
• $`x = \msf{u}(t)`$ なら、$`\mrm{height}(x) := \mrm{height}(t) + 1`$
• $`x = \msf{b}(t_1, t_2)`$ なら、$`\mrm{height}(x) := \mrm{max}(\mrm{height}(t_1), \mrm{height}(t_2) ) + 1`$

台集合は同じで、構文的コンストラクタは1つだけである帰納構造を定義しましょう。

インデキシング集合は $`I := \{0\}`$ （単元集合）として、アリティ関数 $`n`$ と構文的コンストラクタ $`C_0`$ は次のように定義します。

• $`n(0) = 2`$
• $`C_0`$ は、$`\mrm{height}(t_1) = \mrm{height}(t_2)`$ であるペア $`(t_1, t_2)`$ だけに定義される $`(t_1, t_2) \mapsto \msf{b}(t_1, t_2)`$ という部分関数。

$`X_0 := A`$ と定義します。

この帰納構造に対する$`\omega`$-帰納閉包は、左右の部分木の高さがバランスした二分木の全体です。

ここまでの例では、ツリーの分岐の数を制限してましたが、別な状況として、分岐の数は自由だとします。そのような“分岐が自由なツリー”達の集合を $`Y`$ とします。$`Y`$ の定義（通常の帰納的定義）は：

• 空でない集合 $`A`$ の要素は $`Y`$ の要素である。
• $`t`$ が $`X`$ の要素なら、単元リスト $`[t]`$ は $`Y`$ の要素である。
• $`t_1, \cdots, t_n`$ が $`Y`$ の要素なら、長さ $`n`$ のリスト $`[t_1, \cdots, t_n]`$ は $`Y`$ の要素である。
• 以上で定義される要素だけが $`Y`$ の要素である。

インデキシング集合は $`I := \{1, 2, \cdots\} = \mbf{N}_{\ge 1}`$ として、アリティ関数 $`n`$ と構文的コンストラクタ $`C_1, C_2, \cdots`$ は次のように定義します。

• $`n(i) = i\: \text{ for }i \in I`$
• $`C_1`$ は、$`t \mapsto [t]`$ という関数（全域関数）
• $`n \ge 2`$ に対する $`C_n`$ は、$`(t_1, \cdots, t_n) \mapsto [t_1, \cdots, t_n]`$ という関数（全域関数）

$`Y_0 := A`$ と定義します。$`(Y, I, n, (C_i)_{i\in I}, Y_0)`$ は帰納構造となります。

演繹系から作る帰納構造

演繹系〈演繹システム〉については以下の過去記事を参照してください。

• 演繹系とオペラッド

演繹系は、生成系〈system of generators | generating system〉が指定された色付きオペラッド〈colored operad〉とみなすのがよいでしょう。演繹系には別な呼び名〈同義語〉が幾つかあります。正規表現パターンで表すなら：

• {演繹 | 推論 | 導出 | 証明}{系 | システム}

オペラッドと用語と演繹系の用語の対応は以下のとおりです。

論理に出てくるシーケント計算の形式体系は、演繹系のひとつの事例です。

型理論の形式体系もまた演繹系です。が、用語法は型理論特有です。

型理論では、「導出〈derivation〉」という言葉のほうが好まれるようです。公理系に相当する判断達の集まりと、幾つかの判断（仮説）から結論である判断を導く規則〈ルール〉達の集まりが、おおよそ“型理論の導出系”を構成します。型理論の導出系については、以下の過去記事でも書いています。

• 論理や型理論の圏論的意味論 // 導出システムの圏と圏の圏
• カリー／ハワード／ランベック対応のための“呼び名”と“書き方” // 導出系

さて、演繹系から帰納構造を組み立てましょう。演繹系のすべての項達の集合を $`X`$ （台集合）とします。演繹系のステップ達は分類されているとして、その種別の集合 $`I`$ をインデキシング集合とします。同じ種別のステップでは、上段に並ぶ項の個数が決まっているとして、その個数からアリティ関数 $`n:I \to \mbf{N}`$ を決めます。

$`i\in I`$ に対する構文的コンストラクタ $`C_i`$ を定義します。種別 $`i`$ のステップの上段として許されるタプル $`(x_1, \cdots, x_{n(i)})`$ 達の集合を $`\def(C_i)`$ とします。

$`\quad \def(C_i) \subseteq X^{n(i)}`$

部分関数 $`C_i`$ は、次の2つの命題が同値になるように決めます。

• $`C_i(x_1, \cdots, x_{n(i)}) = y`$
• 種別が $`i`$ であるステップで、上段が $`x_1, \cdots, x_{n(i)}`$ で下段が $`y`$ であるものが存在する。

任意の演繹系でこの定義がうまく働くとは限りませんが、うまくいく場合だけを考えることにします。

最後に、公理（の下段にある）項達の集合を $`X_0`$ （ベース集合）とします。こうして作った $`(X, I, n, (C_i)_{i\in I}, X_0)`$ が帰納構造の条件を満たすことも一般には保証されませんが、うまいこと帰納構造となる場合だけを考えます。

演繹系から帰納構造が作れると何が良いかというと、意味論における意味割り当て関数〈解釈関数〉を再帰的に定義できます。関数が再帰的に定義できるとは、当該の帰納構造が帰納原理〈induction principle〉を満たすことです。別な言い方をすると、帰納構造がリカーサー〈recursor | 再帰子〉を持つことです。このことを次節で説明します。

なお、「再帰」と「帰納」の使い分けは習慣に従っているだけで、使い分けの合理的意味的基準はありません。「再帰的構成のために： 順序数の圏 // 再帰と帰納」を参照してください。

帰納的部分集合

$`(X, I, n, (C_i)_{i\in I}, X_0)`$ を帰納構造とします。台集合 $`X`$ の部分集合が帰納的〈inductive〉である、という概念を定義しましょう。帰納的部分集合の定義には、パラメーターとして基数 $`\kappa`$ が入ります。基数については「順序数から基数へ」を見てください。（フォン・ノイマン流の定義では）基数は順序数の特別のものです。集合 $`S`$ の基数〈cardinality〉は $`\mrm{card}(S)`$ と書きます。

基数 $`\kappa`$ に対して、部分集合 $`S\subseteq X`$ が帰納的〈inductive〉であることを、通常の帰納的定義により定義します。

• 空集合 $`\emptyset \subseteq X`$ は帰納的である。
• 部分集合 $`X_0 \subseteq X`$ は帰納的である。
• 部分集合達 $`S_1, \cdots, S_{n(i)} \subseteq X`$ がすべて帰納的であるとき、構文的コンストラクタ $`C_i`$ による像 $`{C_i}_*(S_1, \cdots, S_{n(i)})`$ は帰納的である。
• $`(S_j)_{j\in J}`$ が、互いに共通部分を持たない〈disjoint〉帰納的部分集合達のインデックス付きファミリーであり、かつ $`\mrm{card}(J) \lt \kappa`$ であるとき、合併 $`\bigcup(j\in J | S_j)`$ は帰納的である。
• 以上により定義される部分集合だけが帰納的部分集合である。

基数 $`\kappa`$ に対する帰納的部分集合達の集合は $`\mrm{Pow}(X)`$ の部分集合になります。これを $`\mrm{Ind}_\kappa(X) \subseteq \mrm{Pow}(X)`$ と書きます。$`\mrm{Ind}_\kappa(X)`$ は、背後に帰納構造 $`(X, I, n, (C_i)_{i\in I}, X_0)`$ があることを前提に定義されます。

$`\theta`$-帰納閉包 $`\o{X_0}^\theta`$ が$`\kappa`$-帰納的集合であるとは限りません。帰納構造のインデキシング集合 $`I`$ の基数〈サイズ〉や、順序数 $`\theta`$ によっては、$`\o{X_0}^\theta`$ が$`\kappa`$-帰納的集合にならないことがあります。

$`\kappa`$ が無限基数であり、$`\mrm{card}(I) \le \kappa`$ かつ $`\theta \le \kappa`$ ならば、帰納閉包 $`\o{X_0}^\theta`$ は$`\kappa`$-帰納的部分集合になります。

モーティブ

自然数上のモーティブ〈motive〉については過去記事「帰納原理を完全に書き下す」で述べています。自然数上のモーティブを、帰納構造に対して一般化します。とりあえず、帰納的型／リカーサーの文脈で使われている用語「モーティブ」を使い続けますが、代数幾何の "motive" とコンフリクトしているので、リネームしたほうがいいかも知れません。

帰納的部分集合達の集合 $`\mrm{Ind}_\kappa(X)`$ は $`\mrm{Pow}(X)`$ の部分集合なので、$`\mrm{Pow}(X)`$ が持つ包含順序をそのまま受け継いで順序集合になります。順序集合はやせた圏とみなせます。こうして得られる圏を $`\cat{Ind}_\kappa(X)`$ とします。圏とみなす場合はフォントを変えます。

帰納構造 $`(X, I, n, (C_i)_{i\in I}, X_0)`$ 上のモーティブ〈motive〉$`M`$ は、圏 $`\cat{Ind}_\kappa(X)`$ から集合圏への反変歌手（前層）で、後で述べる条件を満たすものです。

$`\quad M : \cat{Ind}_\kappa(X)^\op \to \mbf{Set} \In \mbf{CAT}`$

モーティブには以下に記す条件があります。

帰納的部分集合 $`A\in \mrm{Ind}_\kappa(X)`$ が、他の帰納的部分集合達 $`B_j`$ の和（共通部分無しの合併）として書けているとします。

$`\quad A = \sum(j\in J\mid B_j) \;\text{ where }B_j\in \mrm{Ind}_\kappa(X)`$

ここでの総和記号は、タグ付きユニオンとしての直和ではなくて、共通部分無しの合併です。

$`B_j\subseteq A`$ なので、集合のあいだの写像 $`M(A) \to M(B_j)`$ が誘導されます。これらの写像達をデカルトタプリングすると、次の写像が規準的に構成できます*2。

$`\quad M(A) \to \prod_{j\in J}M(B_j) \In \mbf{Set}`$

この写像が可逆〈同型〉であることがモーティブの条件です。前層が層である条件に類似しています。

モーティブは、モーティブ条件（上記の条件）を満たす前層なので、モーティブ達はすべての前層達からなる圏 $`\mrm{PSh}(\cat{Ind}_\kappa(X) )`$ の充満部分圏を形成します。

圏 $`\cat{Ind}_\kappa(X)`$ のすべての対象に、特定された単元集合〈distinguished singleton set〉$`\mbf{1}`$ を割り当てる自明なモーティブを $`\mbf{I}`$ とします。$`\mbf{I}`$ は、モーティブ達の圏の終対象です。

モーティブ $`\mbf{I}`$ からモーティブ $`M`$ への射（自然変換）を、$`M`$ のセクション〈section〉と呼びます。セクションは、帰納的部分集合 $`A`$ ごとに、$`M(A)`$ の要素をひとつ選んで割り当てる操作です。

リカーサー

リカーサーは、関数の再帰的定義を実現するメカニズムのことです。リカーサーの正体はひとつの関数です。リカーサーの存在を主張する命題を帰納原理〈induction principle〉と呼びます。リカーサー（という関数）を帰納原理と呼ぶ場合もあります。

$`(X, I, n, (C_i)_{i\in I}, X_0)`$ を帰納構造とします。$`\theta`$ は順序数として、帰納閉包 $`\o{X_0}^\theta`$ を定義域とする部分関数 $`X \hookleftarrow \o{X_0}^\theta \to V`$ を定義することが我々の目標です。

帰納構造のベース集合 $`X_0`$ 上で定義された$`V`$-値関数（{ベース | 初期}関数〈{base | initial} function〉） $`a: X_0 \to V`$ を、構文的コンストラクタ $`C_i`$ に沿って拡張して定義域を $`\o{X_0}^\theta`$ まで拡げます。定義域の拡張手段を与える関数族がステップ関数〈step function〉達のインデックス付きファミリーです。

「帰納的型とリカーサー」に、自然数上の標準的帰納構造に対するリカーサーを記述しています。先に読んでおくとよいかも知れません。

さて、再帰的に定義したい関数を $`f:\o{X_0}^\theta \to V`$ としましょう。$`f`$ を定義するためのデータとして、初期関数 $`a:X_0 \to V`$ と、$`i\in I`$ ごとのステップ関数 $`s_i`$ 達があります。初期関数は単なる関数ですが、ステップ関数の族は複雑な概念です。$`s_i`$ は、とあるモーティブのセクションとして定義します。

再帰的定義がうまくいくように、$`\o{X_0}^\theta \in \mrm{Ind}_\kappa(X)`$ だとします。つまり、目的の関数の域となる集合は、帰納構造の帰納的部分集合になっているとします。

$`i\in I`$ に対してモーティブ $`M_i`$ を次のように定義します。

$`\text{For }A \in |\cat{Ind}_\kappa(X)|\\
\quad M_i(A) := \mrm{Map}(
\mrm{Map}(A, V), \mrm{Map}({C_i}_*(A), V)
)
`$

上記の定義は、反変関手（前層）の対象パートですが、$`A \subseteq B`$ のとき、$`M_i(B) \to M_i(A)`$ も定義できて反変関手になります。

モーティブ $`M_i`$ のセクションを $`s_i`$ とします。$`s_i`$ は自然変換ですが、その成分は次のように書けます。

$`\quad s_{i, A} : \mrm{Map}(A, V) \to \mrm{Map}({C_i}_*(A), V) \In \mbf{Set}`$

$`s_{i, a}`$ は、帰納的部分集合 $`A`$ 上の関数から、$`{C_i}_*(A)`$ 上の関数を構成する働きを持ちます。結果として、関数の域を $`A \cup {C_i}_*(A)`$ まで拡張できます。

モーティブ $`M_i`$ のセクションを $`s_i`$ を、$`i`$-ステップ関数〈$`i`$-step function〉と呼びます。ステップ関数は、帰納的部分集合でインデックス付けられた関数達のファミリーです。

初期関数 $`a`$ とステップ関数達 $`(s_i)_{i\in I}`$ を入力として、$`\mrm{Map}(\o{X_0}^\theta, V)`$ の要素である関数を返す関数がリカーサー〈recursor〉です。リカーサーは、関数の再帰的定義を実行するマシナリーです。

帰納構造が（適当な $`\theta, \kappa`$ に対して）リカーサーを持つとき、その帰納構造では帰納原理が成立する〈holds induction principle〉といいます。

おわりに

書き終わった後で、考え直したほうがいい点が幾つか出てきました。

1. モーティブを中心に据えた定式化がよさそう。
2. 帰納構造の構文的コンストラクタもモーティブとして定義すべきではないか？
3. リカーサーもモーティブとして定義できるかも知れない。
4. それはそうと、「モーティブ」はリネームしたほうが無難。
5. 帰納構造の台集合は大きな集合も許すべきだろう。なんなら台集合を宇宙にとってもいい。
6. 帰納構造を、集合論または型理論の宇宙ともっと密接に関係付けるべきだろう。
7. 帰納構造のベース集合 $`X_0`$ を、構文的コンストラクタの集合として定義してはどうか？
8. 帰納原理／リカーサーは多項式関手と関係あるのではないか？
9. 帰納構造の定義をもっと代数的にスッキリさせたい。

帰納構造のリカーサー／帰納原理は、より一般的な“自由拡張”のフレームワークの一部に過ぎないのではないか、と思っていますが、よく分かりません。諸々、今後の課題です。