[TAPL] Types and Programming Languages Reading at Tokyo

Types and Programming Languages (通称 TAPL) の読書会の第0回が先日あったので報告。

TAPL読書会ですが、下記の様にGoogle groupが出来ました。開催情報とか流れるので興味のある方は登録をお勧めします。
http://groups.google.co.jp/group/taplreading-tokyo
次回開催は 11/3午後で、会場は同じく豆蔵オフィスです。

前回は、Chap.1はスキップ、Chap.2から読み始め、Chap.3の途中まででした。
次回はChap.3の続きから初めて、Chap.4(というか実装のChapterはこの先も)はスキップ、Chap.5を読む予定、となっています。
参加者は予習復習前提で、次回の範囲は予め読んで来ることが前提と、硬派な勉強会ということになりました。
Chap.4のような実装の箇所は各自実装したい人が自分で実装してちょっとデモをするということで。

参加者ですが、前回は総勢４名もCS専攻の大学院生の方が来てくれたのは良かったです。素人の社会人だけで勉強会してると簡単に行き詰るので。

懇親会も大変盛り上がっていたようで、大変有意義な一日でした。しかし、積読率高いですね＞TAPL。買ったけど読んでなかったとか、Chap.3までは読んだけどとか、そういう話ばっかり。

[event] Reading TAPL

Types and Programming Languages ( http://www.amazon.co.jp/dp/0262162091 ) という定番の教科書を読もうという読書会です。
東京近辺の方はぜひどうぞ。

http://atnd.org/events/8291

[Scala] Fibonacci series including 7110

　今更ながら http://recruit.drecom.co.jp/event2010 の「7110を含むフィボナッチ数列で、初期値の組み合わせが一番小さいものをあげろ。※自然数に限る」をScalaで解いてみた。
　もうイベントは終わったから解答公開してもいいよね。

　fib が 7110以下の範囲のフォボナッチ数列を計算する関数。zipとか使って格好良く書けるかもとも思うが、判りやすさ優先で。ysのところにxs'と書けないScalaは残念な感じだ。

scala> def fib(n0:Int,n1:Int) = {                   
     |   def f(xs:List[Int]):List[Int] = xs match { 
     |     case a::b::ys if a < 7110 => f((a+b)::xs)
     |     case _ => xs                             
     |   }                                          
     |   f(n1::n0::Nil)                                    
     | }
fib: (Int,Int)List[Int]

scala> def solve = for( n1 <- (1 to 100).toList;                       
     |   n0 <- (1 to n1).toList if fib(n0,n1).head==7110               
     | ) yield {(n0,n1)}
solve: List[(Int, Int)]

scala> solve
res7: List[(Int, Int)] = List((16,70), (70,86))
scala> 

[Coq] Coq-99 : Part 1

　前にS-99: Ninety-Nine Scala Problemsというのを紹介しましたが、Coqでも入門者が勉強用に解く為の問題集というのを考えてみました。

　まずは命題論理の証明の課題。勿論、tautoとかで一発だと思いますが、練習問題なので入門者は自力で解こう。
　Admitted.を消して証明を書く事が期待されています。

Section Prop_Logic.
  Lemma Coq_01 : forall A B C:Prop, (A->B->C) -> (A->B) -> A -> C.
  Admitted.
  Lemma Coq_02 : forall A B C:Prop, A /\ (B /\ C) -> (A /\ B) /\ C.
  Admitted.
  Lemma Coq_03 : forall A B C D:Prop, (A -> C) /\ (B -> D) /\ A /\ B -> C /\ D.
  Admitted.
  Lemma Coq_04 : forall A : Prop, ~(A /\ ~A).
  Admitted.
  Lemma Coq_05 : forall A B C:Prop, A \/ (B \/ C) -> (A \/ B) \/ C.
  Admitted.
  Lemma Coq_06 : forall A, ~~~A -> ~A.
  Admitted.
  Lemma Coq_07 : forall A B:Prop, (A->B)->~B->~A.
  Admitted.
  Lemma Coq_08: forall A B:Prop, ((((A->B)->A)->A)->B)->B.
  Admitted.
  Lemma Coq_09 : forall A:Prop, ~~(A\/~A).
  Admitted.
End Prop_Logic.

解答例は例えばこれとか。

[Joke]Falso : HyperVerifier and HyperProver

　twitterで知ったジョークサイトなんだが、Falso, by Estatis Inc.があります。

　「ある公理を導入すれば」なんでも証明出来てしまう(笑)という話で、それをいかにも画期的新製品みたいな感じに仕上げているのがおかしい。

　追記：togetter: Falso 定理証明系の大革命

[FM] Maude

　今日はFormal Methods Forumの勉強会で、いつものCoq (CPDT)の話の他に、Maudeをちょっと触ってみた、という話をしました。

　Maudeは項書き換え系の言語で形式仕様記述やモデル検査、DSL記述などにも使える言語です。
　Coqと違って証明も出来るけどメインは仕様記述＆それ自体がプロトタイプとして動く、かなぁ。パズルとかにも役に立つかも。

　あわてて作った資料なんで完成度は低いですがこちら。
Slideshare上のプレゼン
PDF資料

　Maudeに興味のある方はコメント頂けると嬉しいです。

[Coq] CoqUn -- Summer Coq Event in Nagoya

　2010/08/29に名古屋でCoq庵 -- 日本の夏、証明の夏というCoqのイベントが開催されます。
　といっても、Coqユーザが集まって話をしようという比較的緩いイベントなんで、Coq初めてという人も参加すると良いのではなかろうか。入門的な話もあります。

[Coq] Puzzle from Hiyama-san's Blog

　檜山さんのblogに掛け算から足し算を作る（パズルとしてやってみよう）という問題が載っています。
　Coqの練習問題としてちょうど良いかと思い解いてみました。
　思ったより時間がかかってしまい、解き終わる前にネタばらしが出ちゃったのだけど、一応、解いた解答です。http://ideone.com/Staa3

　分配則は簡単だったが、交換則を思いつくまでに苦労した。交換測を思いついたらその延長で結合則もなんとか。ただ、証明はちまちまとrewriteしてるだけ。ここは本当は自動化できるんだろうなぁ。
　Coq初心者的には、inv関係の{a'|a*a'=1}みたいな記法の使い方に慣れたのが良かったか。あとAxiom eq_dec_0:forall a:G, {a=0}+{a<>0}みたいなdecide出来る公理の便利さを実感した。

[Scala] Scala 2.8 Continuation (1)

root/compiler-plugins/continuations/trunk/doc/examples/continuationsに載っているサンプルコードをREPLで写経してみます。

Test0.scala

scala> import scala.util.continuations._            
import scala.util.continuations._

scala> reset {                                      
     |   2 * {                                      
     |     println("up")                            
     |     val x = shift((k:Int=>Int) => k(k(k(8))))
     |     println("down")                          
     |     x                                        
     |   }                                          
     | }
up
down
down
down
res1: Int = 64

これはdef k(i:Int):Int = {println("down"); 2*i}と考えればOK。

Test1.scala

scala> object Test1 {                                 
     |   def testThisMethod() = {                     
     |     1 + (shift((k:Int=>Int) => k(k(k(17)))))   
     |   }
     |   def testThisCallingMethod() = {              
     |     testThisMethod() * 2                       
     |   }
     |   def m() {
     |     val result = reset(testThisCallingMethod())
     |     println(result)
     |   }
     | }
defined module Test1

// ((((((17 + 1) * 2) + 1) * 2) + 1) * 2) = 150

scala> Test1.m()                                      
150

k = (_+1)*2 と考えればこれも予想通りの結果。
resetの中にshiftを書くのはOKだが、resetなしでshiftだけの関数を定義しようとすると下記の様にエラーになります。仕方が無いのでobject Test1 {...} に包みます。

scala> def testThisMethod() = {
     |   1 + (shift((k:Int=>Int) => k(k(k(17)))))
     | }
:2: error: type mismatch;
 found   : Int @scala.util.continuations.cpsSynth @scala.util.continuations.cpsParam[Int,Int]
 required: Int
object RequestResult$line4$object {
                                  ^

Test2.scala

scala> object Test2 {                             
     |   def methA() = {                          
     |     def fun(k:Int=>String) = {             
     |       for(i <- List(1,2,3,4)) println(k(i))
     |       Some("returnvalue")                  
     |     }                                      
     |     2 * shift(fun)                         
     |   }
     |   def methB() = {                          
     |     "+++ "+methA().toString()              
     |   }
     |   def m() = reset(methB())                 
     | }
defined module Test2

scala> Test2.m()
+++ 2
+++ 4
+++ 6
+++ 8
res0: Some[java.lang.String] = Some(returnvalue)

k = "+++" + (2 * _).toString() ですか。

[Scala] Scala 2.8 RC4 and continuation plugin

　Scala 2.8 RC4 が出ました --- が、なんかバグがあるらしく来週には RC5 が出るそうです。なんか品質安定しませんね＞Scala 2.8。

　RC4からは限定継続のコンパイラプラグインが付属される様になりました。
　使い方はこんな感じ。Scala 2.8 RC4を導入したディレクトリに居るとします。pluginにパスを通し、continuationをenableにする必要があります。

% cd ~/scala28rc4
% ./bin/scala -Xpluginsdir ./misc/scala-devel/plugins/ ¥
-Xplugin:continuations -P:continuations:enable
Welcome to Scala version 2.8.0.RC4 (Java HotSpot(TM) 64-Bit Server VM, Java 1.6.0_20).
Type in expressions to have them evaluated.
Type :help for more information.

scala> import scala.util.continuations._         
import scala.util.continuations._

scala> reset {
     |   shift { (k:Int=>Int) =>
     |     k(k(k(7)))
     |   } + 1
     | }
res0: Int = 10

scala> 

限定継続をおいおい勉強しようと思います。

[Coq] How to define complex inductions

Coq の証明の書き方パターンを yoshihiro503 さんに教わったので、忘れないうちに。

自然数に関する定理を証明したい場合に、下記の様な補題が欲しかったとします。

Lemma nat2_ind : forall P:nat -> Prop, P 0 -> P 1 ->
  (forall n:nat, P n -> P (S n) -> P (S (S n))) ->
  (forall n:nat, P n).

教わったコードを元に自分なりに書いてみたのが下記の証明です。

  
  ============================
   forall P : nat -> Prop,
   P 0 ->
   P 1 ->
   (forall n : nat, P n -> P (S n) -> P (S (S n))) -> forall n : nat, P n

nat2_ind < intros P H0 H1 IH.          
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ============================
   forall n : nat, P n

nat2_ind < refine (fix ll n : P n := _).     (* ここで refine を使って ll を定義するのがポイント *)
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  ============================
   P n

(* しかしここで apply ll しても駄目。llはIHの仮定のところで使う *)

nat2_ind < induction n.
2 subgoals
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  ============================
   P 0

subgoal 2 is:
 P (S n)

nat2_ind < exact H0.  (* n=0 のケースは P 0 *)
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  IHn : P n
  ============================
   P (S n)

nat2_ind < induction n.
2 subgoals
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  IHn : P 0
  ============================
   P 1

subgoal 2 is:
 P (S (S n))

nat2_ind < exact H1.  (* n=1 のケース *)
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  IHn : P (S n)
  IHn0 : P n -> P (S n)
  ============================
   P (S (S n))

nat2_ind < apply IH.   (* IH を使う *)
2 subgoals
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  IHn : P (S n)
  IHn0 : P n -> P (S n)
  ============================
   P n

subgoal 2 is:
 P (S n)

nat2_ind < apply ll.  (* IHの仮定のところにはll を使ってOK *)
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  IHn : P (S n)
  IHn0 : P n -> P (S n)
  ============================
   P (S n)

nat2_ind < apply IHn0.          
1 subgoal
  
  P : nat -> Prop
  H0 : P 0
  H1 : P 1
  IH : forall n : nat, P n -> P (S n) -> P (S (S n))
  ll : forall n : nat, P n
  n : nat
  IHn : P (S n)
  IHn0 : P n -> P (S n)
  ============================
   P n

nat2_ind < apply ll.  (* もう一度 ll を使う *)
Proof completed.

nat2_ind < Qed.

そもそもの証明のゴールをrefineを使ってllとして定義して、証明の中でllを使っているので非常に不思議なのですが、変な所（例えばrefine直後に）でapply llしてProof CompleteしてもQedしたとたんにエラーになります。エラーが出ない様にH0,H1,IHを使えば、証明が正しい事になります。

なお、同じ定理を短く書くとkikxさんの証明ゴルフみたいになるようです。すごい。

[Coq] Arithmetic in Coq : N

Nは二進数で表現された自然数の型です。

Require Import NArith.すると使用出来ます。型の定義は下記の様です。

Inductive N : Set :=  N0 : N | Npos : positive -> N

positiveは下記の様に定義されています。

Inductive positive : Set :=
    xI : positive -> positive | xO : positive -> positive | xH : positive

こんな感じで正の数を表現しています。xHが最上位ビットで、xIが x -> 2x+1, xOが x -> 2x ということです。

Coq < Check (xO (xI (xO xH))).
10%positive : positive

これは(1~0~1~0)%positive.とも書けます。

natとの変換は下記で可能。

nat_of_N : N -> nat
N_of_nat : nat -> N

演算子は

Ndouble_plus_one, Ndouble : N -> N
Nsucc, Npred : N -> N
Nplus, Nminus, Nmult : N -> N -> N　。+, -, * もあり。
Ncompare : N -> N -> comparison 。Infixで ?=
  comparisonは、
  Inductive comparison : Set :=
    Eq : comparison | Lt : comparison | Gt : comparison
Nlt, Ngt, Nle, Nge : N -> N -> Prop　。Infix で <, <=, >, >=
Nmin, Nmax : N -> N -> N
Ndiv2 : N -> N

Nに関する帰納法は次の２つの好きな方を使える。Nrectを用いてNindもある。

N_ind_double
     : forall (a : N) (P : N -> Prop),
       P 0%N ->
       (forall a0 : N, P a0 -> P (Ndouble a0)) ->
       (forall a0 : N, P a0 -> P (Ndouble_plus_one a0)) -> P a
Nrect
     : forall P : N -> Type,
       P 0%N -> (forall n : N, P n -> P (Nsucc n)) -> forall n : N, P n

Require Import ZArith.ZOdiv.すれば、

Ndiv_eucl : N -> N -> N * N
Ndiv : N -> N -> N
Nmod : N -> N -> N
Theorem Ndiv_eucl_correct: forall a b,
  let (q,r) := Ndiv_eucl a b in a = (q * b + r)%N.

と除算も使える。

---
追記
ZArith.ZOdivと、ZArithの中でImportしてるZArith.Zdivとは互換性無いのだな。
ZArithを使わないことはまず無いので、ZOdivは使わないほうがよさそう。

[Coq] Arithmetic in Coq : nat

Coqで大きな自然数あるいは整数を使いたくなったので調べてみました。

★nat

　Coqで自然数というと基本はnatです。natというと自分で作る物であるかの様な気すらしますが勿論標準で備わっています。
　natを使う場合Require Import Arith.すると標準ライブラリが使えます。

●基本
Init.Peanoの中で、pred, plus, mult, le, lt, ge, gtが定義されていてImport不要で使える。

●大小比較関係

- eq_nat : nat -> nat -> Prop
-- heorem eq_nat_decide : forall n m, {eq_nat n m} + {~ eq_nat n m}. が使える
- lt_eq_lt_dec n m : {n < m} + {n = m} + {m < n}. こんな感じで使う
Definition nat_compare (n m:nat) :=
  match lt_eq_lt_dec n m with 
    | inleft (left _) => Lt
    | inleft (right _) => Eq
    | inright _ => Gt
  end.
-- le_lt_dec n m : {n <= m} + {m < n}. など

●四則演算

- 末尾再帰なtail_plusというのもある
- minus : nat -> nat -> nat. n - m とかも書ける。結果が負になる場合もOを返す。
- min, max : nat -> nat -> nat.
- div2, double : nat -> nat.
- 除算は無いが、Require Import Arith.Euclid. すれば商と剰余には下記がある
-- quotient : forall n, n > 0 ->
    forall m:nat, {q : nat | exists r : nat, m = q * n + r /\ n > r}.
-- modulo : forall n, n > 0 ->
    forall m:nat, {r : nat | exists q : nat, m = q * n + r /\ n > r}.

[Coq] FoCaLize Tutorial (2)

　[Coq] FoCaLize Tutorial (2)の続き。

　前回のextsubset.fclに

  theorem incl_remove_mem : all s : Self, all v : Val,
                            ~(v << s) -> s <: s - v
    proof = by property mem_congr, mem_remove, mem_incl ;

を追加すると自動証明が失敗するのでFoCaLizeの手動証明を試す予定なのだが...自動証明がそのまま通るみたいだ。

　が、ここは一応Tutorial通り、手動証明も試してみる事にする、証明を下記の様に直してみる。

    proof = <1>1 assume s : Self, v : Val, hypothesis Hv : ~(v << s),
                 prove s <: s - v
              <2>1 assume w : Val, hypothesis Hw : w << s,
                   prove w << s - v
                <3>1 prove ~(Val!( = )(w, v)) /\ w << s
                  <4>1 prove ~(Val!( = )(w, v))
                       by property mem_congr hypothesis Hv, Hw
                  <4>2 prove w << s
                       by hypothesis Hw
                  <4>f conclude
                <3>f qed by property mem_remove step <3>1
              <2>f qed by property mem_incl step <2>1
            <1>f conclude ;

再度コンパイルするとこれでも通る。上記の様に手で証明を記述しても生成されたCoqの証明は短く分割されて読みやすくはなるもののやはり人間向けの証明とは言えない感じである。

証明に通らない例として

  theorem remove_insert : all s : Self, all v : Val,
                          v << s -> s = (s - v) + v
    proof = <1>1 assume s : Self, v : Val, hypothesis Hv : v << s,
                 prove s = (s - v) + v
              <2>1 assume w : Val, hypothesis Hw : w << s,
                   prove w << (s - v) + v
                   by property mem_insert, mem_remove
              <2>2 assume w : Val, hypothesis Hw : w << (s - v) + v,
                   prove w << s
                   by property mem_insert, mem_remove, mem_congr, Val!diff_eq
              <2>f qed by property eq_incl, mem_incl step <2>1, <2>2
            <1>f conclude ;

を試すと下記の様にエラーが出る。

% ~/pkg/bin/focalizec extsubset.fcl
Invoking ocamlc...
>> /Users/miyamoto/pkg/focalize-0.6.0/bin/ocamlc -I /Users/miyamoto/pkg/lib/focalizec-0.6.0 -c extsubset.ml
Invoking zvtov...
>> /Users/miyamoto/pkg/focalize-0.6.0/bin/zvtov -zenon /Users/miyamoto/pkg/focalize-0.6.0/bin/zenon -new extsubset.zv
File "extsubset.fcl", line 61, characters 19-53:                
Zenon error: could not find a proof within the memory size limit
### proof failed
%

これについてもチュートリアルに従い証明を完全に記述するとコンパイルに通る。

　なんとなくCoqに慣れてしまったので、FoCaLizeを用いて証明を記述する方が寧ろ判りにくいようにも思う。

[Coq] FoCaLize Tutorial (1)

　形式手法開発ツールのFoCaLizeをインストールして動かしてみました。

　FoCaLizeは言語名かつツール群の総称です。言語としては、ちょっとオブジェクト指向風（継承などの要素があったり、speciesというクラスっぽいものがある）な純粋関数型言語で、FoCaLizeという言語で書いたプログラムは、OCamlのコードが生成されると共に、（ちょっとしたヒントを人間が与える事で）Zenonという自動証明器がCoq用の証明を自動生成します。
　多分、普通のJavaプログラマとかには、素のCoqよりもFoCaLizeの方が習得しやすい思われる。逆にバリバリのOCamlerみたいな人には素のCoqを使う方が楽なんじゃなかろうか。
　開発元は例によってCoqなどと同じINRIAです。Coq界隈だけでもCoq自体に、FoCaLizeに、Ynotにとなんかツールが多過ぎて全然勉強がおいつきません。

★インストール

Downloadからtar ballをダウンロードして、

# ./configure
# make
# make install

するとOK。Coqが既に動くならそんなに大変じゃないと思う。（前提にghostscriptを要求されたり良く解らんところもあるが）

★superset.fcl

Tutorialに従い、まずはsuperset.fclをコンパイルしてみます。下記を superset.fcl として入力。文法は概ねOCaml風です。

use "basics" ;;
species Superset =
  signature ( = ) : Self -> Self -> basics#bool ;
  property eq_refl : all x : Self, x = x ;
  property eq_symm : all x y : Self, x = y -> y = x ;
  property eq_tran : all x y z : Self, x = y -> y = z -> x = z ;
  theorem eq_symmtran : all x y z : Self, x = y -> x = z -> y = z
    proof = by property eq_symm, eq_tran ;
end ;;

内容は大体見当がつくと思います。Selfというのは、OOな用語で言えば自クラスのことで、自インスタンス(Javaのthis)ではありません --- まぁ
Self -> Self -> basics#bool
を見ればそれは判るか。

% focalizec superset.fcl
でコンパイルすると、OCamlのコード (superset.ml) とかTheoremの証明 (superset.v) などが生成されます。eq_symm, eq_tran を使え、と指示するだけで自動証明されるのでCoqとかに不慣れでも使いやすいかも。ただ生成される証明が

exact(
(NNPP _ (fun zenon_G=>(zenon_notallex (fun x:abst_T=>(forall y:abst_T,(
forall z:abst_T,((Is_true (abst__equal_ x y))->((Is_true (abst__equal_
x z))->(Is_true (abst__equal_ y z))))))) (fun zenon_H2a=>(zenon_ex
abst_T (fun x:abst_T=>(~(forall y:abst_T,(forall z:abst_T,((Is_true (
   ...47行省略...
abst_eq_tran)))) zenon_H1b)) (zenon_notnot _ (refl_equal (abst__equal_
zenon_Tz_k zenon_Ty_e))) zenon_Hb)) zenon_H8 zenon_H9)) in (zenon_noteq
_ zenon_Ty_e zenon_H7)))) (fun zenon_H5=>(zenon_H6 zenon_H5)) zenon_H22)
) zenon_H23)) abst_eq_symm)) zenon_H24)) zenon_H25)) zenon_H26))
zenon_H27)) zenon_H28)) zenon_H29)) zenon_H2a)) zenon_G)))).

みたいな感じで、人間が読む証明じゃないよなー。あとNNPP : forall p : Prop, ~ ~ p -> pを使うのありなんだ、みたいな。

★subset.fcl

同様にsubset.fclを入力。

use "basics" ;;
open "superset" ;;

species Subset(Val is Superset) =
  signature ( << ) : Val -> Self -> basics#bool ;

  signature empty : Self ;
  property mem_empty : all v : Val, ~(v << empty) ;

  signature ( + ) : Self -> Val -> Self ;
  property mem_insert : all v1 v2 : Val, all s : Self,
                        v1 << s + v2 <->
                        (Val!( = )(v1, v2) \/ v1 << s) ;

  signature ( - ) : Self -> Val -> Self ;
  property mem_remove : all v1 v2 : Val, all s : Self,
                        v1 << s - v2 <->
                        (~(Val!( = )(v1, v2)) /\ v1 << s) ;
end ;;

　内容は見れば判ると思いますが<<, +, -が集合の∈、要素の追加、削除に対応します。Val!( = )とうのはValクラスの( = )メソッドを呼び出す、みたいな意味です。

★extsubset.fcl

次に継承を使う例を。ExtSubsetはSubsetを継承します。

use "basics" ;;
open "superset" ;;
open "subset" ;;

species ExtSubset(Val is Superset) =
  inherit Superset, Subset(Val) ;

  signature ( <: ) : Self -> Self -> basics#bool ;
  property mem_incl : all s1 s2 : Self,
                      s1 <: s2 <-> all v : Val, v << s1 -> v << s2 ;
  theorem incl_refl : all s : Self, s <: s
    proof = by property mem_incl ;
  theorem incl_tran : all s1 s2 s3 : Self,
                      s1 <: s2 -> s2 <: s3 -> s1 <: s3
    proof = by property mem_incl ;

  theorem incl_empty : all s : Self, empty <: s
    proof = by property mem_incl, mem_empty ;
  theorem incl_insert : all s : Self, all v : Val, s <: s + v
    proof = by property mem_insert, mem_incl ;
  theorem incl_remove : all s : Self, all v : Val, s - v <: s
    proof = by property mem_remove, mem_incl ;

  let ( = ) (s1, s2) = if (s1 <: s2) then (s2 <: s1) else false ;

  property mem_congr : all v1 v2 : Val, Val!( = ) (v1, v2) ->
                       (all s : Self, (v1 << s) <-> (v2 << s)) ;

  theorem incl_insert_mem : all s : Self, all v : Val,
                            v << s -> s + v <: s
    proof = by property mem_congr, mem_insert, mem_incl ;
end ;;

　この次には、自動証明が失敗するケースを扱います。

[Coq] ASN.1 Library is under construction

　この連休にCoqの練習がてら作っていたASN.1のライブラリで、全然完成してないのだがとりあえず出来たところまで公開。
　Coqdocで生成したドキュメントがTLV.htmlです。（コードが成長したら随時更新予定）

　ASN.1が何かについては、A Layman's Guide to a Subset of ASN.1, BER, and DERあたりを読んで下さい。電子証明書とかで使っているバイナリフォーマットなので、証明付きのライブラリを作りたいのだ。

　本当は

Inductive tlv_value : Set := 
| Primitive : string -> tlv_value 
| Structured : list tlv -> tlv_value
.

みたいに定義したかったのだが、そうするとtlv_value, tlv に関する帰納法をうまく構成出来なかった。まだCPDT Chapter 3の読み込みが足りないのだろうなぁ。
　が、とりあえず幾つかの定理も証明できたし、出だしとしてはこんなものかもとも思う。

　Coqを勉強しようと思う様なプログラマの人は、ある程度複雑な型（相互再帰的だったり再帰がネストしていたり）を定義出来ると思うが、Coqは帰納型に対して帰納法を与える関数が作れないと駄目で、しかしそこが実は難しい、というのがこの連休に得た知見だ。

[Coq] How to use Record

　Coq で Record を使う方法を調べました。基本的には記述を簡単にする構文糖のようです。これを使うと、事前条件を満たす証明を要求するコンストラクタを簡単に書けます。
　使い方は下記の例を見てもらうのが簡単でしょう。

　まず正の有理数を表すRat型を作りたいと考えます。符号は無視するとして、分母が０で無いことを保証したい、分子分母が既約である事を保証したい、とします。こんな感じに書けます。

Record Rat : Set := mkRat {
  numer : nat;
  denom : nat;
  denom_not_zero : denom <> O;
  irreducible : forall g n d:nat, 
    (mult g n)=numer /\ (mult g d)=denom -> g = S O
}.

Ratで 1/2 を定義したい時はこんな感じになります。まず補題を証明しないと値を作れません。

Lemma two_not_zero : 2 <> 0.
Proof.
  discriminate.
Qed.
Lemma one_two_irred : forall g n d:nat, (mult g n)=1 /\ (mult g d)=2 -> g = S O.
Admitted. (* 証明省略 *)

こうして初めて値を作れます。

Definition half : Rat := mkRat 1 2 two_not_zero one_two_irred.
Print half. (* mkRat 1 2 two_not_zero one_two_irred : Rat *)
Eval compute in (numer half). (* 1 : nat *)
Eval compute in (denom_not_zero half). (* two_not_zero *)

アクセサに見えるnumerなどは単なる関数です、従って同じ名前空間でnumerを他に定義出来ません。

Print numer.
numer = 
fun r : Rat => let (numer, denom, _, _) := r in numer
     : Rat -> nat

Ratに関する帰納法は下記の様になります。

Print Rat_ind.
(* forall P : Rat -> Prop,
       (forall (numer denom : nat) (denom_not_zero : denom <> 0)
          (irreducible : forall g n d : nat,
                         g * n = numer /\ g * d = denom -> g = 1),
        P (mkRat numer denom denom_not_zero irreducible)) ->
       forall r : Rat, P r *)

[Alloy][FM] Sample code: Addressbook

　[Coq][FM] Fomal Methods Forum #4でのAlloyチュートリアルの話。

　まず Alloy4 を各自インストールしておくのは前提。但し、JARファイル１つなので、JRE (Java5以上) が入っているコンピュータならば起動は難しくありません。

　表示されるWindowの左側入力欄に下記を打ち込みます。

sig Name, Addr {}
sig Book {
  addr: Name -> lone Addr
}

　sigというのは普通のOO言語のクラス定義の様なもの --- なんですが、Alloy はOOなプログラミング言語ではないのでOOとのアナロジーは時に誤解を与えるかも。どちらかというと、RDBMSに Name, Addr という表を作ったと考えるといいかも。実際、Alloy は関係代数に基づいていますし。
　OO でいうところのインスタンスはAlloyではatomと言います。Alloyでインスタンスというのは、全てのatomから構成されるモデル（モデルの中には求める反例とかも含まれます）のことを指します。用語は間違わない様に。
　また、. (ドット演算子) もOO言語の属性やメソッドを指す様に勘違いしますが、join演算子で、RDBのjoinみたいな振る舞いをします。
　Bookのatomを仮に B0, B1 と書くと、Book は {(B0), (B1)} という集合です。（ () はタプル、{}は集合を表す。）

　lone は 0 or 1 個を表す数量限定子です。他にも all (全ての)、some (１個以上)、one (１個)、no (０個) があります。lone Addr は、関数型言語的には Option Addrのようなものです。
　addr は Book の属性みたいに見えますが、これも関数型言語的には addr : Book -> Name -> Option Addr -> Prop みたいに考えると良いです。addr は (Book, Name, Addr) のタプル型の元の集合、例えば{(B0,N0,D0), (B1,N1,D1)}として表現されます。 （関係 R : R x y は (X,Y) の部分集合として表現出来る）
　Book = {(B0),(B1)} であると、ドットはjoin演算子なので（テンソルとかの添字の縮約の如く）ジョイン演算をします。Bookとaddrの共通のB0を見て(B0).(B0,N0,D1)=(N0,D0)の様に計算して、b=B0ならば、b.addr={(N0,D0)}, Book.addr={(N0,D0),(N1,D1)} となります。

　この時点で sig Book {...} の下に

pred show[] {}
run show for 3

と書いて Execute のボタンを押します。
　右側に Instance found と出るので Instance のリンクを押すと、atom 間の関係を示すダイヤグラムが表示されます。nextを押すと別のインスタンスが表示されます。
　for 3 と書いたので各 sig 毎に 3 atom づつです。

　次にモデルの性質をテストする事を考えます。addr を追加して削除すると元に戻る、という性質が成り立つ事をモデル検査で確認（＝反例が見つからない事を確認）します。
　まず追加と削除を表す述語を定義します。述語なので戻り値は真偽値を返します。

pred add[disj b,b':Book, n:Name, a:Addr] {
  b'.addr = b.addr + (n -> a)
}
pred del[disj b,b':Book, n:Name] {
  b'.addr = b.addr - (n -> Addr)
}

　Alloyは手続き型言語ではないので、b'addrに何か破壊的代入が行われる事は無く、単にbとb'の間の関係を示しているだけです。disjはbとb'とが別atomであるという意味です。

　次いでテストしたい性質を書きます。

assert delUndoesAdd {
  all b,b',b'':Book, n:Name, a:Addr |
    add[b,b',n,a] and del[b',b'',n] implies b.addr = b''.addr
}
check delUndoesAdd for 5

　|はsuch thatみたいな意味、and, implisは論理演算の記号です。

　これを追加してexecuteすると「何故か」counterexampleが見つかったと表示されます。counterexampleをじっと眺めると、bとb'が同じBookであることが判ります。
　これは元々 b に (n -> a) が含まれていた場合、b, b' が同じになるからです。（集合に既にある要素を加えても同じ）
　assertの中身を

    no n.(b.addr) and add[b,b',n,a] and del[b',b'',n] implies b.addr = b''.addr

に修正するとconterexampleが無くなります。

[Coq][FM] Fomal Methods Forum #4

　4/29に第4回FormalMethods勉強会を行いました。

　今回は
Alloy
　Alloyの教科書の例題（アドレス帳）を元に文法を勉強しました。大体文法は把握出来たかな。
　あとは自分で使ってみるべきなんだろうが、あまりモデリングとか仕事でやらないしなぁ。とりあえずパズルをAlloyで解く練習をするかなぁ。

CEGAR
　今回はCEGARという手法の話を聞きました。CEGARはCounterExample-Guided Abstraction Refinementの略で、モデル検査における状態数爆発を抑える為の一手法です。
　モデル検査で扱う検査の中に、到達可能性解析（エラー状態などの特定の状態にと到達するか否かの解析）があります。
　状態数を抑える方法としてモデルの抽象化（モデルの粗視化）があります。抽象化によって、エラー状態に遷移する可能性のある状態と、到達しない状態とが同一視されてしまうと、本当はエラー状態に到達しないにも関わらず、エラー状態に達すると誤って判定されます。
　CEGARは、エラー状態に到達する解に対して、解析（最弱事前条件？）を行って抽象化を修正（状態を分割）して再解析する手法です。エラー状態に達した場合にはそれが本当に達したのか、抽象化を改善して再度解析を実施します。
　原理だけ聞くと、当たり前の話と思えるのですが、実際に自動化するところを実装するのは難しそうというか見当が付かない。

Coq
　CoqはCertified Programming with Dependent TypeのChapter 1,2をざっと流して、Chapter 3を3.3まで読み終わりました。
　当日使用した資料 (PPT, Coqファイル) についてはGoogleグループ上の記事にリンクを纏めましたので、そちらから辿って下さい。
　本当はChapter 3を終わりたかったのですが終わらなかったのはちょっと残念でした。

[Coq] Tail-recursive reverse

　先のreverse (reverse xs) = xsで示した reverse は末尾再帰でなく、効率の悪い定義である。
　そこで末尾再帰な

Fixpoint rev' {A:Set} (xs ys:list A) :=
 match xs with
 | nil => ys
 | cons x xs' => rev' xs' (cons x ys)
 end.
Definition rev {A:Set} (xs:list A) :=
 rev' xs nil.
Eval compute in rev (cons 1 (cons 2 (cons 3 nil))).

について

Theorem reverse_rev : forall (A:Set) (xs:list A),
 reverse xs = rev xs.

が成り立つ事を示そう。まず補題

Lemma rev'_reverse : forall (A:Set) (xs ys:list A),
 rev' xs ys = reverse xs ++ ys.
Proof.
 intros A xs.
 induction xs; simpl.
   intro. reflexivity.
 intro ys'.
 rewrite (IHxs (cons a ys')).
 (* reverse xs ++ cons a ys' =
    (reverse xs ++ cons a nil) ++ ys' *)
 assert (H: cons a ys' = (cons a nil) ++ ys').
 induction ys'; simpl.
   reflexivity.
 reflexivity.
 rewrite H.
 rewrite (append_assoc A (reverse xs) (cons a nil) ys').
 reflexivity.
Qed.

である。証明の冒頭で intros A xs だけを行い、ysについては intro していないが、ys を残したまま xs の帰納法を行わないと、IHxs を apply するときにうまくいかない。「無闇に intro しない方が良い」という良い例なので、ys を一緒に intros してしまうなど自分で試行錯誤してみて欲しい。

　この補題を使えば、

Theorem reverse_rev : forall (A:Set) (xs:list A),
 reverse xs = rev xs.
Proof.
 intros.
 unfold rev.
 induction xs; simpl.
   reflexivity.
 (* reverse xs ++ cons a nil = rev' xs (cons a nil) *)
 rewrite IHxs.
 (* rev' xs nil ++ cons a nil = rev' xs (cons a nil) *)
 rewrite (rev'_reverse A xs nil).
 rewrite (rev'_reverse A xs (cons a nil)).
 assert (H: forall l:list A, l ++ nil = l).
   induction l; simpl.
     reflexivity.
   rewrite IHl.  reflexivity.
 rewrite (H (reverse xs)).
 reflexivity.
Qed.

と証明出来る。