ProofSummit2011振り返り
natはCoqでは5000くらいで止まってしまう
プログラミング言語でのintには対応しないよ
Agdaであそぼ -- プログラム代数の話
- 来年どうするか?
関数型プログラミングのイベントにくっつけるのなら、名古屋でやるんじゃないか?
昔はOCamlだけでやってたけど、OCamlだけのイベントじゃなくなるかも。
くっつける場合は、早めに関数型イベントの日程を教えてもらう。
Purely Functional Data Structures
- 動機
- 小さいサンプルは退屈
- だからといってでかいシステム開発は無理
- やるとしたらライブラリ開発ではないか
- Separation Logicもおいおい勉強していきたい
- Web版と製本の違いは、付録のHaskell版がないところ。
- こまかい違いもあるかと。
- 最終的には計算量の証明もやりたい
Coq-Formalized Proofs of Quicksort's Ararage-Case Complexity
http://weegen.home.xs4all.nl/eelis/research/quicksort/
比較演算子をMonadに持ち上げる
Quicksort自身をMonadに持ち上げている
- lower <- filterM (gt pivot) t >>= qs ; ここgtじゃなくてleだろう
- Monadにする理由は、副作用を加えられるから。
- comparisonはCoqでLt,Gt,Eqが定義されている型。
- 償却計算量(Amortized-Complexity)
- これが平均計算量になる、ということの証明はついてない?
- 比較回数の平均値で計算している。
- Rではomega使えないの?
