--- a/paper/type.tex	Sat Jan 28 09:47:44 2017 +0900
+++ b/paper/type.tex	Sat Jan 28 10:29:37 2017 +0900
@@ -121,9 +121,99 @@
 自然演繹による証明は\ref{agda}章内で触れるが、今回は項表現として導入する。
 
 \begin{definition}
-    
+    項の集合は次の規則によって定義される。
+
+    \begin{prooftree}
+        \AxiomC{$ true \in T $}
+    \end{prooftree}
+
+    \begin{prooftree}
+        \AxiomC{$ false \in T $}
+    \end{prooftree}
+
+    \begin{prooftree}
+        \AxiomC{$ 0 \in T $}
+    \end{prooftree}
+
+    \begin{prooftree}
+        \AxiomC{$ t_1 \in T $}
+        \UnaryInfC{$ succ \; t_1 \in T$}
+    \end{prooftree}
+
+    \begin{prooftree}
+        \AxiomC{$ t_1 \in T $}
+        \UnaryInfC{$ pred \; t_1 \in T$}
+    \end{prooftree}
+
+    \begin{prooftree}
+        \AxiomC{$ t_1 \in T $}
+        \UnaryInfC{$ iszero \; t_1 \in T$}
+    \end{prooftree}
+
+    \begin{prooftree}
+        \AxiomC{$ t_1 \in T $}
+        \AxiomC{$ t_2 \in T $}
+        \AxiomC{$ t_3 \in T $}
+        \TrinaryInfC{$ if \; t_1 \; then \; t_2 \; else \; t_3 \in T$}
+    \end{prooftree}
+
 \end{definition}
 
+最初の$ true, \; false, \; 0 $の3つ規則は再帰的定義の1つめの条件と同じである。
+それ以外の4つの規則は再帰的定義の2つめと3つめの条件と同じである。
+それぞれの規則は「もし線の上に列挙して前提が成立するのならば、線の下の結論を導出できる」と読む。
+$ T $ がこれらの規則を満たす最小の集合である事実は明示的に述べられない。
+
+言語の構文は定義できたので、次は項がどう評価されるかの意味論について触れていく。
+意味論の形式化には操作的意味論や表示的意味論、公理的意味論やゲーム意味論などがあるが、ここでは操作的意味論について述べる。
+操作的意味論とは、言語の抽象機械を定義することにより言語の振舞いを規程する。
+この抽象機械が示す抽象とは、扱う命令がプロセッサの命令セットなどの具体的なものでないことを表している。
+単純な言語の抽象機械における状態は単なる項であり、機械の振舞いは遷移関数で定義される。
+この関数は各状態において項の単純化ステップを実行して次の状態を与えるか、機械を停止させる。
+ここで項 $ t $ の意味は、$ t $ を初期状態として動き始めた機械が達する最終状態である。
+
+なお、一つの言語に複数の操作的意味論を与えることもある。
+例えば、プログラマが扱う項に似た機械状態を持つ意味論の他に、コンパイラの内部表現やインタプリタが扱う意味論を定義する。
+これらの振舞いが同じプログラムを実行した時に何かしらの意味であれば、結果としてその言語の実装の正しさを証明することに繋がる。
+
+まずはブール式のみの操作的意味論を定義する。
+
+\begin{definition}
+
+    構文
+
+    \begin{align*}
+        t ::=                             && \text{項}     \\
+        true                              && \text{定数真} \\
+        false                             && \text{定数偽} \\
+        if \; t \; then \; t \; else \; t && \text{条件式}
+    \end{align*}
+\end{definition}
+
+\begin{definition}
+    値
+
+    \begin{align*}
+        v ::=                             && \text{値} \\
+        true                              && \text{真} \\
+        false                             && \text{偽}
+    \end{align*}
+\end{definition}
+
+\begin{definition}
+    評価
+
+    \begin{align*}
+        if \; true  \; then \; t_2 \; else t_3 \rightarrow t_2 && \text{(E-IFTRUE)}  \\
+        if \; false \; then \; t_2 \; else t_3 \rightarrow t_3 && \text{(E-IFFALSE)} \\
+        \AxiomC{$ t_1 \rightarrow t_1'$}
+        \UnaryInfC{$ if \; t_1 \; then \; t_2 \; else \; t_3 \rightarrow if \; t_1' \; then t_2 \; else \;t_3 $}
+        \DisplayProof
+        && \text{(E-IF)}
+    \end{align*}
+\end{definition}
+
+