Untyped lambda calculus
terms and values
M ::= x | M M | λx.M terms
V ::= λx.M value
full β-reduction evaluation rules
(λx.M) N →β M[x := N]
M1 →β M2
λx.M1 →β λx.M2
M1 →β M2
M1 N →β M2 N
N1 →β N2
M N1 →β M N2
call-by-value evaluation rules
(λx.M) V →cbv M[x := V ]
M1 →cbv M2
M1 N →cbv M2 N
N1 →cbv N2
V N1 →cbv V N2
Church numerals and booleans
0 := λf.λx.x
1 := λf.λx.f x
n := λf.λx. 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
M ::= x | M M | λx : σ.M | true | false | if M then M else M terms
V ::= λx : σ.M | true | false values
types
σ ::= σ → σ | Bool
typing rules
Γ true : Bool (T-TRUE)
Γ false : Bool (T-FALSE)
x : σ ∈ Γ (T-VAR)
Γ x : σ
Γ, x : σ1 M : σ2
(T-ABS)
Γ λx : σ1.M : σ1 → σ2
Γ M1 : σ1 → σ2 Γ M2 : σ1
(T-APP)
Γ M1 M2 : σ2
Γ M1 : Bool Γ M2 : σ Γ M3 : σ
(T-IF)
Γ if M1 then M2 else M3 : σ
Hindley-Milner type system
terms and values
M ::= x | M1 M2 | λx.M | let x = M1 in M2
types
σ ::= α | σ → σ monotypes
τ ::= σ | ∀α.τ type schemes
typing rules
x : τ ∈ Γ
Γ x : τ
(T-VAR)
Γ, x : σ1 M : σ2
Γ λx.M : σ1 → σ2
(T-ABS)
Γ M1 : σ1 → σ2 Γ M2 : σ1
Γ M1 M2 : σ2
(T-APP)
Γ M1 : τ Γ, x : τ M2 : σ
Γ let x = M1 in M2 : σ
(T-LET)
Γ M : τ τ τ
Γ M : τ
(T-INST)
Γ M : τ α ∈ FV (Γ)
Γ M : ∀α.τ
(T-GEN)
System F
terms and values
M ::= x | M M | λx : σ.M | Λα.M | M [σ] terms
V ::= λx : σ.M | Λα.M values
types
σ ::= α | σ → σ | ∀α.σ
typing rules (in addition to λ→
)
Γ M : σ α ∈ FV (Γ)
Γ Λα.M : ∀α.σ
(T-TABS) (T-GEN)
Γ M : ∀α.σ1
Γ M [σ2] : {σ2/α}σ1
(T-TAPP) (T-INST)
evaluation rules (in addition to λ→
)
M → M
M [σ] → M [σ]
(E-TAPP)
(Λα.M) [σ] → {σ/α}M (E-TAPPTABS)