ラムダ計算の表記

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

$ \lambda x. e

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の項の方が少ない

当たり前だがmrsekut.icon

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

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

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

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

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

抽象化

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

code:hs

inc = \x -> x + 1

code:js

const inc = x => x + 1

作用

$ \mathrm{inc}(2)

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

code:hs

inc 2

(\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をβ簡約してみよう

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

https://gyazo.com/a05bb09cd23de4329e08f947f7ad72e5