このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

［参照用 記事］

帰納原理を完全に書き下す

雑記／備忘

帰納的に定義された型〈inductively defined type | inductive type〉では帰納原理〈induction principle〉が働きます。帰納原理を関数として表現したものがリカーサー〈recursor〉です。リカーサーについては「帰納的型とリカーサー」で述べました。

以前の記事では単純なリカーサー $`\mathrm{NatRec}`$ を紹介しましたが、より一般的なリカーサーをこの記事で説明します。ただし、扱う帰納的型は自然数型だけです。例題としてフィボナッチ数列とその一般化を出します。

記事タイトルの「完全に書き下す」は、帰納原理の中身を書き出すのではなくて、写像としての帰納原理のプロファイル（入出力の仕様）をハッキリさせることです。$`\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\In}{\text{ in } }
\require{color}
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }
\newcommand{\For}{\Keyword{For } }
`$

内容：

フィボナッチ数列とその一般化

帰納的に定義される自然数は、要素zeroとサクセッサ関数〈値構成子〉succから構成される zero, succ(zero), succ(succ(zero)), ... のようなモノですが、ここでは、普通の書き方 0, 1, 2, ... を使います。

自然数全体の集合を $`{\bf N}`$ として、$`{\bf N}`$ 上の関数を帰納的に定義することを考えます。例えば、フィボナッチ数列です。フィボナッチ数列 $`\mrm{fib}`$ は次のように定義できます。

  1. $`\mrm{fib}(0) := 0`$
  2. $`\mrm{fib}(1) := 1`$
  3. $`\mrm{fib}(n + 1) := \mrm{fib}(n - 1) + \mrm{fib}(n)\:\:(n \ge 1)`$

関数値 $`f(n + 1)`$ を計算するために、$`f(n)`$ だけでなくて $`f(n -1)`$ も必要とするので、「帰納的型とリカーサー」で説明した方法では計算できません。

フィボナッチ数列を一般化して、$`f(n + 1)`$ の計算に、それまでに計算したすべての関数値が必要な場合も考えてみます。

  1. $`\mrm{xfib}(0) := 0`$
  2. $`\mrm{xfib}(1) := 1`$
  3. $`\mrm{xfib}(n + 1) := \sum_{k = 0}^n \mrm{xfib}(k) \:\:(n \ge 1)`$

実は、この関数 $`\mrm{xfib}`$ は、フィボナッチ数列よりつまらない関数で、最初の2項を除いて

$`\quad \mrm{xfib}(n) = 2^{n - 2}\:\:(n \ge 2)`$

ですが、定義通りに律儀に計算するとすれば、帰納的に定義された関数の良い事例です。

モーティブ

「帰納的型とリカーサー」で説明を省略した概念にモーティブ〈motive〉があります。"motive" の語源も意味合いもよくわからないので、そのままカタカナ書きします*1。例えば、Lean 4（「プログラミング言語Lean 4の現状」参照）で自然数型のリカーサーを表示させると "motive" という語が使われています。

recursor Nat.rec.{u} : {motive : Nat → Sort u} →
  motive Nat.zero → ((n : Nat) → motive n → motive (Nat.succ n)) → 
    (t : Nat) → motive t

モーティブは、帰納原理の枠組みを与えるのですが、通常は意識されず暗黙に設定されるものです。モーティブの実体は、集合 $`{\bf N}`$ をインデックス集合〈indexing set〉とする集合族〈型ファミリー〉です。モーティブ $`M`$ を集合圏の記法で書けば：

$`\quad M:{\bf Nat} \to |{\bf Set}| \In {\bf SET}`$

ここで、$`{\bf SET}`$ は $`|{\bf Set}|`$ のような大きな集合も含む一階層上の集合圏です。

フィボナッチ数列やその一般化を定義するときは、（一例として）モーティブを次のように定義します。

$`\For n\in {\bf N}\\
\quad M(n) := {\bf N}^{n + 1} \;\in |{\bf Set}|`$

具体的には：

  • $`M(0) = {\bf N}^{0 + 1} = {\bf N}^1`$
  • $`M(1) = {\bf N}^{1 + 1} = {\bf N}^2`$
  • $`M(2) = {\bf N}^{2 + 1} = {\bf N}^3`$
  • ‥‥

モーティブは帰納法のステップを実行する関数を定義するために必要です。一般化フィボナッチ数列（つまらない数列）を律儀に総和で計算するなら、次のような関数が必要です。

$`\For n\in {\bf N}\\
\quad s_n : M(n) \to M(n + 1) \In {\bf Set}`$

具体的には：

  • $`s_0 : {\bf N}^1 \to {\bf N}^2 \In {\bf Set}`$
  • $`s_1 : {\bf N}^2 \to {\bf N}^3 \In {\bf Set}`$
  • $`s_2 : {\bf N}^3 \to {\bf N}^4 \In {\bf Set}`$
  • ‥‥

$`s_0`$ は適当に決めますが、$`s_1`$ 以降は総和を使って定義します。

  • $`s_0 (k_1) := (k_1, k_1 + 1)`$
  • $`s_1 (k_1, k_2) := (k_1, k_2, k_1 + k_2)`$
  • $`s_2 (k_1, k_2, k_3) := (k_1, k_2, k_3, k_1 + k_2 + k_3)`$
  • $`s_n (k_1, \cdots, k_n, k_{n + 1}) := (k_1, \cdots, k_n, k_{n+1}, \sum_{i = 1}^{n + 1} k_i)`$

$`s_n`$ 達が、計算を一ステップ進める行為を定式化します。単一の値ではなくて、計算の履歴全体を更新していきます。今までに計算した値はそのまま引き継ぎ、新しい値は総和で計算します。

$`s_n : M(n) \to M(n + 1)`$ を、自然数 $`n`$ における帰納ステップ関数〈{inductive | induction} step function〉と呼ぶことにします。帰納ステップ関数を定義するためには、事前にモーティブが必要です。

関数とセクション

今のセッティングで、帰納的な定義を使って定義したいものは関数 $`f:{\bf N} \to {\bf N}`$ です。しかし、$`f`$ の情報を含む“関数” $`F: {\bf N} \to \sum_{n\in {\bf N} } M(n)`$ があれば十分です。$`f`$ と $`F`$ の関係は以下のようです。

$`\quad F(n) = (f(0), f(1), \cdots, f(n)) \;\in {\bf N}^{n + 1}\\
\quad f(n) = \pi_{n + 1}(F(n)) \;\in {\bf N}`$

$`\pi_{n + 1}`$ はタプルの第(n + 1)成分を取る射影です。0-始まりと1-始まりが混じっているせいで番号がズレているので注意してください。

$`F`$ はシグマ型 $`\sum_{n\in {\bf N} } M(n)`$ への関数ですが、次の性質を持ちます。

$`\quad \forall n\in {\bf N}.\, \pi (F (n)) = n`$

ここで、$`\pi`$ はシグマ型に付随する標準射影です。

$`\quad \pi : \sum_{n\in {\bf N} } M(n) \to {\bf N} \In {\bf Set}`$

先の条件をより簡潔に書けば：

$`\quad F; \pi = \mrm{id}_{\bf N} \In {\bf Set}`$

この条件を満たす関数はシグマ型のセクション〈section〉と呼びます。つまり、$`F`$ はシグマ型のセクションになっています。

$`\quad F \in \mrm{Sect}(\pi : \sum_{n\in {\bf N} } M(n) \to {\bf N})`$

シグマ型のすべてのセクションからなる集合がパイ型なので：

$`\quad F \in \prod_{n\in {\bf N}} M(n) = \mrm{Sect}(\pi : \sum_{n\in {\bf N} } M(n) \to {\bf N})`$

という事情で、帰納的な定義で定義したいモノを、モーティブから作るパイ型の要素（モーティブから作るシグマ型のセクション）と考えることができます。

自然数の帰納原理

自然数の帰納原理と自然数上のリカーサーは事実上同じモノです。「帰納的型とリカーサー」では、単純なリカーサーを $`\mathrm{NatRec}`$ と呼んでいたので、気分を変えてここでは、リカーサー＝帰納原理を $`\mathrm{IndPrinNat}`$（Induction Principle for Natural numbers）と呼ぶことにします。

帰納原理が主張していることは：

  • ゼロに対する初期値と、帰納ステップ関数が与えられると、自然数全体で定義された関数が得られる。

先に説明したモーティブとセクションの言葉を使えば：

  • ゼロに対する初期値 $`a \in M(0)`$ と、帰納ステップ関数 $`s_n`$ 達が与えられると、自然数全体で定義されたセクション $`F`$ が得られる。

帰納ステップ関数の総体 $`s = (s_n)_{n\in {\bf N}}`$ は、自然数 $`n`$ ごとに $`\mrm{Map}(M(n), M(n + 1))`$ の要素（関数）を割り当てているので、関数成分の無限タプルであり、パイ型 $`\prod_{n\in {\bf N}} \mrm{Map}(M(n), M(n + 1))`$ の要素です。したがって、帰納原理への“入力”は：

$`\quad a \in M(0)\\
\quad s \in \prod_{n\in {\bf N}} \mrm{Map}(M(n), M(n + 1))`$

帰納原理〈リカーサー〉という写像は次の対応を与えます。

$`\quad a \in M(0),\, s \in \prod_{n\in {\bf N}} \mrm{Map}(M(n), M(n + 1)) \mapsto F`$

$`F \in \prod_{n\in {\bf N}} M(n)`$ だったことを考慮すると：

$`\For M : {\bf N} \to |{\bf Set}| \In {\bf SET}\\
\quad \mrm{IndPrinNat} : \\
\qquad M(0) \times \prod_{n\in {\bf N}} \mrm{Map}(M(n), M(n + 1)) \to
\prod_{n\in {\bf N}} M(n)`$

$`M`$ を $`\mrm{MAP}({\bf N}, |{\bf Set}|)`$ の要素と考えて、これもパイ型としてまとめてしまえば：

$`\mrm{IndPrinNat} \in \\
\displaystyle{
\quad \prod_{M\in \mrm{MAP}({\bf N}, |{\bf Set}|) } }
\textstyle{
\mrm{Map}(\, M(0) \times \prod_{n\in {\bf N}} \mrm{Map}(M(n), M(n + 1)) ,\, \prod_{n\in {\bf N}} M(n) \,)
}`$

これで、自然数の帰納原理のプロファイルを完全に書き下せました。

*1:フランス語風だと「モチーブ」でしょう。