naohaq
再帰/余再帰という言葉は「数学的帰納法」と関連が深くて、帰納/余帰納とも呼ばれます。
数学的帰納法で任意の自然数nについて性質p(n)が成り立つことの証明をすることを思い出してみます。
(i) Base case: p(0) が成り立つことを示す。
(ii) Hypothesis: ある自然数kについてp(k)が成り立つとする。
(iii) Step case: (ii)の仮定の下で、p(k+1)が成り立つことを示す。
(iv) (i),(ii),(iii) より、任意の自然数nについてp(n)が成り立つと主張して証明終わり。
なぜこれで全ての自然数についての証明になっているかというと、全ての自然数は、0(ないしは1)から順に1を足していったものになっているからです(ペアノの公理)
帰納的データ型を扱う関数は、これとそっくりな書き方ができます。
数学的帰納法で任意の自然数nについて性質p(n)が成り立つことの証明をすることを思い出してみます。
(i) Base case: p(0) が成り立つことを示す。
(ii) Hypothesis: ある自然数kについてp(k)が成り立つとする。
(iii) Step case: (ii)の仮定の下で、p(k+1)が成り立つことを示す。
(iv) (i),(ii),(iii) より、任意の自然数nについてp(n)が成り立つと主張して証明終わり。
なぜこれで全ての自然数についての証明になっているかというと、全ての自然数は、0(ないしは1)から順に1を足していったものになっているからです(ペアノの公理)
帰納的データ型を扱う関数は、これとそっくりな書き方ができます。