TY - GEN

T1 - Capture-avoiding substitution as a nominal algebra

AU - Gabbay, Murdoch

AU - Mathijssen, Aad

PY - 2006

Y1 - 2006

N2 - 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. © Springer-Verlag Berlin Heidelberg 2006.

AB - 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. © Springer-Verlag Berlin Heidelberg 2006.

UR - http://www.scopus.com/inward/record.url?scp=33845960554&partnerID=8YFLogxK

M3 - Conference contribution

SN - 3540488154

SN - 9783540488156

VL - 4281 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 198

EP - 212

BT - Theoretical Aspects of Computing - ICTAC 2006 Third International Colloquium, Proceedings

T2 - Third International Colloquium on Theoretical Aspects of Computing - ICTAC 2006, Proceedings

Y2 - 20 November 2006 through 24 November 2006

ER -