問題タブ [induction]

例えば、

このアルゴリズムの効率は、O(1)、O(n)、またはその他でしょうか?

このアルゴリズムは、任意の正の整数 m、n に対して m^n を計算することを目的としています。n の帰納法によってこのアルゴリズムの正しさを示すにはどうすればよいですか?

私は帰納法によってアルゴリズムを証明し、それがすべての n >= 0 に対して 3 ⁿ - 2 ⁿを返すことを想定しています。これは Eiffel で書かれたアルゴリズムです。

私の理解では、あなたはそれを 3 つのステップで証明します。基礎ステップ、帰納的仮説、および完全性の証明。これは私が現在持っているものです。

基本：

P(0) は 0 を返し、3 ⁰ - 2 ⁰ = 0 を返します。

P(1) は 1 を返し、3 ¹ - 2 ¹ = 1 です。

誘導仮説:

P(k) が0 <= k < n に対して3 ^k - 2 ^{kを返すと仮定します。}

完全性の証明:

n の場合、P(n) は 5(P(n-1)) - 6(P(n-2)) を返します。

5(P(n-1)) - 6(P(n-2))

5(3 ^n-1 - 2 ^n-1 ) - 6(3 ^n-2 - 2 ^n-2 ) <-帰納的仮説に基づく

これは私が立ち往生する部分です。^{これを 3 n} - 2 ⁿのように縮小するにはどうすればよいのでしょうか。

「Software Foundation」という本を読んでいます。「誘導の詳細」の章で、著者は、誘導型が定義されているときに coq によって生成される誘導原理について話します。

演習は次のとおりです。「+」の関連付けの概念を定義にカプセル化し、それに nat_ind を適用します。

定義の最初の推測は次のとおりです。

しかし、これを証明したいときに問題があります。

nat_ind動作しません。だから私はそれがP_plusassoc1つだけの整数ではなく3つに依存しているからだと思った。

だから私はこのように書き直しP_plusassocます：

しかし、それでもうまくいきません。問題はどこだ ？P_plusassocを使用するように定義するにはどうすればよいnat_indですか?

私は、Coursera での Scala の関数型プログラミングの講義に従っています。ビデオ 5.7 の最後で、Martin Odersky は次の方程式の正しさを帰納法によって証明するよう求めています。

複数のリストが含まれている場合、帰納法による証明をどのように処理するのですか?

xs が Nil で ys が Nil である基本ケースを確認しました。xs を x::xs に置き換えたときに方程式が成立することを帰納法によって証明しましたが、ys を y::ys に置き換えた方程式もチェックする必要がありますか?

そしてその場合（エクササイズをあまり台無しにすることなく...とにかく採点されません）、どのように処理します(xs ++ (y::ys)) map fか？

これは、私が同様の例で使用したアプローチであり、

証明 (基本ケースと簡単な x::xs ケースを省略):

これは正しいですか ？