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

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も作ってくれるのか。まあないとコードにならないもんな。

証明駆動開発のステップ

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

感想

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

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

2017-05-11

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

証明駆動開発入門(1)

何かを読む会 という社内勉強会が発足されました。読んだ本の内容を共有しよう。一人で勉強していてもダレるので共有することで無理やり進捗を出そう。他の人の発表を聞いて読んだ気になろう。っていう緩めの会です。途中まで読んで放置していたプログラミング Coq の続きを読んでまとめました。

挿入ソートを証明する。

証明したいことは次の二点。

挿入前と挿入後で要素に変化がないこと(isort_permutation)
挿入後に要素が整列されていること(isort_sorted)

上記を型で示すと以下のようになる。

isort_permutation : forall (l : list nat), Permutation l (insertion_sort l)
isort_sorted      : forall (l : list nat), LocallySorted le (insertion_sort l)

実装

Require Import List.
Require Import Arith.

Fixpoint insert (a : nat) (l : list nat) : list nat :=
  match l with
  | nil => a :: nil
  | x :: xs => if leb a x then a :: l else x :: insert a xs
  end.

Fixpoint insertion_sort (l : list nat) : list nat :=
  match l with
  | nil => nil
  | x :: xs => insert x (insertion_sort xs)
  end.

要素の変化がないこと

あるリストがあるリストと同じ要素で成り立っているのは以下のモジュールで定義されている。

Inductive Permutation : list A -> list A -> Prop :=
  | perm_nil: Permutation [] []
  | perm_skip x l l' : Permutation l l' -> Permutation (x::l) (x::l')
  | perm_swap x y l : Permutation (y::x::l) (x::y::l)
  | perm_trans l l' l'' : Permutation l l' -> Permutation l' l'' -> Permutation l l''.

nil と nil は同じ要素から成り立つ
l と l' が同じ要素から成り立つならば x :: l と x :: l' も同じ要素から成り立つ
y :: x :: l と x :: y :: l は同じ要素から成り立つ
(l と l' が同じ要素から成り立ち、l' と l'‘ が同じ要素から成り立つ) ならば l と l’‘ も同じ要素から成り立つ

isort_permutation の証明

isort_permutation の型

forall (l : list nat), Permutation l (insertion_sort l)

帰納法を使う。 l が nil の時は insertion_sort l は nil なので Permutation nil nil となり自明。

帰納法のため、nの場合にあたる仮定は

forall (l : list nat), Permutation xs (insertion_sort xs)

n + 1 に当たる命題は

forall (l : list nat), Permutation x :: xs (insertion_sort x::xs)

となり、

forall (l : list nat), Permutation x :: xs (insert x (insertion_sort xs)

と変形できる。

つまり

forall (l : list nat), Permuation x :: xs (x :: insertion_sort xs)

と

forall (l : lsit nat), Permutation (x :: insertion_sort xs) (insert x (insertion_sort xs)

を示すことで perm_trans から

forall l l' l'' , Permutation l l' -> Permutation l' l'' -> Permutation l l''

Permutation (x :: xs) (x :: insertion_sort xs) ->
  Permutation (x :: insertion_sort xs) (insert x (insertion_sort xs)) ->
    Permutation (x :: xs) (insert x (insertion_sort xs))

となり、導ける。

A については仮定と Permutation のコンストラクタ

perm_skip : forall x l l', Permutation l l' -> Permutation (x :: l) (x :: l')

から導ける。

まず B を補題として証明する。

isort_permutaiton の証明は以下。

命令	説明
intros	forall などから変数を仮定へ移動する
simpl	簡約
apply	仮定や定理などを適用
destruct	条件分岐しているものなどを subgoal に分ける
induction	帰納法を実施するために subgoal に分ける

どういうふうに証明が進むかは coq ide や proof-general 使って見てください。

Require Import List.
Require Import Arith.
Require Import Sorting.Permutation.
Require Import Sorting.Sorted.

(* isort_permutation *)

Lemma insert_perm : forall (x : nat)(l : list nat), Permutation (x :: l) (insert x l).
  induction l.
  intros.
  simpl.
  apply Permutation_refl.

  intros.
  simpl.
  destruct (leb x a).

  apply Permutation_refl.

  apply perm_trans with (a :: x :: l).
  apply perm_swap.

  apply perm_skip.
  apply IHl.
Qed.

Theorem isort_permutation : forall (l : list nat), Permutation l (insertion_sort l).
  induction l.
  apply perm_nil.
  simpl.
  apply perm_trans with (a :: insertion_sort l).
  apply perm_skip.
  apply IHl.
  apply insert_perm.
Qed.

整列の定義

リスト l が整列されていることはSorting.Sortedモジュールで定義されている.

Induction LocallySorted (A : Type) (R : A -> A -> Prop) : list A :=
  | LSorted_nil : LocallySorted R nil
  | LSorted_cons1 : forall a : A, LocallySorted R (a :: nil)
  | LSorted_consn : forall (a b : A) (l : list A),
    LocallySorted R (b :: l) ->
      R a b -> LocallySorted R (a :: b :: l)

上の定義は次のような意味です。 R a b は a < b のようなものです。

nil は整列している
x :: nil は整列している
b :: l が整列しているとき, R a b ならば a :: b :: l は整列している

整列されていることの証明

こちらでも帰納法で考える。まず l が nil の場合は insertion_sort nil = nil となり、LSorted_nil : LocallySorted le nil から明らか。

LocallySort le (insertion_sort l) -> LocallySort le (insertion_sort (a :: l)) の場合を考える。 LocallySort le (insertion_sort (a ::l) は LocallySort le (insert a (insertion_sort l))と変形できる。この時、insertion_sort l は仮定より整列しているため、

insert_sorted : forall (a : nat) (l : list a), LocallySort le l -> LocallySorted le (insert a l)

を示すことができれば証明できる。

これを補題として証明をすすめる。

整列の証明

Lemma insert_sorted : forall (a : nat) (l : list nat),
    LocallySorted le l -> LocallySorted le (insert a l).
  induction l.
  constructor.

  intro.
  simpl.
  remember (leb a a0).
  destruct b.

  apply LSorted_consn.
  apply H.
  apply leb_complete.
  congruence.

  inversion H.
  simpl.
  apply LSorted_consn.
  apply LSorted_cons1.
  apply lt_le_weak.
  apply leb_complete_conv.
  congruence.

  subst.
  simpl.
  simpl in IHl.
  remember (leb a b).

  destruct b0.
  apply LSorted_consn.
  apply IHl.
  apply H2.

  apply lt_le_weak.
  apply leb_complete_conv.
  congruence.

  apply LSorted_consn.
  apply IHl.
  apply H2.
  apply H3.
Qed.

Theorem isort_sorted : forall (l : list nat) , LocallySorted le (insertion_sort l).
  induction l.
  constructor.

  simpl.

  apply insert_sorted.
  apply IHl.
Qed.

これで isertion_sort はソートの前後で要素が変わらないことと、ソート後に整列されていることが証明できた。

2017-04-09

技術書典2に行ってきた

お昼頃に予定があったので行くか迷っていたが、14時くらいには空いてきたということで技術書典2に行ってきた。

目当ての一つだったインターネットの闇さんのコンパイラの本は既に完売と向かってる最中の電車の中で知る。 Coqに興味があったのでCoqによる定理証明が買えるといいなと思いながら突入。

16時過ぎでもう終わりかけなのになかなか賑わっていた。案の定、既に完売で何も片付けられているスペースもチラホラと。 Coqによる定理証明のスペースを見つけたので、中身を見させてもらいながらCoqについて色々と教えていただいた。入門書かと思っていたけど違った。３部出ているうちの、一番簡単そうな2014年出版のものを買った。まずは入門して、そして読まねば。

その後ぶらぶらしていたら、インターネットの闇さんのスペースを見つけたので、見本を見させてもらいながら色々話した。見本に載っているOCamlのコードはとても読みやすかったので、電子書籍版を期待していると伝え、またフラフラと。

移動してすぐにFortranでオブジェクト指向プログラミングをするという尖ったことをしているところで声をかけられて Fortran の話を聞いた。 Fortran については、科学技術計算で主に使用されていることと、現在使われているプログラミング言語の中で最も古い言語の一つってことくらいしか知らなかったのでおもしろかった。結局バグを減らしたかったり、大学みたいに人が入れ替わる環境だと既存のコードがすぐにレガシーになるので、可読性を高めたいということだった。 Fortran自体にオブジェクト指向が導入されたのはFortran2003かららしいが、ユーザが少ないらしく最適化が後回しにされたりすることもあるらしい。自分が実際に触ることはないだろうけど、知らない言語の話を聞くのは面白かった。入門部分も書かれているという第一部を買った。速習する部分があったので、そこくらいは読んでおきたい。

出不精なので秋葉原までの遠出はつらかったが、普段聞けないことを色々聞けてよかった。

2017-01-12

Pathname#joinの不思議な挙動

ruby

空のPathname同士をjoinした時に期待と違う挙動があった。

 $ ruby -v
ruby 2.3.3p222 (2016-11-21 revision 56859) [x86_64-darwin16]

期待していたのは次の動作。

path = Pathname.new('')         # => #<Pathname:>
path.join(path)                 # => #<Pathname:>

でも実際はこうなっていた。

path = Pathname.new('')         # => #<Pathname:>
path.join(path)                 # => #<Pathname:.>

空のPathnameと空のPathnameをjoinしてるんだから空のPathnameが欲しかったのに、 . がどこからか出てきてる。
なぜこうなっているんだろう。

2016-11-25

剰余を使わないFizzBuzz

Haskell

先日ESMで開かれたよちよち.hsに参加しました．
そこで剰余を使わずにzip3と無限リストを使ってFizzBuzzを書く話があったので書いてみました．

fizzbuzz = map fizzbuzz' $ zip3 [1..] (cycle ["","","Fizz"]) (cycle ["", "", "", "","Buzz"])
  where fizzbuzz' (_, "Fizz", "Buzz") = "FizzBuzz"
        fizzbuzz' (_, "Fizz", _) = "Fizz"
        fizzbuzz' (_, _, "Buzz") = "Buzz"
        fizzbuzz' (n, _, _) = show n

*Main> take 100 fizzbuzz
["1","2","Fizz","4","Buzz","Fizz","7","8","Fizz","Buzz","11","Fizz","13","14","FizzBuzz","16","17","Fizz","19","Buzz","Fizz","22","23","Fizz","Buzz","26","Fizz","28","29","FizzBuzz","31","32","Fizz","34","Buzz","Fizz","37","38","Fizz","Buzz","41","Fizz","43","44","FizzBuzz","46","47","Fizz","49","Buzz","Fizz","52","53","Fizz","Buzz","56","Fizz","58","59","FizzBuzz","61","62","Fizz","64","Buzz","Fizz","67","68","Fizz","Buzz","71","Fizz","73","74","FizzBuzz","76","77","Fizz","79","Buzz","Fizz","82","83","Fizz","Buzz","86","Fizz","88","89","FizzBuzz","91","92","Fizz","94","Buzz","Fizz","97","98","Fizz","Buzz"]

無限リストが扱いやすくていいですね．
こういう書き方もあったとは

2016-10-19

Rollbarでbotが出すエラーを無視する

Rollbar

botから既に削除されたURLへのアクセスがあり，Rollbarのエラーログのノイズがひどかったので，botからのアクセスで起こったActiveRecord::RecordNotFoundを無視する設定を書きました．

上部のバーからSettingsをクリックします．

次に画面左からGroupingをクリック．

jsonでCustom Groupを定義します．

ボットからのアクセスで起こったActiveRecord::RecordNotFoundをグルーピングするには次のようなjsonで定義できます．

[
  {
    "title": "Bot error",
    "fingerprint": "bot-error",
    "condition": {
      "all": [
        { "path": "request.headers.User-Agent",
          "in": [
            "Mozilla/5.0 (compatible; AhrefsBot/5.1; +http://ahrefs.com/robot/)",
            "Mozilla/5.0 (compatible; Yahoo! Slurp; http://help.yahoo.com/help/us/ysearch/slurp)",
            "Mozilla/5.0 (compatible; Googlebot/2.1; +http://www.google.com/bot.html)",
            "Mozilla/5.0 (iPhone; CPU iPhone OS 7_0 like Mac OS X) AppleWebKit/537.51.1 (KHTML, like Gecko) Version/7.0 Mobile/11A465 Safari/9537.53 (compatible; bingbot/2.0; +http://www.bing.com/bingbot.htm)",
            "Mozilla/5.0 (compatible; Exabot/3.0; +http://www.exabot.com/go/robot)"
          ]
        },
        { "path": "body.trace.exception.class",
          "eq": "ActiveRecord::RecordNotFound" }
      ]
    }
  }
]

このpathはOccurrenceのRawJSONで出力されているログのパス。リファレンスはこちら。 in以外にもeqやcontainなどがあります．

https://rollbar.com/docs/custom-grouping/

JSONが書けたら入力欄左下にあるボックスにoccurrence IDを入力してマッチさせたいエラーにマッチするか確認できます．

次にエラーが起こるとBot errorとしてグルーピングされるのでそれをmuteするとDashboardに表示されなくなります．逆に特定のエラーグループのlevelをwarningからcriticalに上げることもできたりもします．

2016-10-04

anagramの別解考えた