### Hereditary substitutions over simply typed λ-calculus

Wednesday, August 13th, 2008 by Chantal KellerLast friday, I talked about what I did during the second part of my internship. I explained an Agda implementation of hereditary substitutions over simply-typed λ-calculus from Thorsten Altenkirch, basing on ideas from Conor McBride and Andreas Abel.

Hereditary substitutions are substitutions over typed λ-calculus that are structurally recursive. It provides an algorithm for normalization whose termination can be proved by a simple lexicographical induction. The main idea of this algorithm is to simultaneously substitute and re-normalize.

We will restrain to simply typed λ-calculus and use de Bruijn notations. We will also use a notation from Conor: if Γ is a context and x a variable in Γ, then Γ-x is the context Γ without the variable x.

Normal forms in simply typed λ-calculus are terms that are as much as possible β-reduced and η-expanded. There are two ways of constructing them:

- λn : Nf (Γ,σ) τ -> Nf Γ (σ → τ)
- ne : Var Γ σ -> Sp Γ σ ο -> Nf Γ ο

where spines are lists of normal forms:

- ε : Sp Γ σ σ
- _,_ : Nf Γ σ -> Sp Γ τ ρ -> Sp Γ (σ → τ) ρ

We want to define hereditary substitutions over normal forms:

_ [ _ := _ ] : Nf Γ σ -> (x : Var Γ τ) -> Nf (Γ-x) τ -> Nf (Γ-x) σ

in parallel with substitutions over spines:

_ { _ := _ } : Sp Γ σ τ -> (x : Var Γ ρ) -> Nf (Γ-x) ρ -> Sp (Γ-x) σ τ

and application of a normal form to a spine:

_ @ _ : Nf Γ σ -> Sp Γ σ τ -> Nf Γ τ

The definitions are the following ones:

_ [ _ := _ ]

- (λn t)[x := u] = λn t[x+ := u+]
- (ne y ts)[x := u] = ne y’ ts{x := u} where y’+x == y if x ≠ y
- (ne x ts)[x := u] = u @ ts{x := u}

_ { _ := }

- ε{x := u} = ε
- (t , ts){x := u} = t[x := u] , ts{x := u}

_ @ _

- u @ ε = u
- (λn u) @ (t , ts) = u[ø := t] @ ts

This is structurally recursive and terminates: for measures, we will consider (type of x, length of the normal form) for _ [ _ := _ ]; (type of x, length of the spine) for _ { _ := _ }; and (type of u) for _ @ _. It is obvious to see that when each function calls itself and when _ [ _ := _ ] and _ { _ := _ } call each other, the measures strictly decrease (for the lexicographical order).

The problem is when _ [ _ := _ ] and _ @ _ call each other. In that case, we have:

- (ne x (t , ts))[x := λn u] = (λn u) @ (t’ , ts’) where (t’ , ts’) == (t , ts){x := λn u}
- (λn u) @ (t’ , ts’) = (u[ø := t']) @ ts’

When (ne x (t , ts))[x := λn u] calls _ @ _, x and (λn u) have type (σ → τ). When (λn u) @ (t’ , ts’) calls _ [ _ := _ ], ø has type σ, and σ < σ → τ; and (u[ø := t']) has type τ, and τ < σ → τ.

Once we have established hereditary substitutions, we can normalize terms:

- nf (var v) = nf’ v ε where:

- nf’ v ts = ne v ts if ts : Sp Γ σ ο
- nf’ v ts = λn nf’ v (ts+,(nf’ ø ε)) if ts : Sp Γ σ (τ → ρ)

- nf (λ t) = λn (nf t)
- nf (app t u) = t’[ø := nf u] where nf t == λn t’

In reverse, we can easily define an embedding function <_> that transforms a normal form into a term.

During my trainee, I intended to prove three properties:

- t ≈ < nf t > (completeness)
- t ≈ u => nf t == nf u (soundness)
- nf <t> == t (stability)

I nearly managed to perform these proofs, nonetheless I miss one proof to complete it: the fact that η-equality stands for normal forms:

λn (app’ t (nf’ ø ε)) == t where t has an arrow type and app’ (λn t) u = t[ø := u]

Proving this is similar to prove: (t+1)[ø := (nf' ø ε)] == t. Nils previously performed this proof but in another framework, and we did not see how to prove this property in the framework exposed above.