A Computer Science Application of Permutation Models of Set
Theory
Andrew M. Pitts,
Cambridge University Computer Laboratory,
Pembroke Street Cambridge CB2 3QG, UK
Joint work with Murdoch J. Gabbay, DPMMS,
Cambridge University, Cambridge CB2 1SB, UK
Abstract
The permutation model of set theory with atoms (FM-sets)
devised by Fraenkel and Mostowski in the 1930s supports notions of
`name-abstraction' and `fresh name' that provide a new way to
represent, compute with, and reason about the syntax of formal
systems involving variable-binding operations. Inductively defined
FM-sets involving the name-abstraction set former (together with
cartesian product and disjoint union) can correctly encode syntax
modulo renaming of bound variables. 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 in computer science.
[slides]