單純型附きλ計算
simply-typed lambda calculus$ \lambda\to
項
變數$ x,y,\dotsは項である
項$ tが項の變數$ xを自由變數として含む事を明示する場合は$ t(x)と書く
$ xが變數で$ tが項ならば$ \lambda x.tも項である (λ抽象)
$ t_1,t_2が項ならば$ t_1~t_2も項である (函數適用)
項$ t_1 が變數$ x を自由變數として含む$ t_1(x) として、變數$ x に項$ t_2 を代入したもの$ t_1[t_2/x] も項である (代入)
型
變數$ \alpha,\beta,\dotsは型である (型變數)
基底型 (ground type。basic type) は適當に備へる
$ A,Bが型ならば$ A\to Bも型である (函數型)
$ \toは右結合
ABS が導入規則であり、APP が除去規則である
證據
型附けの列$ x:A,y:B,\dots
$ \Gamma,\Delta,\dots等と書く
推論規則
變數$ \frac{x:T\in\Gamma}{\Gamma\vdash x:T}({\rm VAR})
.
λ抽象$ \frac{\Gamma,x:A\vdash t:B}{\Gamma\vdash\lambda x.t:A\to B}({\rm ABS})
.
函數適用$ \frac{\Gamma\vdash t_1:A\to B\quad\Gamma\vdash t_2:A}{\Gamma\vdash t_1~t_2:B}({\rm APP})
定理
代入$ \frac{\Gamma,x:A\vdash t_1:B\quad\Gamma\vdash t_2:A}{\Gamma\vdash t_2[t_2/x]:B}