Closed nominal rewriting and efficiently computable nominal algebra equality
Logic in Computer Science
2010-09-16 v1 Programming Languages
Abstract
We analyse the relationship between nominal algebra and nominal rewriting, giving a new and concise presentation of equational deduction in nominal theories. With some new results, we characterise a subclass of equational theories for which nominal rewriting provides a complete procedure to check nominal algebra equality. This subclass includes specifications of the lambda-calculus and first-order logic.
Cite
@article{arxiv.1009.2791,
title = {Closed nominal rewriting and efficiently computable nominal algebra equality},
author = {Maribel Fernández and Murdoch J. Gabbay},
journal= {arXiv preprint arXiv:1009.2791},
year = {2010}
}
Comments
In Proceedings LFMTP 2010, arXiv:1009.2189