再帰と帰納法による証明の関係は?
としましょうfn(n)、
再帰はfn(n)満たされるまで自分自身を呼び出しますbase condition。
誘導が合っている場合は、正しいbase conditionことを証明してみてください。(base case + 1)
再帰と誘導は別の方向にあるようです。1 つは からnまでbase case、もう 1 つは からbase caseまでinfiniteです。
誰かがアイデアを詳細に説明できますか?
9036 次
1 に答える
15
再帰と誘導はほとんど同じものです! これは、Agda などの依存型を持つプログラミング言語を使用すると明らかになりますが、依存型がなくてもある程度実証できます。
カリー・ハワード対応により、型は命題であり、プログラムは証明であることを思い出してください。型の関数Nat -> Nat(ここでは Haskell 表記を使用します) を作成しているときは、与えられた自然数からプログラムが終了し、別の自然数が生成されることを証明しようとしています。今、私たちは次のような定義を持っているかもしれません:
f 0 = 1
f (1 + n) = n * f n
これは、 の再帰的定義でfあると同時に、その終了の帰納的証明でもあります!
次の方法で証明として読み取ることができます。
任意の x に対して fx が終了することを証明しましょう。
- 基本ケース:
f 0定義により定数があるため、終了します。 - 帰納的なケース: 終了すると仮定すると
f n、f (1 + n)終了も終了します (それが呼び出すすべての関数が終了するため)。
再帰はそのカウンターをデクリメントする関数に限定されないので、帰納法も自然数に限定されないことに注意してください。構造再帰に対応する構造帰納法もあり、どちらも数学/プログラミングで非常に人気があります。これらは、物事を証明したり、より複雑なデータ構造 (リスト/ツリー/など) で関数を定義したりするときに使用されます。
ここで、再帰/誘導の「方向」に関する懸念に対処します。ここで、相反する「需要の方向」と「供給の方向」を考えてみるとよいでしょう。
再帰関数を定義すると、要求 (メソッド呼び出し) は大きな値から基本ケースに流れます。一方、供給 (戻り値) は、基本ケースからパラメーターのより大きな値に流れます。「明確さ」は、供給に関する別の考え方です。基本ケースから始まり、再帰ケースを介して無限に伝播します。
さて、帰納的証明をしているとき、定理はあなたの供給であり、目標はあなたの要求です. 基本ケースから定理 T 0 を作成し、帰納的なケースを使用して好きな大きさの T n に改善できます。供給は 0 から無限大に流れます。ここで、目標 G n がある場合、帰納ステップを使用してゼロに達するまで、それからより小さな目標 G (nk) を作成できます。このようにして、需要は n から 0 になります。
ご覧のとおり、どちらの場合も供給の方向は「無限大」であり、需要の方向は「ゼロ」です。
誘導と再帰の説明では、意味を変えずに見かけの順序を逆にすることもできます。
帰納法は、P n が成立することを証明するときです。最初に帰納的なケースを繰り返し適用して目標を P 0 に減らし、次に基本ケースを使用して結果の目標を証明する必要があります。
同様に、再帰とは、最初に基本ケースを定義してから、前の値に関してさらに値を定義する場合です。ほら、方向は簡単に交換できます！
于 2012-06-21T17:49:56.613 に答える