Coqでcall/cc（Coqで継続モナド、その2）
2014_05_17 @suharahiromichi
2014_05_18 @suharahiromichi 「証明」の部分を見直した
継続モナドの続きとして、前回（文献1.）にも定義してあったcall/ccを使ってみる。例題は今回も文献2.からいただいています。
本資料のソースコードは以下にあります。
https://github.com/suharahiromichi/coq/blob/master/ssr/ssr_monad_callcc.v
Require Import ssreflect ssrbool ssrnat seq.
継続モナド
定義（再掲）
Definition MCont R A := (A -> R) -> R.
Definition bind {R A : Type} (c : MCont R A)
(f : A -> MCont R A) : MCont R A :=
fun (k : A -> R) => c (fun (a : A) => f a k).
Definition ret {R A : Type} (a : A) : MCont R A :=
fun k => k a.
(* call/cc、文献3の定義を参考にした。 *)
Definition callcc {R A B : Type}
(f : (A -> MCont R B) -> MCont R A) : MCont R A :=
fun (k : A -> R) => f (fun (a : A) => fun (b : B -> R) => k a) k.
Check callcc.
: ((A -> MCont R B) -> MCont R A) -> MCont R A
すこし強引だが、call/ccの型は、「MCont R」の部分を除いて見ると、古典論理を扱うときの「パースの公理」に対応するといえる。
((P -> Q) -> P) -> P
演算子と、do記法も定義しておく。
Notation "c >>= f" :=
(bind c f)
(at level 42, left associativity).
Notation "s1 >> s2" :=
(s1 >>= fun _ => s2)
(at level 42, left associativity).
Notation "'DO' a <- A ; b <- B ; C 'OD'" :=
(A >>= fun a => B >>= fun b => C)
(at level 100, no associativity).
Notation "'DO' A ; B ; C 'OD'" :=
(A >> B >> C)
(at level 100, no associativity).
例題
大域脱出の例（文献2.）
Definition bar1 (cont : nat -> MCont nat nat) := ret 1 : MCont nat nat.
Definition bar2 (cont : nat -> MCont nat nat) := cont 2 : MCont nat nat.
Definition bar3 (cont : nat -> MCont nat nat) := ret 3 : MCont nat nat.
Definition foo (cont : nat -> MCont nat nat) :=
DO
bar1 cont;
bar2 cont; (* !! *)
bar3 cont
OD.
Definition test := callcc (fun k => foo k) id.
Eval cbv in test. (* 2 *)
flatten list
2次元リストを1次元にする。ただし、空リストがあったら空リストを返す（文献2.）。
モナドを使わない定義
Fixpoint flatten_cps (l : seq (seq nat)) : MCont (seq nat) (seq nat) :=
fun cont =>
match l with
| [::] => cont [::]
| [::] :: _ => [::] (* !! *)
| x :: xs => flatten_cps xs (fun y => cont (x ++ y))
end.
Eval cbv in flatten_cps [:: [:: 1;2];[:: 3;4];[:: 5;6]] id.
Eval cbv in flatten_cps [:: [:: 1;2];[:: 3;4];[::];[:: 5;6]] id. (* [::] *)
Eval cbv in flatten_cps [:: [:: 1;2];[::];[:: 3;4];[:: 5;6]] id. (* [::] *)
モナドを使う定義
Fixpoint flatten' (k : seq nat -> MCont (seq nat) (seq nat))
(l : seq (seq nat)) : MCont (seq nat) (seq nat) :=
match l with
| [::] => ret [::]
| [::] :: _ => k [::] (* !! *)
| x :: xs => flatten' k xs >>= fun y => ret (x ++ y)
end.
Definition flatten_callcc (l : seq (seq nat)) : MCont (seq nat) (seq nat) :=
callcc (fun (k : seq nat -> MCont (seq nat) (seq nat)) => flatten' k l).
Eval cbv in flatten_callcc [:: [:: 1;2];[:: 3;4];[:: 5;6]] id.
Eval cbv in flatten_callcc [:: [:: 1;2];[:: 3;4];[::];[:: 5;6]] id. (* [::] *)
Eval cbv in flatten_callcc [:: [:: 1;2];[::];[:: 3;4];[:: 5;6]] id. (* [::] *)
以上、「Coqで」といいながら証明はありません。call/ccを使って古典論理の定理を証明する話題は、文献4.を参照してください。
文献
-
Coqで継続モナド
http://qiita.com/suharahiromichi/items/f07f932103c28f36dd0e -
お気楽 Haskell プログラミング入門 ●継続渡しスタイル
http://www.geocities.jp/m_hiroi/func/haskell38.html -
モナドのすべて Continuationモナド
http://www.sampou.org/haskell/a-a-monads/html/contmonad.html -
PrologによるSystem Fの型付プログラム
http://qiita.com/suharahiromichi/items/9adc16a40ecb1bc36825