The Community for Technology Leaders
Logic in Computer Science, Symposium on (1999)
Trento, Italy
July 2, 1999 to July 5, 1999
ISSN: 1043-6871
ISBN: 0-7695-0158-3
pp: 214
Andrew Pitts , Cambridge University
Murdoch Gabbay , Cambridge University
ABSTRACT
The Fraenkel-Mostowski permutation model of set theory with atoms (FM-sets) can serve as the semantic basis of meta-logics for specifying and reasoning about formal systems involving name binding, alpha-conversion, capture avoiding substitution, and so on. We show that in FM-set theory one can express statements quantifying over `fresh' names and we use this to give a novel set-theoretic interpretation of name abstraction. Inductively defined FM-sets involving this name-abstraction set former (together with cartesian product and disjoint union) can correctly encode object-level syntax modulo alpha-conversion. In this way, the standard theory of algebraic data types can be extended to encompass signatures involving binding operators. In particular, there is an associated notion of structural recursion for defining syntax-manipulating functions (such as capture avoiding substitution, set of free variables, etc) and a notion of proof by structural induction, both of which remain pleasingly close to informal practice.
INDEX TERMS
abstract syntax, binding, set theory, permutation models
CITATION
Andrew Pitts, Murdoch Gabbay, "A New Approach to Abstract Syntax Involving Binders", Logic in Computer Science, Symposium on, vol. 00, no. , pp. 214, 1999, doi:10.1109/LICS.1999.782617
91 ms
(Ver 3.3 (11022016))