[Home] [CV] [Publications]


Minus 1a5aa4f1c08b567c9107cba729de26bc87c17ab2b2f690eb45059193a1d6f587 A Theory of Binding Structures and Its Applications to Rewriting
Talcott, C. L. - 1993

Binding structures enrich traditional abstract data types by providing support for representing binding mechanisms and schematic presentations. They are intended to facilitate the representation and manipulation of symbolic structures such as programs, logical formulae, derivations, specifications and modules. The notion of binding structure generalizes de Bruijn notation, providing for generalized binding operators, named free variables, nameless bound variables, and syntactic contexts (expressions with holes or meta variables standing for substructures that have been removed, or not yet filled in) in a single framework. Binding structures capture the essence of higher-order abstract syntax, while presenting a first-order, structural/intensional view of binding. In this paper we present a theory of binding structures, and give examples of its application to rewriting. We define the set of binding structures as an abstract algebra, and define a general notion of parameterized homomorphism. A variety of operations on binding structures are presented as homomorphisms, and a collection of properties useful for developing applications is given. Three applications are presented: a generalized notion of term rewriting; a theory of unification for binding structures; and a set of structures and primitive rules intended to serve as a basis for design of rewriting components for (quantified) first-order reasoning systems.