School of Computing

An efficient representation of arithmetic for term rewriting

D. Cohen and P. Watson

In R. Book, editor, Rewrite Techniques and Applications, Proceedings of the 4th Conference on Rewrite Techniques and Applications, Como, Italy, 1991, volume 488 of Lecture Notes in Computer Science, pages 182-196. Springer Verlag, January 1991.

Abstract

We give a locally confluent set of rewrite rules for integer (positive and negative) arithmetic using the familiar system of place notation. We are unable to prove its termination at present, but we strongly conjecture that rewriting with this system terminates and give our reasons. We show that every term has a normal form and so the rewrite system is normalising.

We justify our choice of representation in terms of both space efficiency and speed of rewriting.

Finally we give several examples of the use of our system.



Bibtex Record

@inproceedings{726,
author = {D. Cohen and P. Watson},
title = {An efficient representation of arithmetic for term rewriting},
month = {January},
year = {1991},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1991/726},
    booktitle = {Rewrite Techniques and Applications, Proceedings of the 4th Conference on Rewrite Techniques and Applications, Como, Italy, 1991},
    editor = {R. Book},
    publisher = {Springer Verlag},
    refereed = {Yes},
    series = {Lecture Notes in Computer Science},
    volume = {488},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014