--- a/paper/agda.tex	Sat Feb 08 22:07:16 2020 +0900
+++ b/paper/agda.tex	Mon Feb 10 14:20:21 2020 +0900
@@ -12,14 +12,10 @@
 Agda \cite{agda} は純粋関数型言語である。
 Agda は依存型という型システムを持ち、型を第一級オブジェクトとして扱う。
 
-Agda の記述ではインデントが
-意味を持ち、スペースの有無もチェックされる。
+Agda の記述ではインデントが意味を持ち、スペースの有無もチェックされる。
 コメントは \verb/-- comment/ か \verb/{-- comment --}/ のように記述される。
 また、\verb/_/でそこに入りうるすべての値を示すことができ、
 \verb/?/でそこに入る値や型を不明瞭なままにしておくことができる。
-また、Agda では停止性の検出機能が存在し、プログラム中に停止しない関数が存在するとコンパイル時にエラーが出る。
-\verb/{-# TERMINATING #-}/のタグを付けると停止しないプログラムをコンパイルすることができるがあまり望ましくない。
-
 
 Agda のプログラムは全てモジュール内部に記述される。
 そのため、各ファイルのトップレベルにモジュールを定義する必要がある。
@@ -39,6 +35,7 @@
 \section{Agda のデータ}
 Agda 型をデータや関数に記述する必要がある。
 Agda における型指定は \verb/:/ を用いて \verb/name : type/ のように記述する。
+このとき \verb/name/ に 空白があってはいけない。
 データ型は、代数的なデータ構造で、その定義には \verb/data/ キーワードを用いる。
 \verb/data/ キーワードの後に \verb/data/ の名前と、型、 \verb/where/ 句を書きインデントを深くし、
 値にコンストラクタとその型を列挙する。
@@ -57,7 +54,7 @@
 
 Agda には C 言語における構造体に相当するレコード型というデータも存在する、
 例えば \verb/x/ と \verb/y/ の二つの自然数からなるレコード \verb/Point/ を定義する。\coderef{agda-record}のようになる。
-\lstinputlisting[label=agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda.replaced}
+\lstinputlisting[label=agda-record, caption=Agdaにおけるレコード型の定義] {src/env.agda.replaced}
 レコードを構築する際は \verb/record/ キーワード後の \verb/{}/ の内部に \verb/FieldName = value/ の形で値を列挙する。
 複数の値を列挙するには \verb/;/ で区切る必要がある。
 
@@ -65,6 +62,7 @@
 \section{Agda の関数}
 Agda での関数は型の定義と、関数の定義をする必要がある。
 関数の型はデータと同様に \verb/:/ を用いて \verb/name : type/ に記述するが、入力を受け取り出力返す型として記述される。$\rightarrow$ 、 または\verb/→/ を用いて \verb/input → output/ のように記述される。
+また、\verb/_+_/のように関数名で\verb/_/を使用すると引数がその位置にあることを意味し、中間記法で関数を定義することもできる。
 関数の定義は型の定義より下の行に、\verb/=/ を使い \verb/name input = output/ のように記述される。
 
 例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A → B/ のように書くことができる。
@@ -81,7 +79,6 @@
 
 \lstinputlisting[label=agda-plus, caption=自然数での加算の定義] {src/agda-plus.agda.replaced}
 %% \lstinputlisting[label=agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda.replaced}
-\verb/_+_/のように関数名で\verb/_/を使用すると引数がその位置にあることを意味する。
 
 パターンマッチでは全てのコンストラクタのパターンを含む必要がある。
 例えば、自然数$\mathbb{N}$を受け取る関数では \verb/zero/ と \verb/suc/ の2つのパターンが存在する必要がある。
@@ -105,6 +102,15 @@
 
 \lstinputlisting[label=agda-where, caption=Agda における where 句] {src/AgdaWhere.agda.replaced}
 
+\section{Agda の関数での停止性}
+Agda では停止性の検出機能が存在し、プログラム中に停止しない記述が存在するとコンパイル時にエラーが出る。
+\verb/{-# TERMINATING #-}/のタグを付けると停止しないプログラムをコンパイルすることができるがあまり望ましくない。
+
+ここでは停止する関数と停止しない関数の例\coderef{termination}を扱う。
+%% \lstinputlisting[label=termination, caption=停止する関数、停止しない関数] {src/terminating.agda.replaced}
+
+このように再帰的な定義の関数が停止するときは、何らかの値が減少する必要がある。
+
 
 \section{定理証明支援器としての Agda}
 Agda での証明では関数の記述と同様の形で型部分に証明すべき論理式、 $\lambda$ 項部分にそれを満たす証明を書くことで証明を行うことが可能である。