Tech Reports Home Contact
Technical Report Series
Submit Report
Browse Reports
Information for Authors
Contact Details

Technical Report HW-MACS-TR-0053

TitleCapture-Avoiding Substitution as a Nominal Algebra
AuthorsMurdoch J Gabbay, Aad Mathijssen
AbstractSubstitution is fundamental to the theory of logic and computation. Is substitution something that we define on syntax on a caseby-case basis, or can we turn the idea of ‘substitution’ into a mathematical object? We give axioms for substitution and prove them sound and complete with respect to a canonical model. As corollaries we obtain a useful conservativity result, and prove that equality-up-to-substitution is a decidable relation on terms. These results turn out to be hard and involve subtle use of techniques both from rewriting and algebra. A special feature of our method is the use of Nominal Techniques. These give us access to a stronger assertion language, which includes so-called ‘freshness’ or ‘capture-avoidance’ conditions. This means that the sense in which we axiomatise substitution (and prove soundness and completeness) is particularly strong, while remaining quite general.


Email Technical Report's Administrator
|MACS Home| Top of the Page

Department of Computer Science, Heriot-Watt University, Riccarton, Edinburgh, EH14 4AS, +44 (0) 131 4514152

Last Updated: 02 September 2003 © Copyright Heriot-Watt University, Disclaimer