今日は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 ＠はてな

2010-07-18

TDDBC名古屋に行ってきました。

TDD Boot Camp名古屋に参加しました。

id:t-wadaさんの講演はすばらしく、TDDをずっと推し進めている経験に基づく具体的な知見は大変わかりやすく勉強になりました。
当日のスライドはid:t-wadaさんのブログで見ることができます。TDD Boot Camp 名古屋に登壇させていただきました - t-wadaの日記

テストをするとき、対象とする関数に副作用が含まれる場合に困難が伴います。私は関数型言語チームとしてOCamlやScalaで参加しましたが、関数型言語は副作用を推奨しないということが言語設計の根底にあるため、テストがしやすいといった特徴があるように感じました。

講師のid:t-wadaさん、id:bleis-tiftさんやスタッフの皆さん、ありがとうございました。

2010-07-13

Alloyセミナーに行ってきました

形式手法 Alloy セミナー

7/12に名古屋市工業技術研究所で行われた id:kencobaさんによる Alloyセミナーに、講師補佐としてお手伝いさせてもらいました。当日の資料はこちらから辿れます。Alloy Analyzer入門セミナー - kencobaの日記

TDDBC名古屋で2日間テスト駆動開発を行った直後でしたが、テスト駆動は開発者向けの手法、Alloyはどちらかというと設計者向けのテストツールのように感じました。

プログラミングの手法や品質管理に比べ、設計書をチェックする手法はあまりないように思います。しかし設計段階での記述漏れやあいまいさがありそれに実装段階で気づいた場合、大きな出戻りが発生することがあります。このような設計段階の誤りを減らすためにAlloyのような軽量な検証ツールは非常に効果的なのではないでしょうか。

システム開発において設計者はAlloyを使い、開発者はテスト駆動開発を行えば、極めて効率よく高品質のものができあがるんじゃないかと考えています。

2010-07-04

掛け算から足し算を作る(足し算の一意性について)

Coq

http://d.hatena.ne.jp/kikx/20100629#1277831079 の素晴らしい足し算の存在証明を見つけたので、その存在が一意(ユニーク)であることを証明した。元々のネタはこちら http://d.hatena.ne.jp/m-hiyama/20100629/1277774676

まずは集合AとA上の掛け算とサクセッサSを仮定。この部分はid:kikxさんのコードのコピー。

Axiom A : Set.
Axiom A_eq_dec: forall a b: A, { a = b } + { a <> b }.

Axiom A_mul : A -> A -> A.
Axiom A_zero: A.
Axiom A_one: A.

Infix "*" := A_mul.
Notation "0" := A_zero.
Notation "1" := A_one.

Axiom A_mul_assoc: forall a b c, (a * b) * c = a * (b * c).
Axiom A_mul_comm: forall a b, a * b = b * a.
Axiom A_mul_1_r: forall a, a * 1 = a.
Axiom A_mul_inv_ex: forall a, a <> 0 -> { a': A | a * a' = 1 }.
Axiom A_mul_0_r: forall a, a * 0 = 0.

Lemma A_mul_1_l: forall a, 1 * a = a.
Proof.
  intros.
  rewrite (A_mul_comm 1 a).
  exact (A_mul_1_r a).
Qed.

Definition A_inv a (H: a <> 0) :=
  let (a', H) := A_mul_inv_ex a H in a'.

Axiom S: A -> A.
Axiom S_inv: A -> A.

Axiom S_inv_l: forall a, S_inv (S a) = a.
Axiom S_inv_r: forall a, S (S_inv a) = a.
Axiom S_0:  S 0 = 1.
Axiom  S_mul: forall a b (H: a <> 0),
  S (a * S (b * A_inv a H)) = a * S (S b * A_inv a H).

Lemma inv_is_inv: forall a (H: a <> 0), a * A_inv a H = 1.
Proof.
  intros.
  unfold A_inv.
  case (A_mul_inv_ex a H).
  trivial.
Qed.

ここからA上の足し算も仮定。同時に足し算が満たすべき公理も仮定。

Parameter A_add : A -> A -> A.
Infix "+" := A_add.
Hypothesis A_add_1_r_S: forall a, a + 1 = S a.
Hypothesis A_add_dist: forall a b c,  a * (b + c) = a * b + a * c.
Hypothesis A_add_0_r: forall a, a + 0 = a.
Hypothesis A_add_comm: forall a b, a+ b = b + a.
Hypothesis A_add_assoc: forall a b c, (a + b) + c = a + (b + c).
Hypothesis A_neg_ex: forall a, { a': A | a + a' = 0 }.

id:kikxさんの定義した足し算をA_kikxs_addという名前で用意し、上で仮定した抽象的な足し算A_addがA_kikxs_addと必ず等価になることを証明した。このことからA_addは一意であることが示せた。

Definition A_kikxs_add a b :=
  match A_eq_dec a 0 with
  | left _ => b
  | right H => a * S (b* A_inv a H)
  end.

Theorem uniqueness : forall a b, A_add a b = A_kikxs_add a b.
Proof.
 intros a b.
 unfold A_kikxs_add.
 case (A_eq_dec a 0).

  intro eq; rewrite eq.
  rewrite A_add_comm.
  rewrite A_add_0_r.
  reflexivity.

  intro neq.
  pattern a at 1; rewrite <- (A_mul_1_r a).
  pattern b at 1; rewrite <- (A_mul_1_l b).
  pattern 1 at 2; rewrite <- (inv_is_inv a neq).
  rewrite (A_mul_assoc).
  rewrite <- A_add_dist.
  rewrite (A_add_comm 1 _).
  rewrite A_add_1_r_S.
  rewrite (A_mul_comm _ b).
  reflexivity.
Qed.

2010-05-22

Coqで多変数多項式の簡約

Coq CPDT

変数全体の集合varを{ $x_0,x_1,x_2,...$ }というように自然数の対応で与えられると考え、式expを以下のように定義する。

Inductive exp : Set :=
| Var : var -> exp
| Const : nat -> exp
| Binop : binop -> exp -> exp -> exp.

ここで binop型の値は二項演算子(binary operation)の種類(＋または×)を表すものとして以下で定義されるものとし、定数項は簡単のため自然数(nat)に限るとする。

Inductive binop : Set := Plus | Times.

つまり、この定義のもとでは以下のように多項式が表現される。

多項式	Coqでの表現
$x_0+1$	Binop Plus (Var 0) (Const 1)
$x_0^2+x_1^2$	Binop Plus (Binop Times (Var 0) (Var 0)) (Binop Times (Var 1) (Var 1)

各変数から値への対応 (var -> nat) を環境として、ある環境ctxにおける式eの意味を次で再帰的に与える。

Fixpoint expDenote (ctx: var -> nat) (e : exp) : nat :=
  match e with
    | Var v => ctx v
    | Const n => n
    | Binop b e1 e2 => (binopDenote b) (expDenote ctx e1) (expDenote ctx e2)
  end.

そして式e1とe2の意味が同じという事を $\forall$ ctx, expDenote ctx e1 = expDenote ctx e2として考える事ができる。

ここで式eに対して、定数部分に関する部分的に簡単な形にする畳み込み関数を次で定義し、その健全性を示す。

Fixpoint constFold (e : exp) : exp :=
  match e with
    | Var v => Var v
    | Const n => Const n
    | Binop b e1 e2 =>
      match (constFold e1, constFold e2) with
        | (Const m, Const n) => Const ((binopDenote b) m n)
        | (e1', e2') => Binop b e1' e2'
      end
  end.

eを深さ優先に探索し、定数同士の2項演算を評価している。

ここで、この部分的な評価関数において、式eの意味が絶対変わらないことを証明する。

Lemma const_fold_preserved : forall e ctx,
  expDenote ctx e = expDenote ctx (constFold e).
Proof.

induction e.
 reflexivity.
 
 reflexivity.
 
 intro ctx; simpl; rewrite IHe1; rewrite IHe2.
 destruct (constFold e1); destruct (constFold e2); reflexivity.
Qed.

今回のネタはCPDTのExcercise 3.2 から取ってきた。CPDTはCoqでプログラムするときに必要な知識や便利な技を紹介していて非常にためになるので、Coqプログラミングをやりたい人にはぜひともオススメである。また、現在CPDTを勉強しているグループはFormal Method勉強会やProofCafe - coqグループなどあるので、参加してみてはいかがだろうか。

ソースコード全体と問題文は以下: http://ideone.com/kGLVw