next up previous
Next: Experiments Up: Uniform Lazy Narrowing: Experiments Previous: Uniform Lazy Narrowing: Experiments


Improving Needed Narrowing Implementations

Before we illustrate the availability of these improvements by means of some small experiments, we argue how it is possible to increase the efficiency of functional logic computations by using a uniform term rewriting system instead of a semantically equivalent simple uniform term rewriting system for representing the original program.

Consider the uniform program

\begin{displaymath}
\begin{array}{lll}
R_1: f(a, a) \to a &    R_2: g(a) \to a &    R_3: g(b) \to b.
\end{array}\end{displaymath}

This program can be transformed into the following simple uniform program:

\begin{displaymath}
\begin{array}{ll}
R_{11}: f(a, X) \to f_1(X) &    R_{12}: f_1(a) \to a \\
R_2: g(a) \to a &    R_3: g(b) \to b
\end{array}\end{displaymath}

by exploiting from left to right the inductive positions $1$ and $2$ of $f$ in the original program. Now, given the term $t = f(X, g(X))$, the following uniform lazy narrowing derivation can be proven:

\begin{displaymath}
\begin{array}{l}
f(x,g(x)) \stackrel{\!\!\! [2,R_2,\{X/a\}]...
...,R_1,id]
\;}{{\leadsto}_{\scriptscriptstyle ULN}} a
\end{array}\end{displaymath}

whereas, for the corresponding simple uniform program, uniform lazy narrowing only computes the following derivation:

\begin{displaymath}
\begin{array}{l}
f(x,g(x)) \stackrel{\!\!\! [\mbox{\footnot...
...R_12,id]
\;}{{\leadsto}_{\scriptscriptstyle ULN}} a
\end{array}\end{displaymath}

that consumes an extra step.

In general, when we transform a uniform program into a simple uniform program, we increase the number of rules proportionally to the number of inductive positions in the corresponding definitional trees. As a consequence, the number of computation steps also grows. Due to the strong equivalence between needed narrowing and uniform lazy narrowing over the class of uniform programs, we can reduce the size of the program and avoid unnecessary extra calls, while preserving the intended needed narrowing semantics of the implementation, by compiling the original program into a uniform program.


next up previous
Next: Experiments Up: Uniform Lazy Narrowing: Experiments Previous: Uniform Lazy Narrowing: Experiments
Pascual Julian Iranzo 2002-09-06