- Authors
- Claus-Peter Wirth
- Title
- Syntactic Confluence Criteria for Positive/Negative-Conditional Term Rewriting Systems
- In
- SEKI-Report SR-95-09, Univ. Kaiserslautern, 1995
Bibtex Entry
- Copyright Owner
- SEKI
- 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.
- Full paper
-
- Original version of 1995
-
- Format
- .ps.gz
- Size
- .6 Mbytes
- This site
-
../sr9509/original.ps.gz
- Original site
-
Uni KL site
- Slightly updated version
-
- Format
- .ps.gz
- Size
- .7 Mbytes
- This site
-
../sr9509/all.ps.gz
- Slightly updated version with some strange typesetting, but searchable!
-
- Format
- .pdf
- Size
- 1.3 Mbytes
- This site
-
../sr9509/pdf.pdf