--- a/paper/type.tex	Sat Jan 28 09:02:15 2017 +0900
+++ b/paper/type.tex	Sat Jan 28 09:46:02 2017 +0900
@@ -66,6 +66,67 @@
 
 % }}}
 
+\section{型無し算術式}
+まず、型システムやその性質について述べるためにプログラミング言語そのものの基本的な性質について述べる。
+プログラムの構文と意味論、推論について考えるために整数とブール値のみで構成される小さな言語を扱いながら考察する。
+この言語は二種類の値しか持たないが、項の帰納的定義や証明、評価、実行時エラーのモデル化を表現することができる。
+
+この言語はブール定数 $ true $ と $ false $ 、条件式、数値定数 0 、算術演算子 $ succ $ と $ pred $ 、判定演算子 $ iszero $ のみからなる。
+算術演算子 $ succ $ は与えられた数の次の数を返し、 $ pred $ はその前の数を返す。
+判定演算子$ iszero $ は与えられた項が 0 なら $ true $ を返し、それ以外は $ false $ を返す。
+これらを文法として定義すると以下のリスト\ref{src:expr-term}のようになる。
+
+\lstinputlisting[label=src:expr-term, caption=算術式の項定義] {src/expr-term.txt}
+
+この定義では算術式の項 $ t $ を定義している。
+$ ::= $ は項の集合の定義を表であり、$ t $ は項の変数のようなものである。
+それに続くすべての行は、構文の選択肢である。
+構文の選択肢内に存在する記号 $ t $ は任意の項を代入できることを表現している。
+このように再帰的に定義することにより、 \verb/ if (ifzero (succ 0)) then true else (pred (succ 0)) / といった項もこの定義に含まれる。
+例において、 $ succ $ 、 $ pred $ 、 $ iszero $ に複合的な引数を渡す場合は読みやすさのために括弧でくくっている。
+括弧の定義は項の定義には含んでいない。
+コンパイラなど具体的な字句をパースする必要がある場合、曖昧な構文を排除するために括弧の定義は必須である。
+しかし、今回は型システムに言及するために曖昧な構文は明示的に括弧で指示することで排除し、抽象的な構文のみを取り扱うこととする。
+
+現在、項と式という用語は同一である。
+型のような別の構文表現を持つ計算体系においては式はあらゆる種類の構文を表す。
+項は計算の構文的表現という意味である。
+
+この言語におけるプログラムとは上述の文法で与えられた形からなる項である。
+評価の結果は常にブール定数か自然数のどちらかになる。
+これら項は値と呼ばれ、項の評価順序の形式化において区別が必要となる。
+
+なお、この項の定義においては \verb/succ true/ といった怪しい項の形成を許してしまう。
+実際、これらのプログラムは無意味なものであり、このような項表現を排除するために型システムを利用する。
+
+ある言語の構文を定義する際に、他の表現かいくつか存在する。
+先程の定義は次の帰納的な定義のためのコンパクトな記法である。
+
+\begin{definition}
+    項の集合とは以下の条件を満たす最小の集合 $ T $ である。
+    \begin{eqnarray*}
+        \label{eq:expr}
+        \{true , false , 0\} \subseteq T \\
+        t_1 \in T ならば \{succ \; t_1 , pred \; t_1 , iszero \; t_1\} \subseteq T \\
+        t_1 \in T かつ t_2 \in T かつ t_3 \in T ならば if \; t_1 \; then \; t_2 else \; t_3 \subseteq T
+    \end{eqnarray*}
+\end{definition}
+
+まず1つめの条件は、$ T $ に属する3つの式を挙げている。
+2つめと3つめの条件は、ある種の複合的な式が $ T $ に属することを判断するための規則を表している。
+最後の「最小」という単語は $ T $ がこの3つの条件によって要求される要素以外の要素を持たないことを表している。
+
+また、項の帰納的表現の略記法として、二次元の推論規則形式を用いる方法もある。
+これは論理体系を自然演繹スタイルで表現するためによく使われる。
+自然演繹による証明は\ref{agda}章内で触れるが、今回は項表現として導入する。
+
+\begin{definition}
+    
+\end{definition}
+
+
+
+
 % {{{ 型なしラムダ計算
 \section{型なしラムダ計算}
 まず、プログラミング言語における計算を形式的に定義する。