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 -