# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1386241827 -32400
# Node ID 442e62a339a623f842f5b4046090a70a76c8e9a7
# Parent  9ebac033917d816211a886b413dfe9c6acb86080
on going..

diff -r 9ebac033917d -r 442e62a339a6 agda-prog.ind
--- a/agda-prog.ind	Thu Dec 05 18:40:21 2013 +0900
+++ b/agda-prog.ind	Thu Dec 05 20:10:27 2013 +0900
@@ -7,7 +7,7 @@
 
 --abstract:
 
-Agda\cite{aga} は、Haskell \cite{haskell}上の Dependent type に基づく証明支援系である。
+Agda\cite{Agda} は、Haskell \cite{haskell}上の Dependent type に基づく証明支援系である。
 Agda での証明は型付きλ式であり、証明するべき式も型付きλ式になっている。
 したがって、Agda での証明は、本質的にはλ式を構築していく作業になる。
 
@@ -20,7 +20,7 @@
 行い、その型に沿ったλ式を書いていくという点ではプログラミングそのもの
 である。
 
-Agdaの証明は、Curry Howard対応\cite{}に基づいており、
+Agdaの証明は、Curry Howard対応\cite{Girard:1989:PT:64805}に基づいており、
 すべては、型を表す式と、その型を持つλ式の組で表される。
 Dependent type の特徴は省略可能な引数(暗黙の引数)にあり、
 これは、通常のプログラミング言語にはない概念である。
@@ -53,9 +53,9 @@
 
 % 例題としての圏論
 
-証明支援系の歴史は古く、80年代にはMLで記述されたHOL\cite{}が既に使われるようになってきた。
-ここで使う Agda\cite{} は、証明とλ式が対応するという Curry Howard 対応に基づく証明支援系であり、
-Haskell\cite{} で記述されている。この論文では、Agda での証明の実際をプログラミングの
+証明支援系の歴史は古く、80年代にはMLで記述されたHOL\cite{hol94}が既に使われるようになってきた。
+ここで使う Agda\cite{Agda} は、証明とλ式が対応するという Curry Howard 対応に基づく証明支援系であり、
+Haskell\cite{haskell} で記述されている。この論文では、Agda での証明の実際をプログラミングの
 視点から考察する。
 
 証明支援系は、従来、小さいプログラムが満たす性質を証明しようとしても記述が膨大になると
@@ -63,8 +63,8 @@
 なってきてる。しかし、ここでは、実際のプログラムの性質の証明とは違った視点から
 証明支援系の必要性を調べてみたい。
 
-Haskell などの関数型言語では、I/Oや継続、計算量、並列計算などの計算の様々な様相を Monad の仕組み\cite{}を用いて
-実現している。Monad は圏論(Category theory)\cite{}の概念であり、その性質の証明は若干煩雑である。
+Haskell などの関数型言語では、I/Oや継続、計算量、並列計算などの計算の様々な様相を Monad の仕組み\cite{Moggi:1989:CLM:77350.77353}を用いて
+実現している。Monad は圏論(Category theory)\cite{Lambek:1986:IHO:7517}の概念であり、その性質の証明は若干煩雑である。
 Monad は随伴関手(Adjoint pair)や、Kleisli 圏と対応しているが、それを理解するには一連の証明を
 理解する必要がある。
 
@@ -73,7 +73,7 @@
 理解できれば、関数型プログラミングを学ぶものにとって都合が良いと思われる。特に、
 Haskell で記述された Agda は構文的に Haskell と似ていて、理解しやすい。
 
-プログラムのバグを見つけるにはモデル検証\cite{}が使われるようになってきているが、モデル検証は
+プログラムのバグを見つけるにはモデル検証\cite{Bur90}が使われるようになってきているが、モデル検証は
 式と値の対応に着目して、その可能な対応をすべて列挙することにより反例を見つける。これは、
 命題式に真偽を割り当てていく方法になっている。
 
@@ -82,7 +82,7 @@
 
 証明支援系としては Coq も良く使われている。Agda と Coq は良く似ているが、Agda は Emacs
 を用いた式変形と穴埋め的な使い方をするのに対して、Coq は自動証明を重視したコマンドによる
-式変形を中心とした使い方するようになっている。証明支援系の比較などは、この論文\cite{}が
+式変形を中心とした使い方するようになっている。証明支援系の比較などは、この論文\cite{Wiedijk:2006:SPW:1121735}が
 参考になる。
 
 ここでは Agda での証明の対象して圏論、特に、Monad を用いる。Monad を理解するために、
@@ -288,7 +288,7 @@
 % 
 % emacs との連携
 
-ここでは Agda をざっと概観する。例えば、\cite{} の論文がわかりやすい。
+ここでは Agda をざっと概観する。例えば、\cite{Agda} の論文がわかりやすい。
 Agda は Haskell と同じような構文を持つλ式の集合である。例えば、Agda の List は以下のようになる。
 
     infixr 40 _::_
@@ -312,7 +312,7 @@
 Haskell の型と異なり、Agda では、型と式に同じものを書ける。それだけ強力な型システムjを持っている。型の記述にも型の整合があり、
 値は、その記述された型に整合する必要がある。つまり、Agda での型の整合は一つの式の定義に対して二度行われることになる。
 
-data 型のfiledの数だけパータンマッチングを作ることができ、この場合は、[] と _::_ の二つの場合分けになっている。:: は中置き演算子であり、
+data 型のfiledの数だけパータンマッチングを作ることができ、この場合は、[] と \_::\_ の二つの場合分けになっている。:: は中置き演算子であり、
 
     _::_(a,b) 
 
@@ -331,7 +331,7 @@
 集合になる。Set (suc a) は、Set a の一つ上のレベルの集合を表す。ここでは、任意のレベルの集合に対する
 List を定義している。
 
-infixl, infixr が中置き演算子であり、_  が引数の位置を表す。a ++ b の演算子は _++_ であり、_++_ a b  と同じものを表している。
+infixl, infixr が中置き演算子であり、\_  が引数の位置を表す。a ++ b の演算子は \_++\_ であり、\_++\_ a b  と同じものを表している。
 
 ---data型を使った等号
 
@@ -347,7 +347,7 @@
 a == a というデータ構造を返す。これは、a == a の証明に対応するλ式でもあって、Curry Haward 対応に
 相当する。
 
-これは、実際には、Relation.Binary.PropositionalEquality で _≡_  として定義されているので、自分で定義する必要はない。
+これは、実際には、Relation.Binary.PropositionalEquality で \_≡\_  として定義されているので、自分で定義する必要はない。
 
 data 型の他に record 型あり、この append の例題では使わないが、排他的和を表すデータ構造を提供し、圏や関手を定義することができる。
 
@@ -359,9 +359,9 @@
 --- ? の使い方
 
 
-Agda では、まず、ファイルを読み込み C-L (agda2-load)とすると、 全体の型がチェックされ、色で識別される。
+Agda では、まず、ファイルを読み込み C-L (agda2-load)とすると、 全体の型がチェックされ、色で識別される(図\ref{list-1})。
 
-<img src="fig/agda-list-1.png">
+<center><img src="fig/agda-list-1.pdf" alt="list-1"></center>
  
 定義した式の一部を ? で置き換えると、そこに必要な型を示してくれる。
 
@@ -373,7 +373,7 @@
          ( ( xs ++ ys ) ++ zs ) == ( xs ++ ( ys ++ zs ) )
     list-assoc  = ?
 
-list-assoc は、入力として A の list を取る。そして、結合法則を表す等式(を表したデータ構造 _==_ )を返す。_==_ は、同じものからしか作ることはできない。
+list-assoc は、入力として A の list を取る。そして、結合法則を表す等式(を表したデータ構造 \_==\_ )を返す。\_==\_ は、同じものからしか作ることはできない。
 
 ? は、
 
@@ -392,7 +392,7 @@
     ?0 : [] ++ ys ++ zs == [] ++ (ys ++ zs)
     ?1 : x :: xs ++ ys ++ zs == x :: xs ++ (ys ++ zs)
 
-となる。?0 の方は、_++_ の定義( [] ++ ys = ys )から ys ++ zs になる。これは、Emacs の ?0 上にカーソルを合わせて、
+となる。?0 の方は、\_++\_ の定義( [] ++ ys = ys )から ys ++ zs になる。これは、Emacs の ?0 上にカーソルを合わせて、
 
     \ys zs -> [] ++ ys ++ zs
     \ys zs -> [] ++ (ys ++ zs)
@@ -401,7 +401,7 @@
 
     λ ys₁ zs₁ → ys₁ ++ zs₁
 
-となる。つまり両辺は同じものなので、_==_ のコンストラクタ reflection を使って生成できる。
+となる。つまり両辺は同じものなので、\_==\_ のコンストラクタ reflection を使って生成できる。
 
     list-assoc  [] ys zs = reflection
 
@@ -409,7 +409,7 @@
 
     ?1 : x :: xs ++ ys ++ zs == x :: xs ++ (ys ++ zs)
 
-の方は、_++_ のもう一つのパターンを使う必要がある。こちらの両辺は、C-n を使っても
+の方は、\_++\_ のもう一つのパターンを使う必要がある。こちらの両辺は、C-n を使っても
 
     λ x₁ xs₁ ys₁ zs₁ → x₁ :: (xs₁ ++ ys₁ ++ zs₁)
     λ x₁ xs₁ ys₁ zs₁ → x₁ :: (xs₁ ++ (ys₁ ++ zs₁))
@@ -432,7 +432,7 @@
        ( f : List A → List B ) → {x : List A } → {y : List A} → x == y → f x == f y
     cong1 f reflection = reflection
 
-ここで、cong1 の最初の引数は作用させる関数f で、二つ目の引数は x == y という式である。x == y は _==_ のデータ構造で、
+ここで、cong1 の最初の引数は作用させる関数f で、二つ目の引数は x == y という式である。x == y は \_==\_ のデータ構造で、
 reflection という field を持っている。
 
     cong1 f reflection 
@@ -489,7 +489,7 @@
         (x :: xs) ++ (ys ++ zs)
       ∎
 
-数式が ==⟨ cong1 (_::_ x) (++-assoc A xs ys zs) ⟩ などで変形されている。 ==⟨ reflection ⟩ は、何の変形もしてないが、両方が異なる見かけの同じ正規型
+数式が ==⟨ cong1 (\_::\_ x) (++-assoc A xs ys zs) ⟩ などで変形されている。 ==⟨ reflection ⟩ は、何の変形もしてないが、両方が異なる見かけの同じ正規型
 である時に見かけを変形している。 ==⟨⟩ と書くこともできる。
 
 ---数式変形の記述
@@ -527,8 +527,8 @@
     trans-list :  ∀{n} {A : Set n} {x y z : List A}  → x ==  y → y == z → x == z
     trans-list reflection reflection = reflection
 
-relTo が、等しくなるべき等式を持っていて、証明の最後を示す _∎ _ が、三段論法で繋がったすべての等式が等しいことを要求する。
-最後に　begin_ が _IsRelatedTo_ を _==_ に変換する。
+relTo が、等しくなるべき等式を持っていて、証明の最後を示す \_∎ \_ が、三段論法で繋がったすべての等式が等しいことを要求する。
+最後に　begin\_ が \_IsRelatedTo\_ を \_==\_ に変換する。
 
 数式変形は任意の等式に使えるが、自分用にカスタマイズして使う方が良い。良く使用する推論や定理も一緒に記述する方が良い。
 
@@ -538,7 +538,7 @@
 
 --record の使い方
 
-data は constructor を提供するが、record は数学的構造の存在を示す。以下は\cite{} による圏の定義である。
+data は constructor を提供するが、record は数学的構造の存在を示す。以下は\cite{Lambek:1986:IHO:7517} による圏の定義である。
 
     record IsCategory {c₁ c₂ ℓ : Level} (Obj : Set c₁)
                       (Hom : Obj → Obj → Set c₂)
@@ -573,16 +573,16 @@
 record を入力に使うと、filed は、すべて仮定される。
 つまり、filed に記述した性質を持つ数学的存在を仮定することになる。なので、record は、数学的存在を記述するのに向いている。
 
-ここで、Hom は圏の arrow であり、対象を二つ引数とし何かの集合を返す関数として定義されている。_≈_ は、arrow の等号だが、data 型としては
+ここで、Hom は圏の arrow であり、対象を二つ引数とし何かの集合を返す関数として定義されている。\_≈\_ は、arrow の等号だが、data 型としては
 定義されていなくて、Rel (Hom A B) ℓ)　となっている。これは、Relation.Binary.Core に定義されていて、
 
     Rel : ∀ {a} → Set a → (ℓ : Level) → Set (a ⊔ suc ℓ)
     Rel A ℓ =  A → A → Set ℓ
 
 となっている。つまり arrow と同じように集合で定義されている。ここでは Aという型を持つ引数を二つ持ち、何かの 集合を返す関数である。
-このせいで、arrow には _≡_ を使うことができない。
-合同性 ( 同じものに同じ関数を作用させても同じ ) は、 _≡_  を仮定しているので、この圏の定義では、合同性を
-自由に使うことはできない。もし、arrow が Set であれば、あるいは、_≈_  → _≡_   を仮定すれば、 _≡_  を使うことができる。
+このせいで、arrow には \_≡\_ を使うことができない。
+合同性 ( 同じものに同じ関数を作用させても同じ ) は、 \_≡\_  を仮定しているので、この圏の定義では、合同性を
+自由に使うことはできない。もし、arrow が Set であれば、あるいは、\_≈\_  → \_≡\_   を仮定すれば、 \_≡\_  を使うことができる。
 
 --infix operator
 
@@ -592,8 +592,8 @@
         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_ は、
+では、\_o\_ が infix operator であり、\_ の部分が引数の構文的に置かれる場所を示している。しかし、\_o\_ は、record 内部で
+定義されていて、record のparameter を引数と持っている。実際、Category.\_o\_ は、
 
     λ a b c → Category._o_
 
@@ -606,7 +606,7 @@
 などと定義することがある。これで、圏Cの中での射の演算であることがわかり、表示も綺麗になる。
 
 この圏Cは、module parameter にすると、暗黙の引数として使うことができ、そこで import Category すれば、
-_o_ を本来の infix operator として再定義して、使用することができる。
+\_o\_ を本来の infix operator として再定義して、使用することができる。
 
 --record での変数の位置の選択
 
@@ -659,14 +659,14 @@
  Extensionality a b = {A : Set a} {B : A → Set b} {f g : (x : A) → B x} 
      → (∀ x → f x ≡ g x) → f ≡ g → ( λ x → f x ≡ λ x → g x )             
 
-つまり、全ての値について等しいからと言って、その関数自体が(_≡_ の意味で)等しいということを
+つまり、全ての値について等しいからと言って、その関数自体が(\_≡\_ の意味で)等しいということを
 証明することはできない。これは、仮定する必要がある。関数が仮定ではなく実際に構成されている
 ものならば、この仮定は必要ない。
 
 この式は、Agda のライブラリに記述されていて、必要ならばそれを postulate すれば良い。
 
-Rel で定義された等式から、_≡_ を導くこともできない。もし、圏の射が集合ならば
-射の等式は _≡_ で定義されるべきなので、以下を仮定しても良い、あるいはする必要がある。
+Rel で定義された等式から、\_≡\_ を導くこともできない。もし、圏の射が集合ならば
+射の等式は \_≡\_ で定義されるべきなので、以下を仮定しても良い、あるいはする必要がある。
 
     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
@@ -681,7 +681,7 @@
 
 また、
    a b  : Set 
-の場合に、a ≡ b は証明できない。 _≡_ は、初めから同じもの( x  ≡  x )に対して生成できるので、最初から
+の場合に、a ≡ b は証明できない。 \_≡\_ は、初めから同じもの( x  ≡  x )に対して生成できるので、最初から
 異なる可能性のあるものには成立しない。合同性の逆、写像した先で等しければ、元も等しいは、例えば以下の米田関手の
 Full embededing は、
 
diff -r 9ebac033917d -r 442e62a339a6 fig/agda-list-1.tiff
Binary file fig/agda-list-1.tiff has changed
diff -r 9ebac033917d -r 442e62a339a6 ipsj.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ipsj.tex	Thu Dec 05 20:10:27 2013 +0900
@@ -0,0 +1,63 @@
+\documentclass[techrep]{ipsjpapers}
+\usepackage[dvipdfmx]{graphicx}
+\usepackage{fancyvrb}
+\usepackage{url}
+\usepackage{ucs}
+\usepackage[utf8x]{inputenc}
+\usepackage{autofe}
+
+\DeclareUnicodeCharacter{8718}{\rule{5pt}{10pt}}
+
+% \input{dummy.tex} %% Font 
+
+% ユーザが定義したマクロなど．
+\makeatletter
+
+\input usepackage.tex
+\begin{document}
+
+
+% 和文表題
+\title{ Agda での Programming 技術}
+% 英文表題
+\etitle{Programming Technique in Agda}
+
+% 所属ラベルの定義
+\affilabel{1}{琉球大学工学部情報工学科\\Information Engineering, University of the Ryukyus.}
+
+% 和文著者名
+\author{
+  河野 真治\affiref{1}
+}
+
+% 英文著者名
+\eauthor{
+  Shinji KONO\affiref{1}
+}
+
+% 連絡先（投稿時に必要．製版用では無視される．）
+\contact{河野 真治\\
+        〒903-0213 沖縄県西原町千原1番地\\
+	    琉球大学工学部情報工学科\\
+        TEL: (098)895-2221\qquad FAX: (098)895-8727\\
+        email: kono@ie.u-ryukyu.ac.jp} 
+
+% 和文概要
+\begin{abstract}
+\input{abstract}
+\end{abstract}
+% 英文概要
+\begin{eabstract}
+\end{eabstract}
+
+% 表題などの出力
+\maketitle
+
+% 本文はここから始まる
+
+\input{0}   %
+
+\bibliographystyle{ipsjunsrt}
+\bibliography{ref}
+
+\end{document}
diff -r 9ebac033917d -r 442e62a339a6 ipsjpapers.cls
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ipsjpapers.cls	Thu Dec 05 20:10:27 2013 +0900
@@ -0,0 +1,16 @@
+% Copyright (C) 1995-2007 by Hiroshi Nakashima, Yasuki Saito and
+%                            The Editorial Board of the IPSJ Journal
+%
+% ipsjpapers.cls 13-Mar-07 by Hiroshi Nakashima (ver 2.12)
+% (revision history deleted)
+% ipsjpapers.cls  1-Apr-96 by Hiroshi Nakashima (ver 2.00)
+
+\ifx\pfmtname\undefined
+\NeedsTeXFormat{LaTeX2e}
+\else
+\NeedsTeXFormat{pLaTeX2e}
+\fi
+
+\ProvidesClass{ipsjpapers}[2007/06/15 ver 2.12]
+\input{ipsjpapers.sty}
+\endinput