de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Report

Non-symmetric rewriting

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons45565

Struth,  Georg
Programming Logics, MPI for Informatics, Max Planck Society;

Locator
There are no locators available
Fulltext (public)

1996-2-004
(Any fulltext), 11KB

Supplementary Material (public)
There is no public supplementary material available
Citation

Struth, G.(1996). Non-symmetric rewriting (MPI-I-1996-2-004). Saarbrücken: Max-Planck-Institut für Informatik.


Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-9FEC-B
Abstract
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.