Confluence without Termination via Parallel Critical Pairs

Bernhard Gramlich
Fachbereich Informatik, Universitaet Kaiserslautern
Postfach 3049, D-67653 Kaiserslautern, Germany
E-mail: gramlich@informatik.uni-kl.de

Abstract
We present a new criterion for confluence of (possibly) non-terminating
left-linear term rewriting systems. The criterion is based on certain
strong joinability properties of parallel critical pairs. We show
how this criterion relates to other well-known results, consider some
special cases and discuss some possible extensions. 

Keywords
confluence without termination, strong confluence, 
parallel critical pairs, left-linear term rewriting systems

Source
anonymous FTP server ftp.uni-kl.de [131.246.94.94]
path: /reports_uni-kl/computer_science/SEKI/1995/
file: Gramlich.SR-95-13.ps.gz