問題タブ [induction]

以下は構造誘導の定義ですか？

Haskell での構造誘導の例を教えてもらえますか?

私には2つのアルゴリズムがあります。

BがAよりも速いことを帰納的に証明するにはどうすればよいですか。

この問題には、n>2の場合は2^ n> 2n+1が役立つ可能性があると言われています。私は頭を割っていて、この問題を解決することはできません。ありがとう。

「n」はプログラムのサイズに相当します。

編集：すべてのn>19の場合。

解決：

前提：n ^ 2 + 1,000,000 <2 ^ n

基準：
n = 20
1000400 <1048576 TRUE

誘導：

この最後の行は、Bが常にAよりも大きいことを意味します。

コンパイラー試験の準備をしていますが、過去の論文で次の 2 つの質問に答えられないことがわかりました。

不変変数と帰納変数が何を意味するかは知っていますが、これら 2 つの解決策を説明することに関して、私に何が期待されているかはよくわかりません。

誰かが説明を手伝ってくれたら幸いです。

ありがとう！

文字列順列の再帰的な方法を実装しました。しかし、質問があります:帰納法を使用してこのコードの正しさを証明するにはどうすればよいですか? 本当にわからなかった。

非常に単純な帰納型があるとします。

特定の値が存在しないことを証明したいと思います。具体的には、十分に根拠のない値があってはならないこと: ~exists i, i = ind1 i.

私はインターネットで少し見回しましたが、何も思いつきませんでした。私は書くことができました：

これは機能しますが、本当に醜く、一般的ではないようです。

私は Coq を初めて使用しますが、いくつかの努力により、さまざまな帰納補題を証明することができました。ただし、次の帰納的定義を使用するすべての演習で行き詰まります。

私が得た最も遠いものは、次の補題でした：

次の 2 つの補題は、最初のステップを通過できませexistsんintros。

どんな助けでも大歓迎です！

Rails 4 アプリケーション ディレクトリで、ターミナルに「heroku pg:credentials DATABASE」と入力して、heroku にデプロイされているアプリケーションのデータベースに関するすべての情報を取得しました。postgresqlデータベース内のデータを見たいので、Inductionに情報を入力してみましたが、反応せず、アクティビティモニターに入って強制終了しました。同じ手順をさらに数回繰り返しましたが、すべて同じ結果でした。Induction のバージョンに問題がありますか? データベースを表示するために別のプログラムを使用する必要がありますか? それとも私は何か間違ったことをしていますか？

私はレールに慣れていないので、助けてくれてありがとう!

ゲスト マシン内にある PostgreSQL データベースに接続しようとしています (Vagrant と VirtualBox を使用)。

Inductionで接続しようとしていますが、次のようなエラーが表示されます。

Vagrant でホスト マシンのポート 1234 へのポート転送を行っています。

誘導接続の私の設定は次のとおりです。

開発データベースは Rails を使用して作成されたrake db:create:allものであり、Rails db コンソールから表示されるため、機能することがわかっています。

postgresql.conf ファイルで、外部マシンもリッスンするように設定listen_addressesしました。'*'

私は何を間違っていますか？

編集（私のpg_hba.confを追加）：

編集 (これは、接続しようとしたときに Induction アプリから表示されるエラーです)