Tutorial

Proofs about the simply-typed lambda-calculus

1. Type uniqueness

2. Reasoning about paths in lambda-terms

This example illustrates the expressive power of Beluga. In particular, the theorem we discuss here requires nested impliciations and quantification, in particular negative occurrences of these connectives. For a much simpler theorem, also illustrating the need for handling negative occurrences of implications and quantifiers, see example 5. Reasoning about smaller relation on lambda-terms.

If you'd like to run this example using Beluga, please download path.bel, which contains all the type definitions and the implementation of the proof as a recursive function.

We interpret lambda-terms essentially as a tree-structure and paths describe how to traverse it. We begin by defining paths to describe a path through a given lambda-term. 

datatype path :  type =                              
| bind  : tp → (path → path) → path
| left  : path → path
| right : path → path
| done  : path
; 
%name path P.

We can either go left or right when we encounter an application. When we see an abstraction, we memoize the type of the input argument as well as the binder. We again use higher-order abstract syntax encoding for the constructor bind which describes the path going underneath an abstraction. Finally, we allow partial paths, i.e., paths to sub-expressions, using the constructor done.

Next, we define the inference rules for the traversal of a lambda-term.

datatype is_path : path → exp → type =
| p_lam: is_path (bind T P) (lam T E)
       ← ({x:exp}{q:path}is_path q x → is_path (P q) (E x))
| p_left: is_path (left P) (app M N)
       ← is_path P M
| p_right: is_path (right P) (app M N)
       ← is_path P N
| p_done: is_path done M
;
%name is_path I.

We want to prove the following theorem:

Theorem:For all M, N, if for all paths P, ⊢ is_path P M implies ⊢ is_path P N then ⊢ equal M N.

Since during the proof we will introduce assumptions about variables and the context will not remain empty, we will prove a more general version of the theorem first, and then derive the theorem as a corollary. The generalized version is next:

Lemma:For all M, N, if for all paths P, Γ ⊢ is_path P M implies Γ ⊢ is_path P N then Γ ⊢ equal M N.

The statement of the lemma and theorem are good examples to illustrate the expressive power of Beluga. Because the statements require nested quantification and implication, it is not possible to state these theorems directly in some systems for example the Twelf system.

The context Γ contains assumptions x:exp, q:path, and is_path q x. We pair all these assumptions together to ensure that whenever we have a variable x we also have a path variable q which leads to it and we know the type of it. This is achieved using the following schema declaration which defines the shape of the context Γ 

schema ctx =  block x:exp, p:path . is_path p x ;

Formally, we are using a dependent product type or Σ-type to define the schema. So our concrete syntax of block x:exp, p:path . is_path p x corresponds more formally to Σ x:exp . Σ p:path . is_path p x.

On paper proof:

The proof for the stated lemma can be implemented as a recursive function which has the following type: 

{g:ctx}{M:[g. exp]}{N:[g. exp]}
          ({P:[g. path]} [g. is_path (P ..) (M ..)] → [g. is_path (P ..) (N ..)])
      → [g. eq (M ..) (N ..)]

The type corresponds directly to the specified lemma where {g:ctx} introduces quantification over the context variable g which has schema ctx. The context schema name is annotated with * to denote that declarations of the specified schema may be repeated and that we pass the context explicitely to the function. Meta-variables written with curly braces such as {M::[g. exp]},{N::[g. exp]}, and {P::[g. exp]} correspond to universal quantification over the variables M, N, and P.

The overall type can be read as follows: For all contexts g and for all M and N, if given a proof that for all paths P where is_path (P ..) (M ..) in the context g, we know is_path (P ..) (N ..) in the same context g, then we know that M and N are equal (in g).

We first show one case of the proof how it is written on paper.

Case: M = lam T \x. M' .. x

1for all P.[g. is_path (P ..) (lam T \x.M' .. x)] → [g. is_path (P ..) (N ..)]
by assumption
2[g. is_path (bind T \q.done) (lam T \x.M' .. x)]
→ [g. is_path (bind T \q.done) (N ..)] using bind T \q.done for P
3[g, b:block x:exp,q:path,u:type_of x T.v:is_path q x. is_path done (M' .. b.1)]
   by rule p_done
4[g. is_path (bind T \q.done) (lam T \x.M' .. x)] by rule p_bind
5[g. is_path (bind T \q.done) (N ..)] using line 2 and line 4
6[g, block x:exp,q:path,u:type_of x T.v:is_path q x. is_path done (N' .. b.1)]
 where N = lam T \x.N' .. x using rule p_bind
7[g, block x:exp,q:path,u:type_of x T.v:is_path q x. is_path done (N' .. b.1)]
   using rule p_done
 Let g' = g, b:block x:exp,q:path,u:type_of x T.v:is_path q x
 We need to establish: for all P.[g'. is_path P (M' .. b.1)] → [g'. is_path P (N' .. b.1]
8assume P:path and D:[g'. is_path P (M' .. b.1))]
Recall that assumption 1 is now:
for all Q.[g. is_path (Q ..) (lam T \x.M' .. x)]
→ [g. is_path (Q ..) (lam T \x.N' .. x)]
9[g. is_path (bind T (\x.\q. P .. x q) (lam T \x.M' .. x)]
→ [g. is_path (bind T (\x.\q. P .. x q)) (lam T \x.N' .. x)]
using bind T (\x.\q. P .. x q) for Q
10[g. is_path (bind T (\x.\q. P .. x q) (lam T \x.N' .. x)]
using p_lam and assumption D from line 8
11[g'. is_path (P .. b.1 b.2) (N' .. b.1)] by inversion using p_lam
Hence, we have established a proof for:
for all P.[g'. is_path P (M' .. b.1)] → [g'. is_path P (N' .. b.1]
12[g'. equal (M' .. b.1) (N' .. b.1)] by i.h. on M', N' and the previous line
10M' = N'by rule e_ref
11[g. equal (lam T \x. M' .. x) (lam T \x.N' .. x)] by rule e_ref and line 10

The inductive proof can be implemented as a recursive function in Beluga following closely the more informal development given earlier. We treat computation-level expressions which correspond to quantifier introduction and elimination differently from the expressions corresponding to implication introduction and elimination. To introduce a universally quantified meta-variable P, we write mlam P ⇒ .... To eliminate a universal quantifier, we write e <g.M> where e has type {M:[g. A]}.tau and g.M describes the data-level object used to instantiate the universal quantifier and has type A in the context g. For implication introduction, we write fn x ⇒ ... 

rec eqPath : {g:ctx}{M:[g. exp]}{N:[g. exp]}
             ({P:[g. path]} [g. is_path (P ..) (M ..)] → [g. is_path (P ..) (N ..)])
	    → (eq (M ..) (N ..))[g] = 
mlam g ⇒ mlam M ⇒ mlam N ⇒ fn f ⇒ case [g. M ..] of
 | [g. app (M1 ..) (M2 ..)]  ⇒ 
    let [g. p_left p_done] : [g. is_path (left done) (app (N1 ..) (N2 ..))] 
       = f [g. left done] [g. p_left p_done] in 

   let [g. e_ref] = 
     eqPath [g] [g. M2 ..] [g. N2 ..] 
     (mlam Q ⇒ fn iq ⇒ let [g. D ..] = iq in 
      let [g. p_right (D' ..)] : [g. is_path (right (Q' .. )) (app (N1 ..) (N2 ..))] =
        f  [g. right (Q ..)] [g. p_right (D ..]) 
       in [g. D' ..]  in

   let [g. e_ref]  = 
      eqPath [g] [g. M1 ..] [g. (N1 ..)]
      (mlam Q ⇒ fn iq ⇒ 
       let [g. D ..] = iq in 
       let [g. p_left (D' ..)] : [g. is_path (left (Q' .. )) (app (N1 ..) (N2 ..))] =
         f [g. left (Q ..)] [g. p_left (D .. )] 
       in [g. D' ..]   )                           
    in  		 
     [g. e_ref]

| [g. #p.1 ..] ⇒ 
  let [g. #q.3 ..] = f [g. #p.2 .. ] [g. #p.3 ..] in 
    [g. e_ref]


| [g. lam T (\x. M' .. x)] ⇒ 
  let  [g. p_lam (\x.\p. \i. p_done)]  : 
       [g. is_path (bind T' (\p.done)) (lam _ (\x. N' .. x))]  = 
       f [g. bind T (\p.done)] [g. p_lam (\x.\p.\i. p_done)] in 

  let [g,b:block x:exp, q:path . is_path q x. e_ref] = 
     eqPath [g, b:block x:exp, q:path . is_path q x] 
     [g,b. M' .. b.1] [g,b. N' .. b.1]
     (mlam Q ⇒ fn ip ⇒
      let [g,b:block x:exp, q:path. is_path q x. Qs .. b.2] = 
          [g,b:block x:exp, q:path. is_path q x. Q .. b] in           % strengthening 
      let [g,b:block x:exp, q:path. is_path q x. D .. b] = ip in 
      let [g. p_lam (\x.\q.\iq. D' .. x q iq)] : 
          [g. is_path (bind _ (\q. Q' .. q)) (lam _ (\x. N' .. x))] =  
           f [g. bind T (\q. Qs .. q)]  [g. p_lam (\x.\q.\iq. D .. x,q,iq) ]  
      in
         [g,b. D' .. b.1 b.2 b.3]
       )
  in 
    [g. e_ref]
;

rec path_thm : {M:[ . exp]}{N:[ . exp]}
               ({P:[ . path ]}([ . is_path P M] → [ . is_path P N])
	     → [ . eq M N] = 
mlam M ⇒ mlam N ⇒ fn f ⇒ eqPath [ ] [ . M] [ . N]  f ;

3. Subject reduction

4. Equality reasoning

5. Reasoning about smaller relation on lambda-terms