にわとり小屋でのプログラミング日記

この記事は OCaml Advent Calendar の5日目の記事です。

OCamlと連携して、CoqでもIO処理ができるようにするためのライブラリを作った。

http://github.com/yoshihiro503/coqio

このライブラリを使えば、例えば次のようなコードを書くことができる。

Require Import Monad IO.
Open Scope string_scope.

Definition main : IO unit :=
  do _ <- print "Hello"
  ; println ", world!".

Haskell風のdo式みたいな記法が便利だね。print関数には文字列だけでなく、Showクラスのインスタンスとなる型を持つ式ならばなんでも与えることができる*1。

このコードを次のコマンドでExtractすればcoq.mlというOCamlのソースを得ることができる。

Require Import ExtrOcamlBasic ExtrOcamlString ExtrOcamlIO Hello.

Extraction "coq.ml" main.

これで、あとはOCamlでコンパイルすれば実行できる。

  $ ocamlc coq.ml
  $ ./a.out
Hello, world!

証明された証明支援器をScalaで書いてみた

Scala, Coq, coq2scala |

この記事はTheorem Proving Advent Calendarの7日目の記事である。

静的型付き関数型言語は言語処理系の実装が容易であることから多くの場合、証明支援器(proof assistant)が実装されている。例えばStandard MLではIsabelle/HOL、OCamlでCoq、HaskellでAgdaが実装されている。

しかしながら、Twitter社が使っていることなどで最近有名になっている関数型言語のScalaはそのような証明支援器はあまり見受けられない。これはScalaが言語処理系だけでなく一般のアプリケーションでも効果的であることを示している。そうは言ってもScalaで証明支援器を書いてもいいんじゃないかと思ったので書いてみた。

実装に関して、証明支援器のモデルを実装したCoqのライブラリを使用した。coq2scalaを使ってこれをScalaのライブラリとして使った。*1ソースコードは以下で公開している。

• http://proofcafe.org/wiki/Coq2Scala

ソースコードをダウンロードしてmakeしたのちに

 scala Top

と打てば対話環境が起動する。使えるコマンドは以下の6つだ。最後にピリオド"."を打つ必要があることに注意しよう。*2構文やエラーメッセージはオリジナルのOCaml版と揃えた。

Infer t.                           #項tを型チェックし、型を表示する

Check t : T.                       #項tが型Tを持つかどうかチェックする

Axiom x : T.                       #T型の変数xを公理として仮定する

List.                              #現在仮定されている公理の列を列挙する

Delete.                            #公理を削除する

Quit.                              #終了する

例えば簡単な論理式(∀P, PならばP)の証明は(λP:Prop. λH:P. H)という恒等関数で表現できるが、その証明は次のようにCheckコマンドでチェックできる。∀の式は丸括弧"()"で、λ式はカク括弧"[]"で表現している。

h2o:coqincoq_scala imai$ scala Top
Check [P:Prop][H:P]H : (P:Prop)P->P.
Correct.

「Correct.」と表示されたら成功だ。もっと複雑な論理式にも挑戦してみよう。

CCなので式の構文は項も型も同じである。その構文は以下のようなBNFで定義している。

 <expr> ::=
  | "Set" | "Prop" | "Kind"                     #定数
  | <ident>                                     #変数参照
  | "[" <idents> ":" <expr> "]" <expr>          #関数抽象(ラムダ式)
  | "let"<ident>":"<expr>"="<expr>"in"<expr>    #ローカル変数束縛
  | "(" <idents> ":" <expr> ")" <expr>          #forall型
  | <expr> "->" ... "->" <expr>                 #関数型
  | <expr> " " ... " " <expr>                   #関数適用

まとめ

• Coq extraction pluginさえ用意すれば証明支援器が簡単にかけるよ
• Scalaは関数型言語だからDSLも簡単に書けるよ
• coq2scala使ってね

VSTTE Competition - ソフトウェア検証コンテストにチームTebasakiという名前で参加した。

coq, VSTTE, competition |

VSTTE (Verified Software: Theories, Tools and Experiments) 2012 という学会の併設イベントでソフトウェア検証コンテストというものが開催されることを前日に id:keigoi さんに教えてもらって参加してみた。日時は日本時間で11月9日の0時から48時間。初めて競技プログラミング(プルービング?)に参加したがよい経験になったと思う。

メンバーは id:mzpさん、@pirapiraさん、@hirose_golfさんの4名。チーム名は@pirapiraさんの提案で名古屋っぽいものがよいということでいろいろ候補を挙げて結局Tebasaki (手羽先) に決定。使う検証器や実装言語は何でも良い！ということだったので我々はCoqを使った。コンペ中はプライベートにしておいて後で公開するというためにソースコード管理はbitbucket.org上にリポジトリを置き、gitを使った。しかし、@pirapiraさんはオランダに引っ越したばかりでネットワーク回線がiPhoneしかなく、また、@hirose_golfさんもgitに慣れていないということで、結局私と@mzpだけがコミットした。

以下は感想:

• 0時に開催ということで直前の22:00くらいは寝て、0時に起きて、その後5:00くらいに寝てということをやったため、生活のリズムが狂ってしまった。
• 合宿みたいにして寝ずにやろうと思ったが、やはり集中力のために睡眠は重要なのでちゃんと家に帰って寝た方がよいと思った。
• 難しかったけれど楽しかった。

最後に、証明器や検証器について興味があるけどなかなか手がでないという方のためにハッカソンします！ ProofのHackathonということでハッシュタグは #proofthon(命名 by mzp)です。

ProofCafe - ProofThon

fold_leftとfold_rightが同じになるとき

coq, fold_left, fold_right |

fold_leftとfold_rightの結果が同じになるときが気になったので少し調べてみた。

例えば文字列のリストを連結して一つの文字列を生成する次の例はfold_leftでもfold_rightでも同様に定義できて同じ関数になる。Coqで書くと次のような感じ。

Definition xs := "foo" :: "bar" :: "baz" :: nil.
Eval compute in (fold_left append xs "").
Eval compute in (fold_right append "" xs).

fold_leftとfold_rightの定義はそれぞれ次のとおり

Section Fold_Left_Recursor.
  Variables A B : Type.
  Variable f : A -> B -> A.

  Fixpoint fold_left (l:list B) (a0:A) : A :=
    match l with
      | nil => a0
      | cons b t => fold_left t (f a0 b)
    end.
End Fold_Left_Recursor.

Section Fold_Right_Recursor.
  Variables A B : Type.
  Variable f : B -> A -> A.
  Variable a0 : A.

  Fixpoint fold_right (l:list B) : A :=
    match l with
      | nil => a0
      | cons b t => f b (fold_right t)
    end.
End Fold_Right_Recursor.

(a0: A)と((##): A -> A -> A)に対して次の二つの条件が成り立てばfold_leftとfold_rightの結果が同じになることを示した。

• 任意の(x:A)に対して x ## a0 = a0 ## x
• (##)は結合的。つまり x ## (y ## z) = (x ## y) ## z.

Require Import List.

Section Fold_LR.

Variable A : Set.
Variable op : A -> A -> A.
Variable a0 : A.

Infix "##" := op (at level 60, right associativity).

Axiom assoc : forall (x y z:A), (x ## y) ## z = x ## (y ## z).
Axiom sym_a0 : forall x:A, a0 ## x = x ## a0.

Lemma aux : forall (bs: list A) (a b1: A),
  fold_right op a (b1::bs) = fold_left op (bs ++ (a::nil)) b1.
Proof.
 induction bs; intros.
  reflexivity.

  simpl.
  rewrite <- IHbs.
  simpl.
  rewrite assoc.
  reflexivity.
Qed.

Lemma fold_left_a0_r : forall (xs: list A) (a: A),
  fold_left op (xs ++ (a0::nil)) a = fold_left op xs a ## a0.
Proof.
 induction xs; intro.
  reflexivity.

  simpl.
  rewrite IHxs.
  reflexivity.
Qed.

Lemma fold_left_a0_l: forall (xs: list A) (a: A),
  fold_left op xs (a0 ## a) = a0 ## fold_left op xs a.
Proof.
 induction xs; intros.
  reflexivity.

  simpl.
  rewrite <- IHxs.
  rewrite assoc.
  reflexivity.
Qed.

Theorem fold_lr : forall (xs: list A),
  fold_left op xs a0 = fold_right op a0 xs.
Proof.
 destruct xs.
  reflexivity.

  rewrite aux.
  simpl.
  rewrite fold_left_a0_l.
  rewrite fold_left_a0_r.
  rewrite sym_a0.
  reflexivity.
Qed.

End Fold_LR.

tmiyaさんの練習問題をラムダ式で解いてみた

Coq, 練習問題 |

tmiyaさんがCoq入門者向けの問題をブログで紹介していたので解いてみた。

Functional Programming Memo: [Coq] Coq-99 : Part 1

この問題はCoqを使う人だけでなく論理的な思考力を鍛える良い問題ばかりなので、ぜひとも挑戦してみるとよいと思う。

このようなシンプルな直観主義的な命題論理ならばラムダ式でもシンプルな証明を与えることが出来る。HaskellやMLなどを知っている関数型プログラマやAgda2erならこちらの証明の方がわかりやすいかもしれない。

Section Prop_Logic.

  Definition Coq_01 : forall A B C:Prop, (A->B->C) -> (A->B) -> A -> C :=
    fun A B C H1 H2 H3 => (H1 H3 (H2 H3)).

  Definition Coq_02 : forall A B C:Prop, A /\ (B /\ C) -> (A /\ B) /\ C :=
    fun A B C H =>
      match H with
        | conj H1 (conj H2 H3) => conj (conj H1 H2) H3
      end.

  Definition Coq_03 : forall A B C D:Prop,
    (A -> C) /\ (B -> D) /\ A /\ B -> C /\ D :=
    fun A B C D H =>
      match H with
        | conj H1 (conj H2 (conj Ha Hb)) => conj (H1 Ha) (H2 Hb)
      end.

  Definition Coq_04 : forall A : Prop, ~(A /\ ~A) :=
    fun A H =>
      match H with
        | conj Ha Hna => Hna Ha
      end.

  Definition Coq_05 : forall A B C:Prop, A \/ (B \/ C) -> (A \/ B) \/ C :=
    fun A B C H =>
      match H with
        | or_introl Ha => or_introl _ (or_introl _ Ha)
        | or_intror (or_introl Hb) => or_introl _ (or_intror _ Hb)
        | or_intror (or_intror Hc) => or_intror _ Hc
      end.

  Definition Coq_06 : forall A, ~~~A -> ~A :=
    fun A H Ha => H (fun Hna => Hna Ha).

  Definition Coq_07 : forall A B:Prop, (A->B)->~B->~A :=
    fun A B H Hnb Ha => Hnb (H Ha).

  Definition Coq_08: forall A B:Prop, ((((A->B)->A)->A)->B)->B :=
    fun A B H => H (fun H1 => H1 (fun Ha => (H (fun _ => Ha)))).

  Definition Coq_09 : forall A:Prop, ~~(A\/~A) :=
    fun A H => H (or_intror _ (fun Ha => H (or_introl _ Ha))).

End Prop_Logic.

Coqプログラマの集会、Coq庵でした

Coq, Coq庵 |

発表者の皆さん。お手伝いいただいた皆さん。ありがとうございました。たくさんのCoqerが集まって、大変濃密な時間を過ごす事ができました。

スライドは以下から参照できます。

Coq庵 - coqグループ

CPS変換されたフィボナッチ関数の証明をしてみた

Coq, CPS変換, フィボナッチ |

普通のフィボナッチ関数とCPS変換したフィボナッチ関数をそれぞれ定義して、それらが等価であるということを証明してみた。CPS変換についてちょっと理解できた気がする。

http://ideone.com/3CQOn

しかしfib_cps関数をもっと美しく定義できないものだろうか。

[追記 2010 09/07]

asパターンを使えばパターンマッチを入れ子にしなくても良いことがわかったので、少し実装をシンプルにして書いてみた。証明部分は ほぼ同じ。

http://ideone.com/ZFPeQ

OCamlでlet recを使わずにfact関数を定義する

OCaml, 再帰関数, 不動点演算, ProofCafe, CPDT |

今日はProofCafeでCPDTの三章を読み進めたが、そこでCoqではInductive型のコンストラクタの引数が関数のとき、その関数の左側に自分自身が現れてはいけないということを学んだ。もしそれを可能にしてしまうと無限ループが定義でき、公理系が矛盾してしまうからだ。次のシンプルな例を見てみよう。

Inductive t (A: Set) : Set :=
  | T : (t A -> A) -> t A.

一見なんの問題も無さそうな この型定義は失敗し、次のようなコンパイルエラーが出力される。

Error: Non strictly positive occurrence of "t" in "(t A -> A) -> t A".

もしこの型が定義できたとすると次のような関数が定義できてしまう。

Definition ワォ (T f) := f (T f).

ここで (ワォ (T ワォ)) はいくら評価しても同じ項になり、無限ループしてしまう。無限ループはCoqでは御法度なので以上のようなt型は定義できないということなのだ。

以下からが、本日の本題だ。この現象を逆手に取って OCamlで使えばlet recを使わずにループが表現できるんじゃないかと考えてみた。

OCamlでは上のような再帰型は問題なく定義できる。

type 'a t = T of ('a t -> 'a)
let wow (T f) = f (T f)

let _ = wow (T wow)

このコードはlet recを使っていないが、コンパイルすると無限ループで止まらないプログラムが得られる。もう少し工夫して次のように定義すると、関数fixpが定義出来る。fixpは(fixp f ≡ f (fixp f))を満たす不動点演算子だ。

type ('a,'b) t = F of (('a,'b) t -> (('a -> 'b) -> 'a -> 'b) -> 'a -> 'b)
let fixp_aux (F fld) = fld (F fld)
let v = F (fun self f x -> f (fixp_aux self f) x)
let fixp f x = fixp_aux v f x

このfixpを使って階上を計算するfact関数は次のように記述できる。

let fact =
  fixp (fun fact x -> if x = 0 then 1 else x * fact (x-1))
let _ = print_int (fact 10)

このコードは型定義とlet定義しか使っていないが、ちゃんと(fact 10)が正しい値3628800を返す。OCamlが今偶然手元にない人もIDEONEの結果をみて確かめる事ができる: http://ideone.com/W2yJB。

[追記 2010-07/25]

id:KeisukeNakanoさんのより詳しい記事がありました。多相バリアントを使ったより高度な定義を見る事ができます。 #009 賢人鳥をまねる - λx.x K S K ＠ はてな