Substitution is fundamental to computer science, underlying 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 mathematical object?
We exploit the new framework of Nominal Algebra to axiomatise substitution. 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.
|Title of host publication||Theoretical Aspects of Computing - ICTAC 2006 (Proceedings 3rd International Colloquium, Tunis, Tunisia, November 20-24, 2006)|
|Editors||K. Barkaoui, A. Cavalcanti, A. Cerone|
|Place of Publication||Berlin|
|Publication status||Published - 2006|
|Name||Lecture Notes in Computer Science|