Abstract

Semantic labelling is a powerful tool for proving termination of term rewrite systems. The usefulness of the extension to equational term rewriting described in Zantema (Fundamenta Informaticae 24, 1995) is however rather limited. In this paper we introduce a stronger version of equational semantical labelling, parameterized by three choices: (1) the order on the underlying algebra (partial order vs. quasi-order), (2) the relation between the algebra and the rewrite system (model vs. quasi-model), and (3) the labelling of the function symbols appearing in the equations (forbidden vs. allowed). We present soundness and completeness results for the various instantiations and analyze the relationships between them. Applications of our equational semantic labelling technique include a short proof of the main result of Ferreira et al. (LNCS 1450, 1998)—the correctness of a version of dummy elimination for AC-rewriting which completely removes the AC-axioms—and an extension of Zantema's distribution elimination technique to the equational setting.

BibTeX Entry

@inproceedings{OMG-CSL00,
 author    = "Hitoshi Ohsaki and Aart Middeldorp and J{\"u}rgen Giesl",
 title     = "Equational Termination by Semantic Labelling",
 booktitle = "Proceedings of the 14th Annual Conference of the European
              Association for Computer Science Logic",
 series    = "Lecture Notes in Computer Science",
 volume    = 1862,
 pages     = "457--471",
 year      = 2000,
 doi       = "10.1007/3-540-44622-2\_31"
}