## 定義 再帰的データ型(recursive data type)とは、基底部(base case)と構成子部(constructor case)の2部からなる定義によって指定されるデータ型である。基底部はある既知の数学的要素がデータ型に属することを宣言し、構成子部はすでに構成された要素(または基底部の要素)から新しい要素を構成する規則を与える。文字列A*(空文字列εを基底部、既存文字列の先頭に文字を加える操作を構成子部とする)、括弧の整合した文字列RecMatch、非負整数N(0を基底部、後者n+1を構成子部とする)、算術式Aexp(変数xと数を基底部、和・積・負を構成子部とする)がその代表例である。再帰的データ型上の関数は、データ型定義と同じ場合分けに沿って——基底部の値を直接定義し、構成子部の値を構成要素上の関数値から定義することで——再帰的に定義できる。この定義パターンに対応する証明手法が構造的帰納法(structural induction)であり、基底部の各要素が性質Pを持つことと、構成子を適用する各構成要素がPを持つと仮定したとき構成結果もPを持つことの2部を示すことで、データ型のすべての要素がPを持つと結論する。再帰定義が曖昧(同じ要素が複数の仕方で構成可能)だと、その定義上で関数を再帰的に定義しても矛盾した値を持ちうるため、再帰的データ型の定義は曖昧でない(unambiguous)ことが関数のwell-definednessの前提になる。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 6 Recursive Data Types]] §6.1, §6.1.1, §6.2) ## 横断的知見 - 第4章の[[集合]]・[[関数]]は、集合・数列・タプルなどの数学的データ型を**外延的**(要素を列挙する、あるいは既存の集合演算で構成する)に定義する枠組みを扱う。これに対し第6章の再帰的データ型は、同じ「データ型」という主題を基底部と構成子部からなる**再帰的な構成規則**として定義し直す枠組みであり、両者は同じ対象(文字列・木構造など)を異なる定義原理で扱う相補的なアプローチになっている。第6章はこの違いを明示的に論じてはいないが、非負整数Nを「0と後者」で再帰的に定義する第6章§6.3の扱いは、第4章で外延的に導入された集合Nに、初めて構成規則(construction rule)を与え直すものになっている。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 4 Mathematical Data Types]], [[@2015__MIT__Mathematics for Computer Science - Chapter 6 Recursive Data Types]]) - 第5章は非負整数の添字nに関する通常の帰納法・強帰納法を独立した証明原理として提示するが、第6章§6.3はNそのものを「0を基底部、後者を構成子部とする再帰的データ型」として再定義し、通常の帰納法がこの定義に対する構造的帰納法の特殊ケースに過ぎないことを明らかにする。この結果、第5章で個別の技法として学んだ通常の帰納法・強帰納法・(第2章の)整列原理と、第6章の構造的帰納法は、「対象がどう再帰的に構成されるか」という単一の観点から統一的に理解できることが分かる——添字づけられた非負整数という特殊な再帰的データ型に対する帰納法が通常/強帰納法であり、任意の再帰的データ型に対する一般化が構造的帰納法である。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 5 Induction]], [[@2015__MIT__Mathematics for Computer Science - Chapter 6 Recursive Data Types]]) ## 未解決の問い - 第6章§6.5は「構造的帰納法が通常の帰納法より理論的に強力なのは無限データ型(無限木など)の場合に限られる」と述べるにとどまり、具体的にどのような性質が有限データ型では両者で同じ証明能力になり、無限データ型で乖離するのかは示されていない。第7章(Infinite Sets)で可算・非可算といった無限の扱いを学んだのち、この主張を具体例で検証できるか。 - 再帰的データ型の定義が曖昧でない(unambiguous)ことを、個別の定義ごとに手作業で確認する以外に、系統的に判定する一般的な方法はあるか。第6章はAmbRecMatchのような具体例で曖昧性を指摘するにとどまり、一般的な判定手続きは示していない。 ## 関連 - source: [[@2015__MIT__Mathematics for Computer Science - Chapter 6 Recursive Data Types]] - 概念: [[帰納法]] —— 通常の帰納法・強帰納法・構造的帰納法の相互関係。/ [[集合]]・[[関数]] —— 外延的なデータ型定義の姉妹concept。/ [[状態機械]] —— 段階的プロセスに対する帰納法の再定式化。 ## 出典 - Eric Lehman, F. Thomson Leighton, Albert R. Meyer, *Mathematics for Computer Science*, revised 2015-05-18, Chapter 6.