プログラミング言語や証明支援系において、既存の型を組み合わせるのではなくて、まったく新しい型（値の集合）を定義する場合は、帰納的型〈inductive type〉として定義することになります。
帰納的型の上の関数は、帰納的に定義できます。このことを帰納原理〈induction principle〉と呼びます。帰納原理自体がひとつの関数とみなせます。関数とみなした帰納原理をリカーサー〈recursor〉とも呼びます。一番お馴染みであろう帰納的型である自然数型に関して、そのリカーサーを見てみます。
内容：
自然数型の定義
サンプルコードはLean 4で書くことにします。自然数型 Nat はシステムで定義済みなので、名前がバッティングしないように My という名前空間を作って、そのなかで自前の自然数型を定義することにします。
namespace My inductive Nat where | zero : Nat -- ベース | succ (n : Nat) : Nat -- ステップ end My
この定義を自然言語で書けば：
- ベース： zeroは自然数〈Nat〉型の要素である。
- ステップ： nが自然数〈Nat〉型の要素であるなら、succ n も自然数〈Nat〉型の要素である。
この定義から、以下の項（記号的表現）は自然数であることがわかります*1。
- zero
- succ zero
- succ (succ zero)
- succ (succ (succ zero))
- succ (succ (succ (succ zero)))
- ‥‥
暗黙に次のことも仮定されます。
- 以上に述べた手順で得られた項だけが自然数である。
このような方法を使って定義された型を帰納的型〈inductive type〉といいます。
自然数型の帰納原理とリカーサー
Yをなんらかの型（値の集合）として、自然数の型NatからYへの関数を作りたいとします。（自然数に関する）帰納原理〈induction principle〉は次のことを主張します。
関数 f:Nat → Y を定義するには、以下の2つを定義すればそれでよい。
- ゼロでの値 a = f(zero) ∈Y
- 自然数nと、自然数nでの関数の値 f(n) から f(succ(n)) を計算する手順 s
帰納原理は、次のような関数の存在を保証しているともいえます。
- a と s が与えられると、目的の関数 f を返す関数
このような関数をリカーサー〈recursor〉と呼びます。リカーサーは、帰納原理の実体といえます。帰納的型である自然数型のリカーサーを NatRec という名前で呼びましょう。リカーサー NatRec は最初に決めた型Yごとにあるので、Yに対するリカーサーは NatRecY と書くことにします。
リカーサーの正体
リカーサーは型理論の概念なので、型理論の語彙・用語法で語られますが、型理論に慣れてないと分かりにくいので、ここから先は集合論的な語彙・用語法を使うことにします。$`\newcommand{\mrm}[1]{\mathrm{#1}}
`$
$`\mrm{NatRec}_Y`$ の入出力の仕様は次のようになります。
$`\quad a\in Y, \,s\in \mrm{Map}({\bf N}\times Y, Y) \mapsto \mrm{NatRec}_Y(a, s)\in \mrm{Map}({\bf N}, Y)`$
ここで：
- $`a\in Y`$ は、目的の関数 $`f`$ のゼロでの値。
- $`s : {\bf N}\times Y \to Y`$ は、自然数 $`n\in {\bf N}`$ と $`f(n)\in Y`$ から $`f(\mrm{suc}(n))\in Y`$ を計算する関数。
- $`f = \mrm{NatRec}_Y(a, s) : {\bf N} \to Y`$ が目的の関数。
リカーサーは、型 $`Y`$ ごとにあるのでした。$`Y\mapsto \mrm{NatRec}_Y`$ という対応も考えてみます。
$`\quad \mrm{NatRec}_Y : Y \times \mrm{Map}({\bf N}\times Y, Y) \to \mrm{Map}({\bf N}, Y)`$
であることから、
$`\quad \mrm{NatRec}_Y \in \mrm{Map}( Y \times \mrm{Map}({\bf N}\times Y, Y) , \mrm{Map}({\bf N}, Y) )`$
ここで $`Y`$ を変数だと思うと：
$`\quad Y\in |{\bf Set}| \mapsto \mrm{NatRec}_Y \in \mrm{Map}( Y \times \mrm{Map}({\bf N}\times Y, Y) , \mrm{Map}({\bf N}, Y) )`$
変数 $`Y`$ は、すべての型の集合 $`|{\bf Set}|`$（これは圏論の記法）上を走ります。$`Y`$ ごとに集合 $`\mrm{NatRec}_Y \in \mrm{Map}( Y \times \mrm{Map}({\bf N}\times Y, Y) , \mrm{Map}({\bf N}, Y) )`$ の要素を1個指定していることになるので、$`\mrm{NatRec}`$ は次のような巨大なパイ型*2の要素になります。
$`\quad \mrm{NatRec} \in \prod_{Y \in |{\bf Set}|} \mrm{Map}( Y \times \mrm{Map}({\bf N}\times Y, Y) , \mrm{Map}({\bf N}, Y) )`$
抽象度の高い関数 $`\mrm{NatRec}`$ は次のように順次具体化されます。
- 目的の関数の行き先〈余域〉$`Y`$ を決めると、$`\mrm{NatRec}_Y : Y \times \mrm{Map}({\bf N}\times Y, Y) \to \mrm{Map}({\bf N}, Y)`$ が決まる。
- $`a\in Y`$ と $`s \in \mrm{Map}({\bf N}\times Y, Y)`$ を決めて、$`\mrm{NatRec}_Y`$ に入力すると、$`\mrm{NatRec}_Y(a, s)\in \mrm{Map}({\bf N}, Y)`$ が決まる。
- $`f := \mrm{NatRec}_Y(a, s)`$ と置くと、$`f: {\bf N}\to Y`$ で目的の関数が得られた。
さらに
今までの話では、目的の関数 $`f:{\bf N}\to Y`$ は通常の関数でした。依存型理論では、依存関数〈dependent function〉が出てきます。依存関数の余域（値をとる集合）は自然数 $`n`$ ごとに変わってもかまいません。例えば、$`f(n)`$ は長さ $`n`$ の配列型になるとかです。依存関数に対しても帰納原理を適用しようとすると、リカーサーも複雑化します。
今回は、具体例として自然数型をとりましたが、任意の帰納的型に対してリカーサーを定義する必要があります。依存型／依存関数と帰納的型をサポートしている処理系は、再帰的型が定義されると、自動的にリカーサーを構成します。ということは、“帰納的型の定義”に対してリカーサーを計算するアルゴリズムがあるわけです。そのアルゴリズムを実現する関数はさらに高階・項レベルな関数になります。
