A New Approach to Abstract Syntax Involving Binders

Joint work with Jamie Gabbay (DPMMS)

The Fraenkel-Mostowski permutation model of set theory with atoms (FM-sets) can serve as the semantic basis of a meta-logic for specifying and reasoning about formal systems involving name-binding, alpha-conversion, capture-avoiding substitution, etc. Working in a suitable axiomatization of FM-sets, we show that this setting 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 invovling this 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 datatypes extends to encompass signatures invovling binding operators. In particular, there is an associated notion of primitive 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.

LS Home page or Talks in 1998/99