7.1 再帰的定義と構造的帰納法

目次

最初に、文字列を使って再帰的な定義と証明の例を示す。文字列は当たり前の概念として定義せずに使うことが多いものの、再帰的データ型として扱うと多くのことが学べる。具体的に言えば、文字列は多くの人が既に知っており、知らなくても簡単に理解できるので、再帰的定義の意味するデータ型そのものではなく再帰的定義の仕組みを解説するための最初の例として優れている。

再帰的データ型の定義は二つの部分からなる:

このパターンに従った、特定の文字列集合 \(A\) 上の文字列の定義を次に示す:

定義 7.1.1

\(A\) を非空集合とする。\(A\) をアルファベット (alphabet) と呼び、\(A\) の要素を文字 (character)、記号 (letter)、数字 (digit) などと呼ぶ。アルファベット \(A\) 上の文字列 (string) と呼ばれる再帰的データ型 \(A^{\ast}\) は次の規則で再帰的に定義される:

  • ベースケース: 空文字列 \(\lambda\) は \(A^{\ast}\) に含まれる。

  • 構築ケース: \(a \in A\) かつ \(s \in A^{\ast}\) なら、組 \(\langle a, s \rangle\) も \(A^{\ast}\) に含まれる。

例えば \(\left\{ 0, 1 \right\}^{\ast}\) はビット列全体の集合を表す。

ビット列の表現では \(0\) または \(1\) を要素とする列を使う場合が多い。例えば、長さ \(4\) のビット列 \(1011\) は \(4\) 要素列 \((1, 0, 1, 1)\) と表される。しかし定義 7.1.1 によると、この文字列は入れ子になった組として次のように表される:

\[ \langle 1, \langle 0, \langle 1, \langle 1, \lambda \rangle \rangle \rangle \rangle \]

この入れ子になった組は明らかに書きにくく、奇妙に思った読者もいるだろう。しかし、この記法は Scheme や Python といったプログラミング言語が文字のリストを表現する方法と同様である: \(\langle a, s \rangle\) が \(\text{cons}(a, s)\) に対応する。

空文字列に対しては記号 \(\lambda\) が割り当てられるだけで、それが実際に何なのかは定義されていないことに注目してほしい。それは問題にならないからである。空文字列と認識できて、非空文字列を表す他の記号と混同しなければ表現は何でも構わない。

同様の再帰的なアプローチを使って、次は文字列の長さを定義しよう:

定義 7.1.2

文字列 \(s\) の長さ (length) \(|s|\) は定義 7.1.1に関して再帰的に定義される:

  • ベースケース: \(|\lambda| ::= 0\)

  • 構築ケース: \(| \langle a, s \rangle | ::= 1 + |s| \)

この定義は標準的なパターンに従っている: 再帰的データ型を引数に取る関数は、その再帰的データ型の定義と同じ構造をした再帰的な定義を持つ。具体的に言えば、再帰的データ型を引数に取る関数 \(f\) を定義するには、そのデータ型の定義のベースケースに対する \(f\) の値と、構築ケースのそれぞれについて構成要素から \(f\) を計算する方法を定義する。

もう一つ例を示そう: 文字列 \(s\), \(t\) の連結 (concatenation) \(s \cdot t\) とは、\(s\) の後ろに \(t\) を並べた文字列を言う。これは (空文字列の扱いを除けば) 完全に明確な連結の数学的定義であり、Python や Scheme では \(s \cdot t\) を \(\operatorname{append}(s,t)\) などと表す。この連結を再帰的に定義すると次のようになる:

定義 7.1.3

文字列 \(s, t \in A^{\ast}\) の連結 (concatenation) は定義 7.1.1に関して再帰的に定義される:

  • ベースケース: \(\lambda \cdot t ::= t\)

  • 構築ケース: \(\langle a, s \rangle \cdot t ::= \langle a, s \cdot t \rangle\)

7.1.1 構造的帰納法

構造的帰納法 (structural induction) とは、再帰的データ型に属する全ての要素が何らかの性質を持つことを証明するための技法である。構造的帰納法を使った証明は、再帰的な定義に対応する二つの部分からなる:

構造的帰納法を使った証明の例を示そう。上で示した連結の再帰的な定義 (定義 7.1.3) は \(\lambda \cdot s ::= s\) と定めるので、空文字列が「左単位元 (left identity)」となる。ただ、空文字列は \(s \cdot \lambda = s\) を満たす「右単位元 (right identity)」でもあるはずである。この事実は定義 7.1.3 に含まれないものの、構造的帰納法を使うと簡単に証明できる:

補題 7.1.4

全ての \(s \in A^{\ast}\) で次の等式が成り立つ:

\[ s \cdot \lambda = s \]

証明 連結の再帰的な定義 (定義 7.1.3) に関する構造的帰納法で示す。次の述語 \(P(s)\) を帰納法の仮定として用いる:

\[ P(s) \ \ \overset{\text{def}}{\longleftrightarrow}\ \ s \cdot \lambda = s \]

ベースケース: \(s = \lambda\) のとき、\(s \cdot \lambda\) は次のように変形できる:

\[ \begin{aligned} s \cdot \lambda &= \lambda \cdot \lambda \\ &= \lambda && (\text{連結の定義より } \lambda \text{ は左単位元}) \\ &= s \end{aligned} \]

よって \(s = \lambda\) のとき \(P(s)\) は成り立つ。

構築ケース: \(s = \langle a, t \rangle\) であり、\(P(t)\) が成り立つと仮定する。このとき \(s \cdot \lambda\) は次のように変形できる:

\[ \begin{aligned} s \cdot \lambda &= \langle a, t \rangle \cdot \lambda \\ &::= \langle a, t \cdot \lambda \rangle && (\text{連結の定義の構築ケース}) \\ &= \langle a, t \rangle && (\text{帰納法の仮定 } P(t)) \\ &= s \end{aligned} \]

よって、この場合も \(P(s)\) は成り立つ。これで構築ケースの証明が完了した。従って構造的帰納法の原理より、全ての \(s \in A^{\ast}\) で \(P(s)\) は成り立つ。 ■

再帰的データ型の定義に関する構造的帰納法で再帰的関数の性質を証明できる場合もある。例えば、二つの文字列を連結した文字列の長さは二つの文字列の長さの和である事実の証明では、文字列の定義に関する構造的帰納法を利用できる:

補題

全ての \(s, t \in A^{\ast}\) で次の等式が成り立つ:

\[ |s \cdot t| = |s| + |t| \]

証明 \(A^{\ast}\) の定義に関する構造的帰納法で示す。次の述語 \(P(s)\) を帰納法の仮定とする:

\[ P(s) \ \ \overset{\text{def}}{\longleftrightarrow}\ \ \forall t \in A^{\ast}.\ |s \cdot t| = |s| + |t| \]

ベースケース: \(s = \lambda\) のとき、\(|s \cdot t|\) は次のように変形できる:

\[ \begin{aligned} | s \cdot t | &= |\lambda \cdot t| \\ &= |t| && (\text{連結の定義}) \\ &= 0 + |t| \\ &= |s| + |t| && (|\lambda| \text{ の定義}) \end{aligned} \]

よって \(s = \lambda\) のとき \(P(s)\) は成り立つ。

構築ケース: \(s = \langle a, r \rangle\) であり、\(P(r)\) が成り立つと仮定する。このとき \(|s\cdot t|\) は次のように変形できる:

\[ \begin{aligned} |s \cdot t| &= | \langle a, r \rangle \cdot t | \\[3pt] &= | \langle a, r \cdot t \rangle | && (\text{連結の定義の構築ケース}) \\[3pt] &= 1 + |r \cdot t| && (\text{長さの定義の構築ケース}) \\[3pt] &= 1 + (|r| + |t|) && (\text{帰納法の仮定 } P(r)) \\[3pt] &= (1 + |r|) + |t| \\[3pt] &= |\langle a, r \rangle| + |t| && (\text{長さの定義の構築ケース}) \\[3pt] &= |s| + |t| \end{aligned} \]

よって、この場合も \(P(s)\) は成り立つ。従って構造的帰納法の原理より、\(P(s)\) は全ての \(s \in A^{\ast}\) で成り立つ。 ■

これらの証明を一般的な原理にまとめる:

構造的帰納法の原理 (principle of structural induction)

\(R\) を再帰的に定義されたデータ型、\(P\) を \(R\) に関する述語とする。次の条件が成り立つと仮定する:

  • ベースケースが定義する全ての要素 \(b \in R\) で \(P(b)\) が成り立つ。

  • 構築ケースが定義する任意の二引数の構築手続き \(\textbf{c}\) に対して、全ての \(r, s \in R\) で

    \[ (P(r) \ \operatorname{\text{\footnotesize AND}} \ P(s)) \ \operatorname{\text{\footnotesize IMPLIES}}\ P(\textbf{c}(r, s)) \]

    が成り立つ。さらに、これ以外の個数の引数を取る全ての構築手続きでも同様の関係が成り立つ。

このとき、全ての \(r \in R\) で \(P(r)\) が成り立つ。

広告