Mercurial > hg > Papers > 2013 > kono-prosym
changeset 9:e457d1179e2c
done!
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 06 Dec 2013 00:16:37 +0900 |
| parents | 4ba85665eda7 |
| children | 0ce710b64ed1 |
| files | agda-prog.ind prosym-kono-2014.pdf |
| diffstat | 2 files changed, 103 insertions(+), 62 deletions(-) [+] |
line wrap: on
line diff
--- a/agda-prog.ind Thu Dec 05 22:46:22 2013 +0900 +++ b/agda-prog.ind Fri Dec 06 00:16:37 2013 +0900 @@ -126,12 +126,15 @@ {\tiny Definition 1.1. A concrete category is a collection of two kind of entities called object and morphisms. The former are sets which are endowed with some kind of structure, and the latte are mappings, tha is functions from -one object to another, in some sencse preserving that structure. Among the morphisms, there is atteched to each +one object to another, in some sense preserving that structure. Among the morphisms, there is atteched to each object A the identity mapping $1_A$: A → A such aht $1_A$(a) = a for all a ∈ A. More over, morphims f : A → B -and g : b→ c may be compoosed to prodicue a morphism gf: a → c such hat (gf)a() = g(f(a) for all a ∈ A. +and g : b→ c may be compoosed to producue a morphism gf: a → c such hat (gf)a() = g(f(a) for all a ∈ A. } -関手の定義は、 +となっている。ここでは、この細かい定義が重要なのではなくて、自然言語による定義と、あとで示す Agda での定義を対照させる +ために示している。 圏は、 object (対象)と morphism (射)を持っている。 +ここで重要なのは、(gf)a() = g(f(a) という結合の定義である。ここでは、object や morphism が +何かははっきり書いてない。Agda では両方共、あるレベルの集合になる。 関手の定義は、 {\tiny Definition 1.3. A cuntor F: A→B is first of all a morphism of graph, that is, it sends objects of A to @@ -141,6 +144,8 @@ $ F(1_A) = 1_F(A), F(gf) = F(g)F(f) $ +であり、対象と射の二つの写像により関手が定義されることがわかる。 + 自然変換の定義は、 {\tiny @@ -149,9 +154,11 @@ square commutes for all arrows f: A → in A. that is to say, such that } - G(f)t(a) = t(B)F(f). + G(f)t(A) = t(B)F(f). -と書かれている。さらに、Monad は関手Tと二つの自然変換の組であり以下のように定義されている。 +と書かれている。これが何かを理解することは、この定義だけからでは難しい。 + +さらに、Monad は関手Tと二つの自然変換の組であり以下のように定義されている。 {tiny Definition 6.1 A triple(T,η,μ) on a category A consists of a functor T: A→A and natural transformation η: $1_A$ → T @@ -177,7 +184,8 @@ f * ( g * h ) = ( f * g ) * h -を示せば良い。 +を示せば良い。これで問題は十分に定義されたはずである。しかし、ここから、この式を証明するまでの道のりは +やさしくない。 本の証明は自然言語で書かれていて、簡潔な代わりに多くのものが省略されている。例えば、式\ref{comp-of-func-nat} に出てくるTと式\ref{comp-of-nat-func} に出てくるT は、前者は arrows からarrows の関数であり、後者は @@ -193,13 +201,22 @@ 満たす必要がある。 すると、自然変換はデータ型からデータ型への変換を表す。例えば、SJISのファイルからUTF8へのファイルに変換する -プログラム nkf は、自然変換だと考えられる。実際、 ファイルからファイルへの操作、例えば grep '単位' があった時に、SJIS で SJIS対応のgrepを使ってから、nkf で +プログラム nkf は、自然変換だと考えられる。実際、 ファイルからファイルへの操作、例えば grep があった時に、SJIS で SJIS対応のgrepを使ってから、nkf で UTF8の結果に変換するのと、先にnkfでUTF8に変換してからUTF8対応のgrepを使うのと結果は同じでなければならない。 -これが可換性であり、自然変換であるための条件になる。 +これが可換性であり、自然変換であるための条件になる。ここでは自然変換の引数はUTF8やSJISの型に相当する。 + + grep word | nkf -w + nkf -w | grep word + +ここで結果は同じであるべきだが、前者のgrepは SJIS に対して動き、後者はUTF8に対して動く。 + + G(f)t(A) = t(B)F(f). + +GとFがファイルの型を表していて、 このtが grep に相当する。引数A,BはSJISやUTF8になる。射 f は、この場合は nkf である。 このような特定の分野に向いた例示は定義からは出てこない。 -証明で重要なのは、関手の提供する関手の分配法則と、自然変換の提供する可観測であり、それ以外の余計な直観は必要ない。 +しかし、証明で重要なのは、関手の提供する関手の分配法則と、自然変換の提供する可観測であり、それ以外の余計な直観は必要ない。 ---Monadのjoinとは何か @@ -297,6 +314,7 @@ ここでは Agda をざっと概観する。例えば、\cite{Agda} の論文がわかりやすい。 Agda は Haskell と同じような構文を持つλ式の集合である。例えば、Agda の List は以下のようになる。 +ここでのAgdaの例題は\cite{kono-git-category}で見ることができる。 infixr 40 _::_ data List {a} (A : Set a) : Set a where @@ -457,7 +475,8 @@ f に λ x → ( a :: x ) を使うと eq-cons を証明できる。 - eq-cons : ∀{n} {A : Set n} {x y : List A} ( a : A ) → x == y → ( a :: x ) == ( a :: y ) + eq-cons : ∀{n} {A : Set n} {x y : List A} ( a : A ) + → x == y → ( a :: x ) == ( a :: y ) eq-cons a z = cong1 ( λ x → ( a :: x) ) z 最終的な証明は、 @@ -547,15 +566,16 @@ --record の使い方 -data は constructor を提供するが、record は数学的構造の存在を示す。以下は\cite{Lambek:1986:IHO:7517} による圏の定義である。 +data は constructor を提供するが、record は数学的構造の存在を示す。以下は\cite{category-conn} による圏の定義である。 record IsCategory {c₁ c₂ ℓ : Level} (Obj : Set c₁) - (Hom : Obj → Obj → Set c₂) - (_≈_ : {A B : Obj} → Rel (Hom A B) ℓ) - (_o_ : {A B C : Obj} → Hom B C → Hom A B → Hom A C) - (Id : {A : Obj} → Hom A A) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where + (Hom : Obj → Obj → Set c₂) + (_≈_ : {A B : Obj} → Rel (Hom A B) ℓ) + (_o_ : {A B C : Obj} → Hom B C → Hom A B → Hom A C) + (Id : {A : Obj} → Hom A A) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where field - isEquivalence : {A B : Obj} → IsEquivalence {c₂} {ℓ} {Hom A B} _≈_ + isEquivalence : {A B : Obj} → + IsEquivalence {c₂} {ℓ} {Hom A B} _≈_ identityL : {A B : Obj} → {f : Hom A B} → (Id o f) ≈ f identityR : {A B : Obj} → {f : Hom A B} → (f o Id) ≈ f o-resp-≈ : {A B C : Obj} {f g : Hom A B} {h i : Hom B C} @@ -565,7 +585,7 @@ → (f o (g o h)) ≈ ((f o g) o h) ここでは、圏の要素がコンストラクタ IsCategory に列挙されている。そして、圏が満たす性質(公理)が field に列挙 -されている。 +されている。IsEquivalence は、library で定義されているものを呼び出している。 field は data 型と異なり、要素へアクセスするアクセサを提供している。 なので、record field は、パターンには使えない。圏を作るときには、アクセサをすべて定義する必要がある。 @@ -573,11 +593,11 @@ isKleisliCategory : IsCategory ( Obj A ) KHom _⋍_ _*_ K-id isKleisliCategory = record { isEquivalence = isEquivalence - ; identityL = KidL - ; identityR = KidR - ; o-resp-≈ = Ko-resp - ; associative = Kassoc - } + ; identityL = KidL + ; identityR = KidR + ; o-resp-≈ = Ko-resp + ; associative = Kassoc + } のように record の中で filed を全部定義する。(KidL などは、別に定義されているとする) @@ -638,17 +658,21 @@ 入力となるrecord の field に記述すると、 「record は、その型の値を生成する」になる。なので、どちらに記述するかの 差は大きい。 - record IsFunctor {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (C : Category c₁ c₂ ℓ) (D : Category c₁′ c₂′ ℓ′) - (FObj : Obj C → Obj D) - (FMap : {A B : Obj C} → Hom C A B → Hom D (FObj A) (FObj B)) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where + record IsFunctor {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} + (C : Category c₁ c₂ ℓ) (D : Category c₁′ c₂′ ℓ′) + (FObj : Obj C → Obj D) + (FMap : {A B : Obj C} → Hom C A B → Hom D (FObj A) (FObj B)) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where field - ≈-cong : {A B : Obj C} {f g : Hom C A B} → C [ f ≈ g ] → D [ FMap f ≈ FMap g ] - identity : {A : Obj C} → D [ (FMap {A} {A} (Id {_} {_} {_} {C} A)) ≈ (Id {_} {_} {_} {D} (FObj A)) ] + ≈-cong : {A B : Obj C} {f g : Hom C A B} → + C [ f ≈ g ] → D [ FMap f ≈ FMap g ] + identity : {A : Obj C} → D [ + (FMap {A} {A} (Id {_} {_} {_} {C} A)) ≈ (Id {_} {_} {_} {D} (FObj A)) ] distr : {a b c : Obj C} {f : Hom C a b} {g : Hom C b c} → D [ FMap (C [ g o f ]) ≈ (D [ FMap g o FMap f ] )] - record Functor {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) + record Functor {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} + (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where field FObj : Obj domain → Obj codomain @@ -680,7 +704,8 @@ 射の等式は \_≡\_ で定義されるべきなので、以下を仮定しても良い、あるいはする必要がある。 postulate ≈-≡ : { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } - {a b : Obj A } { x y : Hom A a b } → (x≈y : A [ x ≈ y ]) → x ≡ y + {a b : Obj A } { x y : Hom A a b } → + (x≈y : A [ x ≈ y ]) → x ≡ y 米田レンマは射が集合であることを要求するので、明示的に集合全体の圏に対して証明するか、 任意の圏に対して、これと関数外延性を仮定して証明する必要がある。 @@ -688,7 +713,8 @@ また、集合以外の関係に対する合同性も単独では証明できない。例えば、関手の合同性は、自明には成り立たない ので、以下のように IsFunctor の公理とする必要がある。 - ≈-cong : {A B : Obj C} {f g : Hom C A B} → C [ f ≈ g ] → D [ FMap f ≈ FMap g ] + ≈-cong : {A B : Obj C} {f g : Hom C A B} + → C [ f ≈ g ] → D [ FMap f ≈ FMap g ] また、 a b : Set @@ -736,15 +762,17 @@ ここまでで、 圏の定義と 関手の定義を使ってきた。 自然変換の定義は、以下のようになる。 - record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′) - ( F G : Functor D C ) - (TMap : (A : Obj D) → Hom C (FObj F A) (FObj G A)) + record IsNTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} + (D : Category c₁ c₂ ℓ) (C : Category c₁′ c₂′ ℓ′) + ( F G : Functor D C ) + (TMap : (A : Obj D) → Hom C (FObj F A) (FObj G A)) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where field commute : {a b : Obj D} {f : Hom D a b} → C [ C [ ( FMap G f ) o ( TMap a ) ] ≈ C [ (TMap b ) o (FMap F f) ] ] - record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) + record NTrans {c₁ c₂ ℓ c₁′ c₂′ ℓ′ : Level} + (domain : Category c₁ c₂ ℓ) (codomain : Category c₁′ c₂′ ℓ′) (F G : Functor domain codomain ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ ⊔ c₁′ ⊔ c₂′ ⊔ ℓ′)) where field @@ -763,26 +791,31 @@ これを使って、 Monad の結合性の証明を以下のように行うことができる。まず Monad を定義する。 - record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) - ( T : Functor A A ) - ( η : NTrans A A identityFunctor T ) - ( μ : NTrans A A (T ○ T) T) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where - field - assoc : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] - unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] ≈ Id {_} {_} {_} {A} (FObj T a) ] - unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] ≈ Id {_} {_} {_} {A} (FObj T a) ] + record IsMonad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) + ( T : Functor A A ) + ( η : NTrans A A identityFunctor T ) + ( μ : NTrans A A (T ○ T) T) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where + field + assoc : {a : Obj A} → A [ A [ TMap μ a o TMap μ ( FObj T a ) ] + ≈ A [ TMap μ a o FMap T (TMap μ a) ] ] + unity1 : {a : Obj A} → A [ A [ TMap μ a o TMap η ( FObj T a ) ] + ≈ Id {_} {_} {_} {A} (FObj T a) ] + unity2 : {a : Obj A} → A [ A [ TMap μ a o (FMap T (TMap η a ))] + ≈ Id {_} {_} {_} {A} (FObj T a) ] - record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (T : Functor A A) (η : NTrans A A identityFunctor T) (μ : NTrans A A (T ○ T) T) - : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where - field - isMonad : IsMonad A T η μ - -- g ○ f = μ(c) T(g) f - join : { a b : Obj A } → { c : Obj A } → - ( Hom A b ( FObj T c )) → ( Hom A a ( FObj T b)) → Hom A a ( FObj T c ) - join {_} {_} {c} g f = A [ TMap μ c o A [ FMap T g o f ] ] + record Monad {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) + (T : Functor A A) (η : NTrans A A identityFunctor T) + (μ : NTrans A A (T ○ T) T) + : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where + field + isMonad : IsMonad A T η μ + -- g ○ f = μ(c) T(g) f + join : { a b : Obj A } → { c : Obj A } → + ( Hom A b ( FObj T c )) → ( Hom A a ( FObj T b)) → Hom A a ( FObj T c ) + join {_} {_} {c} g f = A [ TMap μ c o A [ FMap T g o f ] ] -証明するべき式は、 +Id の暗黙の引数は、すべて指定する必要がある。証明するべき式は、 join M h (join M g f) ≈ join M ( join M h g) f @@ -867,27 +900,33 @@ infix 4 _≈_ refl-hom : {a b : Obj A } { x : Hom A a b } → x ≈ x - refl-hom = IsEquivalence.refl (IsCategory.isEquivalence ( Category.isCategory A )) + refl-hom = IsEquivalence.refl + (IsCategory.isEquivalence ( Category.isCategory A )) car : {a b c : Obj A } {x y : Hom A a b } { f : Hom A c a } → x ≈ y → ( x o f ) ≈ ( y o f ) - car {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) ( refl-hom ) eq + car {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) + ( refl-hom ) eq cdr : {a b c : Obj A } {x y : Hom A a b } { f : Hom A b c } → x ≈ y → f o x ≈ f o y - cdr {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) eq (refl-hom ) + cdr {f} eq = ( IsCategory.o-resp-≈ ( Category.isCategory A )) + eq (refl-hom ) - assoc : {a b c d : Obj A } {f : Hom A c d} {g : Hom A b c} {h : Hom A a b} + assoc : {a b c d : Obj A } + {f : Hom A c d} {g : Hom A b c} {h : Hom A a b} → f o ( g o h ) ≈ ( f o g ) o h assoc = IsCategory.associative (Category.isCategory A) distr : { c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} - { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} (T : Functor D A) → {a b c : Obj D} {g : Hom D b c} { f : Hom D a b } + { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} + (T : Functor D A) → {a b c : Obj D} {g : Hom D b c} { f : Hom D a b } → A [ FMap T ( D [ g o f ] ) ≈ A [ FMap T g o FMap T f ] ] distr T = IsFunctor.distr ( isFunctor T ) open NTrans - nat : { c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} + nat : { c₁ c₂ ℓ : Level} {A : Category c₁ c₂ ℓ} + { c₁′ c₂′ ℓ′ : Level} {D : Category c₁′ c₂′ ℓ′} {a b : Obj D} {f : Hom D a b} {F G : Functor D A } → (η : NTrans D A F G ) → A [ A [ FMap G f o TMap η a ] ≈ A [ TMap η b o FMap F f ] ] @@ -941,9 +980,11 @@ Monad を理解するのに、join の結合性を理解することが必須かというと、そのようなことはない。むしろ、それが 重要であることを主張している解説は少ない。しかし、 - T が関手(データ構造) - return が自然変換η (プログラム) - join が自然変換μ (プログラム) +\begin{itemize} +\item T が関手(データ構造) +\item return が自然変換η (プログラム) +\item join が自然変換μ (プログラム) +\end{itemize} という対応を理解しなければ、Monad を使う理由を理解できない。実際、Monad は対象レベルとメタレベルの 双対性(随伴関手)が反映されたものになっている。