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. 

datatype 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)[g. type_of (M ..) T] → [g. step (M ..) (N ..)]
         → [g. type_of (N ..) T] =

Quantification over the context variable g is written using round 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 [g. type_of (M ..) T] and [g. step (M ..) (N ..)] then [g. type_of (N ..) T]. The contextual type [g. type_of (M ..) T] 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)[g. type_of (M ..) T] → [g. step (M ..) (N ..)]
         → [g. type_of (N ..) T] =							      
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