λ計算
lambda calculus
構文
變數記號 (identifier)$ a,b,\dotsは式である
λ抽象 (lambda abstraction)$ \lambda.變數記號.式は式である
函數適用 (application)$ 式~式は式である
代入$ 式[式/變數] は式である
$ 式[變數:=式] とも書く
括弧$ ()は適當に補ふ
束縛變數|自由變數 (free variable)
α-變換
式$ M に變數$ y が自由に表れてゐないし、式$ M で變數$ y が既に束縛されてゐる場所に變數$ x が登場してゐないならば、$ \lambda x.M=\lambda y.M[y/x]
これを公理ではなく、定義上等しい$ \lambda x.M\equiv\lambda y.M[y/x] とする事も多い
β-簡約 (β-變換)
$ (\lambda x.M)~N=M[N/x]
η-變換
公理として
式$ Mに變數$ xが自由に表れてゐない場合に$ \lambda x.M~x=M
推論規則として
外延性$ \frac{M~x=N~x}{M=N}({\rm ext})
體系
公理
$ \beta :$ (\lambda x.M)~N=M[N/x]
$ M=M
推論規則
$ \frac{M=N}{\lambda x.M=\lambda x.N}(\xi)
.
$ \frac{M=N}{M~L=N~L},$ \frac{M=N}{L~M=L~N}
.
$ \frac{L=M\quad M=N}{L=N}
.
$ \frac{M=N}{N=M}
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
λ-μ 計算
μ 演算子
ε計算
? 確定記述子との關聯は
ι演算子
量子λ計算