# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1485504633 -32400
# Node ID 63bbbf54d54167f97403c1b0d50ad6e6374b4b9a
# Parent  9dc9c50a28bdda994e8709335a109eb1ed7995ef
Writing lambda ...

diff -r 9dc9c50a28bd -r 63bbbf54d541 paper/type.tex
--- a/paper/type.tex	Thu Jan 26 17:16:18 2017 +0900
+++ b/paper/type.tex	Fri Jan 27 17:10:33 2017 +0900
@@ -66,6 +66,7 @@
 
 % }}}
 
+% {{{ 型なしラムダ計算
 \section{型なしラムダ計算}
 まず、プログラミング言語における計算を形式的に定義する。
 プログラミング言語は複雑だが、その計算はある本質的な仕組みからの派生形式として定式化可能であることを Peter Ladin が示した。 % TODO: ref TaPL 61
@@ -149,6 +150,96 @@
 名前呼びなどの非正格な戦略は引数が使われる時のみ評価され、これは遅延評価とも呼ばれる。
 
 ラムダ計算において、複数の引数は、関数を返り値として返す高階関数として定義できる。
+項 $ s $ が二つの自由変数 $ x $ と $ y $ を含むとすれば、 $ \lambda x . \lambda y . s $ と書くことで二つの引数を持つ関数を表現できる。
+これは $ x $ に $ v $ が与えられた時、$ y $ を受けとり、 $ s $ の抽象内の自由な $ x $ を $ v $ に置き換えた部分を置換する関数、を返す。
+例えば $ (\lambda x . \lambda y . s) \; v \; w $ は $ (\lambda y . [x \mapsto v] s) w $ に簡約され、 $ [y \mapsto w][x \mapsto v]s $ に簡約される。
+なお、複数の引数を取る関数を高階関数に変換することはカリー化と呼ばれる。
+
+代入の操作は直感的には置換であるが、変数の束縛に注意しなくてはならない。
+例えば抽象への代入を以下のように定義する。
+
+\begin{equation*}
+    [ x \mapsto s ] (\lambda y . t_1) = \lambda y . [ x \mapsto s] t_1
+\end{equation*}
+
+この場合、束縛変数の名前によっては定義が破綻してしまう。例えば以下のようになる。
+
+\begin{equation*}
+    [x \mapsto y](\lambda x . x) = \lambda x . y
+\end{equation*}
+
+$ \lambda $ よって束縛されているはずの $ x $ が書き変わっている。
+これはスコープとして振る舞っていないので誤っている。
+この問題は項 $ t $ 内の変数 $ x $ の自由な出現と束縛された出現を区別しなかったために出現した誤りである。
+
+そこで、$ x $ を束縛する項に対しては置換行なわないように定義を変える。
+
+\begin{itemize}
+    \item $ y = x $ の場合
+        \begin{equation*}
+            [ x \mapsto s ] (\lambda y . t_1) = \lambda y . t_1
+        \end{equation*}
+
+    \item $ y \neq x $ の場合
+        \begin{equation*}
+            [ x \mapsto s ] (\lambda y . t_1) = \lambda y . [ x \mapsto s] t_1
+        \end{equation*}
+\end{itemize}
+
+この場合は束縛された変数を上書きしないが、逆に自由変数を束縛するケースが発生する。
+具体的には以下である。
+
+\begin{equation*}
+    [ x \mapsto z] (\lambda z . x) = \lambda z . z
+\end{equation*}
+
+項 $ s $ 中の自由変数が項 $ t $ に代入されて束縛される現象は変数捕獲と呼ばれる。
+これを避けるためには $ t $ の束縛変数の名前が $ s $ の自由変数の名前と異なることを保証する必要がある。
+変数捕獲を回避した代入操作は捕獲回避代入と呼ばれる。
+
+捕獲回避の条件を追加した代入の定義は以下のような定義となる。
+
+\begin{itemize}
+    \item 変数への代入
+
+        \begin{equation*}
+            [ x \mapsto s ] x = s
+        \end{equation*}
+
+    \item 存在しない変数への代入($ y \neq x $ の時)
+
+        \begin{equation*}
+            [ x \mapsto s ] y = y
+        \end{equation*}
+
+    \item 抽象内の項への代入($ y = x $ の場合)
+
+        \begin{equation*}
+            [ x \mapsto s ] (\lambda y . t_1) = \lambda y . t_1
+        \end{equation*}
+
+    \item 抽象内の項への代入($ y \neq x $ かつ $ y $ が $ s $ の自由変数でない)
+
+        \begin{equation*}
+            [ x \mapsto s ] (\lambda y . t_1) = \lambda y . [ x \mapsto s] t_1
+        \end{equation*}
+
+    \item 適用への代入
+
+        \begin{equation*}
+            [x \mapsto s] (t_1 \; t_2) = (t_1[x\mapsto s])([x \mapsto s] t_2)
+        \end{equation*}
+
+\end{itemize}
+
+この定義は少なくとも代入が行なわれる際には正しく代入が行なえる。
+
+また、項の束縛変数の名前を一貫して変更することにより正しく代入を行なう方法もあり、名前の変更をアルファ変換と呼ぶ。
+さらし、抽象が束縛している変数を名前では無く数字として扱う名無しで束縛変数を扱う方法もあり、この数字で束縛変数を扱う表現を De Brujin 表現と呼ぶ。 % TODO: ref and spell check
+
+形無しラムダ計算 $ \lambda $ の項の定義と評価の要約を示す。
+
+% }}}
 
 \section{単純型付きラムダ計算}
 \section{部分型付け}