λ計算
α-變換
β-簡約 (β-變換)
η-變換
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