The decidability of the βη-equivalence using hereditary
substitutions
Hereditary substitutions are substitutions over the simply typed
λ-calculus that preserve canonical forms and are structurally
recursive. This page is devoted to a formal implementation of
a normalizer for the simply typed λ-calculus using hereditary
substitutions in Agda,
which comes with a proof that this normalizer can be use to decide
the decidability of the βη-equivalence.
Sources
The source code is available under the GPL. It is an archive containing:
- A copy of the text version of the GPL.
- The module hsubst.agda implements hereditary substitutions
for the simply-typed λ-calculus.
- The module lemmas1.agda implements operations to work with
De Bruijn indices.
- The modules lemmas2.agda and lemmas3.agda implements
basic commutation lemmas.
- The module lemmas4.agda implements non trivial commutation
lemmas.
- The module proofs.agda implements the βη-equivalence
and the proofs that hereditary substitutions decide it.
- A Makefile to compile it.
Download:
Software requirements
For Agda:
Top of the page
Suggestions and bug report
Do not hesitate to make any suggestion or to report bugs to
Chantal
Keller (remove the anti-spam dots and at).
Top of the page
Last update: 04/16/10