Sven,
Here is a small clarification about the interesting issues that
you raise. There is a difference in the definition of certain
functions that is not captured by the trees that you show.
For example,
und True x = x;
und x True = x;
is almost (weakly) orthogonal. The TRS is confluent and a viable
narrowing strategy is Parallel Narrowing. In some situations,
distinct "or" branches can be evaluated simultaneously.
However
p x y = isA x;
p x y = isB y;
is not orthogonal. The TRS may not be confluent. A viable
narrowing strategy for this function is Inductively Sequential
Narrowing (a generalization of Needed Narrowing).
The tree that you propose for this function seems inappropriate.
Very loosely speaking, Parallel Narrowing makes "or" choices in
the left-hand sides of rules, whereas Inductively Sequential
Narrowing makes "or" choices in the right-hand sides.
With Inductively Sequential TRSs you get, so to speak, all the
computing power of Almost Orthogonal TRSs (with both pros and
cons). Definitional trees for Inductively Sequential TRSs are (to
most practical purposes) unique, hence there is no need for the
programmer to specify them except for the flex/rigid option. This
option is probably given more conveniently by the programmer
without using trees.
I hope this helps a little.
Sergio
--------------------------------
Sergio Antoy
Dept. of Computer Science
Portland State University
P.O.Box 751
Portland, OR 97207
voice +1 (503) 725-3009
fax +1 (503) 725-3211
internet antoy_at_cs.pdx.edu
WWW
http://www.cs.pdx.edu/~antoy
--------------------------------
Received on Do Nov 05 1998 - 18:31:00 CET