--- a/paper/type.tex	Sat Jan 28 11:28:38 2017 +0900
+++ b/paper/type.tex	Sat Jan 28 12:10:35 2017 +0900
@@ -66,6 +66,7 @@
 
 % }}}
 
+% {{{ 型無し算術式
 \section{型無し算術式}
 まず、型システムやその性質について述べるためにプログラミング言語そのものの基本的な性質について述べる。
 プログラムの構文と意味論、推論について考えるために整数とブール値のみで構成される小さな言語を扱いながら考察する。
@@ -181,7 +182,7 @@
 \begin{definition}
     ブール値(B)
 
-    構文
+    項
     \begin{align*}
         t ::=                             && \text{項}     \\
         true                              && \text{定数真} \\
@@ -274,15 +275,93 @@
 しかし、他の言語における値は一般的に正規形ではない。
 実のところ、値でない正規形は実行時エラーとなって表れる。
 
-実際にこの言語に整数を導入して値では無い正規形を確認していく。
+実際にこの言語に整数を導入し、値では無い正規形を確認していく。
 
 
+\begin{definition}
+    算術式BN (B の拡張) の項
+    \begin{align*}
+        t ::=                             && \text{項}     \\
+        true                              && \text{定数真} \\
+        false                             && \text{定数偽} \\
+        if \; t \; then \; t \; else \; t && \text{条件式} \\
+        0                                 && \text{定数ゼロ} \\
+        succ \; t                         && \text{後者値} \\
+        pred \; t                         && \text{前者値} \\
+        iszero \; t                       && \text{ゼロ判定}
+    \end{align*}
+\end{definition}
+
+\begin{definition}
+    算術式BN  の値
+    \begin{align*}
+        v ::= && \text{値} \\
+        true  && \text{真} \\
+        false && \text{偽} \\
+        nv    && \text{数値} \\
+    \end{align*}
+\end{definition}
+
+\begin{definition}
+    算術式BNの数値
+    \begin{align*}
+        nv ::=  && \text{数値} \\
+        0       && \text{ゼロ} \\
+        succ nv && \text{後者値}
+    \end{align*}
+\end{definition}
+
+\begin{definition}
+    算術式BNの評価($ t \rightarrow t' $)
+    \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)} \\
+        \AxiomC{$ pred \; 0 \rightarrow 0$}
+        \DisplayProof && \text{(E-PREDZERO)} \\
+        \AxiomC{$ pred \; (succ \; nv_1) \rightarrow nv_1$}
+        \DisplayProof && \text{(E-PREDSUCC)} \\
+        \AxiomC{$ t_1 \rightarrow t_1'$}
+        \UnaryInfC{$ pred \; t_1 \rightarrow pred \; t_1'$}
+        \DisplayProof && \text{(E-PRED)} \\
+        \AxiomC{$ iszero \; 0 \rightarrow true$}
+        \DisplayProof && \text{(E-ISZEROZERO)} \\
+        \AxiomC{$ iszero \; (succ \; nv_1) \rightarrow false$}
+        \DisplayProof && \text{(E-ISZEROSUCC)} \\
+        \AxiomC{$ t_1 \rightarrow t_1'$}
+        \UnaryInfC{$ iszero \; t_1 \rightarrow iszero \; t_1'$}
+        \DisplayProof && \text{(E-ISZERO)} \\
+    \end{align*}
+\end{definition}
+
+今回値の定義に数値を表す構文要素が追加されている。
+数は0かある数に後者関数を適用したもののどちらかである。
+評価規則 E-PREDZERO、E-PREDSUCC、E-ISZEROZERO、E-ISZEROSUCC は演算 \verb/pred/ と \verb/iszero/ が数に適用された時にどう振る舞うかを定義している。
+E-SUCC 、 E-PRED 、 E-ISZERO の合同規則も E-IF のように部分項から先に評価することを示している。
+
+数値の構文要素(nv)はこの定義によって重要な役割をはたす。
+例えば、 E-PREDSUCC 規則が適用できる項は任意の項 $ t $ ではなく数値 $nv_1$である。
+これは $ pred \; (succ \; (pred \; 0)) $ を $ pred 0 $ に評価できないことを意味する。
+なぜなら $ pred \; 0 $ は数値に含まれないからである。
+
+ここで言語の操作的意味論について考える時、すべての項に関する振舞いを定義する必要がある。
+すべての項には $ pred \; 0 $ や $ succ false $ のような項も含まれる。
+しかし、 $ succ $ を $ false $ に適用する評価結果は定義されていないため、 $ succ \; false $ は正規形である。
+このような、正規形であるが値でない項は行き詰まり状態であるという。
+つまり、実行時エラーとは行き詰まり状態の項を指す。
+直感的な解釈としてはプログラムが無意味な状態になったこと示しておい、操作的意味論が次に何も行なえないことを特徴付けているのである。
+プログラング言語において実行時エラーはセグメンテーションフォールトや不正な命令などいくつかのものが挙げられるが、型システムを考える際にはこれらのエラーは行き詰まり状態という単一の概念で表す。
+
+% }}}
 
 % {{{ 型なしラムダ計算
 \section{型なしラムダ計算}
-まず、プログラミング言語における計算を形式的に定義する。
+計算とは何か、エラーとは何か、を算術式を定義することによって示してきた。
+ここで、プログラミング言語における計算を形式的に定義していく。
 プログラミング言語は複雑だが、その計算はある本質的な仕組みからの派生形式として定式化可能であることを Peter Ladin が示した。 % TODO: ref TaPL 61
-この時 Landin が使った本質的な仕組みとしての核計算がラムダ計算だった。
+この時 Landin が使った本質的な仕組みとしての核計算がラムダ計算であった。
 ラムダ計算は Alonzo Church が発明した形式的体系の一つである。 % TODO: ref
 ラムダ計算では全ての計算が関数定義と関数適用の基本的な演算に帰着される。
 ラムダ計算はプログラミング言語の機能の仕様記述や、言語設計と実装、型システムの研究に多く使われている。