問題タブ [proof]

マルチスレッドアルゴリズムは、設計/デバッグ/証明が特に困難です。デッカーのアルゴリズムは、正しい同期アルゴリズムを設計することがいかに難しいかを示す代表的な例です。タネンバウムの最新のオペレーティングシステムは、IPCセクションの例でいっぱいです。誰かがこれについての良い参考文献（本、記事）を持っていますか？ありがとう！

私はこの質問を見て、ポンピング補題が何であるかについて興味がありました（ウィキペディアはあまり役に立ちませんでした）。

基本的に、言語が特定のクラスに属するためには真実でなければならない理論的証明であることは理解していますが、それ以上はよくわかりません。

非数学者/計算科学博士が理解できる方法で、かなり細かいレベルでそれを説明しようとする人はいますか?

コンピューター プログラムは、数学的なステートメントと同じように証明できないのはなぜですか? 数学的証明は、さらに多くの証明から構築された他の証明の上に構築され、公理に至るまでです。

コンピュータプログラムはそのような構造を持っていないようです。コンピューター プログラムを作成した場合、以前に証明された作品を使用して、プログラムの真実を示すことができるのはどうしてですか? 存在しないのでできません。さらに、プログラミングの公理とは何ですか? フィールドの非常に原子的な真実？

上記に対する良い答えはありません。しかし、ソフトウェアは科学ではなく芸術であるため、証明できないようです。ピカソであることをどのように証明しますか?

Coq を試していますが、何をしているのか完全にはわかりません。は：

に相当：

編集：そうだと思います。

Coqで（forall x、P x / \ Q x）->（forall x、P x）をどのように証明しますか？何時間も試してみましたが、Coqが消化できるものに先行詞を分解する方法を理解できません。（私は初心者です、明らかに:)

次の例を知っている人はいますか？

1. 証明アシスタント ( Coqなど) における正規表現(後方参照で拡張される可能性があります)に関する証明の開発。
2. 正規表現に関する従属型言語 ( Agdaなど) のプログラム。

数学的な証明を書くときの目標の 1 つは、証明を圧縮し続けることです。証明はより洗練されますが、必ずしもより読みやすくなるわけではありません。圧縮は、不要な文字や冗長性を取り除くため、理解を深めることにつながります。

コードフットプリントをできるだけ小さくすべきだという開発者の声をよく耳にします。これにより、判読不能なコードがすぐに生成される可能性があります。数学では、演習は純粋にアカデミックであるため、そのような問題はありません。しかし、時は金なりの製品コードでは、非常に簡潔なコードが何をしているのかを人々に理解させようとすることはあまり意味がないようです。もう少し冗長なコードでは、読みやすさと節約が得られます。

どの時点でソフトウェア コードの圧縮を停止しますか?

常に有限の時間を要する 2 つの (決定論的) 有限状態マシンの同等性についての一般的な証明は存在しますか? つまり、2 つの FSM が与えられた場合、同じ入力が与えられた場合、FSM を実際に実行しなくても常に同じ出力が生成されることを証明できます (これは終了しない可能性があります)。そのような証明が存在する場合、時間計算量はどのくらいですか?

アルゴリズムの設計やより離散的なコンピューターサイエンスのトピックに取り掛かるとき、私たちは常に物事を証明しなければならないことになります。誰かが証明が本当に上手になる方法を尋ねるのを見るたびに、一般的な（そしておそらく怠惰な）答えは「練習」です。

基本を理解していれば、練習はすべて問題ありませんが、数学的な証明の考え方をどのように理解しますか？誘導はいつクリックしましたか？これらのトピックを教えるのに最適なリソースは何ですか？プルーフライティングにふける前に、どのような基礎トピックを調査する必要がありますか？

再帰ランタイムを処理するときに構築された再帰ツリーの高さを決定するにはどうすればよいでしょうか? 通常の木の高さを決定するのとどう違うのですか?

代替テキスト http://homepages.ius.edu/rwisman/C455/html/notes/Chapter4/ch4-9.gif

編集：申し訳ありませんが、再帰関係から再帰ツリーの高さを取得する方法を追加するつもりでした。