Capture-avoiding substitution as a nominal algebra

Abstract. Substitution is fundamental to computer science, underly-ing for example quantifiers in predicate logic and beta-reduction in the lambda-calculus. So is substitution something we define on syntax on a case-by-case basis, or can we turn the idea of ‘substitution ’ into a math-ematical object? We exploit the new framework of Nominal Algebra to axiomatise sub-stitution. We prove our axioms sound and complete with respect to a canonical model; this turns out to be quite hard, involving subtle use of results of rewriting and algebra. 1