CoqでMonad
当日発表資料
http://study-func-prog.blogspot.com/2011/06/coq-type-class-in-coq.html
Polymorphism
"On Understanding Types, Data Abstruction, and Polymorphism"
adhoc polymorphismで実装
モナド則
returnしてbindすると・・・
'do' a <- e ; c" dとoという別の変数として解釈されないよう、'do'と書く。
Qed.で終わってしまうと、証明後に証明の中身を参照できなくなるらしい。
関数など、定義をするときはDefined.
全部Definedでもいいのかな。
Coqではstructureとrecordは同じ。
Coqで圏論の会のときには、structureで圏を定義している人がいました。
Type classでも同じことができるよ。
Monadを拡張してMonadPlusを作る
Javaでinterfaceをextendsするようなものかな。
monad :> Monad M ;
は継承ではなくsubstructureという扱い
継続モナド
(A->R)->R
RにFalseをとった時には、Aの否定の否定と同じ。
eta_expantionって何？ Print era_expantion.
extentionalityって何？ info extentionality x.
Print functional_extentionality.
集合論の外延性。
@nil A
Coqへの道 @sado_da
ユークリッド幾何はUsers Contributionsにあるけど、ライブラリが長大＆名前がフランス語で書いてある。
Functionが出てきたときにはまずinductionがうまく使えるかを考える。
無限大ってCoqではどう書くの?
Pow_x_infinityに例がある。
Clojureのmonads.clj
Maybeはモナド則満たしてないんじゃないか。
- None
- Some None
- Some (Some a)
A U {bottom}
とやってしまうと、
水島さんたちの書いたScalaの本が今月中頃にでます。
ICFP併設で、Continuationのワークショップがある。
http://logic.cs.tsukuba.ac.jp/cw2011/
9/25のProofSummit2011
発表とかお願いしたい方
- 池上さん：Agdaの入門の話をしてくれるようです。
- mzpさん：日程さえあればきてくれるはず。Coq2Rubyの話とか頼めるかも。
- 今井さん：なんか話してくれるはず。Coq2*の概要とか？
- kikxさん：とにかく何かお話してくれるとか。Ssreflect。
- tmiya_さん：正規表現のお話とか。
- sato_daさん：Coqへの道。
- お茶の水の方とか。
- coqtの中の人がきてくれれば・・・。
- ken.coba：ACL2のお話とか。Listのrev_revは証明しなくてもいいんですけど。
- どなたかIsabelle/HOLやらないかな。
現在集まってる定理証明系のネタ
- Coq,Agda,Isabelle/HOL,ACL2
証明ゴルフ
昨年のCoq庵ではペアプルーフィングがありました。
朝イチで証明課題を出して、みんなで解く。ゴルフ形式。
解きやすい問題を考えよう。解けた上で、ゴルフを頑張れるような問題。
発表で埋まってしまったらそれはそれでOK。余った時間をゴルフ解答に使うか。
その他発表ネタ(聞きたいお話)
- separation logicの話とかないかな。
- おもしろそうなライブラリがあったのでちょっと読んでみました、でもOK。
TODO：
- あらためて発表してほしい方に依頼しよう。
