Capture-avoiding substitution as a nominal algebra

Murdoch Gabbay, Aad Mathijssen

Research output: Contribution to journalArticlepeer-review

35 Citations (Scopus)


Substitution is fundamental to the theory of logic and computation. Is substitution something that we define on syntax on a case-by-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 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. © 2008 British Computer Society.

Original languageEnglish
Pages (from-to)451-479
Number of pages29
JournalFormal Aspects of Computing
Issue number4-5
Publication statusPublished - Jul 2008


  • Binding
  • Capture-avoidance
  • Nominal algebra
  • Nominal rewriting
  • Nominal techniques
  • Omega-completeness
  • Substitution


Dive into the research topics of 'Capture-avoiding substitution as a nominal algebra'. Together they form a unique fingerprint.

Cite this