Given a TRS 
, a definitional tree
with pattern 
is an expression of the form
[Ant92]:
is a variant of a
rule 
.
(called the inductive position), 
are different
constructors for n>0, and each 
is a definitional tree with
pattern 
where k is the arity of 
and 
are new variables.
A defined symbol f is called inductively sequential
if there exists a definitional tree with pattern 
(where are different variables)
whose rule nodes contain all (and only) the rules defining f.
In this case, we say that is a definitional tree for f.
A TRS is inductively sequential if all its defined
function symbols are inductively sequential. An
inductively sequential TRS can be viewed as a set of definitional
trees, each defining a function symbol.
Figure 1: Definitional tree for the function first
Definitional trees are used for describing needed narrowing computations
as follows.
A function 
from
terms t and definitional trees to sets of triples
determines each evaluation step. Here, p is a
position in t, R is the rule to be applied, and
is a substitution which should be applied to t before reducing
it.
Given an operation-rooted term t
and a definitional tree with 
such that
, then 
is defined as follows
[AHLV99]:
This definition ensures that,
whenever 
,
is a valid narrowing step which
is called a needed narrowing step.
Needed narrowing only evaluates
subterms which are needed to compute a value and it is the
best narrowing strategy for inductively sequential TRSs due to its
optimality properties w.r.t. the
length of derivations and the independency of computed solutions
[AEH94].
