Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


Non-symmetric rewriting

Struth, Georg

MPI-I-96-2-004. June 1996, 20 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
Rewriting is traditionally presented as a method to compute normal forms in varieties. Conceptually, however, its essence are commutation properties. We develop rewriting as a general theory of commutation for two possibly non-symmetric transitive relations modulo a congruence and prove a generalization of the standard Church-Rosser theorem. The theorems of equational rewriting, including the existence of normal forms, derive as corollaries to this result. Completion also is purely commutational and we show how to
extend it to plain transitive relations. Nevertheless the loss of symmetry introduces some unpleasant consequences: unique normal forms do not exist, rewrite proofs cannot be found by don't-care nondeterministic rewriting and also simplification during completion requires backtracking. On the non-ground level, variable critical pairs have to be considered.
Acknowledgement: We wish to thank Leo Bachmair, David Basin, Harald Ganzinger, Krishna Rao, J├╝rgen Stuber and Uwe Waldmann
for helpful discussions on the subject of this paper.
Categories / Keywords: Transitive Relations, Rewriting, Commutation, Completion
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-96-2-004.dviMPI-I-96-2-004.psMPI-I-96-2-004.pdf94 KBytes; 251 KBytes; 262 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document:
Hide details for BibTeXBibTeX
  AUTHOR = {Struth, Georg},
  TITLE = {Non-symmetric rewriting},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-96-2-004},
  MONTH = {June},
  YEAR = {1996},
  ISSN = {0946-011X},