A Locally-nameless Backend for Ott

Ott 0.10.15 (and previous versions) uses a fully-concrete representation for metavariables. It is up to the user to define the appropriate fully-concrete representation type for metavariables, e.g.:

metavar var,x ::= {{ coq nat }} {{ com term variable }}
metavar tvar,X ::= {{ coq nat }} {{ com type variable }}

Version 0.10.16 extends the Coq backend of Ott with experimental support for a locally-nameless representation (and co-finite quantification). The user can now specify that a metavariable must be represented in locally-nameless style, e.g.:

metavar var,x ::= {{ repr-locally-nameless }} {{ com term variable }}

As usual, metavariables can be bound in productions, using the bindspec language, as in the lam production below:

grammar
  term,t :: 'term_' ::= {{ com term }}
  | x :: :: var {{ com variable }}
  | \ x . t :: :: lam (+ bind x in t +) {{ com abstraction }}
  | t1 t2 :: :: app {{ com application }}
  | ( t ) :: S :: paren {{ coq [[t]] }}
  | { t1 / x } t2 :: M :: tsub {{ coq (open_term_wrt_term[[x t2]] [[t1]]) }}

This definition gives rise to the datatype term below:

Inductive term : Set :=
| term_var_b : nat -> term
| term_var_f : var -> term
| term_lam : term -> term
| term_app : term -> term -> term.

Remarks:
  1. Productions containing metavariables susceptible to be bound (e.g., term_var) give rise to two distinct constructors, one (term_var_b) for de Bruijn indices to be used when the metavariable is bound, one (term_var_f) for "free" variables. The type var, together with decidable equality and several useful lemmas and functions, is defined in the Metatheory library.

    In the current implementation, metavariables susceptible to be bound in a symbolic term (eg. the x in the term_var production) must be the only element of the production: in our experience, this did not turn out to be a restriction, but please let us know if your language definition requires more flexibility.

  2. Binder metavariables are erased from productions (eg. term_lam), as in de Bruijn representation.
Ott automatically generates the appropriate open functions and lc predicates to test if terms are locally-closed. The other support functions for substitutions and free-variables (subst and fv) are generated once the user declares the relevant substitutions and freevars sections.

Ott automatically compiles the symbolic terms that appear in rule definitions into the appropriate terms in locally-nameless style. For instance, the typing rule for the simply-typed lambda-calculus:

E,x:S |- t : T
---------------- :: lambda
E |- \x.t : S->T

is compiled into its locally-nameless representation:

Inductive typing : env -> term -> type -> Prop := (* defn typing *)
| ...
| typing_lambda : forall (L:vars) (E:env) (t:term) (S T:type),
   (forall x, x \notin L -> typing (E & x ~ S) (open_term_wrt_term t (term_var_f x)) T) ->
   typing E (term_lam t) (type_arrow S T).

For that, Ott follows the algorithm below. For each rule,
  1. for each nonterminal that appears in the rule, compute the maximal set of binders under which it appears: for example, in the rule lambda above, the maximal set of binders for the nonterminal t is the singleton x, and it is empty for all the other nonterminals;
  2. for each pair nonterminal / maximal binder set collected in phase 1., go over all the occurrences of the nonterminal in the rule and open them with respect to all the variables in the maximal binding set except those under which this particular occurrence is bound. In the example, this amounts to opening the occurrence of t in the premise with respect to the metavariable x;
  3. quantify using cofinite-quantification each metavariable that has been used to open a nonterminal;
  4. add hypothesis about local-closure to guarantee the invariant that if a derivation holds, then the top-level terms involved are locally-closed.
In some cases the user may want a finer control on which nonterminals are opened and with respect to which metavariables. Consider for instance the CBV beta-reduction rule:

----------------------- :: ax_app
(\x.t1) v2 --> {v2/x}t1

A naive application of the algorithm described above would open the right hand side occurrence of t1 with respect to a cofinitely-quantified x. Substitution should then be used to replace the occurrences of x with v2, resulting in the awkward term

reduce (term_app (term_lam t1) v2) (subst_term v2 x (open_term_wrt_term t1 (term_var_f x)))

Instead, an idiomatic translation of CBV beta-reduction rule would directly rely on the open function to substitute v2 for the bound occurrences of x in t1, as in:

reduce (term_app (term_lam t1) v2) (open_term_wrt_term t1 v2)

To let the user specify this translation behaviour, Ott 0.10.16 extends the syntax of production homomorphisms. Consider:

term,t :: 'term_' ::= ...
| { t2 / x } t1 :: M :: tsub {{ coq (open_term_wrt_term [[x t1]] [[t2]]) }}

In the homomorphism the nonterminal t1 is referred to with [[x t1]] instead of the usual [[t1]]: the prefixed x specifies that occurrences of t1 should not be opened with respect to the metavariable x. If this homomorphism is specified, then the translation of the ax_app rule is exactly idiomatic Coq shown above.

Current limitations: support for single binders only, no auxfn, Coq only.

Disclaimer: to compile rule definitions, Ott applies blindly the algorithm described above. Although in most of the cases, this generates a correct and idiomatic representation of the language, some language constructs might not be faithfully translated. Please, let us know if you find one of these cases.

Some examples: The generated Coq code requires the Metatheory library by Arthur Charguéraud.

The proof scripts are straightforward adaptations of the analogous scripts by Arthur Charguéraud. It would be easy to adapt Charguéraud's proofs for Fsub and Benton and Kouvatas' proofs for the nu-calculus.

Last update: 9-3-2009
 Copyright Francesco Zappa Nardelli