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. In the final part of the paper we show how our results on persistence give rise to new modularity results.

@article{MO-AI00,
 author    = "Aart Middeldorp and Hitoshi Ohsaki",
 title     = "Type Introduction for Equational Rewriting",
 journal   = "Acta Informatica",
 volume    = 36,
 number    = 12,
 pages     = "1007--1029",
 year      = 2000,
 doi       = "10.1007/PL00013300"
}