profile image(wat-aro)
2017/05/11

プログラミング Coq (証明駆動開発 2)

証明駆動開発入門(2)

上記ページの勉強メモです。

Extraction

coq から OCaml, Haskell, Scheme のコードを出力する。

OCaml にコードを出力するにはそのまま

Extraction map.

とすればいい。
これで

(** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)

let rec map f = function
| Nil -> Nil
| Cons (a, t) -> Cons ((f a), (map f t))

と出力される。（proof-general を使っています。coq-ideの場合はcommand pane で実行）

この時、list が OCaml 組み込みのリストでなく coq で定義された list になっている。
OCaml 組み込みのリストを使うには

Extract Inductive list => "list" ["[]" "(::)"].

を実行する。こうすると

(** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)

let rec map f = function
| [] -> []
| a::t -> (f a)::(map f t)

とOCaml 組み込みのリストを使ったmap関数が生成される。

Haskell や Scheme に出力するにはそれぞれ
Extraction Language Haskell. Extraction Language Scheme. としてからOCamlの場合と同じように出力する。

Extraction Language Haskell.
Extract Inductive list => "list" ["[]" "(::)"].
Extraction map.
map :: (a1 -> a2) -> (list a1) -> list a2
map f l =
  case l of {
   [] -> [];
   (::) a t -> (::) (f a) (map f t)}

正しいけど、あまり綺麗なコードじゃない。

map :: (a -> b) -> (list a) -> list b
map f [] = []
map f x::xs = (f x) :: (map f xs)

くらいには変換してほしいけど、元の形からすると厳しいのかな。

次は scheme.

Extraction Language Scheme.
Extraction map.
(define map (lambdas (f l)
  (match l
     ((Nil) `(Nil))
     ((Cons a t) `(Cons ,(f a) ,(@ map f t))))))

おお。lambdas ってなんだ。match なんて RnRSにないぞ。というか、準クオート使ってるし、,使った式展開も入ってる。
Coq Extension Scheme っていうのがあって、lambdas マクロやmatch マクロ、@マクロが定義されているわけか。
lambdas マクロと @マクロはなかなかよい。
OCaml や Haskell っぽく書きたい時は便利そう。
match マクロは define-syntax みたいな感じかな？
直接変換するならたしかにこういうマクロ欲しくなるな。

insertion_sort の変換

OCamlの場合

Extraction Language Ocaml.

Extract Inductive list => "list" ["[]" "(::)"].
Extract Inductive bool => "bool" ["true" "false"].
Extract Inductive nat => int ["0" "succ"] "(fun fO fS n -> if n = 0 then f O () else fS (n-1))".
Extraction insert.
Extraction insertion_sort.
(** val insert : int -> int list -> int list **)

let rec insert a l = match l with
| [] -> a::[]
| x::xs -> if Nat.leb a x then a::l else x::(insert a xs)

(** val insertion_sort : int list -> int list **)

let rec insertion_sort = function
| [] -> []
| x::xs -> insert x (insertion_sort xs)

Haskellの場合

Extraction Language Haskell.

Extract Inductive list => "([])" ["[]" "(:)"].
Extract Inductive bool => "Bool" ["True" "False"].
Extract Inductive nat => Int ["0" "succ"] "(\fO fS n -> if n == 0 then fO () else fS (n-1))".
insert :: Int -> (([]) Int) -> ([]) Int
insert a l =
  case l of {
   [] -> (:) a [];
   (:) x xs ->
    case leb a x of {
     True -> (:) a l;
     False -> (:) x (insert a xs)}}

insertion_sort :: (([]) Int) -> ([]) Int
insertion_sort l =
  case l of {
   [] -> [];
   (:) x xs -> insert x (insertion_sort xs)}

Schemeの場合

Extraction Language Scheme.

Extraction insert.
Extraction insertion_sort.
(define insert (lambdas (a l)
  (match l
     ((Nil) `(Cons ,a ,`(Nil)))
     ((Cons x xs)
       (match (@ leb a x)
          ((True) `(Cons ,a ,l))
          ((False) `(Cons ,x ,(@ insert a xs))))))))

(define insertion_sort (lambda (l)
  (match l
     ((Nil) `(Nil))
     ((Cons x xs) (@ insert x (insertion_sort xs))))))

ファイルへの出力

Extraction Language Ocaml.
Extraction "insertion_sort.ml" insertion_sort.

と入力して proof-general で C-c C-n すると以下のようなファイルが生成された。

module Nat =
 struct
  (** val leb : Int -> Int -> Bool **)

  let rec leb n m =
    (\fO fS n -> if n == 0 then fO () else fS (n-1))
      (fun _ ->
      True)
      (fun n' ->
      (\fO fS n -> if n == 0 then fO () else fS (n-1))
        (fun _ ->
        False)
        (fun m' ->
        leb n' m')
        m)
      n
 end

(** val insert : Int -> Int ([]) -> Int ([]) **)

let rec insert a l = match l with
| [] -> a:[]
| x:xs ->
  (match Nat.leb a x with
   | True -> a:l
   | False -> x:(insert a xs))

(** val insertion_sort : Int ([]) -> Int ([]) **)

let rec insertion_sort = function
| [] -> []
| x:xs -> insert x (insertion_sort xs)
module Nat :
 sig
  val leb : Int -> Int -> Bool
 end

val insert : Int -> Int ([]) -> Int ([])

val insertion_sort : Int ([]) -> Int ([])

lebも作ってくれるのか。 まあないとコードにならないもんな。

証明駆動開発のステップ

  1. まず書こうとしているプログラムがどういう性質をみたすべきかを記述し、
  2. Coq でそれをみたすようなプログラムを書き、
  3. 実際に最初に考えた性質を証明し、
  4. Extraction して他の言語のコードに変換する

感想

形式証明が慣れてないからなのかとても難しかった。
ただ、証明のステップを追うのはとても気持ちよかった。

次は、最近発売された純粋関数型データ構造読むかなって気分。
SML で書かれているらしいから、OCaml に置き換えながら写経するのが楽かな？
それとも付録に Haskell 実装があるらしいので Haskell に置き換えながら写経して、書けたら答え合わせするほうがいいかな。
悩ましい。

© 2022 wat-aro