λ計算
構文
變數記號 (identifier)$ a,b,\dotsは式である
λ抽象 (lambda abstraction)$ \lambda.變數記號.式は式である
函數適用 (application)$ 式~式は式である
括弧$ ()は適當に補ふ
束縛變數|自由變數 (free variable)
α-變換
β-簡約 (β-變換)
η-變換
encoding
Church encoding
$ 0:=\lambda f.\lambda x.x,$ 0~f~x=x
後者$ Sn:=\lambda n.\lambda f.\lambda x.f~(n~f~x),$ Sn~f~x=f~(n~f~x)
$ n:=\lambda f.\lambda x.f^n~x,$ n~f~x=f^n~x
Church booleans
眞$ \lambda x.\lambda y.x
僞$ \lambda x.\lambda y.y=0
Church pairs
cons$ \lambda x.\lambda y.\lambda z.z~x~y
car$ \lambda p.p~(\lambda x.\lambda y.x)
cdr$ \lambda p.p~(\lambda x.\lambda y.y)
either
left$ \lambda x.\lambda l.\lambda r.l~x
right$ \lambda x.\lambda l.\lambda r.r~x
list
right folded
空 list$ \rm false
cons$ \lambda h.\lambda t.\lambda c.\lambda n.c~h~(t~c~n)
car$ \lambda l.l~(\lambda h.\lambda t.h)~{\rm false}
cdr$ \lambda l.\lambda c.\lambda n.l~(\lambda h.\lambda t.\lambda g.g~h~(t~c))~(\lambda t.n)~(\lambda h.\lambda t.t)
isNil$ \lambda l.l~(\lambda h.\lambda t.{\rm false})~{\rm true}
Scott encoding
再歸を含まない data 型に於いては Church encoding と一致する
$ 0:=\lambda f.\lambda x.x
後者$ Sn:=\lambda n.\lambda f.\lambda x.n
list
left folded
空 list$ \rm false
cons$ \lambda x.\lambda y.\lambda z.z~x~y、car$ \lambda p.p~(\lambda x.\lambda y.x)、cdr$ \lambda p.p~(\lambda x.\lambda y.y) は Church pair と同じ
isNil$ \lambda l.l~(\lambda h.\lambda t.\lambda d.{\rm false})~{\rm true}
Boehm-Berarducci encoding
ε計算
? 確定記述子との關聯は