ラムダ項

ラムダ項 2012/08/05(Sun.)
f : x → y
という形の関数を
λx.y
と書くことにする．これをラムダ式という．
ラムダ式を厳密に定義すると
-- 変数はラムダ式である．
-- xが変数で Mがラムダ式ならば、λx.M はラムダ式
-- M,N がラムダ式ならば、M N はラムダ式
と再帰的に定義する．

2つ目のルールは関数抽象で、3つ目は関数適用だ．

関数適用は左結合で、関数抽象は右結合．
結合の強さは関数抽象よりも関数適用の方が強い．

例えば
λx.λy.M x y === λx.(λy.((M x) y))
である．

シンタックスシュガーとして、
λx.λy.λ..M
これを
λxy.. M
などと、変数をまとめて書くことがある．

コンビネータは結合子などと訳されるが幾つかのラムダ式のこと．
例えば
I = λx.x
K = λxy. x
F = λxy. y
S = λxyz. x z(y z)
B = λxyz. x(y z)
C = λxyz. x z y

構成子、選択子である cons, car, cdr は次のように、上のコンビネータを
含むラムダ式で実装できる．

cons = λxyz. z x y
car = λz. z K
cdr = λz. z F

正しく使えることは次で分かるだろう．
cons 1 2 = λz. z 1 2 = A (とおく)
car A = A K = K 1 2 = 1
cdr A = A F = F 1 2 = 2
consに2つの値を適用したそれはそのふたつの値を持ち続け、
carとcdrでそのどちらかを取り出せる．

先にあげたコンビネータは次のような関係を持つ．
SKK = I
S(KS)K = B
BI = S(KI)
SK = F = KI

Ω = ωω where ω = λx. x x
これは計算が停止しないものとして定番の式．

評価戦略の話をしてなかったけど、Ωの評価として
一つ目のωから順に評価するとして、（何評価戦略でも
そうするだろう）

Ω→ωω→(λx. x x)ω→ωω→・・・

では例えば
(λx. y) Ω
という式は、一つ目は引数に関わらずyを返す定数であるので
Ωの評価値に関わらず
(λx. y) Ω → y
と評価できるだろうが、これが無限ループせずに評価できるのは
一つ目(λx. y)を評価し、引数を一つ取るコトが分かるので
一つ引数としてΩがあるのを見て、この引数の値を評価する前に
関数適用の方を計算する場合である．
つまり、引数の評価と関数適用の順序が問題．

値呼び、名前呼び、必要呼び
コメ(0) | トラ(0)
intime o'
