問題タブ [induction]

私は、オペランドと演算子が後置表記で書かれた文字の配列を読み取るコンピュータープログラムを持っています。次に、プログラムは配列をスキャンして、次のようにスタックを使用して結果を計算します。

このプログラムが後置式を正しく評価することを帰納法によって証明するにはどうすればよいですか? (演習 4.16 Java のアルゴリズム (Sedgewick 2003) から取得)

疑似コードで帰納法による証明を使用する方法がよくわかりません。数式で使用するのと同じようには機能しないようです。

配列内の k で割り切れる整数の数を数えようとしています。

これが正しいことをどのように証明しますか？ありがとう

テストが近づいているので、練習問題の助けが必要です... これを帰納法で証明する必要があります。

再帰関係: m(i) = m(i-1) + m(i - 3) + 1、i >= 3 初期条件: m(0) = 1、m(1) = 2、m(2) = 3

m(i) >= 2^(i/3) を証明する

これまでに私ができることは次のとおりです。

基本ケース: m(3) >= 2 ------> 5 >= 2. したがって、基本ケースが成り立ちます。

帰納仮説m(k) >= 2^(k/3) を満たす ak があるとします。

ここで、k+1 に対して成り立つことを証明しなければなりません。

m(k+1) >= 2^((k+1)/3)

（仮説を代入することにより）等しい：

m(k) + m(k-2) + 1 >= 2^((k+1)/3)

これは私が立ち往生しているところです。ここからどこへ行けばいいのかわからない。どんな助けでも大歓迎です。みんなありがとう！

比較ベースの並べ替えは nlog(n) の大きなオメガであるため、mergesort をO(n)にすることはできません。それにもかかわらず、次の証明で問題を見つけることができません。

命題P(n) : 長さnのリストの場合、mergesort はO(n)時間かかります。

P(0) : 空のリストのマージ ソートは空のリストを返します。

強い帰納法: P(1), ..., P(n-1)を仮定し、 P(n )を証明しようとします。再帰的なマージソートの各ステップで、2 つのほぼ「半分のリ​​スト」がマージソートされてから「圧縮」されることがわかっています。各ハーフリストのマージソートには、帰納法によりO(n/2) 時間かかります。圧縮にはO(n)時間がかかります。したがって、アルゴリズムには、M(n) = 2M(n/2) + O(n)の再帰関係があり、これは2O(n/2) + O(n)であり、O(n)です。

私は、プログラムが正しいことを証明することの意味を正確に学ぼうとしています。私はゼロから始めて、最初のステップ/トピックの紹介に夢中になっています。

トータル関数型プログラミングに関するこの論文では、フィボナッチ関数の2つの定義が与えられています。伝統的なもの：

そして、私が前に見たことがない末尾再帰バージョン：

次に、この論文は、両方の関数がすべての正の整数nに対して同じ結果を返すことを帰納法によって証明することは「簡単」であると主張しました。このようなプログラムを分析することを考えたのはこれが初めてです。2つのプログラムが同等であることを証明できると考えるのは非常に興味深いので、私はすぐに帰納法によってこの証明を試みました。私の数学のスキルがさびているか、タスクが実際にはそれほど単純ではありません。

n=1で証明しました

n=kの仮定をしました

私は、仮定が当てはまる場合、関数はn = k + 1に対しても同等であることを証明しようとし始めます（したがって、すべてのn> = 1 QEDに対してすべて同等です）

適切なタイミングで仮定を代入するなど、さまざまな操作を試みましたが、LHSをRHSと等しくすることができないため、関数/プログラムが同等であることを証明できます。私は何が欠けていますか？論文は、タスクが証明することと同等であると述べています

任意のpの誘導による。しかし、それがどのように真実であるかはまったくわかりません。著者はどのようにしてこの方程式にたどり着きましたか？これは、がの場合にのみ、方程式の有効な変換ですp = 0。それが任意のpに対してどのように機能するかわかりません。任意のpについてそれを証明するには、別の誘導層を通過する必要があります。確かに証明する正しい式は

これまでのところ、それも役に立ちませんでした。誘導がどのように行われるかを誰かに教えてもらえますか？または、証拠を示すページへのリンク（検索しましたが、何も見つかりませんでした）。

私は圧縮試行について読んでいて、次を読みました：

圧縮されたトライは、L 個の葉を持つツリーであり、トライのすべての内部ノードには少なくとも 2 つの子があります。

次に、著者は、すべての内部ノードに少なくとも 2 つの子があり、最大で L-1 個の内部ノードがあるような L の葉を持つツリーを書いています。なぜこれが真実なのか、私は本当に混乱しています。

誰かがそれの帰納的証明を提供できますか?

構造帰納法を使用して定義された関数を Agda の終了チェッカーで受け入れることができません。

この問題を示す最も単純な例として、次の例を作成しました。次の の定義sizeは拒否されますが、厳密に小さいコンポーネントで常に再帰します。

この問題の一般的な解決策はありますか? Recursorデータ型に対してを作成する必要がありますか? はいの場合、どうすればよいですか？Recursor（ forを定義する方法の例があれば、List Aそれで十分なヒントが得られると思いますか？）

これは我慢してください。最初に本の例を説明し、最後に質問をします。

プログラミング言語パラダイムのテキストによると：

帰納的仕様は、値のセットを指定する強力な方法です。この方法を説明するために、これを使用して 、自然数N = {0、1、2 、.の特定のサブセットSを記述します。。。}。

トップダウン定義：

自然数nは、次の場合にのみSに含まれます。

1. n = 0、または
2. n −3∈S。

0∈Sであることがわかります。したがって、（3 − 3）= 0および0∈Sであるため、3∈Sです。同様に、（6−3）= 3および3∈Sであるため、6∈Sです。このように続けると、次のことができます。 3の倍数はすべてSにあると結論付けます。

他の自然数はどうですか？1∈Sですか？1！= 0であることがわかっているため、最初の条件は満たされていません。さらに、（1−3）= −2であり、これは自然数ではないため、Sのメンバーではありません。したがって、2番目の条件は満たされません。

ボトムアップの定義：

セットSを、Nに含まれ、次の2つのプロパティを満たす最小のセットとして定義します。

1. 0∈S、および
2. n∈Sの場合、n+3∈S。

「最小のセット」とは、プロパティ1と2を満たすセットであり、プロパティ1と2を満たす他のセットのサブセットです。S1とS2の両方がプロパティを満たす場合、そのようなセットは1つだけであることがわかります。 1と2であり、両方が最小である場合、S1⊆S2（S1が最小であるため）、およびS2⊆S1（S2が最小であるため）、したがってS1=S2です。残りの2つの条件を満たすセットが多数あるため、この追加の条件が必要です。

推論規則：

これは、前のバージョンの定義の省略表記にすぎません。各エントリは、推論規則または単なる規則と呼ばれます。水平線は「if-then」として読み取られます。線より上の部分は、仮説 または先行詞と呼ばれます。線より下の部分は、結論または後件と呼ばれます。2つ以上の仮説がリストされている場合、それらは暗黙の「and」によって接続されます</ p>

ここに質問があります。

• おそらく最も重要な質問は、なぜこれらの帰納的定義を知る必要があるのか​​、そしてそれらが実際のケースでどのように役立つのかということです。
• Googleが帰納的定義でほとんど結果を返さないのはなぜですか？
• トップダウン、ボトムアップ、および推論規則が本質的に同じものを表示する場合、なぜ同じものを書く3つの方法が必要なのですか？
• 次のような本の例よりも少し複雑な問題の帰納的定義を見つけるのが難しいのはなぜですか。

以下の2つの問題について、トップダウン、ボトムアップ、および推論の定義を見つけたいと思います。あなたは私に答えを与える必要はありませんが、私は帰納的定義を導き出すためにどのように行くのか知りたいです。どこから始めればいいですか？これらのタイプの問題を実行するための体系的なアプローチ（レシピ）はありますか？

与えられたのは、黒または白の最大 30 個の石の列です。ゲームの開始時に隙間は許されませんが、30 個未満の石が存在する可能性があります。目標は、すべての石を取り除くことです。黒い石のみを取り除くことができます。石を取り除くと、その隣の石の色が変わります。取り除かれた石が真ん中にあった場合、これ以上埋めることができないギャップが生じます。その石の隣人は、石が取り除かれた後、隣人とは見なされません。

今、このゲームを力ずくで解くプログラムを作成しました。私は、ゲームが解けるのは、(明らかに) 黒い石がまったくなく、黒い石の数が奇数である場合のみであると結論付けました。また、黒石の数が奇数の場合は、列の最初の黒石を再帰的に取り除くことでゲームを解決できます。

私の問題は、黒い石の数が奇数でなければならず、最初の石を取り除くとゲームが解決するというこの条件を証明できないことです。このアルゴリズムを正しく証明するにはどうすればよいですか?

私はすでに誘導を使用しようとしましたが、私は立ち往生しています:

行 (a,b) = a*黒 + b*白

RemoveFirstBlack(Row(1, b)) = RemoveFirstBlack(black + b*white) = 0 (a=1 または n = 0 の場合、a=2n+1 および n は整数)

RemoveFirstBlack(Row(k*a, b)) = RemoveFirstBlack(k*a*black + b*white) = 0、k = 2p + 1、p を整数と仮定します。

RemoveFirstBlack(Row((k+1)*a, b)) = RemoveFirstBlack((k+1)*a*black + b*white) = RemoveFirstBlack((2(p+1)(2n+1))*black + b*白) = RemoveFirstBlack(2(p+1)*a*黒 + b*白) = 0?

あらゆる指針を前もって感謝します！

偶数の性質を証明するための帰納仮説を書こうとしています。以下を定式化し、証明した。

それが証明されているという事実にもかかわらず、それを使用しようとすると、エラー メッセージが表示されます。

誘導仮説の問題点、またはそれを適用する方法を教えてください。

ありがとう、

マイヤー