© University of Kent - Contact | Feedback | Legal | FOI | Cookies
Infinitary rewriting: meta-theory and convergence
Stefan Kahrs
Acta Informatica, 44(2):182-196, May 2007.Abstract
When infinitary rewriting was introduced by Kaplan et.al. at the beginning of the 1990s, its term universe was explained as the metric completion of a metric on finite terms. The motivation for this connection to topology was that it allowed to import other well-studied notions from metric spaces, in particular the notion of convergence as a replacement for normalisation.
This paper generalises the approach by parameterising it with a term metric, and applying the process of metric completion not only to terms but also to operations on and relations between terms. The resulting meta-theory is studied, leading to a revised notion of infinitary rewrite system. For these systems a method is devised to prove their convergence.
Bibtex Record
@article{2523,
author = {Stefan Kahrs},
title = {Infinitary rewriting: meta-theory and convergence},
month = {May},
year = {2007},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2007/2523},
publication_type = {article},
submission_id = {4765_1178623837},
ISSN = { 0001-5903},
journal = {Acta Informatica},
volume = {44},
number = {2},
publisher = {Springer},
}