Proving Decidability of Local Closure

The Penn solution to the POPLmark challenge uses a locally nameless representation, i.e., free variables are given names, but bound variables are represented using DeBruijn indices. Free variables and bound variables are syntactically distinguished. A term with an unbound index is therefore ill-formed. A locally closed term is a term with no unbound indices. In the Penn implementation, an essentially unary predicate is used to distinguish between locally closed terms and those that are not.

This predicate, term in the solutions that accompany Engineering Formal Metatheory by Chargueraud et al. and lc in the solutions that accompany Abstracting Syntax by Aydemir et al. marks the boundary between the straightforwardly defined inductive types which are used to express the basic syntactic structure of the language and more complex inductive types which contain subexpressions to support cofinite quantification.

It is desirable that local closure should be decidable, i.e., given a lambda calculus term it should be possible to generate a proof that the term is locally closed or, in the case that it is not locally closed a proof that it is not. It turns out that this is not straightforward. Concretely, it would be desirable to prove forall t, lc t \/ ~ lc t. It is impossible to construct a proof of this fact by straightforward induction on the structure of the term. The induction hypotheses generated by induction on the structure of terms will be inadequate for any constructor of lc which contains a cofinitely quantified expression.

Our solution to this problem is to define a measure of the depth of the term. It is then possible to procede by induction on the depth of the term rather than on the term itself. Using the depth measure it is possible to proceed by reflection or by constructing a new induction principle for terms which follows the structure of lc. This induction principle encapsulates the depth calculation, and can be employed in the usual way using the induction tactic.

A tar file of the source code is available here. There are implementations for both collapsed syntax and the related tagged syntax. For each syntax,

• < Syntax Type >_Depth.v defines the depth measure and related tactis. The depth is incremented by one for every constructor.
• < Syntax Type >_Reflection.v demonstrates how decidability of local closure is proved by reflection.
• < Syntax Type >_Induction.v demonstrates how decidability of local closure can be proved directly using an induction principle which follows the structure of lc.

• < Syntax Type >_Depth_Binders.v defines another depth measure , incrementing the depth only when passing through a binder
• < Syntax Type >_Induction_Binders.v demonstrates how decidability of local closure can be proved directly using an induction principle which follows the structure of lc and using the depth measure in < Syntax Type >_Depth_Binders.v.