Simply-Typed Lambda Calculus

Grammar

There are 4 categories of expressions for simply-typed lambda calculus: terms, values, types, and contexts. Values are terms that “cannot be evaluated any further”, they’re as “simple” as possible. Contexts are used for making typing judgments, assertions regarding the type of a term.

“Pure” simply-typed lambda calculus has no base types. That is, the only types allowed are function-types.

The syntax for simply-typed lambda calculus has the following structure:

t ::=        -- terms:
      x      -- variable
      λx:T.t -- abstraction
      t t    -- application

v ::=        -- values:
      λx:T.t -- abstraction values

T ::=        -- types:
      T→T    -- type of functions

Γ ::=        -- contexts:
      ∅      -- empty context
      Γ, x:T -- term variable binding

Evaluation t ⟶ t'

I am endeavouring to use ⟶ for evaluation, and → for function types. Formally, it is a binary relation, and when we have “t ⟶ t’” we state “the evaluation statement (or judgment) t ⟶ t’ is derivable.” For simply-typed lambda calculus, it is the ‘smallest’ one which satisfies three properties.

The first two describe how application “commutes” with evaluation, specifically “on the left” (E-App1) and “on the right” (E-App2)

We also have the hallmark of lambda calculus, beta reduction. This tells us how to substitute a value for a bound variable in a lambda-abstraction. Note the value v₂ must be of type T₁₁ for this to work out, otherwise we cannot evaluate the expression.

Typing Γ ⊢ t : T

Typing statements involve a ternary-relation, the typing relation, which is written “infix” as _ ⊢ _ : _. The first slot is filled by a typing context, the second by a term, and the last by a type.

Typing statements first force us to discuss the typing context. A typing context is a sequence of variables and their types, and the “comma” operator extends the context by “pushing” a new binding on the right. A variable appears at most once in a typing context.

We have the property: a variable has whatever type we are currently assuming it to have. Formally, if we write “x:T ∈ Γ” for “We are assuming x has type T in the current context Γ”, then this property is represented by the typing rule:

Any variable that occurs must either be bound by a lambda-abstraction, or appear in the typing context. If it appears in the typing context x:T' ∈ Γ, then it may appear in the term t judged in the typing relation Γ ⊢ t:T. That is to say, to be more explicit, we may have Γ ⊢ t(x):T where we indicate the possible dependence of t on x explicitly “as if” it were a function.

For example, if we assume b is a boolean, then not(b) is also a boolean. But b is a free variable in not(b) — it’s okay, however, since it is in the typing context Γ=b:boolean. From this we may assemble a lambda-abstraction, moving the b:boolean from the typing context to the variable bound in the lambda expression.

More generally, if our typing context is Γ, x:T₁, and we have t₂:T₂ hold in this context, then we may assemble a lambda-abstraction over x.

The opposite property holds, if we’re given a lambda abstraction of type T₁₁ → T₁₂ and we’re given a term of type T₁₁, then application produces a term of type T₁₂.

Properties

Degeneracy. Pure simply-typed lambda calculus is “degenerate”, in the sense that it has no terms.

Inversion Lemma.

1. If Γ ⊢ x:T, then x:T ∈ Γ
2. If Γ ⊢ λx:T . t : R then R = T→T' for some T', with Γ, x:T ⊢ t:T'.
3. If Γ ⊢ t t' : R, then there is some type T such that Γ ⊢ t : T→R and Γ ⊢ t' : T.

Proof: Immediate from the definition of the typing relation. (End of Proof)

Progress Theorem. Suppose t is a closed, well-typed term (i.e., we have ⊢ t : T for some type T). Then either t is a value, or there is some t' with t ⟶ t'. (End of Theorem)

Proof. By induction typing derivations. We see (T-Var) cannot contribute to this, nor can (T-Abs) — both involve terms that cannot be closed.

We are left with (T-App) as the only case we need to consider, where t = t1 t2 with ⊢ t1 : T11 → T12 and ⊢ t2 : T11.

The inductive hypothesis tells us either t1 is a value, or t2 is a value (or both are values). We must examine these cases each in turn.

• If t1 can take a step, then (E-App1) applies to t
• If t2 can take a step, then (E-App2) applies to t.
• If both t1 and t2 are values, then the inversion lemma tells us t1 takes the form λx:T11 . t12, hence (E-AppAbs) applies to t.

(End of Proof)

Preservation Theorem. If Γ ⊢ t:T and t ⟶ t', then Γ ⊢ t':T. (End of Theorem)

Proof. Again, by induction on a derivation of Γ ⊢ t:T.

• Case (T-Var):
• Case (T-Abs):
• Case (T-App):