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
? を埋めて掛け算を完成させよう。
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)と呼ばれる。
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 を使って完成させてみよう。
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 が合うように ? を埋めよ。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 を等式の変形を利用して証明してみよ。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