ネタ記録庫/Coq のバックアップ(No.10)

• バックアップ一覧
• 差分 を表示
• 現在との差分 を表示
• ソース を表示
• ネタ記録庫/Coq へ行く。
  • 1 (2007-08-20 (月) 22:42:26)
  • 2 (2007-08-20 (月) 22:49:15)
  • 3 (2007-09-28 (金) 16:55:58)
  • 4 (2007-10-02 (火) 16:14:16)
  • 5 (2007-10-15 (月) 02:30:58)
  • 6 (2007-10-15 (月) 02:30:58)
  • 7 (2007-10-16 (火) 10:05:46)
  • 8 (2007-11-27 (火) 14:40:02)
  • 9 (2007-11-27 (火) 14:40:02)
  • 10 (2008-02-27 (水) 12:21:35)
  • 11 (2008-02-29 (金) 09:23:24)
  • 12 (2008-02-29 (金) 17:50:38)
  • 13 (2008-03-20 (木) 10:29:05)
  • 14 (2008-06-11 (水) 15:02:18)
  • 15 (2008-07-18 (金) 09:34:44)

ネタ記録庫/Coq

Coqでニコニコ :-] †

http://www.nicovideo.jp/watch/sm1276083 from にわとり小屋でのプログラミング日記

(youtube : http://jp.youtube.com/watch?v=f9XOdpmeJ0o )

• Javascriptでニコニコも :-] http://www.nicovideo.jp/watch/sm1113536 from Gemmaの日記 -- げんま? 2007-10-16 (火) 15:20:42

本山とりとり亭でのCoq談義に捧ぐ。(07/10/15) †

• 名古屋(2) - ヒビルテ
• 飲み会 - zyxwvの日記
• 飲み会 - すえひろがりっっっ!

Coqに関する発表をしました（2007/9/20 よしひろ） †

「論理と証明 - 安全なWebアプリケーションのために」

Proofs and Types †

Jean-Yves Girard, Yves Lafont and Paul Taylor

• http://www.cs.man.ac.uk/~pt/stable/Proofs+Types.html 定理証明器ネタのページがそろそろ必要か。

reddit.comから †

こんなのがありました。 http://as305.dyndns.org/wiki/index.php?Coq%2Ftactics

定理証明器 Coq でHello, world! (よしひろ) †

Coqで "Hello, world!" を標準出力させるのはちょっと難しい。
なぜなら純粋だから。
今回は29行ほどのOCamlの力を借りて実装した。
具体的には次の三つのファイルを作った。

• coqstring.v
• helloworld.v
• main.ml　(29行のOCamlコード)

ちなみにCoqでは、文字は8bitのascii型、文字列はasciiのリストみたいな感じで定義されている。

(*Coqのスタンダードライブラリより*)
Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool).
Inductive string : Set :=
 | EmptyString : string
 | String : ascii -> string -> string.

まずcoqstring.v
Coqの文字列に関する便利のものたちを定義した。

(* Coqのコード *)
Require Import Ascii.
Require Import Strings.

Definition aH := Ascii false false false true  false false true  false.
Definition ae := Ascii true  false true  false  false true  true  false.
Definition al := Ascii false false true  true   false true  true  false.
Definition ao := Ascii true  true  true  true  false true  true  false.
Definition aCMM := Ascii false false true  true  false true  false false.
Definition aSPC := Ascii false false false false  false true  false false.
Definition aw := Ascii true  true  true  false  true  true  true  false.
Definition ar := Ascii false true  false false  true  true  true  false.
Definition ad := Ascii false false true  false  false true  true  false.
Definition aEXCLAM := Ascii true  false false false  false true  false false.
Definition aLF := Ascii false true  false true   false false false false.

次にhelloworld.v
このソースがこのプログラムの本質部分。

 (* Coqのコード *)
Require Import Ascii.
Require Import Strings.
Require Import coqstring.

Definition msg := 
  String aH 
 (String ae 
 (String al  
 (String al
 (String ao
 (String aCMM
 (String aSPC
 (String aw	
 (String ao
 (String ar
 (String al
 (String ad
 (String aEXCLAM
 (String aLF EmptyString))))))))))))).

Extraction "coqhelloworld.ml" nat_of_ascii msg.

以上のコードをコンパイルした結果、自動生成されるOCamlのコードがこれである。

(* これは上にあるCoqのコードから自動的に生成されたOCamlのコードである。 *)
type bool =
 | True
 | False

type nat =
 | O
 | S of nat

(** val plus : nat -> nat -> nat **)

let rec plus n m =
 match n with
   | O -> m
   | S p -> S (plus p m)

(** val mult : nat -> nat -> nat **)

let rec mult n m =
 match n with
   | O -> O
   | S p -> plus m (mult p m)

type ascii =
 | Ascii of bool * bool * bool * bool * bool * bool * bool * bool

(** val nat_of_ascii : ascii -> nat **)

let nat_of_ascii = function
 | Ascii (a1, a2, a3, a4, a5, a6, a7, a8) ->
     plus
       (mult (S (S O))
         (plus
           (mult (S (S O))
             (plus
               (mult (S (S O))
                 (plus
                   (mult (S (S O))
                     (plus
                       (mult (S (S O))
                         (plus
                           (mult (S (S O))
                             (plus
                               (mult (S (S O))
                                 (match a8 with
                                    | True -> S O
                                    | False -> O))
                               (match a7 with
                                  | True -> S O
                                  | False -> O)))
                           (match a6 with
                              | True -> S O
                              | False -> O)))
                       (match a5 with
                          | True -> S O
                          | False -> O)))
                   (match a4 with
                      | True -> S O
                      | False -> O)))
               (match a3 with
                  | True -> S O
                  | False -> O)))
           (match a2 with
              | True -> S O
              | False -> O))) (match a1 with
                                 | True -> S O
                                 | False -> O)
 
type string =
 | EmptyString
 | String of ascii * string

(** val aH : ascii **)

let aH =
 Ascii (False, False, False, True, False, False, True, False)

(** val ae : ascii **)

let ae =
 Ascii (True, False, True, False, False, True, True, False)

(** val al : ascii **)

let al =
 Ascii (False, False, True, True, False, True, True, False)

(** val ao : ascii **)

let ao =
 Ascii (True, True, True, True, False, True, True, False)

(** val aCMM : ascii **)

let aCMM =
 Ascii (False, False, True, True, False, True, False, False)

(** val aSPC : ascii **)

let aSPC =
 Ascii (False, False, False, False, False, True, False, False)

(** val aw : ascii **)

let aw =
 Ascii (True, True, True, False, True, True, True, False)

(** val ar : ascii **)

let ar =
 Ascii (False, True, False, False, True, True, True, False)

(** val ad : ascii **)

let ad =
 Ascii (False, False, True, False, False, True, True, False)

(** val aEXCLAM : ascii **)

let aEXCLAM =
 Ascii (True, False, False, False, False, True, False, False)

(** val aLF : ascii **)

let aLF =
 Ascii (False, True, False, True, False, False, False, False)

(** val msg : string **)

let msg =
 String (aH, (String (ae, (String (al, (String (al, (String (ao, (String
   (aCMM, (String (aSPC, (String (aw, (String (ao, (String (ar, (String (al,
   (String (ad, (String (aEXCLAM, (String (aLF,
   EmptyString)))))))))))))))))))))))))))

最後に以上をまとめて結果を出すOCamlのコードmain.ml。
この部分だけは証明することができない。

(* OCamlのコード *)
module Coq = Coqhelloworld

let rec int_of_nat = function
 | Coq.O -> 0
 | Coq.S p -> 1 + (int_of_nat p)

let length coqstr =
 let rec length_aux n = function
   | Coq.EmptyString -> n
   | Coq.String (_, tl) -> length_aux (1+n) tl
 in
 length_aux 0 coqstr

let char_of_ascii a =
 char_of_int (int_of_nat (Coq.nat_of_ascii a))

let string_of_coqstring coqstr =
 let n = length coqstr in
 let s = String.create n in
 let rec aux i = function
   | Coq.EmptyString -> ()
   | Coq.String (hd, tl) ->
      s.[i] <- char_of_ascii hd;
      aux (i+1) tl
 in
 aux 0 coqstr;
 s;;

print_string (string_of_coqstring Coq.msg);;

実行結果

Hello, world!

やった！できた！

Proof are Programs †

• http://www.radiumsoftware.com/0605.html#060523
• Philip Wadler. Proofs are Programs: 19th Century Logic and 21st Century Computing
• 数理論理学とコンピュータ・プログラムの間には深い関連性がある。この論文では，近代論理学の開祖であるフレーゲの概念記法を出発点として，ゲンツェンの自然演繹 と，チャーチの型付きラムダ計算の二つの流れを追い，最終的にそれらのモデルがカリー・ハワード対応によって同型として対応付けられるところまでを辿る。