私はagdaを学ぼうとしています。しかし、問題が発生しました。Agda wiki で見つけたすべてのチュートリアルは、私には複雑すぎて、プログラミングのさまざまな側面をカバーしています。agda の 3 つのチュートリアルを並行して読んだ後、簡単な証明を書くことができましたが、実際のアルゴリズムの正確さのためにそれを使用するにはまだ十分な知識がありません。
このテーマに関するチュートリアルをお勧めできますか? Learn Yourself a Haskell に似ていますが、Agda 用です。
5031 次
2 に答える
23
約 1 年前に Agda の学習を開始したとき、利用可能なすべてのチュートリアルを試し、それぞれが新しいことを教えてくれたと思います。
Coq はより多くのユーザー ベースを抱えており、2 冊の優れた書籍が入手できるため、Coq を試してみてください。
- Coq'Art - 少し時代遅れですが、初心者に優しい
- 依存型を使用した認定プログラミング
Software Foundationsも非常に優れています。
良い点は、Agda と Coq が基づいている理論がいくぶん似ていることです。そのため、多くの例を相互に翻訳することができます。Programming in Martin-Löf's Type Theoryは、従属型理論の非常に優れた読みやすい入門書であり、いくつかのことを明確にすることができます。
「実世界のアルゴリズム」とはどういう意味かを知るのに役立ちます。Agda に言及している論文には、多くの開発例が記載されています。
于 2012-02-26T19:53:27.700 に答える