by Chantal Keller on August 13, 2008.
Tagged as: Lunches.
Last 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:
where spines are lists of normal forms:
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:
_ [ _ := _ ]
_ { _ := }
_ @ _
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:
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:
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:
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.