COMFRK宣伝

http://ratiwo.blogspot.com/2010/12/comfrk-vol-2.html

2010年ももう終わり、明日は12月の31日です。12月の31日ということは、コミックマーケット79の3日目であり最終日であります。

皆さんは、ぼくが夏コミにおいてCOMFRKというサークルに参加し、単純型付けλ計算における強正規化性定理(strong normalization theorem)の極めてスタンダ〜ドな記事を書いた事をご存知だと思います。

今回、冬コミにおいてもCOMFRKに1本記事を送りつけました。
夏コミ終わったあたりでは、C++のConceptに対する色んな話を書いてみます的な事を書いていましたが、アレは完全に嘘に成りました。それは又の機会。

今回の記事のタイトルは「型理論におけるパラドクス」となりました。
型理論とパラドクスで大体ピンと来た方は、はい、その通りの事が書いています。あら探しの為に買ってください！

ピンと来ない方でも、Russellのパラドクス、とかそういう単語を連想した事かと思います。
まさにそのパラドクスの事で、本文でもRussellのパラドクスについては触れています。

いやしかし、パラドクスっていうのはこう、集合とか、論理とか、そういう話なんだから型理論というか、型システムというか、つまり型とは、何の関係も無いんじゃ無いの? という疑問があるかもしれません。
そこは簡単に言い切るならば、Curry-Howard Isomorphismで！という話になるのですが、まぁ静的型付けなプログラミング言語というのはある種の論理の系であって、プログラム書いてるのか証明書いてるのか分からなく成る瞬間がある、そんな話です。

そんなパラドクスが言えるような型システムを調べて何に成るの? という疑問が出て来ます。
これには、何故型理論においてパラドクスが生まれてしまったのかを述べる事で答えたいと思います。より優れた道具を使ってプログラムを書きたいとすると、型システムを最強に近づけるというのは自然な要求なわけです。
しかしあるラインを超えてしまうと、従来の型システムの元でなりたった色んな良い性質が損なわれてしまいます。そのあるラインとして、パラドクスを導けるか導けないかというのを考えるわけです。

今回は、最近流行のCoq、そのベースとなる型システム(Calculus of Construction)を拡張するとパラドクスが発生してしまいます！という部分に着眼して書いてみたつもりです。
正確に内容を述べるならば、色んな関連論文を纏めてみましたとかそういう話で、まぁ簡単に言うと勝手に訳をしましたみたいな感じです。つまり、ぼくが導いた話ではありませんよ！！

以下に拡張したCoqがinconistent(全ての命題が証明出来る 矛盾する)であるというCoq自身による証明を載せておきます。記事を読めば、証明が理解出来るようになっていますから、気になる方は、是非とも サークル設置場所 まで、足を運んでください！！

一応当日は色んな参考資料を持って行くようにします。人の邪魔に成らない範囲で、皆様とお話出来る事を楽しみにしています。
そう、ぼくは売り子というなのラブライブマイクロファイバータオル入手係なのです！！

(* proof inconsistency *)

Variable U : Set.
Variable p2b : Prop -> bool.
Variable b2p : bool -> Prop.
Variable p2p : forall (A : Prop) , b2p (p2b A) = A.
Variable b2b : forall (B : bool) , p2b (b2p B) = B.

Definition Pow (X : Set) : Set := X -> bool.

Definition pU := Pow U.

Variable σ : U -> pU.
Variable τ : pU -> U.
Variable paradoxical :
forall (X : pU) , σ(τ X) = (fun (y:U) => p2b (exists x : U , b2p (X x) /\ y = τ(σ x))).

Definition predc y x := (σ x) y. (* y < x *)

Definition induct (X : pU) := forall (x : U) , (forall (y : U) , b2p ((σ x) y) -> b2p (X y)) -> b2p (X x).
Definition wf (x : U) := forall (X : pU) , induct X -> b2p (X x).

Lemma lem1 : forall (x y : U) , b2p (predc y x) -> b2p (predc (τ(σ y)) (τ(σ x))).
Proof.
intros.
unfold predc in H.
unfold predc.
rewrite paradoxical.
rewrite p2p.
exists y.
split.
 assumption.
 
 trivial.
Qed.

Definition Δ := (fun (x:U) => p2b (wf x)).
Definition Ω := τ Δ.

Lemma lem2 : wf Ω.
Proof.
unfold wf.
intros.
unfold induct in H.
unfold Ω.
unfold Δ.
apply (H Ω).
intros.
unfold Ω in H0.
rewrite paradoxical in H0.
rewrite p2p in H0.
unfold Δ in H0.
destruct H0.
destruct H0.
rewrite H1.
clear H1.
clear y.
rewrite p2p in H0.
cut (induct (fun e : U => X (τ (σ e)))).
 intro.
 unfold wf in H0.
 apply (H0 _ H1).
 
 unfold induct.
 intros.
 apply H.
 intros.
 rewrite paradoxical in H2.
 rewrite p2p in H2.
 destruct H2.
 destruct H2.
 rewrite H3.
 apply (H1 x1 H2).
Qed.

Lemma lem4 : wf Ω -> b2p (predc (τ(σ Ω)) Ω).
Proof.
intro.
unfold predc.
unfold Ω at 1.
rewrite paradoxical.
rewrite p2p.
exists Ω.
split.
 unfold Δ.
 rewrite p2p.
 trivial.
 
 trivial.
Qed.

Lemma lem5 : wf Ω -> ~ (b2p (predc (τ(σ Ω)) Ω)).
Proof.
intro.
cut (induct (fun e : U => p2b (~ b2p (predc (τ (σ e)) e)))).
 intro.
 unfold wf in H.
 intro.
 assert (b2p ((fun e : U => p2b (~ b2p (predc (τ (σ e)) e))) Ω)) as tmp.
  apply (H _ H0).
  
  simpl in tmp.
  rewrite p2p in tmp.
  apply tmp.
  assumption.
  
 unfold induct.
 intros.
 rewrite p2p.
 intro.
 assert (b2p (predc (τ (σ (τ (σ x)))) (τ (σ x)))) as tmp.
  apply (lem1 _ _ H1).
  
  assert (~ b2p (predc (τ (σ (τ (σ x)))) (τ (σ x)))) as not_tmp.
   cut (b2p (p2b (~ b2p (predc (τ (σ (τ (σ x)))) (τ (σ x)))))).
    intro.
    rewrite p2p in H2.
    apply False_ind.
    apply H2.
    trivial.
    
    apply (H0 _ H1).
    
   apply not_tmp.
   trivial.
Qed.

Lemma lem6 : ~ (wf Ω).
Proof.
intro.
apply lem5.
 assumption.
 
 apply lem4.
 assumption.
Qed.

Theorem inconsistency : False.
Proof.
apply lem6.
apply lem2.
Qed.

(* construction *)
Definition Univ : Set := forall (X : Set) , ((Pow X -> X) -> Pow X).
Definition tau : Pow Univ -> Univ := fun (X : Pow Univ) (A : Set) (c : Pow A -> A) (a : A) =>
  p2b (forall (P : Pow A) , (forall (x : Univ) , (b2p (X x) -> b2p (P (c ((x A) c))))) -> b2p (P a)).
Definition sig : Univ -> Pow Univ := fun (x : Univ) => x Univ tau.

Axiom ext_eq : forall A B (f g : A -> B),
  (forall x, f x = g x)
  -> f = g.

Definition prop_extensionality := forall A B:Prop, (A <-> B) -> A = B.
Axiom prop_ext_axiom: prop_extensionality.

Lemma prop : forall (X : Pow Univ) (y : Univ) ,
b2p (sig (tau X) y) = b2p (p2b (exists x : Univ , b2p (X x) /\ y = tau(sig x))).
Proof.
intros.
apply prop_ext_axiom.
split.
 intro.
 rewrite p2p.
 unfold sig in H.
 unfold tau in H at 1.
 rewrite p2p in H.
 assert
  ((forall x : Univ,
    b2p (X x) ->
    b2p
      ((fun y : Univ =>
        p2b (exists x0 : Univ, b2p (X x0) /\ y = tau (sig x0)))
         (tau (x Univ tau)))) ->
   b2p
     ((fun y : Univ => p2b (exists x : Univ, b2p (X x) /\ y = tau (sig x))) y))
  as tmp.
  apply
   (H (fun y : Univ => p2b (exists x : Univ, b2p (X x) /\ y = tau (sig x)))).
  
  simpl in tmp.
  rewrite p2p in tmp.
  apply tmp.
  intros.
  rewrite p2p.
  exists x.
  split.
   trivial.
   
   unfold sig.
   trivial.
   
 rewrite p2p.
 intros.
 destruct H.
 destruct H.
 rewrite H0.
 clear H0.
 unfold sig.
 simpl.
 unfold tau at 1.
 rewrite p2p.
 intros.
 apply H0.
 trivial.
Qed.

Lemma prop3 : forall (X : bool) (Y : Prop) , b2p X = b2p (p2b Y) -> X = p2b Y.
Proof.
intros.
rewrite p2p in H.
rewrite <- H.
apply eq_sym.
apply b2b.
Qed.

Lemma prop2 : forall (X : Pow Univ) (y : Univ) ,
(sig (tau X) y) = (p2b (exists x : Univ , b2p (X x) /\ y = tau(sig x))).
Proof.
intros.
apply prop3.
apply prop.
Qed.

Lemma property : forall (X : Pow Univ) , 
(sig (tau X)) = (fun (y:Univ) => p2b (exists x : Univ , b2p (X x) /\ y = tau(sig x))).
Proof.
intros.
apply ext_eq.
intros.
apply prop2.
Qed.