λ計算

　Ocamlと直接関わるトピックではないが、講義中にまとめたメモ。
　ぶっちゃけ理解してないけど書くこと無いので。

λ式構文

　e(λ式)::＝ x（変数）
　　　　　　| λx,e （λ抽象）
　　　　　　| e1 e2 （関数適用）
　λx,eはOcamlの　fun x -> e　と同様。　xを引数にe型の値を返すの意
　
　ex)表記の書き換え例
　　 let x = e1 in e2 は (λx,e2)e1　と等価

β簡約

　small-step操作的意味論を導入して構文を解析するらしい
　（詳細はhtmlだと書きづらいので省略）
　要は(λx.e1)e2が[e2/x]e1に簡約されるということらしい。
　ex)具体例
　　(λx,x)y →　y
　　(λx.λy.x)z　→　λy.z
　　(λx.x)(λy.y)　→　λy.y
　
　早い話が引数を省略する表記
　

部分式のβ簡約

　 (λa.b)cd　→　bd　（導出略）
　つまりは、e1e2という関数適用に対して、e2（引数）を簡約する規則の導入。

自由変数、束縛変数、α変換

　(λx.λy.xy)y　→　λy'.yy'　というような簡約について。
　　一つめ、２つめのyと３つめのyが別々の変数であることに注意。
　　(λx.λy.xy)yにおいて、１つめ、２つめのyは仮引数。ゆえに名前は変わってもOK（便宜上ｙにしているにすぎない。）
　そこで (λx.λy'.xy')y　と書き換えれば最初の簡約がなされる理由がわかる。
　
　λ抽象の仮引数を束縛変数と呼ぶ。（対義語は自由変数）
　　→　(λx.λy'.xy')yにおいて、y'はλy'で束縛されている
　　→　(λx.λy'.xy')yにおいて、yは自由
　
　Ocamlのコードに置き換えると

#let y = (fun a -> fun b -> a) ;;
　val y : 'a -> 'b -> 'a =
#let z = (fun a -> fun b -> b) ;;
　val z : 'a -> 'b -> 'b =
(λx.y)
#let e1 = (fun x -> y);;
　val e1 : 'a -> 'b -> 'c -> 'b =
(λx.z)
#let e2 = (fun x -> z);;
　val e2 : 'a -> 'b -> 'c ->'c =
出力
#e1 "a" "b" "c";;
- : string = "b"
#e2 "a" "b" "c";;
- : string ="c"

　
この場合、、
yは引数２つを受け取って１つめを出力、zは引数２つを受け取って２つめを出力する関数。
e1は引数を受け取りyを出力、e2は引数を受け取りzを出力する関数。
すなわち、e1はyの引数も合わせ3つの引数を受け取り、２つめ（yにとっての１つめ）を出力、
e2はzの引数も合わせ３つの引数を受け取り、３つめ（zにとっての２つめ）を出力する。
という手順を実現している。
　
　この手順では、e1,e2の２つめ、３つめの引数が束縛されていることになる。
　
もっとわかりやすい例を用いれば、
　f(x)＝x+1
g(y)＝y+1
のxとyは束縛変数であるから、fとgは等価であり、べつにxの代わりにa　yの代わりにbを用いても良い。
　
こういうのをα変換と呼び、関数やプログラムの等価性を調べるのに用いられる。
ex)　変数名だけ変えたコピーはα変換すればまるわかり。（変数名以外等価だから）
　
　代入[e2/x]e1を行う場合は、e1の束縛変数がe2の自由変数と衝突しないよう、e1をα変換する。

今後のタスク（試験に向けて）

• 任意の手順についてλ計算式をたてられるようになる
• 任意の関数適用についてβ簡約ができるようになる
• 任意の関数についてα変換ができるようになる。