Agda での否定と有向グラフ

a -> b は、型aから型bへの関数だが、これは、点aから点bへの矢印に過ぎない。

有限な点(vertex)の集合(vertices)と、その間の矢印(edge)の集合(edges)は、有向グラフと呼ばれる。

Agda での有向グラフ

例えば、二つの点と二つの矢印だけを持つグラフを考えよう。

         f0
       -----→
    t0         t1
       -----→
         f1

これらの f とか t0 とかを Agda の data を使って表すことができる。

    data  TwoObject   : Set  where
       t0 : TwoObject
       t1 : TwoObject
    data TwoArrow  : TwoObject → TwoObject → Set  where
       f0 :  TwoArrow t0 t1
       f1 :  TwoArrow t0 t1

別な有向グラフ

         r0
       -----→
    t0         t1
       ←-----
         r1
    data Circle  : TwoObject → TwoObject → Set  where
       r0 :  Circle t0 t1
       r1 :  Circle t1 t0

にはループがある。TwoArrow にはループがない。

ループがない有向グラフをDAG(Directed Acyclic Graph)という。

dag をAgdaで表すには?

ループがないというのをAgdaで表すには否定を定義する必要がある。

新しい論理記号 ⊥ (矛盾)を導入するが、elimination はあるが、introduction はない。矛盾が導入されてしまったら困るので。

　　　　⊥　　----------- ⊥-elim

矛盾からはなんでも出てくる。

これは、constructor のない data として定義される

    data ⊥ : Set where
    ⊥-elim : {A : Set } -> ⊥ -> A
    ⊥-elim ()

この()は「起きない場合分け」を表す。

これを使って、否定を以下のように定義する

     ¬_ : Set → Set
     ¬ A = A → ⊥

ここで、

    ¬ A : A ->  ⊥

ではないことに注意しよう。

connected

有向グラフのedgeをたどって、到達できるvertexを到達可能(connected)という。直接つながっている場合と、間接的につながっている場合がある。それを場合分けしよう。

    data connected { V : Set } ( E : V -> V -> Set ) ( x y : V ) : Set  where
        direct :   E x y -> connected E x y 
        indirect :  { z : V  } -> E x z  ->  connected {V} E z y -> connected E x y

このEにはTwoObjectが入り、VにはTwoArrowかCircleが入る。つまり、data というのはSetとして扱われる。実際、

    data TwoArrow  : TwoObject → TwoObject → Set

とSetと明示されている。 TwoArrow のt0とt1がconnectedなのは、以下のように証明される。

    lemma1 : connected TwoArrow t0 t1
    lemma1 = direct f0

ここで、connected でないことを証明したい。

    lemma2 : ¬ ( connected TwoArrow t1 t0 )
    lemma2 = ?

¬ ( connected TwoArrow t1 t0 ) は、 ( connected TwoArrow t1 t0 ) -> ⊥ なので、入力(connected TwoArrow t1 t0 )を持つ。これは場合分けなので、direct か indirect になる。

しかし、これらに相当する場合があるのはまずい。ないはずである。当てはまる引数がない時には()を使う。

    lemma2 (direct ())
    lemma2 (indirect () (direct _))
    lemma2 (indirect () (indirect _ _ ))

が証明となる。

DAG

DAG はすべての点(Vertices)で、自分自身に戻ってくるパスがない。つまり、以下のように定義できる。

    dag :  { V : Set } ( E : V -> V -> Set ) ->  Set
    dag {V} E =  ∀ (n : V)  →  ¬ ( connected E n n )

TwoArrow はDAG であり、Circle はDAGではない。

    lemma4 : dag TwoArrow
    lemma4 = ?
    lemma5 :  ¬ ( dag Circle )
    lemma5 = ?

lemma4を証明するには、実際に場合分けを尽くして、可能な場合がないことを示す必要がある。

    lemma4 t0 (direct ()) 
    lemma4 t0 (indirect _ (direct ()  ) ) 
    lemma4 t0 (indirect f0 (indirect () _ ) ) 
    lemma4 t0 (indirect f1 (indirect () _ ) ) 
    lemma4 t1 (direct ()) 
    lemma4 t1 (indirect () (direct _) )  
    lemma4 t1 (indirect () (indirect _ _ ) )

lemma5 を証明するには、 ¬ を→で書き直す。

    lemma5 :   dag Circle  → ⊥
    lemma5 :  ( ∀ (n : V)  →  ( connected E n n ) → ⊥ ) → ⊥

つまり、引数がある。

    lemma5 x :  ⊥

ここで、x の型は、

    x : ∀ (n : V)  →  connected E n n  → ⊥

である。欲しいのは、 ⊥ だが、これは、 ⊥-elim を使う。これに、 ⊥ を引数として与えるとなんでも出てくる。

x の引数は、∀ (n : V) → connected E n n だが、

    lemma3 : connected Circle t0 t0
    lemma3 = indirect r0 ( direct r1 )

これで反例を作るこことができる。

    lemma5 :  ¬ ( dag Circle )
    lemma5 x = ⊥-elim ( x t0 lemma3 )

これで証明できた。