A New Approach to Abstract Syntax Involving Binders
Andrew M. Pitts,
Cambridge University Computer Laboratory,
Pembroke Street Cambridge CB2 3QG, UK
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.
The talk is based on joint work with Jamie Gabbay (DPMMS, Cambridge
University).
[slides, paper.]