ラムダ計算の表記

型については、型付け導出の表記を参照

x が引数で e を返す

複数の引数

ラムダ計算では、複数の引数を組み込みでサポートしていない

f=\lambda(x,y).sはf=\lambda x.\lambda y.sと書く

カリー化を用いて、一引数関数だけで表せる

\lambda x_1.(\lambda x_2.(\lambda x_3.M))は\lambda x_1x_2x_3.Mと書ける

略記したときに λ<ここ1>.<ここ2> なったら、

ここ1 より ここ2 の項の方が少ない

当たり前だが

ここ2 の方が多い場合はまだ簡約できる状態である

例えば λxy.x は λx.(λy.(x)) なので、これ以上簡約できない

一つの引数を与えられることで簡約できる

これは文字数が増えても同じ

λxyz.(xz)(yz) は ここ1 は3つで、 ここ2 は2つなので、これ以上監訳できない

抽象化

\mathrm{inc}=\lambda x. x+1

作用

\mathrm{inc}(2)

(\lambda x. x+1)(2)

関数適用は左結合

s t u は (s t) u

抽象の本体は右結合

λx. λy. x y x は λx. (λy. ((x y) x)) と同じ

β簡約の書き方

(\lambda x.t_{12})t_2のことを

[x\mapsto t_2]t_{12}と書く

例えば恒等関数に値を適用すれば(\lambda x.x)yはyとなる

略記の例題

(\lambda xy.s)vwをβ簡約してみよう

引数を提要する順番がしょっちゅうわからんくなる