Module Ltree

Abstract syntax trees with binders and quantifiers

An abstract syntax tree with binders extends a basic first-order term structure with let bindings and quantifiers. The abstract syntax tree is parametrized by the three types of its symbols, its free variables and its sorts.

A basic term is a tree structure, where a term is either a leaf containing a symbol or a variable. A term can also be a node containing a symbol with one or more subterms. All symbols are variadic and arity constraints are not checked or enforced in this module.

For let bindings and quantifiers we add typed lambda abstractions and distinguish between free and bound variables. A typed lambda abstraction is a term where one or more variables are bound. We do nameless abstraction with de Bruijn indexes, hence a bound variables is just its index, whereas free variables are values of the type of free variables.

A let binding is a lambda abstraction of n bound variables together with n terms that are to be substituted for the bound variables. Quantifiers are just lambda abstractions.

In order to maintain invariants about de Bruijn indexes, the type of an abstract syntax term is private to this module and terms must be created with the appropriate constructors.

In addition, there is a type of flat terms, where the topmost let binding has been evaluated. An abstract syntax term can be converted to a flat term with the S.destruct function, which distributes let bindings over nodes and ensures that the top symbols of the term is a node, a leaf or a variable. Subterms of a nodes are abstract syntax terms with binders and S.destruct can be repeatedly applied to these subterms.

Tail-recursive fold and map functions are provided. The S.eval_t function presents the subterms bottom-up and right-to-left to the folding function and lazily evaluates all let bindings. It fails when the term contains quantifiers. The S.map function presents all subterms to the function, again bottom-up and right-to-left, let bindings are not unfolded. Hence, not every subterm is a proper abstract syntax term and the mapping function is given the number of let binding the subterm is under as an argument.

author

Christoph Sticksel