Abstract

Métivier (1983) proved that every confluent and terminating rewrite system can be transformed into an equivalent canonical rewrite system. He also proved that equivalent canonical rewrite systems which are compatible with the same reduction order are unique up to variable renaming. In this note we present simple and formalized proofs of these results. The latter result is generalized to the uniqueness of normalization equivalent reduced rewrite systems.

BibTeX

@inproceedings{NHAMCS-IWC14,
  author    = "Nao Hirokawa and Aart Middeldorp and Christian Sternagel",
  title     = "Normalization Equivalence of Rewrite Systems",
  booktitle = "Proceedings of the 3rd International Workshop on Confluence",
  editor    = "Takahito Aoto and Delia Kesner",
  pages     = "14--18",
  year      = 2014
}