--- a/paper/type.tex	Thu Jan 26 11:03:51 2017 +0900
+++ b/paper/type.tex	Thu Jan 26 17:16:18 2017 +0900
@@ -27,27 +27,27 @@
         他にも、ある種のプログラムにとっては型は保守のためのツールともなる。
         複雑なデータ構造を変更する時、その構造に関連するソースコードを型検査器は明らかにしてくれる。
 
-    \itemize 抽象化
+    \item 抽象化
 
         型は大規模プログラムの抽象化の単位にもなる。
         例えば特定のデータ構造に対する処理をモジュール化し、パッケージングすることができる。
         モジュール化されたデータ構造は厳格に定義されたインターフェースを経由して呼び出すことになる。
         このインターフェースは利用する側に取っては呼び出しの規約となり、実装する側にとってはモジュールの要約となる。
 
-    \itemize ドキュメント化
+    \item ドキュメント化
 
         型はプログラムを理解する際にも有用である。
         関数やモジュールの型を確認することにより、どのデータを対象としているのかといった情報が手に入る。
         また、型はコンパイラが実行されるために検査されるため、コメントに埋め込まれた情報と異なり常に正しい情報を提供する。
 
-    \itemize 言語の安全性
+    \item 言語の安全性
 
         安全性のの定義は言語によって異なるが、型はデータの抽象化によってある種の安全性を確保できる。
         例えば、プログラマは配列をソートする関数があった場合、与えられた配列のみがソートされ、他のデータには影響が無いことを期待するだろう。
         しかし、低水準言語ではメモリを直接扱えるため、予想された処理の範囲を越えてデータを破壊する可能性がある。
         より安全な言語ではメモリアクセスが抽象化し、データを破壊する可能性をプログラマに提供しないという選択肢がある。
 
-    \itemize 効率性
+    \item 効率性
 
         そもそも、科学計算機における最初の型システムは Fortran などにおける式の区別であった。% TODO ref fortran
         整数の算術式と実数の算術式を区別し、数値計算の効率化を測るために導入されたのである。
@@ -67,7 +67,88 @@
 % }}}
 
 \section{型なしラムダ計算}
+まず、プログラミング言語における計算を形式的に定義する。
+プログラミング言語は複雑だが、その計算はある本質的な仕組みからの派生形式として定式化可能であることを Peter Ladin が示した。 % TODO: ref TaPL 61
+この時 Landin が使った本質的な仕組みとしての核計算がラムダ計算だった。
+ラムダ計算は Alonzo Church が発明した形式的体系の一つである。 % TODO: ref
+ラムダ計算では全ての計算が関数定義と関数適用の基本的な演算に帰着される。
+ラムダ計算はプログラミング言語の機能の仕様記述や、言語設計と実装、型システムの研究に多く使われている。
+この計算体系の重要な点は、ラムダ計算内部で計算が記述できるプログラミング言語であると同時に、それ自身について厳格な証明が可能な数学的対象としてみなせる点にある。
 
+ラムダ計算はいろいろな方法で拡張できる。
+数や組やレコードなどはラムダ計算そのもので模倣することができるが、記述が冗長になってしまう。
+それらの機能のための具体的な特殊構文を加えることは言語の利用者の視点で便利である。
+他にも書き換え可能な参照セルや非局所的な例外といった複雑な機能を表現することもできるが、膨大な変換を用いなければモデル化できない。
+それらを言語として備えた拡張に ML や Haskell といったものがある。 % TODO: ref
+
+ラムダ計算(または $ \lambda $ 計算) とは、関数定義と関数適用を純粋な形で表現する。
+ラムダ計算においてはすべてが関数である。
+関数によって受け付ける引数も関数であり、関数が返す結果もまた関数である。
+
+ラムダ計算の項は変数と抽象と適用の3種類の項からなり、以下の文法に要約される。
+変数 $ x $ は項であり、項 $ t_1 $ から変数 $ x $ を抽象化した $ \lambda x . t_1 $ も項であり、項 $ t_1 $ を他の項 $ t_2 $ に適用した $ t_1 t_2 $ も項である。
+
+\begin{multline*}
+    t ::= \\
+        x \\
+        \lambda x . t \\
+        t \, t  \\
+\end{multline*}
+
+ラムダ計算において関数適用は左結合とする。
+つまり、 $ s \, t \, u $ は $ (s \, t) \, u $ となる。
+
+また、抽象の本体はできる限り右側へと拡大する。
+例えば $ \lambda x . \;  \lambda y . \; x \, y \, x $ は $ \lambda x . (\lambda . y ((x \, y) \, x)) $ となる。
+
+ラムダ計算には変数のスコープが存在する。
+抽象 $ \lambda x . t $ の本体 $ t $ の中に変数 $ x $ がある時、 $ x $ の出現は束縛されていると言う。
+同様に、 $ \lambda x $ は $ t $ をスコープとする束縛子であると言う。
+なお、 $ x $ を囲む抽象によって束縛されていない場所の $ x $ の出現は自由であると言う。
+例えば $ x \; y $ や $ \lambda y . \; x \; y $  における $ x $ の出現は自由だが、 $ \lambda x . x $ や $ \lambda z . \lambda x . \lambda y . x (y \; z) $ における $ x $ の出現は束縛されている。
+$ (\lambda x . x) \;x $ においては、最初の $ x $ の出現は束縛されているが、2つ目の出現は自由である。
+
+ラムダ計算において、計算とは引数に対する関数の適用である。
+抽象に対して項を適用した場合、抽象の本体に存在する束縛変数に適用する項を代入したもので書き換える。
+図式的には
+
+\begin{equation*}
+    (\lambda x . t_{12}) t_2 \rightarrow [ x \mapsto t_2] t_{12}
+\end{equation*}
+
+と記述する。
+ここで $ [ x \mapsto t_2] t_{12} $ とは、$ t_12 $ 中の自由な $ x $ を全て $ t_2 $ で置換した項を意味する。
+例えば、 $ (\lambda x . x) \; y $ は $ y $ となり、項 $ (\lambda x . x (\lambda x . x)) (y \; z) $ は $ y \; z \; (\lambda x . x) $ となる。
+
+なお、 $ (\lambda x . t_{12}) t_2 $ という形の項を簡約基(redex, reducible expression) と呼び、上記の規則で簡約基を置換する操作をベータ簡約と呼ぶ。
+ラムダ計算のための評価戦略には数種類の戦略がある。
+
+\begin{itemize}
+    \item 完全ベータ簡約
+
+        任意の簡約基がいつでも簡約されうる。
+        つまり項の中からどの順番で簡約しても良い。
+
+    \item 正規順序簡約
+
+        最も左で最も外側の簡約基が最初に簡約される。
+
+    \item 名前呼び
+
+        正規順序の中でも抽象の内部での簡約を許さない。
+        名前呼びの変種は Algol-60 や Haskell で利用されている。
+        なお、Haskell においては必要呼びという最適化された変種を利用している。
+
+    \item 値呼び
+
+        ほとんどの言語はこの戦略を用いている。
+        基本的には最も左の簡約基をを簡約するが、右側が既に値(計算が終了してもう簡約できない閉じた項)になっている簡約基のみを簡約する。
+\end{itemize}
+
+値呼び戦略は関数の引数が本体で使われるかに関わらず評価され、これは正格と呼ばれる。
+名前呼びなどの非正格な戦略は引数が使われる時のみ評価され、これは遅延評価とも呼ばれる。
+
+ラムダ計算において、複数の引数は、関数を返り値として返す高階関数として定義できる。
 
 \section{単純型付きラムダ計算}
 \section{部分型付け}