Tutorial

Proofs about the simply-typed lambda-calculus

1. Type uniqueness

2. Reasoning about paths in lambda-terms

3. Subject reduction

We explain here how to implement the subject reduction proof for the simply-typed lambda-calculus. If you'd like to run this example using Beluga, please download subject-red.bel, which contains all the data-type definitions and the implementation of the proof as a recursive function.

We first define a big step semantics for the simply-typed lambda-calculus using the familiar LF methodology. We define first the type family notLam which allows us to check whether we encounter an expression which is not a lambda-abstraction. In addition we define the main reduction judgment as the type family step. 

notLam: exp → type.
n_app: notLam (app M N).

step: exp → exp → type.

s_lam: ({x:exp}step x x → notLam x → step (M x) (N x))
      → step (lam T M) (lam T N).

s_app1: step (M' N) R →  step M (lam T M')
	→ step (app M N) R.

s_app2: step N N' → notLam M' → step M M'
     → step (app M N) (app M' N').

To implement the subject reduction theorem, we typically state it as follows:

Theorem (Attempt 1): If Γ ⊢ type_of M T and Ψ ⊢ step M N then Γ ⊢ type_of N T.

We note however that the context Γ and the context Ψ are different; for the proof to go through we need some relationship between the typing assumptions in the context Γ and the assumptions step x x in the context Ψ. A simple way to achieve this is to generalize the theorem and state it with a generalized context which contains both, the typing assumptions about x and the assumption step x x, i.e, the variable x reduces to itself. In addition, we keep track of the assumption that x is not a lambda-abstraction.

We therefore define first a context Φ which contains both these assumptions.

Φ ::= . | Φ, type_of x T, step x x, notLam x

We now restate the subject reduction theorem with the generalized context Φ.

Theorem: If Φ ⊢ type_of M T and Φ ⊢ step M N then Φ ⊢ type_of N T.

In Beluga, we specify the structure of the context using context schema as follows: 

schema ctx = some [t:tp] block x:exp,u:type_of x t, v:step x x . notLam x;

It specifies that the context of schema ctx contains declarations which are a quadruple of the variable declaration x:exp, the type declaration u:type_of x t for some type t, the reduction declaration v:step x x and the fact that variables are not lambda-abstractions as expressed by the declaration notLam x. The some keyword says that concrete declarations of the declared schema may instantiate the type t.

The theorem is represented as a computation-level type in Beluga: 

{g:ctx}(type_of (M ..) T)[g] → (step (M ..) (N ..))[g]
         → (type_of (N ..) T)[g] =

Quantification over the context variable g is written using curly brackets in {g:ctx} indicating that the context variable will be implicit and we do not pass it around explicitely. We make explicit the fact that the terms M and N can depend on the context Φ by associating both meta-variables with .. which denotes the identity substitution on the context g. The type T on the other hand cannot depend on the context and hence it is not associated with anything. We read the type as follows: for all contexts g of schema ctx, if (type_of (M ..) T)[g] and (step (M ..) (N ..))[g] then (type_of (N ..) T)[g]. The contextual type (type_of (M ..) T)[g] directly describes the hypothetical derivation Φ ⊢ type_of M T where we make explicit whether an object can depend on declarations in the context or not.

The proof of the subject reduction theorem is then implemented as a recursive program. Case analysis and inversion in the informal proof are modelled via case analysis and let-expressions in the Beluga implementation. Appeals to the induction hypothesis correspond to recursive calls. 

rec tps: {g:ctx}(type_of (M ..) T)[g] → (step (M ..) (N ..))[g]
         → (type_of (N ..) T)[g] =							      
fn d ⇒ fn s ⇒ case s of 
| [g] s_lam \x.\v. \n. S .. x v n ⇒ 
  let [g] t_lam \x.\u. D .. x u = d in 
  let [g, b: block x:exp, u:type_of x T, v:step x x. notLam x] F .. b.1 b.2 = 
      tps ([g,b:block x:exp,u:type_of x _ ,v:step x x. notLam x] D .. b.1 b.2)
	  ([g,b] S .. b.1 b.3 b.4) in 
  [g] t_lam \x.\u. F .. x u

| [g] s_app1 (S2 ..) (S1 ..) ⇒ 
  let [g] t_app (D2 ..) (D1 ..) = d in 
  let [g] t_lam \x.\u. F .. x u = tps ([g] D1 ..) ([g] S1 ..) in 
     tps ([g] F .. _ (D2 ..)) ([g] S2 ..)

| [g] s_app2 (S2 ..) _ (S1 ..) ⇒
  let [g] t_app (D2 ..) (D1 ..) = d in 
  let [g] F1 .. = tps ([g] D1 ..) ([g] S1 ..) in 
  let [g] F2 .. = tps ([g] D2 ..) ([g] S2 ..) in 
    [g] t_app (F2 ..) (F1 ..)

| [g] #p.3 .. ⇒              % s : step (#p.1 ..)  (N ..)          
  let [g] #q.2 .. = d in     % q : block x:exp,u:type_of x t, v:step x x . notLam x
                            % since step #q.1 #q.1 = step #p.1 (N ..) 
                            % N = #q.1  and #q = #p 
  [g] #q.2 ..
   
;

The implementation of the proof mirrors closely the on-paper proof.

4. Equality reasoning

5. Reasoning about smaller relation on lambda-terms