# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1485595755 -32400
# Node ID d14c3fa5f3eafb713ec07f7f6d88a9c75c8ca157
# Parent  9110813f4f6811d032c52e88a1eb5bec58004a1c
Wrote simple-type

diff -r 9110813f4f68 -r d14c3fa5f3ea paper/atton-master.tex
--- a/paper/atton-master.tex	Sat Jan 28 17:10:51 2017 +0900
+++ b/paper/atton-master.tex	Sat Jan 28 18:29:15 2017 +0900
@@ -75,7 +75,8 @@
 }
 \def\lstlistingname{リスト}
 \def\lstlistlistingname{リスト目次}
-\newtheorem{defi}{定義}[section]
+\newtheorem{theorem}{定理}[section]
+\newtheorem{lemma}{補題}[section]
 
 
 %%% 索引のために以下の2行を追加
diff -r 9110813f4f68 -r d14c3fa5f3ea paper/type.tex
--- a/paper/type.tex	Sat Jan 28 17:10:51 2017 +0900
+++ b/paper/type.tex	Sat Jan 28 18:29:15 2017 +0900
@@ -356,6 +356,8 @@
 
 % }}}
 
+% {{{ 単純型
+
 \section{単純型}
 先程定義した算術式には $ pred \; false $ のようなこれ以上評価できない行き詰まり状態が存在する。
 項を実際に評価する前に評価が行き詰まり状態にならないことを保証したい。
@@ -416,6 +418,26 @@
 項$ t $ に対してある型 $ T $ が存在して $ t : T $ である時、 $ t $ は型付け可能である(または正しく型付けされている)という。
 \end{definition}
 
+型推論をを行なう時、$succ t_1$という項が何らかの型を持つならばそれは Nat 型である、といった言及を行なう。
+型付け関係を逆転させた補題を定義することで型推論の基本的なアルゴリズムを考えることができる。
+なお、逆転補題は型付け関係の定義により直ちに成り立つ。
+
+\begin{lemma}
+    型付け関係の逆転
+    \begin{enumerate}
+        \item $ true : R $ ならば $ R = Bool $ である
+        \item $ false : R $ ならば $ R = Bool $ である
+        \item $ if \; t_1 \; then \; t_2 \; else \; t_3 : R $ ならば $ t_1 : Bool $ かつ $ t_2 : R $ かつ $ t_3 : R $ である。
+        \item $ 0 : R $ ならば $ R = Nat $ である
+        \item $ succ \; t_1 : R $ ならば $ R = Nat $ かつ $ t_1 : Nat $ である
+        \item $ pred \; t_1 : R $ ならば $ R = Nat $ かつ $ t_1 : Nat $ である
+        \item $ iszero \; t_1 : R $ ならば $ R = Bool $ かつ $ t_1 : Nat $ である
+    \end{enumerate}
+\end{lemma}
+
+逆転補題は型付け関係のための生成補題と呼ばれることもある。
+なぜならば、与えられた型付け判断式に対してその証明がどのように生成されたかを示すからである。
+
 型無し算術式の評価導出のように型付けも導出可能であり、それも規則のインスタンスの木である。
 型付け関係に含まれる二つ組 $(t, \; T)$は $ t : T $ を結論とする型付け導出により正当化される。
 例えば $ if \; (iszero \; 0) \; then \; 0 \; else \; (pred \; 0) : Nat $ の型付け判断の導出木である。
@@ -438,11 +460,98 @@
     \TrinaryInfC{ if \; (iszero \; 0) \; then \; 0 \; else \; (pred \; 0) : Nat }
 \end{prooftree}
 
-% TODO: 進行と保存
+項その型付けの定義より、型システムが行き詰まり状態にならないことを示す。
+その証明は指向定理と保存定理によって証明する。
+
+\begin{itemize}
+    \item 進行とは、正しく型付けされた項は行き詰まり状態では無いことである
+    \item 保存とは、評価可能な正しく型付けされた項は評価後も正しく型付けされていることである。
+\end{itemize}
+
+型システムがこれらの性質を持つ時、正しく型付けされた項は行き詰まり状態になりえない。
+
+進行定理の証明の為に Bool 型と Nat 型の標準形(それらの型を持つ正しく型付けされた値)を示す。
+
+\begin{lemma}
+    標準形
+
+    \begin{enumerate}
+        \item $ v $ が $Bool$ 型の値ならば $v$ は $true$ または $false$ である。
+        \item $v$ が $Nat$ 型の値ならば、$0$ もしくは $Nat$ に対して $succ$ を適用した値である。
+    \end{enumerate}
+\end{lemma}
+
+標準形の証明に関しては値における構造的帰納法を用いる。
+この言語における値とは $ true $ と $false $ と $ 0$ と $ succ \; nv$ のいずれかの形をしている。
+Bool型に関して注目した時、 $ true $ と $ false $ は定義によって正しい。
+$ 0 $ と $ succ \; nv $ に関しては逆転補題より Nat 型を持つため、Bool型を持つ値は $ true $ と $ false $ のどちらかとなる。
+Nat についても同様である。
+
+\begin{theorem}
+進行
+
+$ t$ が正しく型付けされたと仮定すると、$ t$ は値であるか、またはある $t'$ が存在して$ t \rightarrow t' $ となる。
+\end{theorem}
+
+証明は $ t : T $ の導出に関する帰納法による。
+T-TRUE 、 T-FALSE 、 T-ZERO の場合は$t$が値であることより成立する。
+
+T-IF の場合、帰納法の仮定により $ t1 $ は値であるか、$t_1'$ が存在して $ t_1 \rightarrow t_1'$ を満たす。
+$ t_1 $ が値ならば、標準形補題により $ true $ か $ false $ であり、その場合は E-IFTRUE か E-IFFALSE が適用可能である。
+一方 $ t_1 \rightarrow t_1' $ ならば E-IF が適用できる。
+
+T-SUCC の場合も帰納法の仮定により $ t1 $ は値であるか、$t_1'$ が存在して $ t_1 \rightarrow t_1'$ を満たす。
+$ t_1 $ が値ならば標準形補題により数値でなければならず、その場合 $ t $ も数値であるため成り立つ。
+一方 $ t_1 \rightarrow t_1' $ ならば E-SUCC が適用できる。
+
+T-SUCC の場合も同様で、 $ t_1 $ が値ならば標準形補題により数値でなければならず、その場合 E-PREDZERO か E-PREDSUCC が使える。
+$ t_1 \rightarrow t_1' $ ならば E-PRED が適用できる。
+
+T-ISZERO の場合も値ならば標準形補題により $ t_1 $ は数値であり、どちらの場合でも E-ISZEROZERO と E-ISZEROSUCC が適用できる。
+$ t_1 \rightarrow t_1' $ ならば E-ISZERO が適用できる。
+
+\begin{theorem}
+保存
+
+$ t : T $ かつ $ t \rightarrow t' $ ならば $ t' : T $ となる。
+\end{theorem}
+
+保存定理も $ t : T $ の導出に関する帰納法によって導ける。
+帰納法の各ステップにおいて全ての部分導出に関して所望の性質が成り立つと仮定し、導出の最後の規則についての場合分けで証明を行なう。
+
+導入の最後の規則がT-TRUE の場合、その規則の形から $ t $ は定数 $ true $ でなければならず、 $ T $ は $ Bool$ となる。
+そして $ t $ は値であるためにどのような $ t' $ も存在せず、定理の要求は満たされる。
+T-FALSE と T-ZERO の場合も同様である。
+
+導入の最後の規則 T-IF の場合は、$ t $ はある $ t_1, \; t_2 \; t_3 $ に対して $ if \; t_1 then t_2 else t_3 $ という形となる。
+さらに $ t_1 : Bool $ と $ t_2 : T $ と $ t_3 : T $ となる部分導出がある。
+ここで if を持つ評価規則において  $ t \rightarrow t'$ を導入できる規則は E-IFTRUE と E-IFFALSE と E-IF のみである。
+それぞれの場合について別々に場合分けをして考える。
+
+\begin{itemize}
+    \item E-IFTRUE の場合(E-IFFALSE も同様)
+
+        $ t \rightarrow t' $ が E-IFTRUE を使った導出ならば、 $ t_1$ は $ true $ であり、結果の項 $ t' $ は $ t_2 $ となる。
+        このことより $ t_2 : T $ であることが分かるため、条件を満たす。
+
+    \item E-IF の場合
+
+        場合分け T-IF の仮定より $ t_1 : Bool $が結論となる、部分導出が得られる。
+        帰納法の仮定を部分導出に適用して $ t_1' : Bool $ とし、 $ t_2 : T $ と  $ t_3 : T $ を合わせると規則 T-IF が適用できる。
+        T-IF を適用すると  $ if \; t_1' \; then \; t_2 \; else \; t_3$となり、$ t' : T $ が成り立つ。
+\end{itemize}
+
+T-SUCC が導入の最後であれば、 $ t \rightarrow t'$ を導くためには E-SUCC のみであり、この形から $ t_1 \rightarrow t_1'$が分かる。
+$ t_1 : Nat $ であることも分かるため、帰納法の仮定より $ t_1' : Nat $ が得られる。
+この時 T-SUCC が適用できるため $ succ \; t_1 : Nat$となって $ t' : T $ が成り立つ。
+T-PRED も同様である。
+
+% }}}
 
 % {{{ 型なしラムダ計算
 \section{型なしラムダ計算}
 計算とは何か、エラーとは何か、を算術式を定義することによって示してきた。
+また、型を導入することにより行き詰まり状態を回避することも示した。
 ここで、プログラミング言語における計算を形式的に定義していく。
 プログラミング言語は複雑だが、その計算はある本質的な仕組みからの派生形式として定式化可能であることを Peter Ladin が示した。 % TODO: ref TaPL 61
 この時 Landin が使った本質的な仕組みとしての核計算がラムダ計算であった。