LoginSignup
3

More than 5 years have passed since last update.

Coqでcall/cc(Coqで継続モナド、その2)

Last updated at Posted at 2014-05-17

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.を参照してください。

文献

  1. Coqで継続モナド
    http://qiita.com/suharahiromichi/items/f07f932103c28f36dd0e

  2. お気楽 Haskell プログラミング入門 ●継続渡しスタイル
    http://www.geocities.jp/m_hiroi/func/haskell38.html

  3. モナドのすべて Continuationモナド
    http://www.sampou.org/haskell/a-a-monads/html/contmonad.html

  4. PrologによるSystem Fの型付プログラム
    http://qiita.com/suharahiromichi/items/9adc16a40ecb1bc36825

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
3