ラムダ計算の練習

今日は型システム入門第5章のラムダ計算でのプログラミングを読んでいます。
その読書メモです。

ラムダ式の項の種類

• x (変数)
• λx. t (ラムダ抽象)
• t t (関数適用)

変数のスコープ
f = λx. x (λx. x)

上記ラムダ式の赤文字のxと青文字のxは別物。
fにaを適用すると、f a = (λx. x (λx. x)) a = a (λx. x)となる。

β簡約
(λx. u) vのような形の項があったとき、uの中に出現するすべてのxをvで置き換える操作のこと。
この式をβ簡約すると、(λx. u) v → u[x := v]となる。（ラムダ式uに出現するxをvに置き換えてる）
上式のuがu=x y zだった場合、上記操作を行うと、(λx. x y z) v → v y zのようになる。

ラムダ抽象に対して関数適用を行った場合、こんな感じで簡略化できますよーということかな？
ラムダ式を使ってて無意識に行っていたことをちゃんと文章にしたらこうなるんですね。

カリー化
ラムダ式のラムダ抽象は、複数の引数を取ることができない。
複数引数を取る関数を使いたい場合は、高階関数を使って同じような関数を作ることができる。
複数の引数を取る関数を高階関数に変換することをカリー化という。

x,yの2つの変数を取る関数f(x, y) = x+yを考える。
ラムダ式では、
f = λx. λy. x+yという風に書く。

f に2と3を適用してみると、

f 2 3
= (λx. λy. x+y) 2 3
= (λy. 2+y) 3
= 2+3

となる。

(λx. λy. x) 2 3 → (λy. 2+y) 3が、λx. λy. x+y → (λy. x+y) [x := 2]のβ簡約。
(λy. 2+y) 3 → 2+3が、(λy. x+y) [x := 2] → (x+y) [x := 2][y := 3]のβ簡約。

複数引数を取る関数と同等の働きをしていることがわかった。

とりあえずここまでです。
次は明日あたりに読みます。