--- a/agda-prog.ind	Thu Nov 28 18:48:14 2013 +0900
+++ b/agda-prog.ind	Sun Dec 01 17:58:05 2013 +0900
@@ -34,66 +34,258 @@
 
 --証明支援系
 
-Monad とか Kan extension とかを知らないと関数型プログラミングできない
-
-Monad の結合性を示すだけでも煩雑な計算が必要
-
-高階述語論理
-
-ハイティング代数
-
-Curry Howard 対応
-
-Coq
+% Monad とか Kan extension とかを知らないと関数型プログラミングできない
+% 
+% Monad の結合性を示すだけでも煩雑な計算が必要
+% 
+% 高階述語論理
+% 
+% ハイティング代数
+% 
+% Curry Howard 対応
+% 
+% Coq
 
 例題としての圏論
 
+証明支援系の歴史は古く、80年代にはMLで記述されたHOL\cite{}が既に使われるようになってきた。
+ここで使う Agda\cite{} は、証明とλ式が対応するという Curry Howard 対応に基づく証明支援系であり、
+Haskell\cite{} で記述されている。この論文では、Agda での証明の実際をプログラミングの
+視点から考察する。
+
+証明支援系は、従来、小さいプログラムが満たす性質を証明しようとしても記述が膨大になると
+いう欠点があった。近年では、数万行程度のプログラムも証明の対象にすることができるように
+なってきてる。しかし、ここでは、実際のプログラムの性質の証明とは違った視点から
+証明支援系の必要性を調べてみたい。
+
+Haskell などの関数型言語では、I/Oや継続、計算量、並列計算などの計算の様々な様相を Monad の仕組みを用いて
+実現している。Monad は圏論(Category theory)の概念であり、その性質の証明は若干煩雑である。
+Monad は随伴関手(Adjoint pair)や、Kleisli 圏と対応しているが、それを理解するには一連の証明を
+理解する必要がある。
+
+Monad の非数学的な説明はいくつかあるが、Monad を使ってプログラムを記述する必然性を
+理解しようとすれば証明を避けるのは好ましくない。そこで、証明支援系を使って、Monad を
+理解できれば、関数型プログラミングを学ぶものにとって都合が良いと思われる。特に、
+Haskell で記述された Agda は構文的に Haskell と似ていて、理解しやすい。
+
+プログラムのバグを見つけるにはモデル検証が使われるようになってきているが、モデル検証は
+式と値の対応に着目して、その可能な対応をすべて列挙することにより反例を見つける。これは、
+命題式に真偽を割り当てていく方法になっている。
+
+Agda の論理は、証明を提示すことによって命題式が真であることを示すハイティング代数という
+ものである。モデル検証とは本質的に異なる方法である。
+
+証明支援系としては Coq も良く使われている。Agda と Coq は良く似ているが、Agda は Emacs
+を用いた式変形と穴埋め的な使い方をするのに対して、Coq は自動証明を重視したコマンドによる
+式変形を中心とした使い方するようになっている。証明支援系の比較などは、この論文\cite{}が
+参考になる。
+
+ここでは Agda での証明の対象して圏論、特に、Monad を用いる。Monad を理解するために、
+Agda をどのように使えるか、そこで使える Agda でのいつくかの tips を示す。
+
+
 --人による証明
 
-数学の本に書いてある証明
+%数学の本に書いてある証明
+%
+%省略された部分
+%
+%問題を解いてわかる部分
+%
+%手書きの証明
+%
+%清書された証明
+%
+%Proof System 上の証明
+%
+%理解するとはどういうこと?
+%
+%モデルを理解する
+%
+%証明を理解する
+%
+%パターンを理解する
 
-省略された部分
+Agda での証明の実際に入る前に、本に書かれているような証明について調べてみよう。
+
+数学の本には証明が極めて簡潔に書かれている。Monad を理解するためには、圏(Category)、関手(Functor)、
+自然変換(Natrual Transformation)、Monad が満たす関手と自然変換の性質を理解して、Haskell の Monad の
+join の結合法則 
+
+   f * ( g * h ) = ( f * g ) * h
+
+を証明することが目標だとしよう。ここでは Introduction to higher order categorical logic を例として用いる。
+
+圏の定義は、
 
-問題を解いてわかる部分
+   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
+   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.
+
+関手の定義は、
+
+   Definition 1.3. A cuntor F: A->B is first of all a morphism of graph, that is, it sends objects of A to
+   object so B and arrows of A to arrows of B such that, if f: A->A' then F(f):F(A)->F(A'). Moreover
+   functor preserves identities and compisition; thus
+      F(1_A) = 1_F(A), F(gf) = F(g)F(f)
+
+自然変換の定義は、
 
-手書きの証明
+    Definition 2.1. Given functors F,G: A -> B, a natural transformatin t: F -> G is a familty of
+    arrows t(A): F(A) -> G(A) in B, one arrow for each object A of A, suc that the following
+    square commutes for all arrows f: A -> in A.
+
+    that is to say, such that
+
+       G(f)t(a) = t(B)F(f).
+
+と書かれている。さらに、Monad は関手Tと二つの自然変換の組であり以下のように定義されている。
 
-清書された証明
+    Definition 6.1 A triple(T,η,μ) on a category A consists of a functor T: A->A and natural transformation η: 1_A -> T
+    and μ:T^2 -> T satifying the equation
+
+      μ○Tη = 1_T = μ○ηT, μ○μT = μ○Tμ
+
+となっている。 ここで、関手Tと自然変換ηの 合成 Tηの定義は
+
+     (Tη)(A) = T(η(A))     \label{comp-of-func-nat}
+     (ηT)(A) = η(T(A))     \label{comp-of-nat-func}
+
+である。
 
-Proof System 上の証明
+これらの定義から証明するべきなのは、join の結合性であり、join は以下のように記述される。
+
+    g * f =def μ(A'')T(g)f 
+
+以上の定義に対して、
+
+   f * ( g * h ) = ( f * g ) * h
+
+を示せば良い。
+
+本の証明は自然言語で書かれていて、簡潔な代わりに多くのものが省略されている。例えば、式\ref{comp-of-func-nat}
+に出てくるTと式\ref{comp-of-nat-func} に出てくるT は、前者は arrows からarrows の関数であり、後者は
+object から object への関数である。つまり、同じ T で二つの異なる関数を表している。確かに関手の定義には、
+二つの関数が記述されている。これは、文章による証明の記述では記号が polymorphic に使われることを示している。
+つまり、それが要求される型によって異なる関数が対応している。
 
-理解するとはどういうこと?
+---関手とは何か、自然変換とは何か
+
+関手は定義の通りのものだが、Monad の視点から見ると、データ型のコンストラクタに相当する。
+例えば、文字の集合があった時に、文字列やファイルを作るのは、文字の集合に相当する圏から、
+ファイルの集合に相当する圏への関手になる。この場合、関手は文字列の結合に対する分配則を
+満たす必要がある。
+
+すると、自然変換はデータ型からデータ型への変換を表す。例えば、SJISのファイルからUTF8へのファイルに変換する
+プログラム nkf は、自然変換だと考えられる。実際、 ファイルからファイルへの操作、例えば grep '単位' があった時に、SJIS で SJIS対応のgrepを使ってから、nkf で
+UTF8の結果に変換するのと、先にnkfでUTF8に変換してからUTF8対応のgrepを使うのと結果は同じでなければならない。
+これが可換性であり、自然変換であるための条件になる。
+
+このような特定の分野に向いた例示は定義からは出てこない。
+
+証明で重要なのは、関手の提供する関手の分配法則と、自然変換の提供する可観測であり、それ以外の余計な直観は必要ない。
+
+---Monadのjoinとは何か
 
-モデルを理解する
+Monad は一つの関手Tと二つの自然変換(η,μ)を含む複雑な概念だが、T は Monad を表すデータ構造のコンストラクタだと考えて良い。
+これは、計算の様々な様相を表すメタデータと、通常の入力との組であることが多い。
+
+ηは、メタデータから通常のデータだけを取ってくる自然変換であり、Haskell Monad のreturnに相当する。μは、結合されるべき二つの
+関数が生成する二つのTを一つのTにまとめる自然変換である。これは、Haskell Monad の join に相当する。
+
+--手書きの証明
+
+定義は与えられたので、証明するべき命題、
+
+   f * ( g * h ) = ( f * g ) * h
+
+を定義に沿って展開すれば良い。これはかなり長い式になる。右側と左側から両方を展開する。そして、見比べる。
+これを関手の分配則と、自然変換が持つ可観測により変形して等しいことを示せば良い。
+
+ここで、可換図が重要になる。可換図は自然変換の可換則の具体例を示すのに使える。つまり、自然変換の等式の
+変数を具体的に決めたものを与える。これを使って、計算することになる。
 
-証明を理解する
+--証明の清書
+
+手書きの証明が終わると、これを例えば LaTeX などで清書する。清書には一部可換図も含まれる。ここでは以下のような式の変形と可換図が
+得られる。
+
+--証明を理解するということ
+
+ここでは証明は式の一連の変形であり操作に過ぎない。この操作を理解することと、関手や自然変換が何かを理解することは別物である。
 
-パターンを理解する
+圏や関手の公理を満たす例を考えることは、その数学構造のモデルを考えることに相当する。モデルとは、ここでは、公理をすべて正しくするような
+変数の値の組である。
+
+モデルとして圏や関手を理解することと、証明を理解することは違うことだが、モデルがあれば、その理論は整合的であることが言える。
+また、証明があれば、その式は正しい。
+
+Monad の定義から自明に join の結合法則を導くようなモデルを考えることは難しいが、証明自体は式の変形でわかりやすい。しかし、
+量も多く煩雑な操作となる。ここで、証明支援系が役に立つと思われる。
+
 
 --Agda
 
-式
-
-Lambda 式
+% Append の例
+% 
+% 式
+% 
+% Lambda 式
+% 
+% 変数の定義
+% 
+% 変数の型
+% 
+% データ型
+% 
+% レコード型
+% 
+% 等号
+% 
+%    データ型を使った等号
+%    関係を表す集合としての等号
+% 
+% 集合のレベル
+% 
+% 暗黙の引数
+% 
+% emacs との連携
 
-変数の定義
+Agda は Haskell と同じような構文を持つλ式の集合である。例えば、Agda の append は以下のようになる。
 
-変数の型
-
-データ型
 
-レコード型
+    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)
+
+このプログラムは、Haskell の定義とほぼ同じである。Haskell と違い型定義を省略することはできない。また、List の要素の型 A が Set として
+明示されている。最初の data List が List のデータ型を定義している。append は ++ で定義される。
 
-   データ型を使った等号
-   関係を表す集合としての等号
+つまり、Agda では、一つの関数を定義するのに、型と関数の両方を定義する必要がある。Agda の型は、また、Agda の式であり、それ自体の
+型の整合性が要求される。 一つの名前を定義するのに、: で型を定義して、= で、その値を定義する。 
+
+data 型の要素の数だけパータンを作ることができ、この場合は、[] と _::_ の二つの場合分けになっている。:: は中置き演算子であり、
+
+    _::_(a,b) 
 
-集合のレベル
+と
+
+   (a :: b)
 
-暗黙の引数
+は同じものを表している。
 
-emacs との連携
+ここでは型には ( 変数名 : 型名 ) による型の要素の定義と、(入力型→出力型)で表される関数の二種類がある。
+
+
 
 --Agda での証明方法
 
@@ -105,6 +297,8 @@
 
 数式変形用に ? を使う
 
+証明の例 (Append の結合)
+
 record の使い方
 
 数学的構造の存在を示す
@@ -135,6 +329,17 @@
 
 Mono morphism から来る問題
 
+--圏論の例
+
+圏の定義
+
+関手の定義
+
+自然変換の定義
+
+Monad の結合性の証明
+
+
 --Agda の有効性
 
 Haskell の構文との親和性