It has recently been proved that inductively sequential TRSs and Huet and Lévy's strongly sequential CB-TRSs coincide [HLM98]. In [HLM98], Hanus et al.\ also discuss the precise relation between definitional trees and Strandh's index trees [Str89], a data structure which was proved equivalent by Durand [Dur94] to Huet and Lévy's matching dags (i.e., the original data structure which serves to implement strongly needed reductions in strongly sequential TRSs [HL79, HL91]).
Roughly speaking, an index tree for an
orthogonal TRS 
is (despite its name) a directed acyclic graph whose
inner
nodes are index points, i.e., pairs 
,
where 
is a strict prefix of a lhs of (with the variables
replaced by a special symbol 
) and p is a strong index of
,
which satisfy some suitable conditions (see
[Dur94]). There is a special
root node
. Given a node and a
function symbol f, there is an (ordinary) arc from
to 
if either is an index
point or 
is a lhs of a rule whose variables
have been replaced by 's (in the
latter case, we discard q and just write
to denote this node at the end of an arc).
There are also failure arcs, which are used to proceed after a
failing partial matching without being compelled
to start from scratch.
Orthogonal TRSs such that a
corresponding index tree exists are called bounded TRSs.
Durand proved that the class of bounded TRSs and strongly sequential
TRSs
coincide [Dur94]. The proof
is based on the existence of a precise and immediate
correspondence between Huet and Lévy's matching dags and Strandh's
index trees.
According to the definition of index
trees, some nodes might not be reachable from the initial node
via ordinary arcs
(failure arcs can be necessary to access them). Strandh defined the
forward branching index trees, which are those index
trees such that all nodes
can be reached from the root
node through an ordinary path
[Str89],
and introduced
the class of forward branching TRSs ( 
) to contain those TRSs
which
admit a forward
branching index tree. Strandh proved (actually, that was the main aim
of [Str89]) that forward branching
index trees are suitable for
implementing incremental strongly needed reductions
and provided an algorithm which does perform incrementally.
Later on, and
following a different line of work, Toyama et al. investigated the
existence of the transitive strongly needed redexes, which can
be reduced incrementally also
[TSvEP93]. They did not provide any
particular data structure (comparable to forward branching index trees)
to ease the search for the redexes but only defined the
transitive TRSs ( 
) as those which grant the
transitive strongly needed reductions.
Durand showed that
[Dur94].
Huet and Lévy had previously defined a particular class of strongly sequential TRSs, namely the simple systems [HL79, HL91], with a very simple associated matching dag; actually, they showed that the corresponding matching dag is almost a tree (that is, the ordinary arcs and the corresponding nodes make up a tree, see [HL91], pages 439-440). Nevertheless, they did say nothing about the possibility of performing incremental reductions with simple systems; Huet and Lévy only noticed that there is a very simple algorithm for supplying a simple system with a matching dag. Durand and Salinier [DS93] demonstrated that simple systems are forward branching and, correspondingly, the matching dag which is associated to a simple system exactly coincides with the forward branching index tree which would be constructed using the algorithm in [Dur94]. As a consequence, it is possible to perform incremental reductions in simple systems.
By glueing together all these facts, and since
strongly sequential CB-TRSs (hence inductively sequential ones)
are simple systems [HL79, HL91], we get that the
forward branching index tree which corresponds to an inductively
sequential TRS is `almost' a tree. Actually, we can say that it
is a
tree since,
as a benefit of the constructor discipline,
failing arcs are not present in the index trees of
inductively sequential TRSs (see
Definition
2.21 of [Dur94] for more
details).
Now, by using the connection between index trees and definitional
trees given in [HLM98] we obtain,
from the forward branching index
tree associated to an inductively sequential system, a
forest of definitional trees which consists of the immediate subtrees
stemming from the special node .
On the other hand, the
nonexistence of failing arcs (in CB-TRSs)
allows
us a further refinement in the representation, which immediately
derives in our incremental definitional trees. This redeems
definitional trees from unnecessarily mimicking the structure of index trees
when we consider CB-TRSs.
Nevertheless, for arbitrary (possible non-constructor) simple
systems, the need to record failing arcs prevents one from
considering an index
tree as a simple collection of definitional trees.
On the other hand, Huet and Lévy and Strandh only considered rewriting computations, wheras our incremental trees do not only ease pattern matching but also support the variable instantiation in input terms which is necessary for the narrowing steps. In the following section, we give an incremental definition of needed narrowing which can be thought of as the functional logic counterpart of Strandh's algorithm for the incremental reduction of terms in forward branching TRSs [Str89].