data と Sum type

Menu


data または 排他的論理和(Sum)

ここで扱っている論理(直観主義論理)では∧に対称的な形で∨を定義することはしない。導入は対称的になるが除去はおかしくなってしまう。

     除去                           導入
      A ∨ B                   A                  B
   -------------         ----------- case1   ---------- case2
     A    B                 A ∨ B               A ∨ B

除去の値が二つあるので、証明の仕組みにあってない。推論に相当する関数の返し値が二つになってしまう。

そこで次のように定義することになっている。

  除去                           導入
               A      B
               :      :
    A ∨ B      C      C            A               B
   ------------------------  ----------- case1 ---------- case2
           C                     A ∨ B           A ∨ B 

Agda では以下のデータ定義を用いる。

    data _∨_ (A B : Set) : Set where
      case1 : A → A ∨ B
      case2 : B → A ∨ B

dataはCで言えばcase文とunion に相当する。Scala のCase Classもこれである。Cと違いunionにはどの型が入っているかを区別するtagが付いている。

    ex3' : {A B C : Set} → ( A ∨ B ) → C 
    ex3' (case1 a) = ?         ---    A → C
    ex3' (case2 b) = ?         ---    B → C

case1 と case2 は A ∨ B を構成する constructor (推論ではintroduction)であり、case 文が eliminator に相当する。

Haskellと同様にp1/p2はパターンマッチで場合分けする。

    ex3 : {A : Set} → ( A ∨ A ) → A 
    ex3 = ?

場合分けには、? の部分にcursolを合わせて C-C C-C すると場合分けを生成してくれる。

    ex3 : {A : Set} → ( A ∨ A ) → A 
    ex3 (case1 x) = ?
    ex3 (case2 x) = ?

data の使い道はいろいろあって、List や Nat そして、否定を作れる。


場合分けのやり方

    ex3 : {A B : Set} → ( A ∨ A ) → A
    ex3 = ?

これを証明したい。∨ なので入力があって、二つの場合がある。

    ex3 : {A B : Set} → ( A ∨ A ) → A
    ex3 x = ?

ここで、? に cursol を合わせて、C-c C-e (control と c)を押す。

    A : Set   (not in scope)
    B : Set   (not in scope)
    x : A ∨ A

としたに表示される。つまり、x は A ∨ A である。そういう data / sum-type。

ここで、? に cursol をあわせる(正確には色の変わった所)C-c C-c とする。

    pattern variables to case (empty for split on result): 

とか言われるので、そのまま enter する。

    ex3 : {A B : Set} → ( A ∨ A ) → A
    ex3 {A} {B} (case1 x) = ?
    ex3 {A} {B} (case2 x) = ?

となる。つまり、A ∨ A は二つの場合がある。


問題2.3 Agdaのdata

data1.agda

黄色の問題

    ex2 : {A B : Set} → B → ( A ∨ B ) 
    ex2 = λ b → case2 b

ここで、case2 b を case2 _ と書くと、_ は新しい変数になる。これを型チェックすると黄色くなる。

つまり、兎または馬をもらったはずだが、存在しない馬をもらった場合みたいになる。

これでは証明にならない。data / record を構成する型に対応する値は、具体的に存在する必要がある。もらってきた入力でも良い。


矛盾 ⊥

        除去                  導入
           ⊥               
   ------------------------   (ない)
           C                
    data ⊥ : Set where

矛盾からは何でもでる。

    ⊥-elim : {A : Set } -> ⊥ -> A
    ⊥-elim x = ?

実際、x は ⊥ という型を持つことを C-c C-e で確認できる。

これを C-c C-c で場合分けする。

    ⊥-elim :  {A : Set } → ⊥ → A
    ⊥-elim ()

() が、当てはまる場合がないことに相当する。

これで証明終わり。

    ⊥-elim : {A : Set } -> ⊥ -> A
    ⊥-elim = λ ()

こう書いても良い。入力がありえないλ項。

否定は以下のように定義する。

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


パズルと排中律

    猫か犬を飼っている人は山羊を飼ってない
    猫を飼ってない人は、犬かウサギを飼っている
    猫も山羊も飼っていない人は、ウサギを飼っている

を仮定して以下を示す。

    山羊を飼っている人は、犬を飼っていない
    山羊を飼っている人は、ウサギを飼っている
    ウサギを飼っていない人は、猫を飼っている

仮定を record でかく。

  record PetResearch ( Cat Dog Goat Rabbit : Set ) : Set where
     field
        fact1 : ( Cat ∨ Dog ) → ¬ Goat
        fact2 : ¬ Cat →  ( Dog ∨ Rabbit )
        fact3 : ¬ ( Cat ∨ Goat ) →  Rabbit

これは排中律が必要

  postulate 
     lem : (a : Set) → a ∨ ( ¬ a )

これは Agda / 直観主義論理では証明できない。構成的には証明できないという反例がある。

非構成的な存在物を認めれば問題ない。つまり、これを仮定しても矛盾はでない。(証明がある)

これに反例がある、つまり、これが証明できないとしても矛盾はでない。

moudule の入力で仮定して証明する。

  module tmp ( Cat Dog Goat Rabbit : Set ) (p :  PetResearch  Cat Dog Goat Rabbit ) where
    open PetResearch
    problem0 : Cat ∨ Dog ∨ Goat ∨ Rabbit
    problem0 = ?
    problem1 : Goat → ¬ Dog
    problem1 = ?
  
    problem2 : Goat → Rabbit
    problem2 = ?


with statemnt

場合分けを排中律(あるいは、dataを返す関数)を使っておこなう。

    problem0 : Cat ∨ Dog ∨ Goat ∨ Rabbit
    problem0 with lem Cat
    ... | case1 cat = ?
    ... | case2 ¬cat = ?

with と書いて、後ろに場合分けする関数をかく。| を使って場合分けを増やせる。

    problem0 : Cat ∨ Dog ∨ Goat ∨ Rabbit
    problem0 with lem Cat  | lem Goat
    ... | case1 cat | x = ?
    ... | case2 ¬cat | x = ?

caseの作り方は、? に case1 ? とか書いていく。? の型がしたに表示される。

    ... | case2 ¬cat | case2 ¬goat = case2 { }6 where   
    ============
    ?6 : Rabbit

ここに Rabbit を入れてやれば良い。複雑な式が表示された場合は、それを lemma1 とかにする。

    ... | case2 ¬cat | case2 ¬goat = case2 (fact3 p { }6) where
    ?6 : ¬ (Cat ∨ Goat)

だったら、

    ... | case2 ¬cat | case2 ¬goat = case2 (fact3 p lemm1 ) where
       lemma1 : ¬ (Cat ∨ Goat)
       lemma1 = { }5

などとする。5 は入力から作れる。


否定をつかった証明の一つの方法

       lemma1 : ¬ (Cat ∨ Goat)
       lemma1 (case1 cat) = ?
       lemma1 (case2 goat) = ?

で、⊥ を作れれば良い。

    ¬cat   : Cat → ⊥
    cat    : Cat

なので、

       lemma1 (case1 cat) = ¬cat cat

とできる。


有限な集合と Nat

data は有限な要素を持つ集合を構成できる。

    data Three : Set where
      t1 : Three
      t2 : Three
      t3 : Three
    open Three
    data 3Ring : (dom cod : Three) → Set where
       r1 : 3Ring t1 t2
       r2 : 3Ring t2 t3
       r3 : 3Ring t3 t1

これは、三つのVertexとEdgeを持つグラフをdataで表してみたものである。

任意の個数を表すためには自然数(Natural Number)を作る必要がある。ペアノの公理が有名だが、dataを使って以下のように構成する。

    data Nat : Set where
      zero : Nat
      suc  : Nat →  Nat
    add : ( a b : Nat ) → Nat
    add zero x = x
    add (suc x) y = suc ( add x y )
    mul : ( a b : Nat ) → Nat
    mul zero x = ?
    mul (suc x) y = ?


問題2.4 Nat

? を埋めて掛け算を完成させよう。

data


Equality

自然数を導入したので方程式を記述したい。そのためには等式を導入する必要がある。導入は

   ---------------
      x == x

だが、ここには隠れた仮定がある。x は何かの集合の要素なはず。

     { x : A }
   ---------------
      x == x

さらに左辺と右辺は等しいが、

     add zero zero == zero

では左辺と右辺は項として同じではない。計算して同じということにして欲しい。つまり、

  Agdaの項には計算していくと決まった形に落ちる

という性質があって欲しい。この計算はλ項に対して定義する必要がある。この計算をreduction(縮約)、決まった形をnormal form(正規形)と言う。

Reduction Agda での定義は以下のようになる。

    data _==_ {A : Set } : A → A → Set where
       refl :  {x : A} → x == x

refl は reflection (反映) の略である。refl は 等式のconstructorになる。

Elmination は変数の置き換えになる。

      x == y    f x y
   ------------------------
          f x x

x == y は入力の型であり、refl とうパターンでしか受けられない。この時に、x と y が等しい必要がある。

しかし、x と y は項なので変数を含むことがある。Agda に等しいことを確信させる必要がある。この問題はパターンマッチの時にもすででていた。これは項(正規化された)を再帰的に比較していく手順が必要になる。これは単一化(Unification)と呼ばれる。

Unification

    ex1 : {A : Set} {x : A } → x == x
    ex1  = ?
    ex2 : {A : Set} {x y : A } → x == y → y == x
    ex2 = ?
    ex3 : {A : Set} {x y z : A } → x == y → y == z → x == z
    ex3 = ?
    ex4 : {A B : Set} {x y : A } { f : A → B } →   x == y → f x == f y
    ex4 = ?


問題 2.5

以上の証明を refl を使って完成させてみよう。

equality


induction

induction は以下のように書ける

    P : (x : Nat) → Set    ---  ある自然数  x に対する命題 P x
    initial : P zero       ---   P zero が成立
    induction-setp : (x : Nat) → P x → P (suc x)  -- P x が成立すれば P (suc x)が成立
    (x : Nat) → P x  --     ∀ x について P x が成立

なので、

    induction : (P : (x : Nat) → Set) 
        → (initial : P zero ) 
        → (induction-setp : ((x : Nat) → P x → P (suc x))) 
        → (x : Nat) → P x
    induction P initial induction-setp x = ?

証明を完成さてみよう。


問題 2.6

nat の例題

集合のLevel

論理式は型であり、それは基本的はSetになっている。例えば、A → B は Set である。

    ex1 : { A B : Set} → Set
    ex1 {A} {B} =  A → B

Agda は高階論理なので、論理式自体を返す論理式も作ることができる。

    ex2 : { A B : Set} →  ( A → B ) → Set
    ex2 {A} {B}  A→B  =  ex1 {A} {B}

では、これを論理式を要素として持つ直積を作ってみよう。

    record FuncBad (A B : Set) : Set where
      field
         func : A → B → Set

Agda は以下のように文句をいう。

    The type of the constructor does not fit in the sort of the
    datatype, since Set₁ is not less or equal than Set
    when checking the definition of FuncBad

自己参照的な集合の定義を避けるために集合には階(level)という概念が導入されている。

    open import Level
    record Func {n : Level} (A B : Set n ) : Set (suc n) where
      field
        func : A → B → Set n

のように集合の階(Level)を明示する必要がある。


問題2.7 集合のLevel

level が合うように ? を埋めよ。

level


List

List は cons か nil かどちらかの構造で、cons は List を再帰的に含んでいる。

    postulate A : Set
    postulate a : A
    postulate b : A
    postulate c : A
    infixr 40 _::_
    data  List  (A : Set ) : Set  where
       [] : List A
       _::_ : A → List A → List A
    infixl 30 _++_
    _++_ :   {A : Set } → List A → List A → List A
    []        ++ ys = ys
    (x :: xs) ++ ys = x :: (xs ++ ys)
    l1 = a :: []
    l2 = a :: b :: a :: c ::  []
    l3 = l1 ++ l2

等式の変形を利用して、List の結合法則を証明してみよう。

    open  import  Relation.Binary.PropositionalEquality
    ++-assoc :  (L : Set ) ( xs ys zs : List L ) → (xs ++ ys) ++ zs  ≡ xs ++ (ys ++ zs)
    ++-assoc A [] ys zs = let open ≡-Reasoning in
      begin -- to prove ([] ++ ys) ++ zs  ≡ [] ++ (ys ++ zs)
       ( [] ++ ys ) ++ zs
      ≡⟨ refl ⟩
        ys ++ zs
      ≡⟨⟩
        [] ++ ( ys ++ zs )
      ∎
    ++-assoc A (x :: xs) ys zs = let open  ≡-Reasoning in ?

≡⟨⟩ などの定義はどこにあるのか?


問題2.8 List

lemma を等式の変形を利用して証明してみよ。

List


DAGと否定

グラフには接続されてない二点が存在する。それを表現するために否定¬と矛盾⊥を導入する。

       ⊥
    ------------- ⊥-elim
       A

矛盾からは何でも導くことができる。この場合、A はSetである。⊥ を導入する推論規則はない。

これは、contructor のない data で表すことができる。

    data ⊥ : Set where

⊥-elim は以下のように証明できる。

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

() は「何にもmatchしないパターン」である。これは型を指定した時に「可能な入力がない」必要がある。つまり、このケースは起こり得ないことを Agda が納得する必要がある。納得できないと error message がでる。

    λ ()

という構文も存在する。

⊥ を使って否定は以下のように定義される。

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

否定には入力があることを意識しておこう。

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

というグラフは以下のように記述する。

    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

矢印をたどって繋がっている点は接続(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

直接繋がっているか、間接的に繋がっているかどちからになる。この構造は自然数に似ている。

t0 と t1 が TwoArrow の場合に繋がっていることを証明してみる。

    lemma1 : connected TwoArrow t0 t1
    lemma1 =  ?

t1 から t0 にはいけない。

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

dag (Directed Acyclic Graph) は、すべての点(Vertex)で自分自身につながる経路(Edge)がないグラフ

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


問題2.9 DAGと否定

TwoArrow が dag で、Circle が dag ではないことを証明してみよう。

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

DAG


教科書の第一章

chapter 0

Shinji KONO / Wed Oct 19 16:15:36 2022