第 7 章再帰的データ型

再帰的データ型 (recursive data type) はプログラミングで中心的な役割を果たす。そして再帰的データ型の議論では数学的帰納法が欠かせない。

再帰的データ型は、既存の要素から新しい要素を作る方法を示す再帰的定義 (recursive definition) で記述される。再帰的データ型だけではなく、それに関する性質や関数も再帰的定義を持つ。最も重要なこととして、構造的帰納法 (structural induction) と呼ばれる再帰的定義を利用する証明技法を使うと、特定の再帰的データ型の全ての要素が何らかの性質を持つことを証明できる。

本章では次の再帰的データ型と、それに作用する再帰的関数の例を見ていく: