プログラミング好きの備忘録

関数型言語とか、証明とか

Coq

減少性が示せない?

一日ごろごろしてました。 ほとんど成果ないですが、引っかかっているポイントが浮かび上がってきたので、メモしておきます。 Haskell 前回の畳み込みを使った表現がまだ解決していないCoq 4で割ると3余るならば真を返す関数が定義できないFixpoint is_4n_3 …

ソフトウェアの基礎、継続中

ソフトウェアの基礎、115ページまで。演習問題はoptional,recommendedであるものはやってません。多相性の部分はXをどこに置くのかはっきり理解しておらず、コンパイルエラーが起きているので後回しに。先に高階関数のほうに進みます。 いずれは証明駆動開発…

ソフトウェアの基礎

今日は8月に入って初めての、予定がまったく入っていない日でした。 自分で設定した、夏休みの課題を推めることにしました。・TAPL 読み始めると(遅々ながら)のめり込むことができる。でも、とっかかりが難しい。というわけで、今日はTAPLは進まなかった(意…

夏期休暇にやりたいこと

やるべきことがあるときに限って、そうじゃないことが捗る… 試験前の掃除、とか。発端を忘れてしまいましたが、気になる単語からリンクを飛んでいった結果、やりたいことが浮かび上がってきました。 ・圏論の本を読む 途中挫折の可能性もありますが、とにか…