Untyped lambda calculus
terms and values
M ::= x | MM | λx.M
V ::= λx.M
full β-reduction evaluation rules
(λx.M)N →β M[x := N]
M1 →β M2
λx.M1 →β λx.M2
M1 →β M2
M1N →β M2N
N1 →β N2
MN1 →β MN2
call-by-value evaluation rules
(λx.M)V →β M[x := V ]
M1 →β M2
M1N →β M2N
N1 →β N2
V N1 →β V N2
Church numerals and booleans
0 := λf.λx.x
1 := λf.λx.f x
n := f(f . . . (f
n-times
(x) . . .) = λf.λx.fn
(x)
true := λx.λy.x
false := λx.λy.y
Simply-typed lambda calculus λ→
with Booleans
terms and values
t ::= x | t t | λx : T.t | true | false | if t then t else t
v ::= λx : T.t | true | false
types
T ::= T → T | Bool
typing rules
Γ true : Bool (T-True)
Γ false : Bool (T-False)
x : T ∈ Γ (T-Var)
Γ x : T
Γ, x : T1 t : T2
(T-Abs)
Γ λx.t : T1 → T2
Γ t1 : T1 → T2 Γ t2 : T1
(T-App)
Γ t1 t2 : T2
Γ t1 : Bool Γ t2 : T Γ t3 : T
(T-If)
Γ if t1 then t2 else t3 : T
Hindley-Milner type system
term and values
t ::= x | t t | λx.t | let x = t in t
types
T ::= α | T → T
S ::= T | ∀α.T
typing rules
x : S ∈ Γ
Γ x : S
(T-Var)
Γ, x : T1 t : T2
Γ λx.t : T1 → T2
(T-Abs)
Γ t1 : T1 → T2 Γ t2 : T1
Γ t1 t2 : T2
(T-App)
Γ t1 : S Γ, x : S t2 : T
Γ let x = t1 in t2 : T
(T-Let)
Γ t : S S S
Γ t : S
(T-Inst)
Γ t : S α ∈ FV (Γ)
Γ t : ∀α.S
(T-Gen)
System F
term and values
t ::= x | t t | λx : T.t | Λα.t | t [T]
v ::= λx : T.t | α.t
types
T ::= α | T → T | ∀α.T
typing rules (in addition to λ→
)
Γ t : T α ∈ FV (Γ)
Γ Λα.t : ∀α.T
(T-TAbs) (T-Gen)
Γ t : ∀α.T1
Γ t [T2] : {T2/α}T1
(T-TApp) (T-Inst)
evaluation rules (in addition to λ→
)
t → t
t [T] → t [T]
(E-Tapp)
(Λα.t) [T] → {T/α}t (E-TappTabs)