- Authors
- Claus-Peter Wirth
- Title
- Shallow Confluence of Conditional Term Rewriting Systems
- In
- J. Symbolic Computation, 2009, 44:60--98
Bibtex Entry
- Permanent URL
- http://dx.doi.org/10.1016/j.jsc.2008.05.005
- Copyright Owner
- Elsevier
- Abstract
-
Recursion can be conveniently modeled with
left-linear positive/negative-conditional term rewriting systems,
provided that non-termination, non-trivial critical overlaps,
non-right-stability, non-normality, and extra variables are admitted.
For such systems we present novel sufficient criteria for shallow confluence
and arrive at the first decidable confluence criterion admitting non-trivial
critical overlaps.
To this end, we
restrict the introduction of extra variables of right-hand sides
to binding equations
and require the critical pairs to have somehow complementary
literals in their conditions.
Shallow confluence implies [level] confluence,
has applications in functional logic programming, and
guarantees the object-level consistency of the underlying data types
in the inductive theorem prover QuodLibet