--- a/agda-prog.ind	Tue Dec 03 17:17:57 2013 +0900
+++ b/agda-prog.ind	Thu Dec 05 18:40:21 2013 +0900
@@ -1,8 +1,13 @@
 -title: Agda での Programming 技術
 
+--author: Shinji KONO <kono@ie.u-ryukyu.ac.jp>
+
+\usepackage{tikz}
+\usepackage{tikz-cd}
+
 --abstract:
 
-Agda は、Haskell 上の Dependent type に基づく証明支援系である。
+Agda\cite{aga} は、Haskell \cite{haskell}上の Dependent type に基づく証明支援系である。
 Agda での証明は型付きλ式であり、証明するべき式も型付きλ式になっている。
 したがって、Agda での証明は、本質的にはλ式を構築していく作業になる。
 
@@ -15,7 +20,7 @@
 行い、その型に沿ったλ式を書いていくという点ではプログラミングそのもの
 である。
 
-Agdaの証明は、Curry Howard対応に基づいており、
+Agdaの証明は、Curry Howard対応\cite{}に基づいており、
 すべては、型を表す式と、その型を持つλ式の組で表される。
 Dependent type の特徴は省略可能な引数(暗黙の引数)にあり、
 これは、通常のプログラミング言語にはない概念である。
@@ -46,7 +51,7 @@
 % 
 % Coq
 
-例題としての圏論
+% 例題としての圏論
 
 証明支援系の歴史は古く、80年代にはMLで記述されたHOL\cite{}が既に使われるようになってきた。
 ここで使う Agda\cite{} は、証明とλ式が対応するという Curry Howard 対応に基づく証明支援系であり、
@@ -58,8 +63,8 @@
 なってきてる。しかし、ここでは、実際のプログラムの性質の証明とは違った視点から
 証明支援系の必要性を調べてみたい。
 
-Haskell などの関数型言語では、I/Oや継続、計算量、並列計算などの計算の様々な様相を Monad の仕組みを用いて
-実現している。Monad は圏論(Category theory)の概念であり、その性質の証明は若干煩雑である。
+Haskell などの関数型言語では、I/Oや継続、計算量、並列計算などの計算の様々な様相を Monad の仕組み\cite{}を用いて
+実現している。Monad は圏論(Category theory)\cite{}の概念であり、その性質の証明は若干煩雑である。
 Monad は随伴関手(Adjoint pair)や、Kleisli 圏と対応しているが、それを理解するには一連の証明を
 理解する必要がある。
 
@@ -68,7 +73,7 @@
 理解できれば、関数型プログラミングを学ぶものにとって都合が良いと思われる。特に、
 Haskell で記述された Agda は構文的に Haskell と似ていて、理解しやすい。
 
-プログラムのバグを見つけるにはモデル検証が使われるようになってきているが、モデル検証は
+プログラムのバグを見つけるにはモデル検証\cite{}が使われるようになってきているが、モデル検証は
 式と値の対応に着目して、その可能な対応をすべて列挙することにより反例を見つける。これは、
 命題式に真偽を割り当てていく方法になっている。
 
@@ -153,7 +158,9 @@
      (Tη)(A) = T(η(A))     \label{comp-of-func-nat}
      (ηT)(A) = η(T(A))     \label{comp-of-nat-func}
 
-である。
+である。これらの英語は、大学初年度の数学の知識があれば読んで理解することが期待されている。この本の記述は、
+既に圏論を知っている人向けに書かれており、特に簡潔に書かれている。以下に示す Agda の定義は、これらの
+10倍程度の量になる。
 
 これらの定義から証明するべきなのは、join の結合性であり、join は以下のように記述される。
 
@@ -212,6 +219,34 @@
 手書きの証明が終わると、これを例えば LaTeX などで清書する。清書には一部可換図も含まれる。ここでは以下のような式の変形と可換図が
 得られる。
 
+まず、左辺と右辺を定義に沿って展開する。
+
+\begin{eqnarray*}
+g * (f * h)  & = & g * (μ(c)T(f)h) \\
+\mbox{}              & = & μ(d)(T(g))(μ(c)T(f)h) \\
+\mbox{}              & = & μ(d)  T(g)μ(c)  T(f)h \\
+\\
+(g * f) * h  & = & (μ(d)T(g)f) * h \\
+\mbox{}              & = & μ(d)T(μ(d)T(g)f)h \\
+\mbox{}              & = & μ(d)  T(μ(d))T^2(g)  T(f)h \\
+\end{eqnarray*}
+
+これが等しいことは、μの可換性からわかる。
+
+$ μ(d)μ(d)T = μ(d)Tμ(d) $
+
+$ μ(T(d))T^2(g) = T(g)μ(c) $ naturality of $μ$.
+
+$ μ(d)Tμ(d)T^2(g) = μ(d)μ(T(d))T^2(g) = μ(d)T(g)μ(c) $
+
+可換図は以下のようになる。
+
+\begin{tikzcd}
+\mbox{} &  T^2(d) \arrow[leftarrow]{r}{Tμ(d)} \arrow{d}[swap]{μ(d)} & T^2(T(d)) \arrow[leftarrow]{r}{T^2(g)} \arrow{d}{μ(T(d))} & T^2(c) \arrow{d}{μ(c)}& \mbox{} \\
+\mbox{} & T(d) \arrow[leftarrow]{r}{μ(d)} & T(T(d)) \arrow[leftarrow]{r}{T(g)} & T(c)  & \mbox{} \\
+\end{tikzcd}
+
+
 --証明を理解するということ
 
 ここでは証明は式の一連の変形であり操作に過ぎない。この操作を理解することと、関手や自然変換が何かを理解することは別物である。
@@ -254,13 +289,14 @@
 % emacs との連携
 
 ここでは Agda をざっと概観する。例えば、\cite{} の論文がわかりやすい。
-Agda は Haskell と同じような構文を持つλ式の集合である。例えば、Agda の append は以下のようになる。
+Agda は Haskell と同じような構文を持つλ式の集合である。例えば、Agda の List は以下のようになる。
 
     infixr 40 _::_
     data  List {a} (A : Set a) : Set a where
        [] : List A
        _::_ : A → List A → List A
 
+これに対して append のプログラムは以下のようになる。
 
     infixl 30 _++_
     _++_ : ∀ {a} {A : Set a} → List A → List A → List A
@@ -273,7 +309,10 @@
 つまり、Agda では、一つの関数を定義するのに、型と関数の両方を定義する必要がある。Agda の型は、また、Agda の式であり、それ自体の
 型の整合性が要求される。 一つの名前を定義するのに、: で型を定義して、= で、その値を定義する。 
 
-data 型の要素の数だけパータンを作ることができ、この場合は、[] と _::_ の二つの場合分けになっている。:: は中置き演算子であり、
+Haskell の型と異なり、Agda では、型と式に同じものを書ける。それだけ強力な型システムjを持っている。型の記述にも型の整合があり、
+値は、その記述された型に整合する必要がある。つまり、Agda での型の整合は一つの式の定義に対して二度行われることになる。
+
+data 型のfiledの数だけパータンマッチングを作ることができ、この場合は、[] と _::_ の二つの場合分けになっている。:: は中置き演算子であり、
 
     _::_(a,b) 
 
@@ -341,7 +380,7 @@
     ?0 : {A₁ : Set} (xs ys zs : List A₁) →
         xs ++ ys ++ zs == xs ++ (ys ++ zs)
 
-だと Agda が教えてくれるが、これは、証明すべき型を返しているだけで証明のヒントにはならない。
+という型だと Agda が教えてくれるが、これは、証明すべき型を返しているだけで証明のヒントにはならない。
 
 List は、二つのfieldを持つデータ構造なので、それを場合分けすることができる。
 
@@ -545,6 +584,30 @@
 合同性 ( 同じものに同じ関数を作用させても同じ ) は、 _≡_  を仮定しているので、この圏の定義では、合同性を
 自由に使うことはできない。もし、arrow が Set であれば、あるいは、_≈_  → _≡_   を仮定すれば、 _≡_  を使うことができる。
 
+--infix operator
+
+infix operator には任意の Unicode を使うことができ、数学らしい記号を使うことが可能になっている。これは、Agda が
+monomorphism な言語であるために、型の組み合わせ毎に別な名前を用意する必要がある状況で特に便利になっている。
+
+        associative : {A B C D : Obj} {f : Hom C D}  {g : Hom B C} {h : Hom A B}
+                                      → (f o (g o h)) ≈ ((f o g) o h)
+
+では、_o_ が infix operator であり、_ の部分が引数の構文的に置かれる場所を示している。しかし、_o_ は、record 内部で
+定義されていて、record のparameter を引数と持っている。実際、Category._o_ は、
+
+    λ a b c → Category._o_
+
+という型を持っていて、引数を三つ持っている。最初の引数は record であり、次の二つが、Hom (arrow) である。
+なので、折角、infix operator を定義しても、record の外で使う時には、引数がずれてしまう。そこで、
+
+    _[_o_] : ∀{c₁ c₂ ℓ} → (C : Category c₁ c₂ ℓ) → {a b c : Obj C} → Hom C b c → Hom C a b → Hom C a c
+    C [ f o g ] = Category._o_ C f g
+
+などと定義することがある。これで、圏Cの中での射の演算であることがわかり、表示も綺麗になる。
+
+この圏Cは、module parameter にすると、暗黙の引数として使うことができ、そこで import Category すれば、
+_o_ を本来の infix operator として再定義して、使用することができる。
+
 --record での変数の位置の選択
 
 record 型を入力で使う場合は、
@@ -662,15 +725,6 @@
 ここまでで、 圏の定義と 関手の定義を使ってきた。 自然変換の定義は、以下のようになる。
 
 
---        F(f)                                                                                                                                
---   F(a) ---→ F(b)                                                                                                                           
---    |          |                                                                                                                            
---    |t(a)      |t(b)    G(f)t(a) = t(b)F(f)                                                                                                 
---    |          |                                                                                                                            
---    v          v                                                                                                                            
---   G(a) ---→ G(b)                                                                                                                           
---        G(f)                                                                                                                                
-
     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))
@@ -686,6 +740,14 @@
         TMap :  (A : Obj domain) → Hom codomain (FObj F A) (FObj G A)
         isNTrans : IsNTrans domain codomain F G TMap
 
+これは、以下のような可換図に対応する
+
+\begin{tikzcd}
+F(a) \arrow{r}{F(f)} \arrow{d}{t(a)} & F(b) \arrow{d}{t(b)} & \mbox{} \\
+G(a) \arrow{r}[swap]{G(f)} & G(b) & \mbox{} \\
+\end{tikzcd}
+
+
 今までと同じように二つにわけて定義している。
 
 これを使って、 Monad の結合性の証明を以下のように行うことができる。まず Monad を定義する。
@@ -781,12 +843,58 @@
 括弧のレベルの深い部分に推論規則を適用することを示す。
 begin/∎  の式変形は入れ子にすることができて、式の特定の部分に対して、着目して変形することできる。
 
+これらの定義は以下のようになっている。
+
+    module ≈-Reasoning {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where
+      _o_ :  {a b c : Obj A } ( x : Hom A a b ) ( y : Hom A c a ) → Hom A c b
+      x o y = A [ x o y ]
+
+      _≈_ :  {a b : Obj A }   → Rel (Hom A a b) ℓ
+      x ≈ y = A [ x ≈ y ]
+
+      infixr 9 _o_
+      infix  4 _≈_
+
+      refl-hom :   {a b : Obj A } { x : Hom A a b }  →  x ≈ x
+      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
+
+      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  )
+
+      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 }
+         →   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₂′ ℓ′}
+             {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 ] ]
+      nat η  =  IsNTrans.commute ( isNTrans η  )
+
+
 IsMonad.assoc ( isMonad M)  は、Monad の結合則が使われている部分である。
 
 この証明は、もちろん手での証明、清書された証明と同一である。、この
 証明を見ると、Monad の規則にうち、結合則のみを使っていることがわかる。
 自然変換の可換則を一箇所、T の分配則を二箇所で使っていることがわかる。
 
+手書きの式に比べるとかなり長いが、そこでの式の対応は Agda 言語にそって決まっている。また、
+証明を構築していく時に、? を使った単一化が道標となる。式の変形では、ad-hoc な記号が使われる。
+実際、T は、射の関数と対象の関数で同じ T が使われているが、それは別な式になっている。
+これになれるには、それなりの演習を解く必要があるが、Agda では FMap, FObj などで明示的に
+区別されている。
+
 --Agda の有効性
 
 Agda は Haskell の構文との親和性があり、Haskell を知っていれば、他の証明支援系よりも学びやすいと思われる。