■

いい加減、ベースになってる理論も知っとくべきだとか思ったので、Wikipediaを見た。
http://en.wikipedia.org/wiki/Calculus_of_constructions
Calculus of Constructions(CoC)は、型をファーストクラスとして扱える高階型付きラムダ計算です、とのこと。私には、さっぱりラムダ計算に見えません。それに、帰納法を付け加えたのが、Calculus of Inductive constructionsで、今のCoqのベースらしい。今は、Coinductionも一応あるけど。CoCの生みの親がCoquandという人らしいので、Coqの名前の由来はそこから？

単純型付き計算がCurry Howard対応によって、直観主義命題論理の自然演繹に対応するのに対して、直観主義述語論理に対応するものを作ろうというのが基本方針らしいけど、あとはまあ、The basics of the calculus of constructionsを見ても、さっぱりわからんな。"Defining logical operators"がなんか凄い。Coqで

Coq < Variable A:Prop.
Coq < Goal forall x:A,A.
1 subgoal

  ============================
   A -> A

forall x:A,BがちゃんとA->Bと見なされてるっぽい。意味わかんねー。A->Bの定義はいまいち謎だけど、他はなんとなく分かる。A->B->A/\Bに相当する

Coq < Variable B:Prop.
Coq < Goal A->B->(forall C:Prop , (A->B->C)->C). 

とかが証明できるし。「Aでない」というのは、「Aから任意の命題Cが導ける」と解釈するのもまあ理解できる。うーん。関連項目のLambda Cubeって昔聞いたけど、Borg Cubeの親戚かよ！としか思わなかったなー

というわけで、理論はよく分からないので諦める。それから、実験的な機能だけど、プログラム抽出というのが面白い。
http://coq.inria.fr/doc/Reference-Manual021.html

Coq < Require Import Euclid.
Coq < Recursive Extraction quotient.
type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f

type nat =
  | O
  | S of nat

type 'a sig0 = 'a
  (* singleton inductive, whose constructor was exist *)

type sumbool =
  | Left
  | Right

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

let rec minus n m =
  match n with
    | O -> O
    | S k -> (match m with
                | O -> S k
                | S l -> minus k l)

(** val le_lt_dec : nat -> nat -> sumbool **)

let rec le_lt_dec n m =
  match n with
    | O -> Left
    | S n0 -> (match m with
                 | O -> Right
                 | S n1 -> le_lt_dec n0 n1)

(** val le_gt_dec : nat -> nat -> sumbool **)

let le_gt_dec n m =
  le_lt_dec n m

(** val lt_wf_rec : nat -> (nat -> (nat -> __ -> 'a1) -> 'a1) -> 'a1 **)

let rec lt_wf_rec p f =
  f p (fun y _ -> lt_wf_rec y f)

(** val gt_wf_rec : nat -> (nat -> (nat -> __ -> 'a1) -> 'a1) -> 'a1 **)

let gt_wf_rec n x =
  lt_wf_rec n x

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

let quotient b a =
  gt_wf_rec a (fun n h0 ->
    match le_gt_dec b n with
      | Left -> S (h0 (minus n b) __)
      | Right -> O)

非常に頭悪いコードだけど、quotientで商を計算できる(多分)。Euclidライブラリはここらへん。他の言語もいける

Coq < Extraction Language Scheme.
Coq <  Recursive Extraction quotient.
;; This extracted scheme code relies on some additional macros
;; available at http://www.pps.jussieu.fr/~letouzey/scheme
(load "macros_extr.scm")

(define __ (lambda (_) __))

(define minus (lambdas (n m)
  (match n
     ((O) `(O))
     ((S k) (match m
               ((O) `(S ,k))
               ((S l) (@ minus k l)))))))

(define le_lt_dec (lambdas (n m)
  (match n
     ((O) `(Left))
     ((S n0) (match m
                ((O) `(Right))
                ((S n1) (@ le_lt_dec n0 n1)))))))

(define le_gt_dec (lambdas (n m) (@ le_lt_dec n m)))

(define lt_wf_rec (lambdas (p f) (@ f p (lambdas (y _) (@ lt_wf_rec y f)))))

(define gt_wf_rec (lambdas (n x) (@ lt_wf_rec n x)))

(define quotient (lambdas (b a)
  (@ gt_wf_rec a (lambdas (n h0)
    (match (@ le_gt_dec b n)
       ((Left) `(S ,(@ h0 (@ minus n b) __)))
       ((Right) `(O)))))))

マクロないと動かないけど、サイトにアクセスできないので、macros_extr.scmを入手できない。まあ、雰囲気で。基礎になってる原理は、構成的プログラミングとか、そういうのだと思う。よく分かってないけど。生成されるコードは頭悪いし、そもそもCoqで証明書く方が大体大変なので、今のところ実用にはならないけど

Prologなんかで、appendを書く場合(Prolog使ったことないけど)

appendp(X, Y, Z) :- X = [] , Z = Y. 
appendp(X, Y, Z) :- X = [W|X1] , appendp(X1, Y, Z1) ,  Z = [W|Z1].

みたく書くけど、こういう定義と、forall x y:list,exists z:list,appendp(x,y,z)の証明(帰納法)から、普通のappend関数を抽出できたりすると面白い。xに関する帰納法で証明したら、

(define (append X Y) (foldr cons Y X))
;但し
(define (foldr f init L) (if (null? L) init (f (car L) (foldr f init (cdr L)))))

みたいなコードが生成されるはず。foldrが出てくるのは、証明に帰納法を使ったから。

(2006/10/11)以下の話は、間違っていたので修正。http://d.hatena.ne.jp/m-a-o/20061011#p2も参考
foldrに倣って、自然数に対するfoldを書くとこんな感じかな

(define (fold-nat f init x) (if (= x 0) init (f (fold-nat f init (- x 1)))))

何をやってるのか、私にもよく分かりませんが、例えば(fold-nat + 0 n)で、0〜nの総和を計算。

(define (f b)
 (lambda (y)
   (cond
    ( (= (cdr y) (- b 1)) (cons (+ (car y) 1) 0) )
    ( else (cons (car y) (+ (cdr y) 1)) ))))

(define (div a b)
 (fold-nat (f b) (cons 0 0) a))

で割り算みたいな。div関数は、商と余りのペアを返す関数。

で、何本かCoq使った論文眺めて見たけど、ライブラリは数学の定理やるんでもなければ、リスト以外はあんまりいらないっぽいので、あとは適当にtacticの使い方練習しながら、論文読んでけばいいのかもしれない。と言いつつ既にCoqに飽きてきた。まあ、これ以上使うつもりなら、ちゃんとCoq'Artとか読んだ方がいいのかもしれない。