 |
 |
|
|
|
|
|
|
Technical Report HW-MACS-TR-0053
| Title | Capture-Avoiding Substitution as a Nominal Algebra |
|---|
| Authors | Murdoch J Gabbay, Aad Mathijssen |
|---|
| Date | 2007-08-30 |
|---|
| Abstract | Substitution 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. |
|---|
| Group | ULTRA |
|---|
| Notes | |
|---|
| Download |   |
|---|
|
|
|
|
|
Email
Technical Report's Administrator |
|
 |
|
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 |
|
