Syntactic Confluence Criteria for 
Positive/Negative-Conditional 
Term Rewriting Systems

Claus-Peter Wirth
Fachbereich Informatik, Universitaet Kaiserslautern
D-67663 Kaiserslautern, Germany
E-mail: wirth@informatik.uni-kl.de

Abstract
We study the combination of the following already 
known ideas for showing confluence of unconditional 
or conditional term rewriting systems into 
practically more useful confluence
criteria for conditional systems:
Our syntactical separation into constructor 
and non-constructor symbols,
Huet's introduction and Toyama's generalization
of parallel closedness for non-noetherian 
unconditional systems,
the use of shallow confluence for proving confluence 
of noetherian and non-noetherian conditional systems, 
the idea that certain kinds of 
limited confluence can be assumed for
checking the fulfilledness or 
infeasibility of the conditions of 
conditional critical pairs,
and the idea that (when termination is given)
only prime superpositions have to be considered
and certain normalization restrictions can be applied
for the substitutions fulfilling the 
conditions of conditional critical pairs.
Besides combining and improving already known methods, 
we present the following new ideas and results:
We strengthen the criterion for overlay joinable 
noetherian systems, and, by using the expressiveness of 
our syntactical separation into constructor and 
non-constructor symbols, we are able to present 
criteria for level confluence that are 
not criteria for shallow confluence actually
and also able to weaken the
severe requirement of normality 
(stiffened with left-linearity) in the 
criteria for shallow confluence 
of noetherian and non-noetherian conditional systems
to the easily satisfied requirement of quasi-normality.
Finally, the whole paper may also give a practically useful
overview of the syntactical means for
showing confluence of conditional term rewriting systems.

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