Correctness of weak head-normal evaluator

1. Weak Head Normal Forms
- 1.1. Definition: Weak head-normal evaluation
- 1.2. Weak Head-normal forms
2. Abstracting fix
3. Proofs

We use our β-equivalence checker to partially machine-check a proof that our weak head-normal evaluator eval is correct. The proof strategy is the following:

We specify weak head normal evaluation, and weak head normal forms.
Then we machine-check a series of proofs about the behavior of evalV on terms of particular form.
We use induction on a normalizing sequence of reductions e ↝* v from a term e to its weak head normal form v to prove that eval maps the representation of e to the representation of v.

We employ the following techniques to make this work:

We use a new syntactic sugar const X : T; for declaring uninterpreted constants. These are implemented using free variables.
We machine check β-equivalence by comparing β-normal forms. Some terms of interest do not have normal forms, in particular an application of the recursive function evalV to an uninterpreted constant. To address this, we define an alternate version of evalV, replacing the fixpoint combinator with an uninterpreted constant. We then use helper functions to unfold evalV a finite number of times.

For each machine-checked proof, we list the code that is checked for β-equivalence. Our β-equivalence checker expects a Church-pair of the form \c{λf:T → T → T. f a b}. It then projects out \c{a} and \c{b} and compares them for equivalence.

1 Weak Head Normal Forms

1.1 Definition: Weak head-normal evaluation

   e1 ↝ e1'
--------------- WHN-App
e1 e2 ↝ e1' e2

------------------------------ WHN-AppAbs
(λx:A. e1) e2  ↝  e1[x := e2]

  e ↝ e'
----------- WHN-TApp
e T ↝ e' T

------------------------- WHN-TAppTAbs
(ΛX:K. e) T  ↝  e[X := T]

             e ↝ e'
---------------------------------  WHN-Unfold
unfold T1 T2 e ↝ unfold T1 T2 e'

----------------------------------  WHN-UnfoldFold
unfold T1 T2 (fold T1' T2' e) ↝ e

1.2 Weak Head-normal forms

(Head-normal forms) V ::= N | (λx.T. E) | (ΛX:K. E) | fold T1 T2 E
(Neutral terms)     N ::= x | N E | N T | unfold T1 T2 N

2 Abstracting `fix`

We define variants of evalV and eval in which the fixpoint combinator fix has been abstracted. This makes them strongly normalizing. If apply eval to the concrete implementation of fix, we recover the version shown in the paper. If we apply eval to an uninterpreted constant it normalizes without unfolding the recursive definition of evalV. We also define wrapper functions fix1 and fix2 that can be used to reason about 1 or 2 unfoldings of evalV respectively. This is sufficient for our proof of correctness.

2.1 `eval` with `fix` abstracted

decl evalV : (∀A:*. (A → A) → A) →
             (∀V : * → *. ∀A:*. PExp V A → PExp V A) =
 λfix : (∀A:*. (A → A) → A).
 fix (∀V : * → *. ∀A:*. PExp V A → PExp V A) (
 λevalV : (∀V : * → *. ∀A:*. PExp V A → PExp V A).
 ΛV:* → *. ΛA:*. λe:PExp V A.
 matchExp V A e (PExp V A)
  (constVar V A (PExp V A) e)
  (constAbs V A (PExp V A) e)
  (ΛB:*. λf : PExp V (B → A). λx : PExp V B.
   let f1 : PExp V (B → A) = evalV V (B → A) f in
   let def : PExp V A = app V B A f1 x in
   matchAbs V (B → A) (PExp V A) f1 def
    (ΛB1:*. ΛA1:*. λeq : Eq (B1 → A1) (B → A).
     λf : PExp V B1 → PExp V A1.
     let eqL : Eq B B1 = sym B1 B (arrL B1 A1 B A eq) in
     let eqR : Eq A1 A = arrR B1 A1 B A eq in
     let f' : PExp V B → PExp V A =
       eqR (PExp V) ∘ f ∘ eqL (PExp V)
     in evalV V A (f' x)))
  (constTAbs V A (PExp V A) e)
  (ΛB : *. λp : IsAll B. λi : Inst B A. λe1 : PExp V B.
   let e2 : PExp V B = evalV V B e1 in
   let def : PExp V A = tapp V B A p i e2 in
   matchTAbs V B (PExp V A) e2 def
    (λp : IsAll B. λs : StripAll B. λu : UnderAll B.
     λe3 : All Id (PExp V) B. evalV V A (i (PExp V) e3)))
  (constFold V A (PExp V A) e)
  (ΛF : (* → *) → * → *. ΛB : *.
   λeq : Eq (F (μ F) B) A. λe1 : PExp V (μ F B).
   let e2 : PExp V (μ F B) = evalV V (μ F B) e1 in
   let def:PExp V A = eq (PExp V) (unfld V F B e2) in
   matchFold V (μ F B) (PExp V A) e2 def
    (ΛF1 : (* → *) → * → *. ΛB1 : *.
     λeq1 : Eq (μ F1 B1) (μ F B).
     λe3 : PExp V (F1 (μ F1) B1).
     let eq2 : Eq (F1 (μ F1) B1) A =
       trans (F1 (μ F1) B1) (F (μ F) B) A 
         (eqUnfold F1 B1 F B eq1) eq
     in eval A (eq2 (PExp V) e3)));

decl eval : (∀A:*. (A → A) → A) →
            (∀A:*. Exp A → Exp A) =
  λfix : (∀A:*. (A → A) → A).
  ΛA : *. λe : Exp A. ΛV : * → *.
  evalV fix V A (e V);

2.2 Lemma: `fix1 fix ≡ fix`

decl fix : (Pi A:*. (A → A) → A) =
  \A:*.
  \f:A → A.
  let x : (Rec A) = fold RecF A (\r : Rec A. f (unfold RecF A r r)) in
  f (unfold RecF A x x)
;

decl fix1 : (Pi A:*. (A → A) → A) → (Pi A:*. (A → A) → A) =
  \fix : (Pi A:*. (A → A) → A).
  \A : *.
  \f : A → A.
  f (fix A f)
;

  fix
= ΛA:*. λf: A → A.
  let x : (Rec A) = fold RecF A (\r : Rec A. f (unfold RecF A r r)) in
  f (unfold RecF A x x)
≡ ΛA:*. λf: A → A.
  let x : (Rec A) = fold RecF A (\r : Rec A. f (unfold RecF A r r)) in
  f ((\r : Rec A. f (unfold RecF A r r)) x)
≡ ΛA:*. λf: A → A.
  let x : (Rec A) = fold RecF A (\r : Rec A. f (unfold RecF A r r)) in
  f (f (unfold RecF A x x))
≡ ΛA:*. λf: A → A.
  f (let x : (Rec A) = fold RecF A (\r : Rec A. f (unfold RecF A r r)) in
     f (unfold RecF A x x))
≡ ΛA:*. λf: A → A.
  f ((ΛA:*. λf: A → A.
      let x : (Rec A) = fold RecF A (\r : Rec A. f (unfold RecF A r r)) in
      f (unfold RecF A x x)) A f)
≡ ΛA:*. λf: A → A.
  f (fix A f)
= fix1 fix

From now on, we will use fix1 fix interchangably with fix.

2.3 Lemma: `fix2 fix ≡ fix`

decl fix : (Pi A:*. (A → A) → A) =
  \A:*.
  \f:A → A.
  let x : (Rec A) = fold RecF A (\r : Rec A. f (unfold RecF A r r)) in
  f (unfold RecF A x x)
;

decl fix2 : (Pi A:*. (A → A) → A) → (Pi A:*. (A → A) → A) =
  \fix : (Pi A:*. (A → A) → A).
  \A : *.
  \f : A → A.
  f (f (fix A f))
;

  fix
= ΛA:*. λf: A → A.
  let x : (Rec A) = fold RecF A (\r : Rec A. f (unfold RecF A r r)) in
  f (unfold RecF A x x)
≡ ΛA:*. λf: A → A.
  let x : (Rec A) = fold RecF A (\r : Rec A. f (unfold RecF A r r)) in
  f ((\r : Rec A. f (unfold RecF A r r)) x)
≡ ΛA:*. λf: A → A.
  let x : (Rec A) = fold RecF A (\r : Rec A. f (unfold RecF A r r)) in
  f (f (unfold RecF A x x))
≡ ΛA:*. λf: A → A.
  let x : (Rec A) = fold RecF A (\r : Rec A. f (unfold RecF A r r)) in
  f (f ((\r : Rec A. f (unfold RecF A r r)) x))
≡ ΛA:*. λf: A → A.
  let x : (Rec A) = fold RecF A (\r : Rec A. f (unfold RecF A r r)) in
  f (f (f (unfold RecF A x x)))
≡ ΛA:*. λf: A → A.
  f (f (let x : (Rec A) = fold RecF A (\r : Rec A. f (unfold RecF A r r)) in
        f (unfold RecF A x x)))
≡ ΛA:*. λf: A → A.
  f (f ((ΛA:*. λf: A → A.
        let x : (Rec A) = fold RecF A (\r : Rec A. f (unfold RecF A r r)) in
        f (unfold RecF A x x)) A f))
≡ ΛA:*. λf: A → A.
  f (f (fix A f))
= fix2 fix

From now on, we will use fix2 fix interchangably with fix.

3 Proofs

3.1 Lemma: Canonical head-normal values

If e is closed, well-typed and head-normal, it is an abstraction or a fold.

Proof Sketch: by induction on the size of the term.

Case λ, Λ, fold. Immediate.
Case x: contradicts closed.
Case neutral application. e = e1 e2, where e1 is a smaller closed, well-typed head-normal term. By induction, e1 is an abstraction or a fold. For e1 to be well-typed, e1 must have an arrow type. Therefore e1 must be a lambda abstraction (λx:T. e1'). Contradiction: e is not head-normal
Remaining neutral cases are similar.

3.2 Lemma: Substitution on representations

[e1[x:=e2]] = [e1][x := [e2]]

By straightforward induction on e1.

Suppose e1 = x. Then [e1]=x also. Therefore, [e1[x:=e2]] = [x[x:=e2]] = [e2], and [e1][x := [e2]] = x[x:=[e2]] = [e2].

Suppose e1 = y, and x ≠ y. Then [e1]=y. Therefor, [e1[x:=e2]] = [y[x:=e2]] = [y] = y, and [e1][x:=[e2]] = [y][x:=[e2]] = y[x:=[e2]] = y.

Suppose e1 = (λy:T1.e1'). Without loss of generality (by renaming), we can assume x ≠ y. By induction, we have that [e1'[x:=e2]] = [e1'][x:=[e2]]. We have that [e1[x:=e2]] = [(λy:T1.e1')[x:=e2]] = [(λy:T1. e1'[x:=e2])] = abs T1 T2 (λy:PExp V T1. [e1'[x:=e2]]) = abs T1 T2 (λy:PExp V T1. [e1'][x:=[e2]]).

Further, [e1]=(abs T1 T2 (λy: PExp V T1. [e1'])). Since abs is closed, we have that [e1][x:=[e2]]=(abs T1 T2 (λy:T1. [e1']))[x:=[e2]] = abs T1 T2 (λy:T1. [e1'][x:=[e2]]).

Therefore, [e1[x:=e2]] = [e1][x:=[e2]] as required.

The remaining cases are straightforward.

3.3 Lemma: Type substitution on representations

[e[X := T]] = [e][X := T]

Proof: By straightforward induction, similar to Lemma: Substitution on representations.

3.4 Lemma: Semantics of Inst Functions

Forall X,K,T,S,F,e:

inst[X,K,T,S] F e ≡ e S

Proof:

  inst[X,K,T,S] F e
= (ΛF : * → *. λx : (∀X:K. F T). x S) F e
≡ e S

3.5 Lemma: `eval` to `evalV`

If A : * and e : Exp A, then

eval fix A e ≡ (ΛV:* → *. evalV fix V A (e V))

Proof: Machine-checked.

whnfCorrectEvalEvalV.fw

load "WeakHeadNormalFormAbsFix";
load "Fix";

const fix : (∀A:*. (A → A) → A);
const A : *;
const e : Exp A;

decl T : * = Exp A;

decl t1 : T =
  eval fix A e
;

decl t2 : T =
  (ΛV:* → *. evalV fix V A (e V))
;

λf : T → T → T.
f t1 t2

3.6 Lemma: WHNF-Abs

For any V, A, B, f (appropriately typed):

evalV fix V A B (abs V A B f)
  ≡ 
abs V A B f

Proof: Machine-checked.

whnfCorrectAbs.fw

load "WeakHeadNormalFormAbsFix";
load "Fix";

const fix : (∀A:*. (A → A) → A);
const V : * → *;
const A : *;
const B : *;
const f : PExp V A → PExp V B;

decl T : * = PExp V (A → B);
decl t1 : T = evalV (fix1 fix) V (A → B) (abs V A B f);
decl t2 : T = abs V A B f;

λf : T → T → T.
f t1 t2

3.7 Lemma: WHNF-AppAbs

For any V, A, B, f, x (appropriately typed):

evalV fix V B
  (app V A B (abs V A B f) x)  
  ≡
evalV fix V B (f x)

Proof: whnfCorrectAppAbs.fw

load "WeakHeadNormalFormAbsFix";
load "Fix";

const fix : (∀A:*. (A → A) → A);
const V : * → *;
const A : *;
const B : *;
const f : PExp V A → PExp V B;
const x : PExp V A;

decl T : * = PExp V B;

decl t1 : T =
  evalV (fix2 fix) V B
    (app V A B (abs V A B f) x);

decl t2 : T =
  evalV (fix1 fix) V B (f x);

λf : T → T → T.
f t1 t2

3.8 Lemma: WHNF-TAbs

For any V, T, p, s, u, e (appropriately typed):

evalV fix V T (tabs V T p s u e)
  ≡ 
tabs V T p s u e

Proof: Machine-checked.

whnfCorrectTAbs.fw

load "WeakHeadNormalFormAbsFix";
load "Fix";

const fix : (∀A:*. (A → A) → A);
const V : * → *;
const A : *;
const p : IsAll A;
const s : StripAll A;
const u : UnderAll A;
const e : All Id (PExp V) A;

decl T : * = PExp V A;

decl t1 : T =
  evalV (fix1 fix) V A
    (tabs V A p s u e)
;

decl t2 : T =
  tabs V A p s u e
;

λf : T → T → T.
f t1 t2

3.9 Lemma: WHNF-TAppTAbs

For any V, A, B, p, s, u, e, i (appropriately typed):

evalV (fix2 fix) V B
  (tapp V A B p i
    (tabs V A p s u e))
  ≡
evalV (fix1 fix) V B (i (PExp V) e)

Proof: whnfCorrectTAppTAbs.fw

load "WeakHeadNormalFormAbsFix";
load "Fix";

const fix : (∀A:*. (A → A) → A);
const V : * → *;
const A : *;
const B : *;
const p : IsAll A;
const s : StripAll A;
const u : UnderAll A;
const e : All Id (PExp V) A;
const i : Inst A B;

decl T : * = PExp V B;

decl t1 : T =
  evalV (fix2 fix) V B
    (tapp V A B p i
      (tabs V A p s u e))
;

decl t2 : T =
  evalV (fix1 fix) V B (i (PExp V) e)
;

λf : T → T → T.
f t1 t2

3.10 Lemma: WHNF-Fold

For any V, F, A, e (appropriately typed):

evalV fix V (μ F A) (fld V F A e)
  ≡ 
fld V F A e

Proof: Machine-checked.

whnfCorrectFold.fw

load "WeakHeadNormalFormAbsFix";
load "Fix";

const fix : (∀A:*. (A → A) → A);
const V : * → *;
const F : (* → *) → * → *;
const A : *;
const e : PExp V (F (μ F) A);

decl T : * = PExp V (μ F A);

decl t1 : T =
  evalV (fix1 fix) V (μ F A)
    (fld V F A e)
;

decl t2 : T =
  fld V F A e
;

λf : T → T → T.
f t1 t2

3.11 Lemma: WHNF-UnfoldFold

For any V, T1, T2, e (appropriately typed):

evalV (fix2 fix) V (F (μ F) A)
  (unfld V F A (fld V F A e))
  ≡
evalV (fix1 fix) V (F (μ F) A) e

Proof: Machine-checked.

whnfCorrectUnfoldFold.fw

load "WeakHeadNormalFormAbsFix";
load "Fix";

const fix : (∀A:*. (A → A) → A);
const V : * → *;
const F : (* → *) → * → *;
const A : *;
const e : PExp V (F (μ F) A);

decl T : * =
  PExp V (F (μ F) A)
;

decl t1 : T =
  evalV (fix2 fix) V (F (μ F) A)
    (unfld V F A
      (fld V F A e))
;

decl t2 : T =
  evalV (fix1 fix) V (F (μ F) A) e
;

λf : T → T → T.
f t1 t2

3.12 correctness of `evalV`

Theorem: If Γ ⊢ e : T and e ↝* v, then evalV fix V T [e] ≡ [v].

Proof: By structural induction on the sequence of steps e ↝* v.

3.12.1 Base case: Reflexivity.

Then e is a value.
Want to show evalV fix V T [e] ≡ [e]

3.12.1.1 Case: `e = x`.

Contradiction, by Lemma: Canonical head-normal values

3.12.1.2 Case: `e = (λx:T1. e')`.

Then we have that

T = T1 → T2
[e] = abs V T1 T2 (λx : PExp V T1. [e'])

By Lemma: WHNF-Abs, we have:

evalV fix V T [e] 
  = 
evalV fix V (T1 → T2) (abs V T1 T2 (λx : PExp V T1. [e']))
  ≡
abs V T1 T2 (λx : PExp V T1. [e'])
  =
[e]

3.12.1.3 Case: ~e = v e'~.

Contradiction, by Lemma: Canonical head-normal values

3.12.1.4 Case: `e = (ΛX:K. e')`.

Then we have that

T = (∀X:K. T')
[e] = tabs V isAll[X,K,T'] stripTAbs[K] underTAbs[X,K,T'] (ΛX:K. [e'])

By WHNF-TAbs, we have:

evalV fix V T [e]
  =
evalV fix V T (tabs V isAll[X,K,T'] stripTAbs[K] underTAbs[X,K,T'] (ΛX:K. [e']))
  ≡ 
tabs V isAll[X,K,T'] stripTAbs[K] underTAbs[X,K,T'] (ΛX:K. [e'])
  =
[e]

3.12.1.5 Case: `e = v T`.

Contradiction, by Lemma: Canonical head-normal values

3.12.1.6 Case: ~e = fold F A e'~.

Then we have that

T = μ F A
[e] = fld V F A [e']

By WHNF-Fold, we have that:

evalV fix V T [e]
  =
evalV fix V T (fld V F A [e'])
  ≡
fld V F A [e']
  =
[e]

3.12.1.7 Case: ~e = unfold T1 T2 e'~.

Contradiction, by Lemma: Canonical head-normal values

3.12.2 Induction case

There exists a term e'~ such that ~e ↝ e'~ and ~e' ↝* v.
By preservation, ⟨⟩ ⊢ e' : T.
Induction hypothesis: evalV fix V T [e'] ≡ [v].

Proceed by case analysis on the step ~e ↝ e'~.

3.12.2.1 Case: App/Abs

We have that:

e = (λx:T2. e1) e2
e' = e1[x := e2]
[e] = app V T2 T (abs V T2 T (λx : PExp V T2. [e1])) [e2]
[e'] = [e1[x := e2]]

By Lemma: Substitution on representations:

[e1][x := [e2]] = [e1[x := e2]] = [e']

By WHNF-AppAbs, with:

A = T2
B = T
f = (λx : PExp V T2. [e1])
x = [e2]

We have that:

evalV fix V T [e]
  ≡
evalV fix V T ((λx : PExp V T2. [e1]) [e2])
  ≡
evalV fix V T ([e1] [x := [e2]])
  ≡
evalV fix V T ([e1[x := e2]])
  ≡
evalV fix V T [e']
  ≡
[v]

3.12.2.2 Case: TApp/TAbs

We have that:

T = T1 [X := T2]
e = (ΛX:K. e1) T2
e' = e1 [X := T2]
p = isAll[X,K,T1]
s = stripAll[K]
u = underAll[X,K,T1]
i = inst[X,K,T1,T2]
[e] = tapp V (∀X:K.T1) T p i (tabs V (∀X:K.T1) p s u (ΛX:K. [e1]))
[e'] = [e1 [X := T2]]

By Lemma: Type substitution on representations:

[e1][X := T2] = [e1[X := T2]] = [e']

By Lemma: Semantics of Inst Functions:

i (PExp V) (ΛX:K. [e1]) ≡ (ΛX:K. [e1]) T2 ≡ [e1][X := T2] ≡ [e']

By WHNF-TAppTAbs, with:

A = (∀X:K. T1)
B = T1 [X := T2] = T

We have that:

evalV fix V T [e]
  ≡
evalV fix V T 
  (tapp V (∀X:K.T1) T p i 
    (tabs V (∀X:K.T1) p s u (ΛX:K. [e1])))
  ≡
evalV fix V T (i (PExp V) (ΛX:K. [e1]))
  ≡
evalV fix V T [e']
  ≡
[v]

3.12.2.3 Case: Unfold/Fold

We have that:

T = T1 (μ T1) T2
e = unfold T1 T2 (fold T1 T2 e')
[e] = unfld T1 T2 (fld T1 T2 [e'])

By WHNF-UnfoldFold, we have that:

evalV V T (unfld T1 T2 (fld T1 T2 [e']))
  ≡
evalV V T [e']
  ≡
[v]

3.13 correctness of `eval`

Theorem: If ⟨⟩ ⊢ e : T and e ↝* v, then eval fix T (ΛV:* → *. [e]) ≡ (ΛV:* → *. [v]).

Proof:

By Lemma: eval to evalV and correctness of evalV, we have that

  eval fix T (ΛV:* → *. [e]) 
≡ (ΛV:* → *. evalV fix V A ((ΛV:* → *. [e]) V))
≡ (ΛV:* → *. evalV fix V A [e])
≡ (ΛV:* → *. [v])

The first step is by Lemma: eval to evalV, and the last step is by correctness of evalV.

Correctness of weak head-normal evaluator

Table of Contents

1 Weak Head Normal Forms

1.1 Definition: Weak head-normal evaluation

1.2 Weak Head-normal forms

2 Abstracting fix

2.1 eval with fix abstracted

2.2 Lemma: fix1 fix ≡ fix

2.3 Lemma: fix2 fix ≡ fix

3 Proofs

3.1 Lemma: Canonical head-normal values

3.2 Lemma: Substitution on representations

3.3 Lemma: Type substitution on representations

3.4 Lemma: Semantics of Inst Functions

3.5 Lemma: eval to evalV

3.6 Lemma: WHNF-Abs

3.7 Lemma: WHNF-AppAbs

3.8 Lemma: WHNF-TAbs

3.9 Lemma: WHNF-TAppTAbs

3.10 Lemma: WHNF-Fold

3.11 Lemma: WHNF-UnfoldFold

3.12 correctness of evalV

3.12.1 Base case: Reflexivity.

3.12.1.1 Case: e = x.

3.12.1.2 Case: e = (λx:T1. e').

3.12.1.3 Case: ~e = v e'~.

3.12.1.4 Case: e = (ΛX:K. e').

3.12.1.5 Case: e = v T.

3.12.1.6 Case: ~e = fold F A e'~.

3.12.1.7 Case: ~e = unfold T1 T2 e'~.

3.12.2 Induction case

3.12.2.1 Case: App/Abs

3.12.2.2 Case: TApp/TAbs

3.12.2.3 Case: Unfold/Fold

3.13 correctness of eval

2 Abstracting `fix`

2.1 `eval` with `fix` abstracted

2.2 Lemma: `fix1 fix ≡ fix`

2.3 Lemma: `fix2 fix ≡ fix`

3.5 Lemma: `eval` to `evalV`

3.12 correctness of `evalV`

3.12.1.1 Case: `e = x`.

3.12.1.2 Case: `e = (λx:T1. e')`.

3.12.1.4 Case: `e = (ΛX:K. e')`.

3.12.1.5 Case: `e = v T`.

3.13 correctness of `eval`