For orthogonal term rewriting systems (TRSs), Huet and Lévy's strong
sequentiality provides a formal basis for the
mechanization of sequential, normalizing rewriting computations
[HL79, HL91]. In [HL79, HL91], Huet and Lévy defined the notion
of strongly needed redex and showed that, for the class of strongly
sequential
TRSs (SS), the steady reduction of strongly
needed redexes is normalizing. Huet and Lévy showed that the strong
sequentiality of a TRS is decidable. They also provided an algorithm to
identify a strongly needed redex within a reducible term, thus giving an
effective procedure for implementing rewriting computations: given an
input expression, first use Huet and Lévy's algorithm to find out a redex;
if
such a redex does not exist, then stop (the term is in normal
form); otherwise, reduce the redex using the (unique)
rule that can be applied; repeat these steps as long as possible.
Within Huet and Lévy's algorithm, the search for a new redex
after each replacement starts from the root of the term.
In general, only this way to proceed is safe;
nevertheless,
Strandh introduced the so-called
forward branching TRSs (FB) and provided an
algorithm
which does not only hit upon a strongly needed redex in the term but
also performs the corresponding replacement and resumes
the reduction process incrementally, that is, without
(necessarily) turning back
to the root of the term in order to start the search for a new redex
[Str89].
FB is a subclass of
SS [Dur94]. Strandh proved
that his incremental algorithm preserves the optimality and
normalizing properties of Huet and Lévy's reduction of strongly needed
redexes. Toyama et al. defined the class of transitive systems (TR) and
the notion of transitive index which, for transitive systems, can
be advantageously used for incremental evaluation of terms also
[TSvEP93]. Durand showed that
[Dur94].
Functional logic languages (see [Han94] for a
survey) with a complete operational semantics
are usually based on narrowing, an operational mechanism which
combines reduction (from the functional part) and variable
instantiation (from the logic part) [Hul80, Red85, Sla74].
A narrowing step instantiates variables of an expression
and then applies a reduction step to a redex of the instantiated expression.
Unfortunately, simple narrowing can have a
huge search space and great effort has been made to develop
sophisticated narrowing strategies without losing completeness.
Needed narrowing [AEH94] is currently the best complete
narrowing strategy due to its optimality properties
regarding the length of the derivations and the independence of computed
answers [AEH94].
Based on the notion of constructor system and inductive sequentiality
[Ant92], needed narrowing rebuilds, in the functional logic
setting, the unique (peerless) properties of the strongly needed reduction
of (pure) equational and functional programs
[O'D98, PvE93].
In [AEH94], needed narrowing is formalized by means of a
function 
which, for a given term, yields the position, rule,
and
substitution to be applied in order to reduce the considered expression.
Therefore, the
function accomplishes the role of Huet and Lévy's
procedure to implement needed reduction and, similarly to that one,
the corresponding calculus is not incremental.
For constructor systems, inductive sequentiality and strong sequentiality
coincide [HLM98].
Since it is known that constructor strongly sequential systems are
forward branching [DS93], it seems
reasonable to consider the possibility to define an incremental
needed narrower which is able to efficiently conduct needed functional
logic reductions. In this paper, we first give an incremental
definition
of needed narrowing and demonstrate that it is strongly
equivalent to the original function (also concerning its
optimality results [AEH94]) and more efficiently implementable
thanks
to the incremental extent. Our incremental
definition covers two different features of the implementation of needed
narrowing: first, we provide an incremental definition of the
data structure which is used to guide needed narrowing computations,
namely,
the
definitional trees, and then we formalize an incremental definition of
, i.e., an incremental procedure which actually implements needed
narrowing computations.
We have applied our
techniques to the optimization of the multi-paradigm language
Curry [HKMN95, HAK 
99],
an extension of Haskell [HPW92] which is supported by an
international initiative with the aim of becoming a standard in the area and
whose operational model is based on needed narrowing.
We prove that all the proposed optimizations are actually
(and independently) effective by comparing a basic, non-optimized
version of UPV-Curry (a novel, public
implementation of Curry [EAL98]), and three refined implementations.
Finally, we provide an experimental comparison of our
implementation and other existing Curry interpreters, namely
TasteCurry and PACS-TasteCurry, the most popular
(and, the only public currently available)
implementations of Curry.
Compiling functional logic
programs into another high-level language
for which efficient implementations
exist is a well known technique for the efficient
implementation of integrated languages [Han94].
Compilation into Prolog is the most popular option
[BCG 89, LLR93, Han95].
Prolog-based implementations
implicitly reap the benefits of incrementality
thanks to Prolog's SLD resolution mechanism.
Unfortunately, no formal demonstration that
these kinds of implementations fit the original
(nonincremental) semantics of Curry had been provided before.
By having proved the strong equivalence between the standard Curry
semantics and the incremental one, our work can be thought of
as a formal warranty that compiling functional logic programs
into Prolog code is not only simple and
practical but also reliable.
A similar argument applies to those
implementations based on abstract narrowing machines [KLMR90],
which also enjoy the incrementality
implicitly which is embedded into standard compilation techniques.
On the other hand, programmers working on other implementation techniques can also rely on the present work for achieving incremental evaluation safely. Although it cannot compete with an implementation based on the compilation into low-level (abstract) machine code, our interpreter written in Prolog demonstrates that all optimizations are effective and could generate new insights for further developments in this field.
In Section 2, we give some Preliminares. Section 3 describes the proposed incremental optimization of definitional trees. Section 4 formalizes the incremental needed narrowing calculus. Section 5 gives some experimental results. Section 6 concludes. Benchmark programs are given in Appendix.