*******************************************************************

Title: Conditional Confluence

Topic: Confluence of Terminating CTSRs
       - types: 0, 1, 2, 3
       - equality: semi-equational, join, normal, oriented

Abstract: aspects for abstract
- confluence criteria for terminating conditional rewrite systems
- unified presentation of known confluence criteria plus extended
  ones, 
- revised uniform proofs, 
- practical importance of conditional rewriting
- (inherent) difficulty and complexity of conditional rewriting

Structure of the paper:
- abstract
- introduction
- preliminaries (on trs and ctrs)
- basic problems in conditional rewriting
- confluence criteria with proofs and counterexamples (main part) 
- comparison with related work, discussion, related topics
- conclusion

Presentation / terminology:
- omit (2.2) in favour of (3)? probably yes!
- give tables for results (criteria / types of CTRSs /
  counterexamples)  


Questions / to be considered: 
- all/other types of CTRSs considered?
- syntactic/semantic notions of critical peaks covered?
- (un)decidability / computability issues
- examples (also new ones, from different domains)
- local vs. global versions of confluence criteria
- weakening(s) of normality possible?
- counterexamples to omitting any condition
- weakenings of decreasingness (for oriented deterministic CTRSs): 
  quasi-reductive, quasi-simplifying

Contributions:

Differences to previous results as already published (important for
journal publication!): 
- uniform presentation in a unifying framework
- previous preliminary presentations of these results scattered around
  in several papers
- new: stronger local versions of (1) and (2.1)
- improvements / generalizations / extensions:
  - slightly generalized versions of decreasingness
    - require solvability of condition for considered substitutions
      before ordering checks; strictly more general, but non-effective
      in general
    - left-to-right decreasingness
    - compatibility with a termination pair
  - new / simplified counterexamples
- systematic study of different types of CTRSs

Underlying papers: mainly the following:
(1) Dershowitz/Okada/Sivakumar, CADE'88 
     1:   confluence via decreasingness
(2) Dershowitz/Okada/Sivakumar, CTRS'87 
     2.1: confluence via left-linearity, normality plus shallow joinability
     2.2: confluence via overlay systems with joinable critical pairs
(3) Gramlich/Wirth, RTA'96
     3:   confluence via quasi-overlay joinability of shared parallel
          critical peaks, generalizes overlay criterion of (2.2))

Related papers:
- Bergstra/Klop, JCSS'86
  - orthogonal normal 2-CTRSs are (level-/shallow-) confluent
- Toyama'87: membership conditional rewrite systems
- Dershowitz, CADE'90
- Dershowitz/Okada, FGCS'88
- Dershowitz/Okada, LICS'88
- Gramlich, CAAP'96
- Wirth, PhDthesis'97
- Avenhaus/Loria-Saenz, LPAR'94 (Uwe shold have proceedings):
  - strongly deterministic and quasi-reductive 3-CTRSs with joinable
    critical pairs are confluent (study proof!): induction
    wrt. subterm ordering:
    - proper critical pair case easy
    - variable overlap easy
    - improper (self-overlap) case: interesting part where the
      restrictions are exploited
- Suzuki/Middeldorp/Ida, RTA'95:
  - level-(shallow-)confluence of orthogonal properly oriented
    right-stable 3-CTRSs
  - proof uses extended parallel rewriting relation; extends to join
    system and to systems with infeasible critical pairs, with local
    definitions, and with strict equality
  - consider generalization by imposing (some decreasing-like)
    termination and joinability of (certain) critical pairs!

Related topics:
- confluence criteria without termination
- logicality of CTRSs
- modularity
- transformational techniques
- (un)decidability / effectiveness / infinitary issues in conditional
  rewriting, regarding in particular:
  - one-step reduction
  - joinability of critical pairs
  - (in)feasibility of critical pairs

Results obtained:
(1)   Decreasing join 2-CTRSs with joinable critical pairs are confluent.
(2.1) Terminating, left-linear normal 2-CTRSs with shallow joinable
      critical pairs are confluent (shallow confluent).
      [try to extend this result!!!]
(2.2) Terminating 2-CTRSs are confluent, if all critical pairs are
      joinable overlays.
(3)   Terminating 2-CTRSs with quasi-overlay joinable shared parallel
      critical peaks are confluent.
    
Proof structures:
(1)   Prove confluence by induction wrt. the decreasing ordering.
(2.1) Prove confluence by induction on the pair (m+n, s) wrt. the
      lexicographic combination of >_nat and the terminating reduction
      relation 
(2.2) Prove the following more general result:
      Lemma: R terminating join 2-CTRS s.t. all critical pairs are
             joinable overlays. Then: If u[s]_Pi -->* v and s -->* t,
             then u[t]_Pi and v are joinable.
      Proof by induction on the triple (s, n, u[s]) wrt. the
      lexicographic combination of
      - (--> \cup proper_subterm_relation)
      - natural number ordering
      - -->
(3)   Prove the following (more general) technical key result:
      Lemma: Let R be join 2-CTRS s.t.
             (*) all feasible innermost instances of all shared
                 parallel critical peaks of R are quasi-overlay joinable.
             Then: for every s \in T(F,V) with SN(s), every t \in
                   T(F,V), very u,v \in T(F',V), every Pi s.t. u|_pi =
                   s for all pi \in \Pi: If s -->*R' v and s -->*R t,
                                         then u[t]_Pi -->*R' o <--*R' v.
      Proof (of the slightly strengthened generalized version) by
      induction on the complexity measure M(s,t,u,v,Pi) = <s,n,k>
      using the lexicographic combination of 
      - >_1=(--> \cup proper subterm)+_{below \var{s}}
      - >_nat
      - >_nat
      Corollary: In any join 2-CTRS satisfying (*), any terminating
                 term is confluent (localized).
      Corollary: Any terminting 2-CTRS satisfying (*) is confluent.
      Corollary: Any terminating 2-CTRS with quasi-overlay joinable
                 shared parallel critical peaks is confluent.
      Extension: use orderings and adapt (*)


Setting (which types/classes of systems):


*******************************************************************

Uebrigens scheint das mit den Variablenbedingungen rechts (plus links!)
doch nicht so ganz trivial, und wie ich glaube bei Dir in SR-95-09
auch falsch: Zum Beipiel hat, wenn ich mich nicht taeusche, das (join)
CTRS 

  fc -> a
  fd -> b 
  fe -> e'
  x  -> y  <== fy = a, fy = b, fx = e'

nach Deiner Definition ueberhaupt keine feasible critical peaks, ist
aber nicht (lokal) konfluent: Das Problem ist ein nichttrivialer
root-self-overlap der letzten Regel (in eine Variable!):

  c <- e -> d, mit c,d irreduzibel

*******************************************************************