Abstract

Type introduction is a useful technique for simplifying the task of proving properties of rewrite systems by restricting the set of terms that have to be considered to the well-typed terms according to any many-sorted type discipline which is compatible with the rewrite system under consideration. A property of rewrite systems for which type introduction is correct is called persistent. Zantema showed that termination is a persistent property of non-collapsing rewrite systems and non-duplicating rewrite systems. We extend his result to the more complicated case of equational rewriting. As a simple application we prove the undecidability of AC-termination for terminating rewrite systems. We also present sufficient conditions for the persistence of acyclicity and non-loopingness, two properties which guarantee the absence of certain kinds of infinite rewrite sequences.

BibTeX Entry

@inproceedings{OM-LFCS97,
 author    = "Hitoshi Ohsaki and Aart Middeldorp",
 title     = "Type Introduction for Equational Rewriting",
 booktitle = "Proceedings of the 4th Symposium on Logical Foundations of
              Computer Science",
 series    = "Lecture Notes in Computer Science",
 volume    = 1234,
 pages     = "283--293",
 year      = 1997,
 doi       = "10.1007/3-540-63045-7\_29"
}