Expression
An expression could be a number, or a boolean,
or addition of two expressions,
or a variable,
or an abstraction,
or an application of two expressions. or an if branch.
e ::=
| #t|#f
| (*ee)
| x
| (λ (x) e)
| (e e)
| (ifeee)
1|2|3|…
Type
A type could describe a number,
or a boolean,
or a function from one type to another.
τ ::=
| Bool
Nat
| (→ τ τ )
Context
A context could be an empty list, Γ ::= ε
or a pair consed on another context. | x,τ;Γ (The pair is a variable and its type.)
Judgment
A judgment is a formalized sentence. (The sentence may or may not make sense.)
With context Γ, expression e has type τ. Γ⊢e:τ In context Γ, variable x has type τ. Γ(x)=τ
Inference Rules
An inference rule has
0+ premise judgments, J0 J1 … a horizontal line,
and 1 conclusion judgment. J
Inference Rule for Multiplication
If
with Γ, e1 has type Nat
and with Γ, e2 has type Nat,
then
with Γ, (∗e1 e2) has type Nat. Γ⊢(∗e1 e2):Nat
Γ⊢e1 :Nat Γ⊢e2 :Nat
Inference Rule for Numbers and Booleans
If
(nothing is required)
then
with Γ, any number n has type Nat.
Γ⊢n:Nat
If
(nothing is required)
then
with Γ, any boolean b has type Bool. Γ ⊢ b : Bool
Inference Rule for Sub1
If
with Γ, e has type Nat, Γ⊢e :Nat
then
with Γ, (sub1 e) has type Nat. Γ ⊢ (sub1 e) : Nat
Inference Rule for Zero?
If
with Γ, e has type Nat, Γ⊢e :Nat
then
with Γ, (zero? e) has type Bool. Γ ⊢ (zero? e) : Bool
Inference Rule for If
If
with Γ, e1 has type Bool,
with Γ, e2 has type τ,
with Γ, e3 has type τ,
then
with Γ, (if e1 e2 e3) has type τ. Γ⊢(if e1 e2 e3):τ
Γ⊢e1 :Bool Γ⊢e2 :τ Γ⊢e3 :τ
Inference Rule for Variables
If
in context Γ, variable x has type τ, Γ(x)=τ then
with context Γ, variable x has type τ. Γ⊢x :τ
Inference Rule for Applications
If
in context Γ, e1 has type (→τin τout), Γ⊢e1 :(→τin τout)
and in context Γ, e2 has type τin ,
then
with context Γ, (e1 e2) has type τout . Γ ⊢ (e1 e2) : τout
Γ⊢e2 :τin
Inference Rule for Abstractions
If
with the extended Γ, e has type τout, x : τin;Γ⊢e :τout
then
with Γ, (λ (x) e) has type (→τin τout) Γ⊢(λ (x) e):(→τin τout)
Inference Rule for Fix
We need this rule for recursion because (x x) does not type check.
If
with the extended Γ, e has type τ , x : τ ; Γ ⊢ e : τ
then
with Γ, (fix (λ (x) e)) has type τ Γ⊢(fix (λ (x) e)):τ