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 ∨ BAgda では以下のデータ定義を用いる。
data _∨_ (A B : Set) : Set where case1 : A → A ∨ B case2 : B → A ∨ Bdataは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 → Ccase1 と 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 == xrefl は reflection (反映) の略である。refl は 等式のconstructorになる。
Elmination は変数の置き換えになる。
x == y f x y ------------------------ f x xx == 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 → BAgda は高階論理なので、論理式自体を返す論理式も作ることができる。
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 → SetAgda は以下のように文句をいう。
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