\documentstyle[lib/tex/defpaper]{article}
\setnormaldefaults
\addtolength{\oddsidemargin}{-.35in}
\addtolength{\textwidth} {+.5in}
\addtolength{\topmargin} {-.4in}
\addtolength{\textheight} {.4in}
\input{psfig}

% \renewcommand{\baselinestretch}{1.1}
\renewcommand{\ifff}{\mbox{$ :- $}}
% \renewcommand{\spcrunch}{}

\title{Controlling the Search in Bottom-Up Evaluation\thanks{
This work was supported by a David and Lucile Packard Foundation Fellowship
in Science and Engineering, a Presidential Young Investigator Award,
with matching grants from Digital Equipment Corporation, Tandem and Xerox,
and NSF grant IRI-9011563.}}

\author{Raghu Ramakrishnan ~~~~~ Divesh Srivastava ~~~~~ S. Sudarshan\\
Computer Sciences Department,\\
University of Wisconsin-Madison, WI 53706, U.S.A.\\
\{raghu,divesh,sudarshan\}@cs.wisc.edu}

\date{}

\begin{document}
\bibliographystyle{alpha}

\maketitle

\begin{abstract}
Bottom-up evaluation of queries on deductive databases has
many advantages over an evaluation scheme such as Prolog.
It is sound and complete with respect to the declarative
semantics of least Herbrand models for positive Horn clause programs,
and in many database 
applications much more efficient than Prolog due to its set-orientedness.
These advantages have made bottom-up evaluation the 
evaluation strategy of choice for deductive databases.
However, a completely breadth-first search strategy has certain
disadvantages.  For example, intuitive unique model semantics have
been proposed for several classes of programs with negation (and
aggregation).  To evaluate programs according to these semantics,
it is necessary to order the inferences; in essence, we must evaluate
all answers to a negative subgoal before making an inference that
depends upon the negative subgoal.  As another example, the depth-first
strategy of Prolog is attractive when only one solution is required.

With these observations as the motivation, we 
present a technique to order the use of generated subgoals that is 
a hybrid between pure breadth-first and pure depth-first search.
The technique, called {\sf Ordered\_Search},
can be understood in terms of a ``subgoal-dependency graph''.
Intuitively it generates several immediate children of a subgoal together,
then chooses one of them to evaluate, and evaluates it completely before
considering the other children.
This provides some of the benefits of a depth-first search strategy while
retaining several of the benefits of bottom-up evaluation, 
including soundness, completeness for DATALOG, the non-repetition property, 
and set-oriented generation of answers to subgoals.
(However, there is a cost:  the technique is not complete for programs with
function symbols.)

We demonstrate the power of the {\sf Ordered\_Search} technique through two
applications.  First, we show that {\sf Ordered\_Search} 
can be used to evaluate programs
with modularly stratified negation and aggregation
more efficiently than with any previously known technique.
Second, we illustrate its use for optimizing single-answer queries.
In particular, we prove that it is close to Prolog in this respect for 
linear programs.
\end{abstract}

\sections{Introduction}
\label{sec:intro}

Several studies (\cite{br:ont,r:mag,u:bot,s:ont,b:quer}) have shown
similarities between several top-down evaluation methods and Magic Templates
(or, Alexander Templates) based bottom-up evaluation methods for 
positive programs when all the answers to a query are desired.
In essence, the same goals and answers are generated by 
these methods when they use the same orderings of body literals in 
evaluating rules.  It is important to note that
there are important differences as well.
In particular, the order in which facts and subgoals are generated and 
used in top-down evaluation strategies is different from the order in 
which they are generated and used in bottom-up evaluations.
Top-down evaluations typically synchronize the generation of subgoals 
and answers to those subgoals, whereas bottom-up evaluations
generate facts asynchronously.
This difference is not relevant for positive programs when all 
answers to a query are desired.
However, when only a single answer to the query is desired, the order
in which facts are generated and used becomes important,
and the depth-first search strategy of a top-down evaluation scheme
such as Prolog can perform much better than the breadth-first
search strategy of bottom-up evaluation methods.
Again, when the program contains negation (or aggregation), the order 
in which inferences are performed becomes crucial to the correctness 
of the method, even when all answers to the query are desired.

\eat{
%%%%%%%%%%%%%%
There are three main aspects to the evaluation of logic programs:
(1)~generation of subgoals, 
(2)~selecting the order in which to use generated subgoals, and
(3)~generation of answers to the subgoals.
A subgoal could be used to generate further subgoals, and 
to generate answers to the subgoals.
Aspect~(2) above concerns itself with the point in the evaluation at which a
subgoal is first made available for use (in either generating new subgoals
or answers).  Once a subgoal is made available, it continues to be available
for the rest of the computation.  

A tuple-oriented top-down evaluation strategy like Prolog 
{\em synchronizes\/} all the three aspects.
Conceptually, a stack of generated subgoals is maintained and the top-most
subgoal on the stack is selected to be used.
A new subgoal is generated by resolving the top-most subgoal on the stack
against a rule, and answers are generated using answer substitutions.

Top-down evaluation can be simulated (to some extent) by bottom-up
evaluation by using Magic Templates rewriting (\cite{r:mag,ull:vol1and2}), 
where magic facts correspond to the subgoals set up during a 
top-down evaluation.
Bottom-up evaluation of the Magic Templates transformed program
generates subgoals and answers to the subgoals 
{\em asynchronously}, by applying program rules (in the rewritten 
program); this results in improved efficiency of evaluation compared 
to a (non-memoing) top-down evaluation~\cite{u:bot,rs91:tdvsbup}.
Further, all generated subgoals are available for use in the program 
evaluation immediately after they are generated.
Thus the order in which subgoals are selected to be used is, 
unlike top-down evaluation, {\em the same as\/} the order in 
which they are generated.
%%%%%%%%%%%%%%
}

We describe a memoing technique called {\sf Ordered\_Search}
that works on the transformed program obtained using 
Magic Templates rewriting, and is a hybrid between
tuple-oriented top-down evaluation and set-oriented bottom-up evaluation.
This technique generates subgoals and answers to subgoals asynchronously, 
as in bottom-up evaluation, while ordering the use of generated subgoals 
in a manner reminiscent of top-down evaluation. 
As a consequence, {\sf Ordered\_Search} is able to efficiently
evaluate modularly stratified programs \cite{ross:modstrat:full}
(see Sections \ref{sec:basicresults} and \ref{sec:spacetimeresults}),
and restrict the search space in many cases when we want a 
single answer to the query (see Section \ref{sec:ordresults}).
{\sf Ordered\_Search} compares favorably with other top-down and 
bottom-up methods for evaluating logic programs in the literature, 
and we present a summary below.

\begin{description}
\spcrunch
\item [Prolog]:
{\sf Ordered\_Search} is sound, complete for DATALOG and 
has the non-repetition property (i.e., no derivation step is repeated
in the evaluation).
Prolog is not complete even for DATALOG, nor does it have the non-repetition
property.
Also, Prolog does not evaluate the class of modularly stratified programs 
correctly.\footnote{Of course, a meta-interpreter can be written using Prolog
to evaluate such programs.}
Although {\sf Ordered\_Search} does give a measure of control for
single answer queries, the Prolog search strategy is still likely
to be superior in this respect 
(except for the class of linear programs; see Section 
\ref{sec:ordresults}).
%%%%%%
% However, the form of depth-first search used by Prolog is likely to be
% more useful when single answers to the query are desired.
%%%%%%

\item [QSQR and Extension Tables]:
Extension Tables \cite{d:ext} is similar to Prolog, 
except that it memos facts and goals and can detect loops.
QSQR \cite{v:rec} is a top-down, memoing set-oriented strategy
that is closely related to bottom-up evaluation with Supplementary Magic 
rewriting.
Like Prolog, these techniques cannot deal with modularly stratified
negation/aggregation.  The tuple-oriented search strategy of
Extension Tables is closer to Prolog, and is likely to be
more useful than {\sf Ordered\_Search} when single
answers are desired.  
(This method is complete for DATALOG, but not for programs
with function symbols.)
The ET* variant of Extension Tables and QSQR repeat computation, unlike
{\sf Ordered\_Search}.\footnote{There is a variant of QSQR, 
called QoSaQ~(\cite{v:qosaq}), and a variant of Extension Tables called
$ET_{interp}$ implemented in the XWAM~(\cite{w89:xwam}), 
that do not repeat computation.  
However, the other commments
with respect to QSQR and Extension Tables also apply to these variants.}

\item [Subquery Completion]:
Lefebvre~\cite{lef:agg} described a modification of QSQR
to handle a class of acyclic recursive aggregates.  This class is
strictly contained in the class of modularly stratified programs.
(See Section \ref{sec:rel:work} for details.)

\item [Bottom-up Evaluation]:
In computing all answers to a query for positive programs, 
{\sf Ordered\_Search} retains the space complexity of 
bottom-up evaluation, and for all practical purposes retains the
time complexity as well.
More precisely, if the original time complexity was $ O(N) $, the
time complexity of {\sf Ordered\_Search} is $ O(N \alpha(N)) $, where
$ \alpha(N) $, the inverse Ackermann function, grows extremely
slowly (for $N < 2^{32}, \alpha(N) \leq 4$).
Bottom-up evaluation without ordering of inferences cannot evaluate
programs with negation or aggregation; however, it is complete
for all positive Horn clause programs.
As we mentioned earlier, {\sf Ordered\_Search} is likely to be more
efficient for single-answer queries.

\item [Ross' Technique]:
{\sf Ordered\_Search} can evaluate a similar class of programs
as Ross~\cite{ross:modstrat:full}.
It is always at least as space efficient and, for all practical 
purposes, at least as time efficient as the technique described 
in \cite{ross:modstrat:full} to evaluate modularly stratified programs;
we also present examples where {\sf Ordered\_Search} improves on Ross' technique
by an order of magnitude in asymptotic space and time complexities.
\end{description}

\spcrunch
There are other proposed techniques that control the order of inferences
in a bottom-up evaluation in some way.
Sloppy Delta Iteration \cite{skgb87:sloppy} provides a way to ``hide''
facts until they are to be used.  Techniques for hiding facts are used
in \cite{ggz90:minmax,sr91:aggr} to evaluate programs with aggregate operations
efficiently.  These results are only tangentially related to {\sf Ordered\_Search}
since the (motivation as well as the nature of the) orderings considered
are quite different.  

The rest of this paper is organized as follows.
We begin by presenting some examples that motivate our work.
Preliminaries are covered in Section~\ref{sec:backgnd}.
The data structures and algorithms needed to evaluate a program using
{\sf Ordered\_Search} are described in Section~\ref{sec:works}.
We present results about the soundness, completeness, and 
efficiency of our procedure in Section~\ref{sec:o-s:results}.
In this section, we also characterize the order in which generated 
subgoals are selected to be used in terms of a depth-first traversal 
of the ``subgoal-dependency'' graph.
Related work is described in Section~\ref{sec:rel:work}, and
directions for future research are indicated in Section \ref{sec:concl}.

\subsections{Motivating Examples}
\label{sec:motiv:init}

\begin{namedexample} {Modular negation}
\label{ex:dumpross:1}
The class of programs with modular negation~\cite{ross:modstrat:full} 
naturally extends the class of programs with stratified
and locally stratified negation while retaining a two-valued model.
Consider the following modularly stratified 
program-query pair $\langle P_{even},Q_{even} \rangle$:
\logicprog{
\lrule {r1:} {even(X)} {pred(X,Y1), pred(Y1,Y), even(Y)} \\
\lrule {r2:} {even(X)} {pred(X,Y), \neg even(Y)} \\
\lfact {r3:} {even(0)} \\
\lheader {$pred(1,0). ~~  pred(2,1). ~~  \ldots ~~ pred(n,n-1)$} \\
\lquery {\neg even(m)} 
}

Ross~\cite{ross:modstrat:full} proposed a supplementary magic sets 
rewriting (SMR) of $\langle P_{even},Q_{even} \rangle$ in conjunction with
a bottom-up method for evaluating SMR($\langle P_{even},Q_{even} \rangle$).
This bottom-up method uses meta-variables and meta-level predicates to
incorporate information about negative dependencies into its computation.
We omit the details of SMR($\langle P_{even},Q_{even} \rangle$).
\eat{
%%%%%%%%
except to note that 
it has rules defining: $magic(even(X),+)$ (i.e., which subgoal was generated
positively), $magic(even(X),-)$ (i.e., which subgoal was generated negatively),
$dp(even(X),even(Y))$ (i.e., which negatively generated subgoal $even(X)$ 
depends positively on subgoal $even(Y)$), and
$dn(even(X),even(Y))$ (i.e., which negatively generated subgoal $even(X)$
depends negatively on subgoal $even(Y)$).
%%%%%%%%
}
\eat{
%%%%%%%%%%%%%%%%%
SMR($P$) includes the following rules (by unfolding rules defining
supplementary predicates) in addition to other rules, which are not
relevant for our purpose:
\setrulebodywidth{3.75in}
{
\logicprog{
\lrule {mr1:} {magic(even(Y),+)} {magic(even(X),\_), pred(X,Y1), \lbok 
		pred(Y1,Y)}\\
\lrule {mr2:} {magic(even(Y),-)} {magic(even(X),\_), pred(X,Y)} \\
\lfact {mr3:} {magic(even(10),-)} \\
\lrule {dr1:} {dp(even(X),even(Y))} {magic(even(X),-), magic(even(X),\_), \lbok
		pred(X,Y1), \lbok pred(Y1,Y)} \\
\lrule {dr2:} {dn(even(X),even(Y))} {magic(even(X),-), magic(even(X),\_), \lbok
		pred(X,Y)} \\
\lrule {dr3:} {dp(P,even(Y))} {dp(P,even(X)), magic(even(X),\_), \lbok
		pred(X,Y1), \lbok pred(Y1,Y)} \\
\lrule {dr4:} {dn(P,even(Y))} {dp(P,even(X)), magic(even(X),\_), \lbok
		pred(X,Y)}
}
}

Ross' algorithm to evaluate SMR($P$) would compute the facts
shown in Table~\ref{tbl:ross:ex1}.

\begin{table}
\centerline{
\begin{tabular}{|l|l|} \hline
Relation & Facts \\ \hline
$magic(even(X),-)$ & $X = 4, 3, 2, 1, 0$ \\
$magic(even(X),+)$ & $X = 2, 1, 0$ \\
$dp(even(X), even(Y))$ & $(X,Y) = (4,2), (3,1), (2,0), (4,0)$ \\
$dn(even(X), even(Y))$ & $(X,Y) = (4,3), (3,2), (2,1), (1,0), (4,1), (3,0)$ \\
\hline
\end{tabular}
}
\caption{Evaluation of SMR($P$) using Ross' Technique}
\label{tbl:ross:ex1}
\end{table}
%%%%%%%%%%%%%%
}
For $m \leq n$, Ross' approach on this example
would take $O(m^2)$ space and make $O(m^2)$ derivations since
it would compute and store all the dependencies between 
subgoals transitively.

The technique presented in this paper, {\sf Ordered\_Search}, would
only compute and store information about direct dependencies; hence, it would 
use $O(m)$ space and make $O(m)$ derivations in computing the query answer.  
(For more details, see Example~\ref{ex:dumpross:1:us}.)

The only other bottom-up technique we are aware of for computing 
modularly stratified models is the doubled program
technique of Kemp et al.~\cite{kss91:wfn} for computing well-founded 
models.
On this example, the doubled program approach would also use
$O(m)$ space and make $O(m)$ derivations.
However, if rule $r1$ were removed from $P_{even}$, the doubled
program approach to answering the query would make $O(m^2)$ 
derivations, though it would still use only $O(m)$ space.
Even on this modified program, {\sf Ordered\_Search} would 
compute the answer to the query using $O(m)$ space and making 
$O(m)$ derivations.
%%%%%%%%%%
% Top-down schemes such as ``subquery completion'' of \cite{lef:agg} would
% also be able to evaluate this program, though the efficiency depends on
% whether the QSQR or QoSaQ mechanism is used.
%%%%%%%%%%
\end{namedexample}

\begin{namedexample} {Obtaining a single answer}
\label{ex:choice:4}
There are many cases where the user may want a single answer to a query.
Consider, for example, the following program-query pair 
$\langle P_{path}, Q_{path} \rangle$. 
\logicprog{
\lrule {r1:} {path(X,Y,[X,Y])} {edge(X,Y)}\\
\lrule {r2:} {path(X,Y,[X|P])} {edge(X,Z), path(Z,Y,P)} \\
\lheader {$edge(1,2). ~~ edge(1,3). ~~ edge(2,1). 
	~~ edge(2,4). ~~ edge(3,4).$} \\
\lquery {path(1,4,X)}
}

A naive way of obtaining a single answer to the query is to evaluate 
the (magic transformed) program bottom-up until we get an answer to 
the query, and then terminate the evaluation.
With this approach, subgoals are solved in parallel as they are generated. 
Thus, there is likely to be a lot of redundant computation done 
before the first query answer is generated.

Note that a top-down, tuple-oriented evaluation strategy, like Prolog, 
would set up a query on $path$, and solve the subgoals in a 
depth-first fashion.
However, since there is a cycle in the $edge$ relation, Prolog
would not terminate on the given query.

The technique presented in this paper, {\sf Ordered\_Search}, would 
also solve subgoals in a depth-first fashion, but since it performs
memoing, it would not repeat computation and would terminate on this
program.
In general, it provides an alternative evaluation strategy to the
breadth-first strategy of bottom-up evaluation, and for many programs
(the above program is one such)
it would compute fewer facts than bottom-up evaluation.
(For more details, see Example~\ref{ex:choice:4:us}.)
\end{namedexample}

\sections{Preliminaries}
\label{sec:backgnd}

We assume familiarity with logic programming terminology
(see~\cite{lloyd:logic:pgm}) and the issues involved
in the bottom-up evaluation of logic programs.
For the purposes of this paper, a {\em program\/} is a set 
of {\em normal rules}.
The techniques described in this paper are applicable to 
programs with uninterpreted function symbols, though we 
restrict the programs to compute only ground facts.

We use the notion of a {\em subgoal-dependency graph\/} 
to characterize some of the results in this paper.
Intuitively, the subgoal-dependency graph of a program-query pair
is an AND/OR directed graph that characterizes the dependencies
between subgoals set up in a top-down evaluation.
Given a subgoal on the head of a rule, there are directed arcs in the
subgoal-dependency graph to each subgoal set up during the evaluation 
of the body of that rule.
We formalize this using SLP-trees and negation trees 
(see~\cite{ross:modstrat:full}) in the full version of the paper.

We assume the reader is familiar with the definition of
modularly stratified programs and the meaning of such programs
(see~\cite{ross:modstrat:full}).
Intuitively, a program is modularly stratified iff its mutually recursive
components are locally stratified once all instantiated rules
with a false subgoal that is defined in a ``lower'' component
are removed.
Consequently, in the subgoal-dependency graph for modularly 
stratified programs, there is no cyclic dependency 
involving a negated subgoal.
Ross'~\cite{ross:modstrat:full} technique as well as our technique
makes essential use of this property in evaluating programs with
modularly stratified negation.

\subsections{Modified Magic Templates Rewriting}
\label{sec:magic}

We also assume familiarity with Magic Templates rewriting and its 
supplementary variant (see~\cite{r:mag}).
Intuitively, the Magic Templates rewriting defines a new predicate
$m\_p$ (the magic predicate) for each predicate $p$ in the original 
program $P$.
The predicate $m\_p$ contains subgoals on $p$ that need to be solved.
Additional rules (derived from rules in $P$) that generate these
subgoals are introduced in the rewritten program.
Also, original program rules defining $p$ are guarded by an $m\_p$ 
literal that ensures that only $p$ facts matching the desired 
$m\_p$ subgoals are generated.
The supplementary variant of Magic Templates avoids some recomputation 
by identifying common subexpressions, but at the cost of storing 
additional relations.

For the purpose of this paper, we {\em modify\/} the Magic Templates
rewriting as follows:
(1)~For each (magic) predicate $m\_p$ in the Magic Templates 
transformed program $P^{mg}$, we create a new predicate $m\_p_{done}$, 
which contains those subgoals on $p$ that have been completely solved.
(2)~For each rule $R$ in $P^{mg}$, and for each negated literal, say 
$ \neg q_i (\overline{t_i})$ in the body of $R$, we add the literal
$ m\_q_{i_{done}} (\overline{t_i^1})$ to the body of $R$
just before the occurrence of $\neg q_i (\overline{t_i})$.

Intuitively, the literal $m\_q_{i_{done}} (\overline{t_i^1})$ will be
satisfied only when the complete set of $q_i$ answers matching
$\overline{t_i^1}$ have been computed.
Hence, this literal acts as a {\em guard\/} on the use of the subsequent 
negated $q_i$ literal.
In a similar fashion, we can also define the modified Supplementary 
Magic Templates rewriting.
In the rest of this paper, unless otherwise noted, when we refer to 
the (Supplementary) Magic Templates rewriting, we assume that 
this modification has been done.

\eat{
%%%%%%%%%%%%%%%%
\subsection*{Subgoal Dependency Relation}

A program is said to be {\em non-floundering\/} if each selected
negative subgoal is completely ground.

Consider a non-floundering program $P$, and a query $Q$, where
a query is a conjunction of literals.
For ease of exposition, we restrict ourselves to left-to-right sips, 
so that the leftmost subgoal is always selected.\footnote{
The definitions can be easily extended to handle other sips.}
In this section, we define when the solution of subgoal $Q_1$ ``depends on''
the solution of another subgoal $Q_2$.

\begin{nameddefinition} {SLP-trees} (\cite{ross:modstrat:full})
\label{def:slp:tree}
Let $P$ be a non-floundering program, and let $Q$ be a query.
We define the SLP-tree $T_Q$ for $Q$.
The root of $T_Q$ is $Q$.
If the query $Q'$ appears as a node of $T_Q$ then its children are obtained as
follows:

\begin{itemize}
\spcrunch
\item If $Q'$ is empty, then we call it a successful leaf.

\item Suppose that the leftmost literal $L$ in $Q'$ is positive.
Let $U_L$ be the set of program rules whose heads unify with $L$.
The children of $Q'$ are obtained by resolving $Q'$ with
(a variant of) each of the rules in $U_L$ over the literal $L$
using most general unifiers.
If there is no such $U_L$ then $Q'$ has no children, and is a failed leaf.

\item Suppose the leftmost literal $L$ in $Q'$ is negative, say $\neg A$.
(By our assumption about the absence of floundering, $L$ must be ground.)
Recursively construct the SLP-tree $T_A$ for $A$.

\begin{description}
\item [--] If $T_A$ is successful, then $Q'$ is a failed leaf.
\item [--] If $T_A$ is failed, then $Q'$ has a single child that is
formed by deleting $L$ from $Q'$.
\item [--] Otherwise, $T_A$ is an indeterminate leaf.
\end{description}
\end{itemize}

\spcrunch
\noindent
If $T_Q$ has a successful leaf, then $T_Q$ is {\em successful}.
If every leaf of $T_Q$ is failed, then $T_Q$ is {\em failed}.
Otherwise, $T_Q$ is {\em indeterminate}.

A {\em branch\/} of $T_Q$ is an acyclic path from the root of $T_Q$.
We associate with each successful leaf $V$ an {\em answer substitution},
which is the composition of the most general unifiers used along
the branch to $V$.
\end{nameddefinition}

\begin{nameddefinition} {Negation tree} (\cite{ross:modstrat:full})
Given a goal $G$, the {\em negation tree\/} $N_G$ is defined as follows:
The nodes of $N_G$ are goals, and the root of $N_G$ is $G$.
Let $H$ be any node of $N_G$.
For every atom $A$ for which $T_A$ is recursively constructed in 
constructing $T_H$, $A$ is a child of $H$.
\end{nameddefinition}

\begin{nameddefinition}{Depends on}
\label{def:subg:dep}
We say that the solution of subgoal $Q_1$ {\em depends on\/} the solution of 
another subgoal $Q_2$, if $Q_2$ is an instance of the leftmost literal
of some node in the SLP-tree $T_A$, where $A$ is a node in the
negation tree for $Q_1$.
\end{nameddefinition}

When the solution of subgoal $Q_1$ depends on the solution of subgoal $Q_2$,
we loosely use the notation ``subgoal $Q_1$ depends on subgoal $Q_2$''.
Note that, unlike \cite{ross:modstrat:full}, we do {\em not\/} 
distinguish between positive and negative dependencies.
%%%%%%%%%%%%%%%%
}

\eat{
%%%%%%%%%%%%%%%%
\subsection*{Basic Semi-Naive Evaluation}

\begin{nameddefinition} {Non-repetition property}
(\cite{rss:eval:full})
An evaluation of a program is said to have the {\em non-repetition property\/}
if no derivation step is repeated in the evaluation.
\end{nameddefinition}

A number of researchers including \cite{b:nai,b85:qeddb:sn,br:adijlp}
independently proposed an evaluation technique, which we call
{\em Basic Semi-Naive}, or BSN, that has the non-repetition property.
In this section, we informally describe BSN evaluation, and refer the 
reader to \cite{br:adijlp} for further details.

There are essentially two components to the BSN evaluation of a program $P$.
The first is a rewriting of the program that
defines ``differential'' versions of predicates,
in order to distinguish facts that have been newly generated (and not yet
used in derivations) from older facts.
For each predicate $p$ defined in $P$, we have four predicates:
$p^{old}$, containing facts derived prior to the previous iteration;
$\delta p^{old}$, containing facts derived in the previous iteration;
$p$, containing facts derived prior to the current iteration
($p = p^{old} \cup \delta p^{old}$), and 
$\delta p^{new}$, containing (newly derived) facts derived in this iteration.
The rewriting described in \cite{br:adijlp} generates $n$ rules 
from each rule in $P$ that contains $n$ derived literals.

The second component is a technique to apply the rewritten rules
and update these differentials, ensuring that
all derivations are made exactly once.
The semi-naive program rules are applied repeatedly in 
iterations until no new facts can be computed.
At the end of each iteration, the differential relations are updated
using Procedure {\sf SN\_Update} below.

\algorithm{
\> SN\_Update($ p_{i} $) \+ \\
\{ \+ \\
$ p_{i}^{old} := p_{i}^{old} \sqcup \delta p_{i}^{old} $. \\
\> /* no duplicate elimination is done by $\sqcup$. */ \\
$ \delta p_{i}^{old} := \delta p_{i}^{new} - p_{i}^{old} $. \\
$ \delta p_{i}^{new} := \phi $. \\
$ p_i := p_i^{old} \sqcup \delta p_i^{old}$. \- \\
\} \-
}
%%%%%%%%%%%%%%%%
}

\eat{
%%%%%%%%%%%%%%%%%%%%%%
We briefly describe BSN for programs rewritten using the standard
Magic Templates rewriting,
and refer the reader to \cite{rss90:eval} for further details.
Consider a program-query pair $\langle P,Q \rangle$.
Let $\langle P^{mg}, Q^{mg} \rangle$ be obtained from $\langle P,Q \rangle$ 
using Magic Templates rewriting (not modified as described in 
Section~\ref{sec:magic}).
There are essentially two components to the BSN evaluation of a program
$\langle P^{mg}, Q^{mg} \rangle$.

\begin{enumerate}
\spcrunch
\item The first is a rewriting of the program that
defines ``differential'' versions of predicates,
in order to distinguish facts that have been newly generated (and not yet
used in inferences) from older facts.
For each predicate $p$ defined in $P^{mg}$
(this includes the magic predicates), we 
have four predicates $p, p^{old}, \delta p^{old}$ and $\delta p^{new}$.

For each rule in $P^{mg}$ of the form:\footnote{
Since we are dealing with programs rewritten using Magic Templates, 
each rule in the rewritten program has at least one body occurrence
of a predicate defined by $P^{mg}$.}
\logicprog{
\lrule {R:} {p} {p_{1} , \ldots , p_{n} , q_{1} , \ldots , q_{m}}
}
where $ p_{1} , \ldots , p_{n} $ ($n>0$) are defined in $P^{mg}$ and 
$ q_{1} ,\ldots, q_{m} $ are EDB predicates, the following
$n$ (recursive) semi-naive rewritten rules are obtained 
(\cite{br:adijlp}) from $R$:

\logicprog{
\lrule {R_1:} {\delta p^{new}} {\delta p_1^{old},
p_2, \ldots, p_n, q_{1} , \ldots , q_{m}} \\
\lrule {R_2:} {\delta p^{new}} {p_1^{old}, \delta p_2^{old},
p_3, \ldots, p_n, q_{1} , \ldots , q_{m}} \\
 & \vdots \\
\lrule {R_n:} {\delta p^{new}} {p_1^{old}, p_2^{old}, \ldots,
p_{n-1}^{old}, \delta p_{n}^{old}, q_{1} , \ldots , q_{m}}
}

\item The second component is a technique to apply the rewritten rules
and update these differentials, ensuring that
all derivations are made exactly once.
Procedure {\sf BSN\_Evaluate($P^{mg}, Q^{mg}$)} below describes this component.
\end{enumerate}

\algorithm{
\> procedure BSN\_Evaluate($P^{mg}, Q^{mg}$) \+ \\
\{ \+ \\
Let $p_1, \ldots, p_n$ be the non-magic predicates defined in $P^{mg}$. \\
Let $m\_p_1, \ldots, m\_p_n$ be the magic predicates defined in $P^{mg}$. \\
Insert $Q^{mg}$ into the appropriate $\delta m\_p^{new}$ relation. \\
Let ${\cal R}$ be the rules of $P^{mg}$. \\
Let ${\cal R}_{SN}$ be the semi-naive rules obtained from ${\cal R}$ as 
	described. \\
repeat \+ \\
  for each predicate $p_i, 1 \leq i \leq n$, ~~ SN\_Update($p_i$). \\
  for each predicate $m\_p_i, 1 \leq i \leq n$, ~~ SN\_Update($m\_p_i$). \\
  Apply each rule in ${\cal R}_{SN}$ once. \- \\
until (no facts in any $\delta p^{new}$ or $\delta m\_p^{new}$ relation) \\
return answers to $Q^{mg}$. \- \\
\} \\
end BSN\_Evaluate \- 
}
%%%%%%%%%%%%%%%%%%%%%%
}

\sections{Ordered Search}
\label{sec:works}

We describe a memoing technique, which we call {\sf Ordered\_Search}, 
that works on the transformed program obtained using Magic Templates or
Supplementary Magic Templates rewriting, and is in
a sense a hybrid between pure (tuple-oriented) top-down evaluation 
and pure (set-oriented) bottom-up evaluation.
This technique generates subgoals and answers to subgoals asynchronously, 
as in bottom-up evaluation, while ordering the use of generated subgoals 
in a manner similar to top-down evaluation. 
We informally describe how {\sf Ordered\_Search} works on the transformed
program-query pair $\langle P^{mg},Q^{mg} \rangle$ and provide a detailed
algorithmic description in Appendix~\ref{sec:algs}.

First, we informally describe semi-naive bottom-up evaluation.
There are essentially two components to the semi-naive evaluation of 
a program.
The first component is a rewriting of the program that defines 
``differential'' versions of predicates, in order to distinguish 
facts that have been newly generated (and not yet used in derivations) 
from older facts.
The second component is a technique to apply the rewritten rules
and update these differentials, ensuring that
all derivations are made exactly once.
The semi-naive program rules are applied repeatedly in
iterations until no new facts can be computed, and
the differential relations are updated at the end of each iteration.

\subsections{An Overview}

The central data structure used by {\sf Ordered\_Search}, the $Context$,
is used to preserve ``dependency information'' between subgoals.
{\sf Ordered\_Search} can be understood as modifying semi-naive
bottom-up evaluation (\cite{br:adijlp}) as follows:

\begin{enumerate}
\spcrunch
\item 
Newly generated magic and supplementary facts 
are inserted in the $Context$ instead of being directly inserted in 
the differential relations.
Consequently, these facts are hidden 
from the evaluation.
(Other newly generated facts are inserted in the differential relations,
and made available to the evaluation, as usual.)
\item 
Magic and supplementary facts from $Context$ are {\em selectively\/} 
inserted into the differential relations (i.e., made available for 
further use by the evaluation) when no new facts can be derived
using the current set of facts available to the evaluation
(i.e., a fixpoint has been reached).
\end{enumerate}

\spcrunch
Thus, the $Context$ is used as an intermediate data structure
where magic and supplementary facts are hidden before they are
selectively made available to the evaluation.
The $Context$ stores the magic and supplementary facts in an ordered 
fashion, such that if magic fact (or subgoal) $Q_1$ ``depends on'' 
the magic fact (or subgoal) $Q_2$, then $Q_2$ is stored
after or along with $Q_1$ in the $Context$.
The order in which magic facts are selected for use ensures that $Q_2$ 
will be made available for use before $Q_1$ is considered to be 
completely evaluated.
When a fact in $Context$ is made available to the evaluation, it 
is said to be ``marked.''

\subsections{Data Structures: $Context$}

The $Context$ is a doubly linked list of nodes.
Each node in $Context$ has an associated set of magic facts and 
supplementary facts; a node is said to be ``marked'' if any fact
associated with the node is marked.
The sequence of marked nodes in $Context$ can be viewed as a subsequence
of the nodes of $Context$, and is also maintained as a doubly linked list.
The ordering of nodes in $Context$ satisfies the following invariants.
\begin{enumerate}
\spcrunch
\item All unmarked facts in nodes between 
two consecutive marked nodes have been derived from some marked fact 
in the earlier marked node; hence, the marked fact ``depends on''
these latter unmarked facts.
\item At least one marked fact in the latter
marked node has been derived from a marked fact in the earlier marked node.
\item If the set of facts in a marked node is {\em not\/} a singleton set,
then each fact in the set ``depends on'' the other facts in the set.
\end{enumerate}

\spcrunch
As a consequence of the above invariants, facts in a marked node 
``depend on'' facts in all later (marked and unmarked) nodes in 
the $Context$.
These claims are intended to provide some intuition about how 
$Context$ is used in {\sf Ordered\_Search}; they are stated formally 
later in the paper.

Along with each fact associated with a node in $Context$, we also 
keep a pointer to the (magic or supplementary) fact that was used 
to derive this fact.
This can be used to infer direct dependencies between subgoals.

\eat{
%%%%%%%%%%%%%%
Each node in $Context$ has the following fields.
\begin{itemize}
\item
$Subgoals:$  A link to a set of 
subgoals associated with the node; initially empty.
\item
$unmarkedSubgoals:$  A link to a set of 
``unmarked'' subgoals associated with the node; initially empty.
\item
$mark:$  Indicates marked/unmarked status of the node; initially unmarked.
\item
$next$ and $prev:$  Pointers to successor and predecessor $Context$ 
nodes; initially nil.
\item
$number:$  An integer node number; initially $0$.
%%%
% The numbers in this field are not necessarily continuous - collapsing of
% nodes can cause holes in this numbering.
%%%
\item
$nextMarked$ and $prevMarked:$  Pointers in a doubly linked list of
``marked'' nodes; initially nil.
\end{itemize}

\spcrunch
\noindent
Along with each subgoal in $Context$ we keep the following:
\begin{itemize}
\spcrunch
\item
$mark:$  Indicates marked/unmarked status of the subgoal; initially unmarked.
\item
$parent:$  The subgoal that was used to generate this subgoal.
\reminder{Reword this so that it is equally applicable to Magic
Templates and Supplementary Magic Templates.}
\end{itemize}
%%%%%%%%%%%%%%
}

\subsections{Algorithms}

We give an intuitive description of the {\sf Ordered\_Search} technique
and in the process make several claims informally.
These are formally stated and proved in the full version of the paper.

\noindent {\bf Inserting Facts into $Context$}

Newly generated magic and supplementary facts (obtained by applying
the semi-naive program rules defining magic and supplementary predicates)
are inserted in the $Context$ before they are selectively
made available to the evaluation.
When applying the semi-naive program rules, {\sf Ordered\_Search}
records which magic or supplementary fact was used to make each
derivation of each magic and supplementary fact.
(From the form of rules in the (Supplementary) Magic Templates 
transformation, there is exactly one such fact.)
Let $F_1$ be a newly computed magic/supplementary fact 
derived from magic/supplementary fact $F_2$.
\begin{itemize}
\spcrunch
\item
If $F_1$ is a magic fact $m\_p (\overline{t_1})$ that has been completely 
evaluated, it will be present in the $m\_p_{done}$ relation.

In this case, {\sf Ordered\_Search} does not insert $F_1$ in $Context$.
\item
Else, since magic/supplementary facts that have been made 
available for use but have not
been completely evaluated are marked in the $Context$, we know that 
$F_2$ occurs marked in $Context$.

The fact $F_1$ is now inserted in $Context$ as an (unmarked) node after the
(marked) node associated with $F_2$, and immediately before the next 
marked node after $F_2$ in $Context$.
(If there is no such marked node, $F_1$ is inserted at the top of 
$Context$.)
\end{itemize}

\spcrunch
Since $F_1$ is derived using $F_2$, ``answers'' to $F_1$ could 
be used in computing ``answers'' to $F_2$.
Insertion, as above, is used to maintain dependency information between 
subgoals within the $Context$ as a linear sequence.
The order in which facts from $Context$ are made available to the 
evaluation will ensure that $F_1$ is made available to the evaluation
before $F_2$ is said to be completely evaluated.

Duplicate elimination is now done in the $Context$ to ensure that there 
is at most one copy of $F_1$ in $Context$.
If there is more than one unmarked copy of $F_1$ in $Context$ at this stage,
only the ``highest'' copy of $F_1$ is retained.
If there is a marked copy of $F_1$ in $Context$, i.e., if $F_1$ has
already been made available to the evaluation, there are two 
possibilities:
\begin{itemize}
\spcrunch
\item 
If the marked copy of $F_1$ occurs after the unmarked copy,
only the marked copy of $F_1$ is retained in $Context$.
\item 
If the unmarked copy of $F_1$ occurs after the marked copy,
$F_1$ depends on itself.
We have thus detected a cyclic dependency between the set of all 
marked facts in $Context$ in between the two occurrences of $F_1$.
{\sf Ordered\_Search} recognizes this and collapses 
this set of marked facts into the node of 
the marked copy of $F_1$ in $Context$.
\end{itemize}

Collapsing marked facts into a single node when a cyclic dependency is
detected is essential to the correctness of the technique in the
presence of cycles in the subgoal-dependency graph.
(Note that in modularly stratified programs there can be positive
cyclic dependencies, but no negative ones.)
Since all these facts (cyclically) depend on each other, we cannot
guarantee that any of these facts is completely evaluated until we
know that all of them have been completely evaluated.

\noindent {\bf Making Facts Selectively Available}

Intuitively, a magic fact $Q_1$ on $Context$ (that has been made available to 
the evaluation) can be considered to be {\em completely evaluated\/} if:
\begin{enumerate}
\spcrunch
\item
no new facts can be generated using the currently available set 
of facts (i.e., the iterative application of the semi-naive rules has 
reached a fixpoint), and 
\item
every magic fact $Q_2$ that $Q_1$ depends on has been 
completely evaluated.
\end{enumerate}

\spcrunch
When no new facts can be computed using the set of available facts,
all facts from $Context$ above the node containing the highest 
unmarked fact in $Context$ are completely evaluated.
All these facts are removed from $Context$ and 
all magic facts among these are moved to the corresponding
$m\_p_{done}$ relations.
Thus, when (and no sooner than) a magic fact $m\_p (\overline{t_1})$ 
on $Context$ has been completely evaluated, it is moved to $m\_p_{done}$.

The highest node in $Context$ now contains at least one unmarked 
(magic or supplementary) fact.
{\sf Ordered\_Search} now chooses one such unmarked fact from $Context$,
marks it and makes it available to the evaluation by inserting it
in the corresponding differential relation.

\subsections{Motivating Examples Revisited}
\label{sec:motiv}

We briefly describe how {\sf Ordered\_Search} can be used to evaluate
the examples presented in Section~\ref{sec:motiv:init}.

\begin{figure}
\centerline{\hbox{
\psfig{figure=figures/even1.ps,height=3.0cm,bbllx=272pt,bblly=705pt,bburx=540pt,bbury=851pt}
\psfig{figure=figures/cyclicpath.ps,height=3.0cm,bbllx=220pt,bblly=743pt,bburx=490pt,bbury=885pt}
}}
\caption{Subgoal Dependency Graphs for Motivating Examples}
\label{fig:ex:dumpross:1:us}
\end{figure}

\begin{namedexample}{Obtaining a single answer}
\label{ex:choice:4:us}
Consider the program-query pair $\langle P_{path}, Q_{path} \rangle$
from Example~\ref{ex:choice:4}, where the user wants a single answer
to the query.
For this program-query pair, the subgoal-dependency graph is shown
in Figure~\ref{fig:ex:dumpross:1:us}.
Note that the subgoal-dependency graph has a cycle; consequently,
Prolog would not terminate on this example program-query pair.

\eat{
%%%%%%%%%%%%%%%%
The Supplementary Magic Templates rewriting of the above program-query
pair would result in $\langle P_{path}^{mg}, Q_{path}^{mg} \rangle$ below:
\logicprog{
\lrule {r1:} {path(X,Y,[X,Y])} {m\_path(X,Y), edge(X,Y)} \\
\lrule {r2:} {path(X,Y,[X|P])} {supp(X,Y,Z), path(Z,Y,P)} \\
\lrule {r3:} {supp(X,Y,Z)} {m\_path(X,Y), edge(X,Z)} \\
\lrule {r4:} {m\_path(Z,Y)} {supp(X,Y,Z)} \\
\lfact {Q^{mg}:} {m\_path(1,4)} \\
\lheader {$edge(1,2). ~~ edge(1,3). ~~ edge(2,1).
	~~ edge(2,4). ~~ edge(3,4).$}
}
%%%%%%%%%%%%%%%%
}

\begin{table}
\centerline{
\begin{tabular}{|c|c|l|} \hline
Iter Num & Facts & {\sf Ordered\_Search} \\ \hline
$0$ & $path$ & $\{ \}$ \\
  & $Context$ & $m\_path(1,4)$ \\ \hline 
$1$ & $path$ & $\{ \}$ \\
  & $Context$ & $m\_path(1,4)^{\ast}, supp(1,4,3), supp(1,4,2)$ \\ \hline
$2$ & $path$ & $\{ \}$ \\
  & $Context$ & $m\_path(1,4)^{\ast}, supp(1,4,3), supp(1,4,2)^{\ast},
			m\_path(2,4)$ \\ \hline
$3$ & $path$ & $\{ path(2,4,[2,4]) \}$ \\
  & $Context$ & $m\_path(1,4)^{\ast}, supp(1,4,3), supp(1,4,2)^{\ast},
			m\_path(2,4)^{\ast}, supp(2,1,4)$ \\ \hline
$4$ & $path$ & $\{ path(2,4,[2,4]), path(1,4,[1,2,4]) \}$ \\
  & $Context$ & $\{m\_path(1,4)^{\ast},supp(1,4,2)^{\ast},m\_path(2,4)^{\ast},
			supp(2,1,4)^{\ast}\}, supp(1,4,3)$ \\ \hline
\end{tabular}
}
\caption{{\sf Ordered\_Search} evaluation of 
    $\langle P_{path}^{mg}, Q_{path}^{mg} \rangle$}
\label{tbl:ex:choice:4:us}
\end{table}

The Supplementary Magic Templates transformed 
program $\langle P_{path}^{mg}, Q_{path}^{mg} \rangle$
is straightforward and we do not describe it
except to note that only one supplementary predicate $supp$ is created.
We describe the evaluation of $\langle P_{path}^{mg}, Q_{path}^{mg} \rangle$
using {\sf Ordered\_Search} briefly in Table~\ref{tbl:ex:choice:4:us}.
Facts in $Context$ marked with an $^{\ast}$ indicate facts made 
available to the evaluation.
Note that an answer is produced in iteration $4$, as in 
semi-naive bottom-up evaluation of 
$\langle P_{path}^{mg}, Q_{path}^{mg} \rangle$.
However, the evaluation using {\sf Ordered\_Search} has computed
fewer facts than would be computed by pure bottom-up evaluation.
Also note that a cycle was detected since
$m\_path(1,4)$ would also be derived from $supp(2,1,4)$, and this
magic fact occurs with an $^{\ast}$ earlier in $Context$.
As a result, in iteration $4$, several nodes in $Context$ have been
collapsed together.
\end{namedexample}

\begin{namedexample}{Modular negation}
\label{ex:dumpross:1:us}
Consider the modularly stratified program $P_{even}$ from
Example~\ref{ex:dumpross:1}, and the query $? \neg even(4)$.
For this program-query pair, the subgoal-dependency graph is shown
in Figure~\ref{fig:ex:dumpross:1:us}.

We omit the details of the Supplementary Magic Templates transformed
program $\langle P_{even}^{mg}, Q_{even}^{mg} \rangle$.
The evaluation of the supplementary magic program using {\sf Ordered\_Search}
computes and stores only information about direct dependencies
as a linear ordering of the magic and supplementary facts on 
$Context$; hence, the evaluation uses linear space and makes 
a linear number of derivations.

The technique described in \cite{ross:modstrat:full} computes and
stores the transitive dependencies in addition to the direct dependencies
on this example; consequently, it would use quadratic space and make
a quadratic number of derivations.
We omit details because of space limitations and describe this example
in detail in the full version of the paper.
\end{namedexample}

\eat{
%%%%%%%%%%%%%%%%
In this section, we give some example programs and describe their evaluation
using {\sf Ordered\_Search}.
In the first example, we illustrate how {\sf Ordered\_Search}
handles function symbols and non-ground terms.
The ``depends on'' relation for subgoals is acyclic in this example.

\begin{example} 
\label{ex:dfs:mpdone}
Consider the following program-query pair $\langle P,Q \rangle$:
\logicprog{
\lrule {r1:} {p(5)} {p(8)} \\
\lrule {r2:} {p(5)} {p(4), p(9)} \\
\lrule {r3:} {p(8)} {p(4), p(f(g(X)))} \\
\lrule {r4:} {p(9)} {p(8)} \\
\lfact {r5:} {p(4)} \\
\lfact {r6:} {p(f(X))} \\
\lquery {p(5)}
}

%%%%%%%%%%%%%%%%%%
% The subgoal-dependency graph is shown in Figure~\ref{fig:dfs:1:ex2}.
% 
% \begin{figure}
% \centerline{\psfig{figure=figures/dfsgoal1.ps,height=5.0cm,bbllx=319pt,bblly=718pt,bburx=469pt,bbury=925pt}}
% \caption{Subgoal Dependency Graph}
% \label{fig:dfs:1:ex2}
% \end{figure}
%%%%%%%%%%%%%%%%%%

Using complete left-to-right sips, Magic Templates would transform 
$\langle P,Q \rangle$ to $\langle P^{mg},Q^{mg} \rangle$ below:
\logicprog{
\lrule {r1:} {p(5)} {m\_p(5), p(8)} \\
\lrule {r2:} {p(5)} {m\_p(5), p(4), p(9)} \\
\lrule {r3:} {p(8)} {m\_p(8), p(4), p(f(g(X)))} \\
\lrule {r4:} {p(9)} {m\_p(9), p(8)} \\
\lrule {r5:} {p(4)} {m\_p(4)} \\
\lrule {r5:} {p(f(X))} {m\_p(f(X))} \\
\lrule {mr1:} {m\_p(8)} {m\_p(5)} \\
\lrule {mr2:} {m\_p(4)} {m\_p(5)} \\
\lrule {mr3:} {m\_p(9)} {m\_p(5), p(4)} \\
\lrule {mr4:} {m\_p(4)} {m\_p(8)} \\
\lrule {mr5:} {m\_p(f(g(X)))} {m\_p(8), p(4)} \\
\lrule {mr6:} {m\_p(8)} {m\_p(9)} \\
\lfact {Q^{mg}:} {m\_p(5)}
}
A possible evaluation of this program using 
{\sf Ordered\_Search($P^{mg}, Q^{mg}$)}
could proceed as shown in Table~\ref{tbl:dfs:1:ex2}.
The iteration number indicates the iteration of the inner
``{\sf repeat \ldots until}'' loop in Procedure
{\sf Ordered\_Search}.
\end{example}

\begin{table}
\centerline{
\begin{tabular}{|c|c|l|} \hline
Iteration Number & Relation & Facts \\ \hline
$0$ & $p$ & $\{ \}$ \\
 & $m\_p$ & $\{ \}$ \\
 & $m\_p_{done}$ & $\{ \}$ \\
 & $Context$ & $m\_p(5)$ \\ \hline
$1$ & $p$ & $\{ \}$ \\
 & $m\_p$ & $\{ m\_p(5) \}$ \\
 & $m\_p_{done}$ & $\{ \}$ \\
 & $Context$ & $m\_p(5)^{\ast}, m\_p(4), 
	m\_p(8)$ \\ \hline
$2$ & $p$ & $\{ \}$ \\
 & $m\_p$ & $\{ m\_p(5), m\_p(8) \}$ \\
 & $m\_p_{done}$ & $\{ \}$ \\
 & $Context$ & $m\_p(5)^{\ast}, 
	m\_p(8)^{\ast}, m\_p(4)$ \\ \hline
$3$ & $p$ & $\{ p(4) \}$ \\
 & $m\_p$ & $\{ m\_p(5), m\_p(8), m\_p(4) \} $ \\
 & $m\_p_{done}$ & $\{ \}$ \\
 & $Context$ & $m\_p(5)^{\ast}, 
	m\_p(8)^{\ast}, m\_p(4)^{\ast}$ \\ \hline
$4$ & $p$ & $\{ p(4) \}$ \\
 & $m\_p$ & $\{ m\_p(5), m\_p(8), m\_p(4) \} $ \\
 & $m\_p_{done}$ & $\{ \}$ \\
 & $Context$ & $m\_p(5)^{\ast},
	m\_p(9), m\_p(8)^{\ast}, m\_p(f(g(X))), m\_p(4)^{\ast}$ \\ \hline
$5$ & $p$ & $\{ p(4) \}$ \\
 Inner & $m\_p$ & $\{ m\_p(5), m\_p(8), m\_p(4) \} $ \\
 Loop & $m\_p_{done}$ & $\{ m\_p(4) \}$ \\
 Fixpoint & $Context$ & $m\_p(5)^{\ast},  
	m\_p(9), m\_p(8)^{\ast}, m\_p(f(g(X)))$ \\ \hline
$6$ & $p$ & $\{ p(4), p(f(g(X))) \}$ \\
 & $m\_p$ & $\{ m\_p(5), m\_p(8), m\_p(4), m\_p(f(g(X))) \} $ \\
 & $m\_p_{done}$ & $\{ m\_p(4) \}$ \\
 & $Context$ & $m\_p(5)^{\ast}, 
	m\_p(9), m\_p(8)^{\ast}, m\_p(f(g(X)))^{\ast}$ \\ \hline
$7$ & $p$ & $\{ p(4), p(f(g(X))), p(8) \}$ \\
 & $m\_p$ & $\{ m\_p(5), m\_p(8), m\_p(4), m\_p(f(g(X))) \} $ \\
 & $m\_p_{done}$ & $\{ m\_p(4) \}$ \\
 & $Context$ & $m\_p(5)^{\ast},
	m\_p(9), m\_p(8)^{\ast}, m\_p(f(g(X)))^{\ast}$ \\ \hline
$8$ & $p$ & $\{ p(4), p(f(g(X))), p(8), p(5) \}$ \\
 & $m\_p$ & $\{ m\_p(5), m\_p(8), m\_p(4), m\_p(f(g(X))) \} $ \\
 & $m\_p_{done}$ & $\{ m\_p(4) \}$ \\
 & $Context$ & $m\_p(5)^{\ast},
	m\_p(9), m\_p(8)^{\ast}, m\_p(f(g(X)))^{\ast}$ \\ \hline
$9$ & $p$ & $\{ p(4), p(f(g(X))), p(8), p(5) \}$ \\
 Inner & $m\_p$ & $\{ m\_p(5), m\_p(8), m\_p(4), m\_p(f(g(X))) \} $ \\
 Loop & $m\_p_{done}$ & $\{ m\_p(4), m\_p(f(g(X))), m\_p(8) \}$ \\
 Fixpoint & $Context$ & $m\_p(5)^{\ast},  
	m\_p(9)$ \\ \hline
$10$ & $p$ & $\{ p(4), p(f(g(X))), p(8), p(5), p(9) \}$ \\
 & $m\_p$ & $\{ m\_p(5), m\_p(8), m\_p(4), m\_p(f(g(X))), m\_p(9) \} $ \\
 & $m\_p_{done}$ & $\{ m\_p(4), m\_p(f(g(X))), m\_p(8) \}$ \\
 & $Context$ & $m\_p(5)^{\ast}, 
	m\_p(9)^{\ast}$ \\ \hline
$11$ & $p$ & $\{ p(4), p(f(g(X))), p(8), p(5), p(9) \}$ \\
 Inner & $m\_p$ & $\{ m\_p(5), m\_p(8), m\_p(4), m\_p(f(g(X))), m\_p(9) \} $ \\
 Loop & $m\_p_{done}$ & $\{ m\_p(4), m\_p(f(g(X))), m\_p(8), m\_p(9), m\_p(5) \}$ \\
 Fixpoint & $Context$ & \\ \hline
\end{tabular}
}
\caption{Evaluation of $\langle P^{mg},Q^{mg} \rangle$ 
using {\sf Ordered\_Search}}
\label{tbl:dfs:1:ex2}
\end{table}

The following example illustrates the evaluation of 
Procedure {\sf Ordered\_Search} in the presence of cyclic dependencies.

\begin{example}
\label{ex:o-s:cycles}
Consider the following program-query pair $\langle P,Q \rangle$:
\logicprog{
\lrule {r1:} {p(1)} {p(2)} \\
\lrule {r2:} {p(1)} {p(3)} \\
\lrule {r3:} {p(3)} {p(1)} \\
\lfact {r4:} {p(2)} \\
\lquery {p(1)}
}
Magic Templates would transform $\langle P,Q \rangle$ to give
$\langle P^{mg},Q^{mg} \rangle $ below:
\logicprog{
\lrule {r1:} {p(1)} {m\_p(1), p(2)} \\
\lrule {r2:} {p(1)} {m\_p(1), p(3)} \\
\lrule {r3:} {p(3)} {m\_p(3), p(1)} \\
\lrule {r4:} {p(2)} {m\_p(2)} \\
\lrule {mr1:} {m\_p(2)} {m\_p(1)} \\
\lrule {mr2:} {m\_p(3)} {m\_p(1)} \\
\lrule {mr3:} {m\_p(1)} {m\_p(3)} \\
\lfact {Q^{mg}} {m\_p(1)}
}
A possible evaluation of this program using 
{\sf Ordered\_Search($P^{mg}, Q^{mg}$)}
could proceed as shown in Table~\ref{tbl:cyc:1:ex3}.
The iteration number indicates the iteration of the inner
``{\sf repeat \ldots until}'' loop in Procedure
{\sf Ordered\_Search}.
A cyclic dependency is detected in iteration $2$, and the cycle of magic
facts is collapsed to a single node in $Context$.
\end{example}

\begin{table}
\centerline{
\begin{tabular}{|c|c|l|} \hline
Iteration Number & Relation & Facts \\ \hline
$0$ & $p$ & $\{ \}$ \\
 & $m\_p$ & $\{ \}$ \\
 & $m\_p_{done}$ & $\{ \}$ \\
 & $Context$ & $m\_p(1)$ \\ \hline
$1$ & $p$ & $\{ \}$ \\
 & $m\_p$ & $\{ m\_p(1) \}$ \\
 & $m\_p_{done}$ & $\{ \}$ \\
 & $Context$ & $m\_p(1)^{\ast}, m\_p(2), 
	m\_p(3)$ \\ \hline
$2$ & $p$ & $\{ \}$ \\
 & $m\_p$ & $\{ m\_p(1), m\_p(3) \}$ \\
 & $m\_p_{done}$ & $\{ \}$ \\
 & $Context$ & $\{ m\_p(1)^{\ast}, m\_p(3)^{\ast} \},
	m\_p(2)$ \\ \hline
$3$ & $p$ & $\{ p(2) \}$ \\
 & $m\_p$ & $\{ m\_p(1), m\_p(3), m\_p(2) \} $ \\
 & $m\_p_{done}$ & $\{ \}$ \\
 & $Context$ & $\{ m\_p(1)^{\ast}, m\_p(3)^{\ast} \},
	m\_p(2)^{\ast}$ \\ \hline
$4$ & $p$ & $\{ p(2), p(1) \}$ \\
 & $m\_p$ & $\{ m\_p(1), m\_p(3), m\_p(2) \} $ \\
 & $m\_p_{done}$ & $\{ \}$ \\
 & $Context$ & $\{ m\_p(1)^{\ast}, m\_p(3)^{\ast} \},
	m\_p(2)^{\ast}$ \\ \hline
$5$ & $p$ & $\{ p(2), p(1), p(3) \}$ \\
 & $m\_p$ & $\{ m\_p(1), m\_p(3), m\_p(2) \} $ \\
 & $m\_p_{done}$ & $\{ \}$ \\
 & $Context$ & $\{ m\_p(1)^{\ast}, m\_p(3)^{\ast} \},
	m\_p(2)^{\ast}$ \\ \hline
$6$ & $p$ & $\{ p(2), p(1), p(3) \}$ \\
 Inner & $m\_p$ & $\{ m\_p(1), m\_p(3), m\_p(2) \} $ \\
 Loop & $m\_p_{done}$ & $\{ m\_p(2), m\_p(3), m\_p(1) \}$ \\
 Fixpoint & $Context$ & \\ \hline
\end{tabular}
}
\caption{Evaluation of $\langle P^{mg},Q^{mg} \rangle$ 
using {\sf Ordered\_Search}}
\label{tbl:cyc:1:ex3}
\end{table}
%%%%%%%%%%%%%%%%
}

\sections{Results about Ordered Search}
\label{sec:o-s:results}

All results in this section are applicable to programs with 
function symbols, except where stated otherwise.
We also assume that the supplementary magic program evaluated by 
{\sf Ordered\_Search} computes only ground facts; range-restrictedness 
of the supplementary magic program is a sufficient syntactic 
condition to ensure this.

The correctness and ordering results in 
Sections~\ref{sec:basicresults} and \ref{sec:ordresults}
are also applicable to the case with non-ground facts.
However, the space and time complexity results in 
Section~\ref{sec:spacetimeresults} do not easily extend
to the non-ground case; intuitively, this is because 
{\sf Ordered\_Search} does not always maintain an irrset
(\cite{mr:dej}) representation of a non-ground relation.
(Details are given in the full version of the paper.)

\subsections{Results on Soundness, Completeness and Non-repetition}
\label{sec:basicresults}

\eat{
%%%%%%%%%%
\begin{nameddefinition}{SMTMS Programs}
\label{def:mtms}
Consider a left-to-right modularly stratified program-query pair
$\langle P, Q \rangle$, and complete left-to-right sips on rules of $P$.
The program $\langle P^{mg},Q^{mg} \rangle $ obtained by 
the Supplementary Magic Templates rewriting of $\langle P, Q \rangle$ is 
said to be a {\em SMTMS program}\footnote{
SMTMS program stands for Supplementary Magic Templates transformation of a
Modularly Stratified program.}.
\end{nameddefinition}
%%%%%%%%%%
}

Given a left-to-right modularly stratified program-query pair
$\langle P, Q \rangle$, we refer to the program obtained by
the Supplementary Magic Templates rewriting 
(as described in Section~\ref{sec:magic}) of $\langle P, Q \rangle$ as 
a {\em SMTMS program}.\footnote{SMTMS program stands for Supplementary 
Magic Templates transformation of a Modularly Stratified program.}
We use the term SMR($P$) to refer to the rewriting of program $P$
used by Ross in \cite{ross:modstrat:full} to evaluate modularly 
stratified programs.

%%%%%%%
% In comparing our technique with Ross, we assume that the same set
% of sips is chosen for both rewritten programs.
%%%%%%%

%%%%%%%%%%%%%%
% We can easily extend the definition of MTMS programs to allow for adornment. 
% that are range-restricted.
% For the magic program to be range-restricted, the adornment step of Magic 
% Templates rewriting (and rectification \cite{u:bot} in the case of
% DATALOG programs) needs to be done before the magic rewriting 
% described in Section~\ref{??}.
%%%%%%%%%%%%%%

\eat{
%%%%%%%%%%%%
Some of our results are for range-restricted MTMS programs.
In comparing our technique with the technique in \cite{ross:modstrat:full}
for DATALOG programs, 
we assume that rectification (see~\cite{u:bot}) has been performed prior
to the Magic Templates rewriting.
%%%%%%%%%%%%
}

%%%%%%%%%%
% When we make comparisons with other techniques (in particular, with
% Ross' technique) for range-restricted magic programs, we assume that 
% the steps of adornment (and rectification, in the case of DATALOG programs)
% have been performed by the other technique.
%%%%%%%%%%

%%%%%%%%
% We also conjecture that our results extend naturally to the 
% class of logic programs with finite negation trees~\cite{ross:modstrat:full}.
%%%%%%%%

\eat{
%%%%%%%%%%%%
The first result establishes a connection between the relative order of 
subgoals in $Context$ and the ``depends on'' relation between
subgoals (Definition~\ref{def:subg:dep}).

\begin{lemma}
\label{lm:o-s:depends:context}
Let $ \langle P^{mg}, Q^{mg} \rangle $ be an MTMS program.
Consider an evaluation of {\sf Ordered\_Search($P^{mg}, \lbok Q^{mg}$)}, 
and let $m\_p_j(\overline{t_2})$ be any marked subgoal in $Context$.
Then,

\begin{enumerate}
\spcrunch
\item If $m\_p_i(\overline{t_1})$ is any subgoal in $Context$ {\em after\/} 
$m\_p_j(\overline{t_2})$, the solution of $m\_p_j(\overline{t_2})$
depends on the solution of $m\_p_i(\overline{t_1})$, and

\item If $m\_p_i(\overline{t_1})$ is any subgoal in $Context$ in the
{\em same\/} node as $m\_p_j(\overline{t_2})$, the solution of 
$m\_p_j(\overline{t_2})$ depends on the solution of 
$m\_p_i(\overline{t_1})$, and the solution of $m\_p_i(\overline{t_1})$ 
depends on the solution of $m\_p_j(\overline{t_2})$.
$\Box$
\end{enumerate}
\end{lemma}
%%%%%%%%%%%%
}

\eat{
%%%%%%%%%%%%%%%%%%%%%%%
\begin{proof} 

NOTE: all the proofs in this section must work with induction on 
insertions.  Induction on separation is meaningless, since we need to 
then assume that the given structure already has some properties,
that can only  be proved by induction on insertions.
END NOTE.

By induction on the separation between nodes in $Context$.
First consider the case where $Context$ has no collapsed nodes.
Only the first part of the theorem needs to be proved.

\noindent Base Case: \\
Consider any subgoal $m\_pi(\overline{t_1})$ in $Context$ 
after $m\_pj(\overline{t_2})$ up to (and including) the next subgoal 
marked `$\ast$'.
These were put there by Procedure {\sf Add\_After} because 
\reminder{Prove this!}
$m\_pj(\overline{t_2})$ was used to compute $m\_pi(\overline{t_1})$.
Hence, $m\_pi(\overline{t_1})$ is a successor OR node of 
$m\_pj(\overline{t_2})$ in the subgoal-dependency graph.

\noindent Induction Case: \\
Let $m\_pk(\overline{t_3})$ be the next subgoal marked `$\ast$'
after $m\_pj(\overline{t_2})$.
By the induction hypothesis, for each subgoal $m\_pi(\overline{t_1})$ after 
$m\_pk((\overline{t_3})$ in $Context$, there is a path from
$m\_pk((\overline{t_3})$ to $m\_pi(\overline{t_1})$ in the 
subgoal-dependency graph.
From the base case, we know there is a path from
$m\_pj(\overline{t_2})$ to $m\_pk((\overline{t_3})$ in the 
subgoal-dependency graph.
By concatenating the two paths, we have a path from
$m\_pj(\overline{t_2})$ to $m\_pi(\overline{t_1})$ in the subgoal-dependency
graph.
This concludes the proof of the theorem, when $Context$ has no collapsed
nodes.

We next consider the case where $Context$ has collapsed nodes.
The proof of the two parts of the theorem are similar to above.
\reminder{Complete proof of theorem.}
\end{proof}
%%%%%%%%%%%%%%%%%%%%%%%
}

\eat{
%%%%%%%%%%%
Lemma~\ref{lm:o-s:mpdone} below indicates the order in which 
Procedure {\sf Ordered\_Search} completely evaluates subgoals.
First we need to establish that if subgoal $m\_p_i(\overline{t_1})$
depends on subgoal $m\_p_j(\overline{t_2})$, then every answer to
$m\_p_j(\overline{t_2})$ is available before we claim that 
$m\_p_i(\overline{t_1})$ is completely evaluated.
Once every subgoal $m\_p_i(\overline{t_1})$ depends on has been 
completely evaluated, and no new answers or subgoals can be generated
using the available facts (i.e., a fixpoint has been reached), we 
can conclude that $m\_p_i(\overline{t_1})$ has been completely evaluated.
Hence, we have:
%%%%%%%%%%%
}

\eat{
%%%%%%%%%%%%%
\begin{lemma}
\label{lm:o-s:mpdone}
Let $\langle P^{mg},Q^{mg} \rangle$ be an MTMS program obtained from
$ \langle P,Q \rangle$.
Consider an evaluation of {\sf Ordered\_Search($P^{mg}, Q^{mg}$)}.
If the solution of subgoal $m\_p_i(\overline{t_1})$ depends on the 
solution of subgoal $m\_p_j(\overline{t_2})$, every $p_j$ fact
that is an answer to $m\_p_j(\overline{t_2})$ in the well-founded
model of $ \langle P^{mg},Q^{mg} \rangle$ is present in the $p_j$
relation before $m\_p_i(\overline{t_1})$ is moved to $m\_p_{i_{done}}$.
$\Box$
\end{lemma}
%%%%%%%%%%%%%
}

The first result shows that magic facts are moved from $Context$
to the corresponding $m\_p_{done}$ relations only when the subgoal
has been completely evaluated.
This is the key result needed to show that {\sf Ordered\_Search}
computes the modularly stratified model of a program.

\begin{lemma}
\label{lm:o-s:mpdone}
Let $\langle P^{mg},Q^{mg} \rangle$ be a SMTMS program.
In an evaluation of {\sf Ordered\_Search($P^{mg}, \lbok Q^{mg}$)},
if a magic fact $m\_p(\overline{t_1})$ is present in the $m\_p_{done}$
relation, every $p$ fact that is an answer to $m\_p(\overline{t_1})$
in the modularly stratified model of $\langle P, Q \rangle$ is present 
in the $p$ relation.
$\Box$
\end{lemma}

The soundness result below then follows from the exhaustive nature of the 
evaluation and the correctness of the Supplementary Magic Templates 
rewriting with the $m\_p_{done}$ literals as guards for negative 
body literals.

\begin{theorem}
\label{thm:o-s:sound}
Let $\langle P^{mg},Q^{mg} \rangle$ be a SMTMS program.
An evaluation of {\sf Ordered\_Search($P^{mg}, \lbok Q^{mg}$)} is
{\em sound\/} wrt the modularly stratified semantics 
of $\langle P, Q \rangle$. 
$\Box$
\end{theorem}

\eat{
%%%%%%%%%%%%
\begin{proof} (Sketch)
By induction on the height of derivation trees in $P^{mg}$, show that all
required magic facts (goals) are included in the magic relation and used
in the computation.
\end{proof}
%%%%%%%%%%%%
}

Duplicate elimination of newly generated magic and supplementary
facts in $Context$ ensures that the evaluation does not 
repeat derivations.

\begin{theorem}
\label{thm:o-s:non-rep}
Let $\langle P^{mg},Q^{mg} \rangle$ be a SMTMS program.
An evaluation of {\sf Ordered\_Search($P^{mg}, Q^{mg}$)} has the 
non-repetition property.
$\Box$
\end{theorem}

\eat{
%%%%%%%%%%%%%
Note that in the presence of non-ground facts, some redundant derivations 
may be performed since we do not maintain an irredundant representation 
(see~\cite{mr:dej}) of the non-ground magic relations;
however, this does not compromise the non-repetition property.
%%%%%%%%%%%%%
}

\eat{
%%%%%%%%%%%%%%%%%%%
\reminder{Give a precise characterization of what it means to be
partially complete.}

\begin{theorem}
\label{thm:o-s:part:compl}
Let $\langle P^{mg},Q^{mg} \rangle$ be an MTMS program.
An evaluation of Procedure {\sf Ordered\_Search($P^{mg}, Q^{mg}$)} is
partially complete (as defined above) wrt the well-founded semantics 
for $\langle P^{mg},Q^{mg} \rangle$.
\end{theorem}
%%%%%%%%%%%%%%%%%%%
}

For modularly stratified programs with function symbols, there is 
no effective procedure that can guarantee completeness in general.
If there is an infinite sequence of subgoals, each depending 
on the next one in the sequence, and {\sf Ordered\_Search} 
chooses to explore such an infinite path, it may not compute an answer
to the original query, even if one exists.
Such paths cannot exist for DATALOG programs.
Hence, we have:

\begin{theorem}
\label{thm:o-s:gnd:datalog:compl}
Let $\langle P^{mg},Q^{mg} \rangle$ be a SMTMS DATALOG program.
An evaluation of {\sf Ordered\_Search($P^{mg}, \lbok Q^{mg}$)}
terminates and is complete wrt the modularly stratified semantics 
of $\langle P, Q \rangle$.
$\Box$
\end{theorem}

In general, we have that whenever the evaluation of a SMTMS 
program (even with function symbols) terminates, it is the 
modularly stratified model that is computed.

\subsections{Results about Space and Time Complexity}
\label{sec:spacetimeresults}

\eat{
%%%%%%%%%%%%%%%%
\begin{theorem}
\label{thm:o-s:subs:context}
Let $\langle P^{mg},Q^{mg} \rangle$ be an MTMS program.
Consider an evaluation of {\sf Ordered\_Search($P^{mg}, Q^{mg}$)}, and
let $m\_pi(\overline{t_1})$ be any subgoal in $Context$.

If $m\_pi(\overline{t_2})$ is any subgoal in $Context$ after 
$m\_pi(\overline{t_1})$, then $m\_pi(\overline{t_1})$ is not
subsumed by $m\_pi(\overline{t_2})$.
$\Box$
\end{theorem}
%%%%%%%%%%%%%%%%
}

\eat{
%%%%%%%%%%%%%%%%
\begin{proof} (Sketch)
Procedure {\sf Insert\_in\_Context} does the proper subsumption checks:
Step (b-i) inserts $m\_pi(\overline{t_1})$ into $Context$.
If it is subsumed by some later subgoal $m\_pi(\overline{t_2})$,
Step (b-ii) deletes the subgoal $m\_pi(\overline{t_1})$ from $Context$.
If $m\_pi(\overline{t_1})$ subsumes some earlier unmarked
subgoal $m\_pi(\overline{t_3})$, Step (b-iii) deletes the 
subgoal $m\_pi(\overline{t_3})$.
If $m\_pi(\overline{t_1})$ subsumes some earlier marked subgoal
$m\_pi(\overline{t_3})$, Step (b-iii) and Procedure 
{\sf Collapse\_Nodes} guarantees the result.
\end{proof}
%%%%%%%%%%%%%%%%
}

\eat{
%%%%%%%%%%
\begin{lemma}
\label{lm:o-s:sz:context}
Let $\langle P^{mg},Q^{mg} \rangle$ be an MTMS program.
In an evaluation of {\sf Ordered\_Search($P^{mg}, \lbok Q^{mg}$)},
the size of $Context$ is proportional to the number of distinct magic 
facts generated.
\end{lemma}
%%%%%%%%%%
}

%%%%%%%%%%%%%%%%%%%
% If $\langle P^{mg},Q^{mg} \rangle$ is range-restricted,
% and if $S$ is the space used by the facts in the magic and non-magic 
% relations, the evaluation of {\sf Ordered\_Search} takes space $O(S)$.
%%%%%%%%%%%%%%%%%%%

\eat{
%%%%%%%%%%
Note that in the presence of non-ground facts, ``distinct'' does {\em not\/}
mean ``irredundant.''
%%%%%%%%%%
}

In maintaining an auxiliary data structure, the $Context$, 
{\sf Ordered\_Search} uses more space than ordinary semi-naive
bottom-up evaluation (which only needs to maintain differential
relations).
One of the main results in this section is that there is no increase 
in asymptotic space complexity compared to other bottom-up 
evaluation strategies.
Intuitively, this is so because duplicate elimination on the $Context$ 
guarantees that the same set of facts are computed by the various 
evaluation strategies, and the space used by $Context$ is proportional to 
the space used by the magic and supplementary facts.

\begin{theorem}
\label{thm:o-s:space:gnd}
Let $\langle P^{mg},Q^{mg} \rangle$ be the result of the 
Supplementary Magic Templates transformation of program-query pair 
$\langle P,Q \rangle$.

\begin{enumerate}
\spcrunch
\item If $\langle P,Q \rangle$ is positive, let a bottom-up semi-naive
evaluation of $\langle P^{mg},Q^{mg} \rangle$ use space $S$.
Then, an evaluation of {\sf Ordered\_Search($P^{mg}, Q^{mg}$)}
uses space $O(S)$.

\item If $\langle P,Q \rangle$ is modularly stratified and 
$\langle P^{mg},Q^{mg} \rangle$ is a SMTMS program, let an evaluation of 
$\langle P,Q \rangle$ using the algorithm in {\rm \cite{ross:modstrat:full}}
to evaluate SMR($P$) use space $S$.
Then, an evaluation of {\sf Ordered\_Search($P^{mg}, Q^{mg}$)}
uses space $O(S)$.
$\Box$
\end{enumerate}
\end{theorem}
%%%%%%%%%%%%
% The claim can be strengthened for positive programs and non-ground
% computations, since Procedure {\sf Ordered\_Search} is easily
% modified so that it takes space $O(S)$ on all positive programs.
%%%%%%%%%%%%
Note that Ross' algorithm to evaluate SMR($P$) may use
asymptotically more space than {\sf Ordered\_Search}.
For instance, in Example~\ref{ex:dumpross:1}, Ross' algorithm uses
$O(m^2)$ space, whereas {\sf Ordered\_Search} uses $O(m)$ space.
Hence, our algorithm for evaluating modularly stratified programs is 
{\em strictly better\/} than the algorithm in \cite{ross:modstrat:full},
in terms of the asymptotic space complexity.

\eat{
%%%%%%%%%%%%%%%
In the presence of non-ground computations, no strategy dominates the other.
Sometime we may have to maintain say, both $m\_p(1)$ and $m\_p(X)$ in 
the $Context$ simultaneously, and use more space than Ross' evaluation 
strategy.
In other cases, storing the kind of dependency information computed
in \cite{ross:modstrat:full} may result in Ross' evaluation strategy 
taking up more space.
%%%%%%%%%%%%%%%
}

\eat{
%%%%%%%%%%%%%%%%
\begin{proof} 
\reminder{Change proof to reflect collapsing of nodes.}
Let $S_P$ be the space taken by the non-magic facts, and 
$S_M$ the space taken by the magic facts, in a bottom-up 
evaluation of $\langle P^{mg},Q^{mg} \rangle$.
Then, $S = S_P + S_M$.
In an evaluation of Procedure {\sf Ordered\_Search($P^{mg}, Q^{mg}$)},
the space taken by non-magic facts remains unchanged.
However, each magic fact $m\_p(\overline{a})$ could be stored twice:
one copy in the $m\_p$ relation, and one copy, either in
the $m\_p_{done}$ relation or in $Context$.
(Note that no magic fact can appear both in the $m\_p_{done}$ 
relation and in $Context$.)
Hence, the total amount of space taken by magic facts in an
evaluation of Procedure {\sf Ordered\_Search($P^{mg}, Q^{mg}$)} is
$O(S_M)$.
This concludes the proof.
\end{proof}
%%%%%%%%%%%%%%%%
}

The next few results compare the asymptotic time complexity of 
{\sf Ordered\_Search} compared to other bottom-up evaluation strategies.
We first compare the number of inferences made.

\begin{lemma}
\label{lm:o-s:num:deriv}
Let $\langle P^{mg},Q^{mg} \rangle$ be the result of the Supplementary 
Magic Templates transformation of program-query pair $\langle P,Q \rangle$.

\begin{enumerate}
\spcrunch
\item If $\langle P,Q \rangle$ is positive, let a bottom-up 
evaluation of $\langle P^{mg},Q^{mg} \rangle$ make $D_P$ derivations.
Then, an evaluation of {\sf Ordered\_Search($P^{mg}, Q^{mg}$)}
also makes $D_P$ derivations.

\item If $\langle P,Q \rangle$ is modularly stratified and 
$\langle P^{mg}, Q^{mg} \rangle$ is a SMTMS program, let an evaluation of
$\langle P,Q \rangle$ using the algorithm in {\rm \cite{ross:modstrat:full}}
to evaluate SMR($P$) make $D_P$ derivations.
Then, an evaluation of {\sf Ordered\_Search($P^{mg}, Q^{mg}$)}
makes no more than $ D_P$ derivations.
$\Box$
\end{enumerate}
\end{lemma}

Note that Ross' algorithm to evaluate SMR($P$) may make 
asymptotically more inferences than {\sf Ordered\_Search}.
For instance, in Example~\ref{ex:dumpross:1}, Ross' algorithm to 
evaluate SMR($P$) makes $O(m^2)$ inferences, whereas 
{\sf Ordered\_Search} makes $O(m)$ inferences.
%%%%%%%%
% In the presence of non-ground facts, Procedure {\sf Ordered\_Search}
% may make more inferences than other evaluation strategies since we 
% do not always maintain irredundant representations of relations.
%%%%%%%%

\eat{
%%%%%%%%%%%%%
\reminder{Describe the parts of each step, and the time it takes to 
implement each step for the ground case.}
%%%%%%%%%%%%%
}

In order to obtain the total time taken by the evaluation in terms
of the asymptotic cost of derivations, we need to obtain the cost of each 
derivation in the {\sf Ordered\_Search} evaluation.
As shown in \cite{rs91:tdvsbup}, unification of ground facts can
be done in constant time using hash-consing
\cite{sg76:hashcons} for ground terms;
indexing and insertion of ground facts in relations can also be 
done in constant time using hash based indexing.

\eat{
%%%%%%%%%%%%%
\begin{assumption}
\label{ass:const:time}
We make the following assumptions wrt the costs of the various steps
in the evaluation of range-restricted programs:
\begin{enumerate}
\spcrunch
\item Unification of ground facts can be done in constant time.
\item Indexing of ground facts can be done in constant time.
\item Insertion of ground facts into ground relations can be done in 
constant time.
$\Box$
\end{enumerate}
\noBox
\end{assumption}

These can be seen to be reasonable assumptions since
the time bound on unification can be achieved using hash-consing 
\cite{goto74:hashcons,sg76:hashcons} for ground terms, and
the time bound on indexing and insertion into relations can be achieved 
using hash based indexing.
%%%%%%%%%%%%%
}

%%%%%%%%%%%
% We can extend the results to the case where non-magic facts can have
% variables in them.
% The results still hold, since the assumptions above are satisfied.
%%%%%%%%%%%

\eat{
%%%%%%%%%%%%%
By associating increasing numbers with nodes (as described in
{\sf Initialize\_SN\_Relations}), one can thus check in amortized
time $O(\alpha(N))$ which (marked) subgoal precedes which other (marked)
subgoal in $Context$.
The costly step in inserting a newly generated magic fact in $Context$ 
involves finding where to insert it: this can be done in
amortized time $O(\alpha(N))$; actually inserting it in the doubly
linked list takes constant time.
Finding and deleting unmarked subgoals can also be achieved in 
amortized time $O(\alpha(N))$.
The only other expensive operation is collapsing of nodes in $Context$,
the cost of which can be amortized among the various subgoals involved
to obtain an amortized time $O(\alpha(N))$ per subgoal in $Context$.
Removing marked subgoals from $Context$ and inserting them in the 
$m\_p_{done}$ relations can be achieved in constant time.
Combining all of these, we have that evaluating a program using
{\sf Ordered\_Search} increases the cost of each derivation made at most
by a factor of $\alpha(N)$.
Consequently, we have:
%%%%%%%%%%%%%
}

\eat{
%%%%%%%%%%%%%%%%5
To find the node associated with a subgoal, we first use the index on subgoals
to find its occurrence in $Context$.
This does not directly tell us which node it is in --- we first perform 
a $ find $ operation to find the ``name'' of the set the subgoal is in,
in other words, a unique representative of the set.
We have kept with this representative a reference to the node, which is now 
read off directly.

We use the $ union-find $ technique (\cite{tarjan:ds}) to perform the
find operation efficiently.
Note that this is possible since the only operations on the sets of
subgoals are union, find, and delete entire set.
This techniques gives us an amortized cost of $ O(\alpha(N)) $ time per
union/find operation.

%%%%%
% Intuitively, the added cost of each derivation comes from maintaining
% collapsed nodes in $Context$ as a set using Tarjan's union-find algorithm
% \cite{tarjan:ds}.
%%%%%

\begin{proposition}
If Assumption~\ref{ass:const:time} holds,
given a subgoal, we can find its node in $Context$ in $ O(\alpha(N)) $ time,
where $ N $ is the total number of magic facts generated.
\end{proposition}

Given a subgoal $ m\_p $ that is newly inserted into $Context$, we index the
subgoal $ m\_p' $ that generated it ($m\_p'$ is stored in the $parent$ field of 
$ m\_p $), and find the node of $ m\_p' $, from which we read off the 
node number (the node is marked, and will have a number associated with it).
Call this number $ n1 $.
Given any other subgoal $ m\_q $, we similarly find which subgoal 
generated it.
As before we find the node of this subgoal (and the node is marked),
and find its number;  call this number $ n2 $.
Now, $ m\_q $ is before $ m\_p $ iff $ n2 \leq n1 $.
This the following result follows.

\begin{proposition}
If Assumption~\ref{ass:const:time} holds, 
given a subgoal that has just been inserted into $Context$ and another 
subgoal that is in $Context$, we can test which one is earlier in
$Context$ in $ O(\alpha(N)) $ time, where $ N $ is the total number of
magic facts generated.
\end{proposition}

If all magic facts are ground, given any subgoal, there can be at most
one subgoal in $Context$ that subsumes/is subsumed by it (this follows
trivially from Theorem~\ref{thm:o-s:subs:context}).

\begin{lemma}
Suppose Assumption~\ref{ass:const:time} holds, and let $ N $ be the 
total number of magic facts generated.
Then the following results hold (note that all times are {\em amortized}
times, due to the use of the union-find procedure):
\items Procedure {\sf Add\_After} takes time $ O(\alpha(N)) $ time. \\
\items Procedure {\sf Collapse\_Nodes} takes a total time of $ O(N \alpha(N)) $,
or $ \alpha(N) $ per magic fact generated.
\items Procedure {\sf Remove\_Marked\_Subgoals} runs in overall time 
$ O(N) $, or $ O(1) $ per magic fact generated.
\items Procedure {\sf Insert\_in\_Context} takes time $ O(1) $ per
magic fact generated.
\end{lemma}
\begin{proof}
Consider Procedure {\sf Add\_After} first.
The test in Step (a) requires us to find the node of $ m\_pj (\overline{t_2})$,
which takes $ O(\alpha(N)) $ time.
Its easy to see how the rest of the operations can be done in $ O(1) $ time.

Next consider Procedure {\sf Collapse\_Nodes}.
Suppose $ n $ nodes are removed in Step (a)(i).
Then Step (a) (i) takes $ O(n + \alpha(N)) $ time.
Steps (a) (ii) and (iii) can each be done in $ O(n) $ time as follows.
The sets of nodes are maintained as linked lists and can be concatenated 
in constant time per list.
There is also an auxiliary data structure to support the $ find $
operations on sets of subgoals.
Doing the $ union $ operation for these data structures can be done in
amortized time $ O(\alpha(N)) $ per union.
Steps (b) and (c) can each be done in $ O(\alpha(N)) $ time (to index and
find the node of the subgoal).
Overall, this procedure takes time $ O(\alpha(N)) $ per node removed.
But since at most one node is created for each subgoal generated,
{\sf Collapse\_Node} runs in amortized time $ O(\alpha(N)) $ per subgoal
that is generated.

Now consider Procedure {\sf Remove\_Marked\_Subgoals}.
This takes time $ O(1) $ per goal that is removed, or time $ O(N) $ overall.

Finally consider Procedure {\sf Insert\_in\_Context}.
The main direct time consumption in this procedure is in indexing
relation (Step (a)) or indexing $Context$ (Steps (b)(ii) and (b)(iii))
to find subgoals that subsume/are subsumed by a new subgoal.
This takes $ O(1) $ time overall, since all subgoals are ground, and
there can be at most one subgoal that subsumes/is subsumed (and in fact
it must be equal to the new subgoal).
Deletion of subgoals also takes time $ O(1) $ (only unmarked subgoals are
deleted, and so no set manipulation is required).
Thus the total time spent in {\sf Insert\_in\_Context} is 
$ O(1) $ per magic fact generated.
The time spent in each of the procedures called from {\sf Insert\_in\_Context}
is accounted for separately.
\end{proof}


\begin{proposition}
\label{prop:o-s:insert:time}
Consider any program-query pair $\langle P,Q \rangle$.
Let $\langle P^{mg},Q^{mg} \rangle$ be the result of the 
Magic Templates transformation of $\langle P,Q \rangle$.
Suppose that $\langle P^{mg},Q^{mg} \rangle$ is range-restricted.
We have:

\begin{enumerate}
\item If $\langle P,Q \rangle$ is positive, let the cost of each 
derivation in a 
bottom-up evaluation of $\langle P^{mg},Q^{mg} \rangle$ be $T_D$.
Then, in an evaluation of Procedure {\sf Ordered\_Search($P^{mg}, Q^{mg}$)}
the cost of each inference is $O(T_D \alpha (T_D))$.

\item If $\langle P,Q \rangle $ is modularly stratified, let the cost of 
each derivation in an evaluation of
$\langle P,Q \rangle $ using Ross' algorithm to evaluate SMR($P$) be $T_D$.
Then, in an evaluation of Procedure {\sf Ordered\_Search($P^{mg}, \lbok 
Q^{mg}$)} the cost of each inference is $O(T_D \alpha (T_D))$.
$\Box$
\end{enumerate}
\end{proposition}

\eat{
%%%%%%%%%%%
\begin{proof} (Sketch)
\reminder{Change proof to reflect collapsing of nodes.}
$Context$ can be implemented as a doubly linked list.
Use the same index structure as used for $m\_p$ to index into $Context$,
since $Context$ has at most one occurrence of each magic fact.
To find if a newly inserted node is lower than another node, we find
the number of node of the (marked) subgoal that generated the new node,
and compare it with the node number of the subgoal that generated the other
node.
Finding the node numbers involves doing a find operation to find the
set in which the subgoal appears, and (directly) reading off the node number
of the set.
This takes amortized time $ O(\alpha(N)) $ where $ N $ is the number of
subgoals.
Once we have the node numbers, a simple arithmetic comparison tells us 
which node is higher, and which lower.
\end{proof}
%%%%%%%%%%%
}

Combining the results of Lemmas~\ref{lm:o-s:num:deriv}
and \ref{prop:o-s:insert:time}, we have:
%%%%%%%%%%%%%%%%5
}

Hence, the cost of each derivation depends on the operations on $Context$,
and several of these operations are operations on sets: 
finding the node corresponding to a fact associated with a node, 
taking the union of facts associated with nodes, and deleting
entire sets of facts associated with a node.
These operations can be efficiently implemented using 
Tarjan's union-find technique~\cite{tarjan:ds}, with
an amortized cost of $O(\alpha(N))$ per operation, where $N$ is the 
total number of these operations on $Context$, and 
$\alpha(N)$ is the inverse Ackermann function.
Consequently, we have:

\begin{theorem}
\label{thm:o-s:time}
Let $\langle P^{mg},Q^{mg} \rangle$ be the result of the 
Supplementary Magic Templates transformation of program-query 
pair $\langle P,Q \rangle$.

\begin{enumerate}
\spcrunch
\item If $\langle P,Q \rangle$ is positive, let the time taken
(in terms of asymptotic derivation cost) to evaluate 
$\langle P^{mg}, \lbok Q^{mg} \rangle$ in a bottom-up semi-naive 
evaluation be $T$.
Then, an evaluation of {\sf Ordered\_Search($P^{mg}, Q^{mg}$)}
takes time $O(T \alpha(T) )$.

\item If $\langle P,Q \rangle$ is modularly stratified and 
$\langle P^{mg}, \lbok Q^{mg} \rangle$ is a SMTMS program, let the 
time to evaluate $\langle P,Q \rangle$ using Ross' algorithm to 
evaluate SMR($P$) be $T$.
Then, an evaluation of {\sf Ordered\_Search($P^{mg}, \lbok Q^{mg}$)}
takes time $O(T \alpha(T) )$.
$\Box$
\end{enumerate}
\end{theorem}

\eat{
%%%%%%%%%%%%%
\begin{proof} 
Let $T_P$ be the time taken to process non-magic facts, and
$T_M$ be the time to process magic facts in a bottom-up 
evaluation of $\langle P^{mg}, Q^{mg} \rangle $.
Then, $T = T_P + T_M$.
During an evaluation of Procedure {\sf Ordered\_Search($P^{mg}, Q^{mg}$)},
the time taken to process non-magic facts remains unchanged.
By the earlier lemma, the time taken to process magic facts is $O(T_M)$.
This concludes the proof.
\end{proof}
%%%%%%%%%%%%%
}

Since $\alpha(T)$ is very small even for very large values of $T$,
{\sf Ordered\_Search} compares favorably in asymptotic (space and time) 
complexity both to semi-naive bottom-up evaluation for positive programs, 
and to Ross' evaluation of modularly stratified programs.
Note that SMR($P$) can be much worse than {\sf Ordered\_Search},
as Example~\ref{ex:dumpross:1} showed.

\subsections{Results on Ordering Selection of Subgoals}
\label{sec:ordresults}

By ordering the newly generated facts in $Context$, {\sf Ordered\_Search} 
makes facts selectively available to the evaluation in a manner 
considerably different from pure bottom-up evaluation.
\eat{
%%%%%%%%%%%%%%
We formally define the subgoal-dependency graph in terms of the 
SLP-tree (Definition~\ref{def:slp:tree}).
SLP-trees contain information about subgoals as well as answers to subgoals.
Since we are interested only in the subgoals and dependencies between
them, we first define a {\em reduced SLP-tree}, which contains all
the information contained in SLP-trees about the subgoals.
We then define the AND/OR subgoal-dependency graph $S(P,Q)$,
based on reduced-SLP trees.

\begin{nameddefinition} {Reduced SLP-trees}
Let $P$ be a non-floundering program, let $Q$ be a single positive
literal, and let $T_Q$ be the SLP-tree for $Q$.
We define the {\em reduced SLP-tree\/} $R_Q$ for $Q$.
Each node $N$ in $R_Q$ is the same as some node $N'$ in $T_Q$, and 
we refer to $N'$ as the node corresponding to $N$.
(If there is more than one corresponding node, one is arbitrarily chosen.
Which node is chosen does not affect the reduced SLP-tree.)

The root of $R_Q$ is $Q$.
If the SLP-tree $T_Q$ is a single node, then so is $R_Q$.
Otherwise, the children of $Q$ in $R_Q$ are the same as the children 
of $Q$ in $T_Q$. 
If the query $Q'$ is any (non-root) node of $R_Q$, then its children
are obtained as follows:
Let $Q_1'$ be a corresponding node in $T_Q$.

\begin{itemize}
\spcrunch
\item If $Q_1'$ has only one literal $L$, $Q'$ has no children.
\item Else, let $Q_1' = L_1, L_2, \ldots, L_m$.
Consider a path $B$ in $T_Q$ from $Q_1'$ down to a leaf of $T_Q$.
Let $Q_2'$ be the highest node (i.e., closest to $Q_1'$) in $B$
that is an instance of $L_2, \ldots, L_m$.
Let $S_Q'$ be the set (after eliminating duplicates\footnote{
Duplicate elimination involves deleting a goal if it is the {\em same as\/}
another goal, modulo variable renaming.}) of all such $Q_2'$ 
obtained along different paths in $T_Q$ from $Q_1'$ down.
\begin{itemize}
\item If $S_Q'$ is empty, $Q'$ has no children.
\item Else, each element of $S_Q'$ is a child of $Q'$. ~~~ $\Box$
\end{itemize}
\end{itemize}
\noBox
\end{nameddefinition}

For ease of understanding, we define the 
subgoal-dependency graph for the restricted case when 
only ground magic facts are computed.
(Note that magic facts can be obtained from subgoals by projecting
on a subset of arguments that are bound; hence, subgoals are 
{\em not\/} restricted to be ground, only a certain subset of its
arguments are.)

\begin{nameddefinition} {Subgoal dependency graph}
\label{def:subgoal:dep}
The {\em subgoal-dependency graph\/} $S(P,Q)$ has two types of 
nodes: AND nodes and OR nodes.
There is one OR node in $S(P,Q)$ for the leftmost literal
of each node in $T_H$, for each $H$ that is a node in 
the negation tree for $Q$.

The children of an OR node are unordered, and
each OR node $L$ (corresponding to a literal) in $S(P,Q)$ has one AND
child for each branch in the reduced-SLP tree $R_L$.
Consider an AND node $N$ and the associated branch $B_N$ in $R_L$.
Let the leftmost literals in each node along the branch $B_N$ be
$L, L_{1,0}, L_{2,1}, L_{3,2}, \ldots L_{k,k-1}$. 
The AND node $N$ has $k$ children, ordered from left-to-right (to 
reflect the order in which subgoals are solved), where $L_{i,i-1}$ is the 
$i$'th child of $N$.
\end{nameddefinition}
%%%%%%%%%%%%%%
}
We now show that the order in which 
generated subgoals (magic facts) are selected to be used 
by {\sf Ordered\_Search} is related to a top-down evaluation.
%%%%%%
% More precisely, it corresponds to a depth-first traversal (with marking)
% of the subgoal-dependency graph.
%%%%%%

\begin{theorem}
\label{thm:o-s:traversal}
Let $\langle P^{mg},Q^{mg} \rangle$ be a SMTMS program.
In an evaluation of {\sf Ordered\_Search($P^{mg}, Q^{mg}$)},
the order in which magic facts are marked corresponds to a 
{\em depth-first traversal\/} (with marking) of the subgoal-dependency
graph of $\langle P,Q \rangle$ starting from $Q$.
$\Box$
\end{theorem}

The order in which Prolog explores the subgoal-dependency graph also 
corresponds to a depth-first traversal, although Prolog does not
``mark'' nodes, and hence may repeat computation.
In the case when no subgoals are repeated, i.e., the subgoal-dependency
graph is a tree, the order in which {\sf Ordered\_Search} selects
subgoals to be evaluated is the same as the order in which Prolog
selects them to be evaluated.
However, even in this case, the order in which {\sf Ordered\_Search}
generates answers to the subgoals is different from the order in which
Prolog generates the answers.
The difference arises because Prolog generates and makes new 
subgoals available to the evaluation on obtaining a single answer 
to a subgoal, backtracking on failure, whereas
{\sf Ordered\_Search} makes new subgoals
available to the evaluation only on reaching a fixpoint, which
avoids the need for backtracking.
Consequently Prolog may perform a lot less computation than 
{\sf Ordered\_Search} in obtaining a single answer to the query.
For linear programs, however, delaying the availability of 
subgoals to the {\sf Ordered\_Search} evaluation does not delay 
the computation of the first answer to the query (because of the
asynchronous way in which answers are generated).
We conjecture that {\sf Ordered\_Search} is most useful for 
computing single answers to a query for the class of linear programs.

\eat{
%%%%%%%%%%%%%%%%%%%%%%
\begin{theorem}
\label{thm:o-s:tree:traversal}
Let $\langle P^{mg},Q^{mg} \rangle$ be a range-restricted MTMS program.
Suppose the subgoal-dependency graph $S(P,Q)$ is a tree, with root $Q$.
In an evaluation of {\sf Ordered\_Search($P^{mg}, Q^{mg}$)},
the order in which subgoals are marked corresponds to a 
{\em depth-first traversal\/} (with marking) of $S(P,Q)$ starting from $Q$.
$\Box$
\end{theorem}

If the subgoal-dependency graph is not a tree, the order in which
subgoals are marked corresponds to an approximate depth-first
traversal of $S(P,Q)$.
Here, we state the result when the subgoal-dependency graph is 
an acyclic graph.
A similar (but slightly more complex) result holds for general graphs.

\begin{theorem}
\label{thm:o-s:dag:traversal}
Let $\langle P^{mg},Q^{mg} \rangle$ be a range-restricted MTMS program
obtained from a (modularly stratified) program-query pair
$\langle P,Q \rangle$.
Let the subgoal-dependency graph $S(P,Q)$ be a directed acyclic graph (DAG),
with source $Q$.
In an evaluation of {\sf Ordered\_Search($P^{mg}, Q^{mg}$)},
the order in which subgoals are marked is as follows:
Initially, the source $Q$ is marked.
Now, consider a marked OR node $L$ in $S(P,Q)$, such that 
the corresponding magic fact $m\_p (\overline{t})$ is the latest 
marked subgoal in $Context$.
\begin{enumerate}
\spcrunch
\item If $m\_p (\overline{t})$ has any unmarked grandchildren,
non-deterministically choose an AND child $N$ with unmarked children;
visit and mark the leftmost unmarked child of $N$.
\item If $m\_p (\overline{t})$ has no unmarked grandchildren
(a special case is if $m\_p (\overline{t})$ is a sink node in $S(P,Q)$),
return to its (marked) grandparent, and continue.
$\Box$
\end{enumerate}
\end{theorem}

\eat{
%%%%%%%%%%%
\reminder{Have an example here in the full paper, illustrating why this 
is not a depth-first traversal of the subgoal-dependency graph, in general.}
%%%%%%%%%%%
}

In two special cases of the DAG, the approximate depth-first traversal
reduces to a true depth-first traversal of the AND/OR 
subgoal-dependency graph.

The first case corresponds to determinate programs, where there is 
precisely one way of answering each subgoal set up in the computation.

\begin{corollary}
\label{cor:dag:sp1}
Consider a directed acyclic subgoal-dependency graph $S(P,Q)$, with 
at most one child for each OR node.
In an evaluation of {\sf Ordered\_Search}, the order in which
subgoals are marked corresponds to a
{\em depth-first traversal\/} (with marking) of $S(P,Q)$ starting from $Q$.
$ \Box $
\end{corollary}

The second case corresponds to linear programs, where precisely
one subgoal is set up for each way of answering a subgoal.

\begin{corollary}
Consider a directed acyclic subgoal-dependency graph $S(P,Q)$, with
at most one child for each AND node.
In an evaluation of {\sf Ordered\_Search}, the order in which
subgoals are marked corresponds to a
{\em depth-first traversal\/} (with marking) of $S(P,Q)$ starting from $Q$.
$ \Box $
\end{corollary}
%%%%%%%%%%%%%%%%%%%%%%
}


\eat{
%%%%%%%%%%%%%
\section{Uses of Ordered Search}

\subsection{Modular Negation and Aggregation}

Ross~\cite{ross:modstrat:full} proposed a bottom-up evaluation method for 
computing answers to queries on modularly stratified programs.
This bottom-up method uses meta-variables and meta-level predicates to 
incorporate information about negative dependencies into its computation.
We illustrate, using an example, the kinds of dependency
information computed by Ross in \cite{ross:modstrat:full}.

%%%%%%%%%%
% \reminder{Cut out details of example, and just retain a short note saying
% that $ O(n^2) $ facts are generated (and mention what the form of the 
% facts is -  dependency of a negative subgoal on all subgoals that it 
% depends on.
% Describe what {\sf Ordered\_Search} does on this example.
% }
%%%%%%%%%%

\begin{example}
\label{ex:dumpross:1:us}
Consider the following modularly stratified program-query pair 
$\langle P,Q \rangle$:
\logicprog{
\lrule {r1:} {even(X)} {pred(X,Y1), pred(Y1,Y), even(Y)} \\
\lrule {r2:} {even(X)} {pred(X,Y), \neg even(Y)} \\
\lfact {r3:} {even(0)} \\
\lheader {$pred(1,0). ~~  pred(2,1). ~~  \ldots ~~ pred(n,n-1)$} \\
\lquery {\neg even(4)} 
}
Ross describes a supplementary magic sets rewriting (SMR) of 
$\langle P,Q \rangle$
as well as an algorithm to evaluate SMR($P$).
We omit the details of SMR($P$) except to note that 
it has rules defining: $magic(even(X),+)$ (which subgoal was generated
positively), $magic(even(X),-)$ (which subgoal was generated negatively),
$dp(even(X),even(Y))$ (which negatively generated subgoal $even(X)$ 
depends positively on subgoal $even(Y)$), and
$dn(even(X),even(Y))$ (which negatively generated subgoal $even(X)$
depends negatively on subgoal $even(Y)$).
\eat{
%%%%%%%%%%%%%%%%%
SMR($P$) includes the following rules (by unfolding rules defining
supplementary predicates) in addition to other rules, which are not
relevant for our purpose:
\setrulebodywidth{3.75in}
{
\logicprog{
\lrule {mr1:} {magic(even(Y),+)} {magic(even(X),\_), pred(X,Y1), \lbok 
		pred(Y1,Y)}\\
\lrule {mr2:} {magic(even(Y),-)} {magic(even(X),\_), pred(X,Y)} \\
\lfact {mr3:} {magic(even(10),-)} \\
\lrule {dr1:} {dp(even(X),even(Y))} {magic(even(X),-), magic(even(X),\_), \lbok
		pred(X,Y1), \lbok pred(Y1,Y)} \\
\lrule {dr2:} {dn(even(X),even(Y))} {magic(even(X),-), magic(even(X),\_), \lbok
		pred(X,Y)} \\
\lrule {dr3:} {dp(P,even(Y))} {dp(P,even(X)), magic(even(X),\_), \lbok
		pred(X,Y1), \lbok pred(Y1,Y)} \\
\lrule {dr4:} {dn(P,even(Y))} {dp(P,even(X)), magic(even(X),\_), \lbok
		pred(X,Y)}
}
}
%%%%%%%%%%%%%%%%%
}
Ross' algorithm to evaluate SMR($P$) would compute the facts
shown in Table~\ref{tbl:ross:ex1}.

\begin{table}
\centerline{
\begin{tabular}{|l|l|} \hline
Relation & Facts \\ \hline
$magic(even(X),-)$ & $X = 4, 3, 2, 1, 0$ \\
$magic(even(X),+)$ & $X = 2, 1, 0$ \\
$dp(even(X), even(Y))$ & $(X,Y) = (4,2), (3,1), (2,0), (4,0)$ \\
$dn(even(X), even(Y))$ & $(X,Y) = (4,3), (3,2), (2,1), (1,0), (4,1), (3,0)$ \\
\hline
\end{tabular}
}
\caption{Evaluation of SMR($P$) using Ross' Technique}
\label{tbl:ross:ex1}
\end{table}

Let us see how this query would be evaluated using {\sf Ordered\_Search}.
We omit the details of the Magic Templates transformation and 
only describe the state 
of the $Context$ in various iterations, in Table~\ref{tbl:ross:ex1:dfs}.
The iteration number indicates the iteration of the inner
``{\sf repeat \ldots until}'' loop in Procedure {\sf Ordered\_Search}.

\begin{table}
\centerline{
\begin{tabular}{|c|c|l|} \hline
Iteration Number & Relation & Facts \\ \hline
$0$ & $even$ & $\{ \}$ \\
 & $m\_even$ & $\{ \}$ \\
 & $m\_even_{done}$ & $\{ \}$ \\
 & $Context$ & $m\_even(4)$ \\ \hline
$1$ & $even$ & $\{ \}$ \\
 & $m\_even$ & $\{ m\_even(4) \}$ \\
 & $m\_even_{done}$ & $\{ \}$ \\
 & $Context$ & $m\_even(4)^{\ast}, m\_even(3), m\_even(2)$ \\ \hline
$2$ & $even$ & $\{ \}$ \\
 & $m\_even$ & $\{ m\_even(4), m\_even(2) \}$ \\
 & $m\_even_{done}$ & $\{ \}$ \\
 & $Context$ & $m\_even(4)^{\ast}, m\_even(3), m\_even(2)^{\ast},
	m\_even(0), m\_even(1)$ \\ \hline
$3$ & $even$ & $\{ \}$ \\
 & $m\_even$ & $\{ m\_even(4), m\_even(2), m\_even(1) \}$ \\
 & $m\_even_{done}$ & $\{ \}$ \\
 & $Context$ & $m\_even(4)^{\ast}, m\_even(3), m\_even(2)^{\ast},
	m\_even(1)^{\ast}, m\_even(0)$ \\ \hline
$4$ & $even$ & $\{ even(0) \}$ \\
 & $m\_even$ & $\{ m\_even(4), m\_even(2), m\_even(1), m\_even(0) \}$ \\
 & $m\_even_{done}$ & $\{ \}$ \\
 & $Context$ & $m\_even(4)^{\ast}, m\_even(3), m\_even(2)^{\ast},
	m\_even(1)^{\ast}, m\_even(0)^{\ast}$ \\ \hline
$5$ & $even$ & $\{ even(0), even(2) \}$ \\
 & $m\_even$ & $\{ m\_even(4), m\_even(2), m\_even(1), m\_even(0) \}$ \\
 & $m\_even_{done}$ & $\{ \}$ \\
 & $Context$ & $m\_even(4)^{\ast}, m\_even(3), m\_even(2)^{\ast},
	m\_even(1)^{\ast}, m\_even(0)^{\ast}$ \\ \hline
$6$ & $even$ & $\{ even(0), even(2), even(4) \}$ \\
 & $m\_even$ & $\{ m\_even(4), m\_even(2), m\_even(1), m\_even(0) \}$ \\
 & $m\_even_{done}$ & $\{ \}$ \\
 & $Context$ & $m\_even(4)^{\ast}, m\_even(3), m\_even(2)^{\ast},
        m\_even(1)^{\ast}, m\_even(0)^{\ast}$ \\ \hline
$7$ & $even$ & $\{ even(0), even(2), even(4) \}$ \\
 Inner & $m\_even$ & $\{ m\_even(4), m\_even(2), m\_even(1), m\_even(0) \}$ \\
 Loop & $m\_even_{done}$ & $\{m\_even(0), m\_even(1),m\_even(2)\}$ \\
 Fixpoint & $Context$ & $m\_even(4)^{\ast}, m\_even(3)$ \\ \hline
$8$ & $even$ & $\{ even(0), even(2), even(4) \}$ \\
 Inner & $m\_even$ & $\{ m\_even(4), m\_even(2), m\_even(1), m\_even(0), 
	m\_even(3) \}$ \\
 Loop & $m\_even_{done}$ & $\{m\_even(0), m\_even(1),m\_even(2),m\_even(3),
	m\_even(4)\}$ \\
 Fixpoint & $Context$ & \\ \hline
\end{tabular}
}
\caption{Evaluation of $\langle P^{mg},Q^{mg} \rangle$
using {\sf Ordered\_Search}}
\label{tbl:ross:ex1:dfs}
\end{table}

In general, if the query was:
\logicprog{
\lquery {\neg even(m)}
}
for $m \leq n$, Ross' algorithm to evaluate SMR($P$) would compute 
$O(m^2)$ facts for the $dp$ and $dn$ predicates, even though
only $O(m)$ facts would be produced for the $magic$ and $even$ predicates.
Thus, the evaluation of SMR($P$) would take $O(m^2)$ space and make
$O(m^2)$ derivations.
In contrast to Ross' algorithm, Procedure {\sf Ordered\_Search} 
takes only $O(m)$ space and makes $O(m)$ derivations to compute the 
answer to the above query.
\end{example}
%%%%%%%%%%
% \reminder{Say some more re. this.}
%%%%%%%%%%

\subsection{Obtaining a Single Answer}

There are many cases where the user may want a single answer to a query.
This is one of the main motivations for the {\em choice} construct
in LDL and CORAL.
A naive way of obtaining a single answer to the query 
is to evaluate the program 
bottom-up until we get an answer to the query, and then terminate 
the evaluation.
However, this might lead to a lot of redundant computation as the following
example illustrates.

\begin{example}
\label{ex:choice:4:us}

Consider the following program. 
\logicprog{
\lrule {r1:} {path(X,Y,[X,Y])} {edge(X,Y)}\\
\lrule {r2:} {path(X,Y,[X|P])} {edge(X,Z), path(Z,Y,P)} \\
\lfact {f1:} {edge(1,2)}\\
\lfact {f2:} {edge(1,3)}\\
\lfact {f3:} {edge(2,4)}\\
\lfact {f4:} {edge(3,4)}\\
\lquery {path(1,4,X)}
}
Suppose we want just one answer to the query.
Table~\ref{tbl:choice:ex4} shows the facts computed in a
bottom-up evaluation, and in an ordered evaluation of the query on the program.
The iteration number indicates the iteration of the inner
``{\sf repeat \ldots until}'' loop in Procedure
{\sf Ordered\_Search}, or the outermost iteration in a bottom-up
evaluation.
We omit details of the magic program, and the exact manipulations
of $Context$, but an intuitive idea of how $Context$ is manipulated should
suffice to follow the steps in this simple example.
We have compressed some data in this table---in particular, lists of 
nodes in a path have been replaced by a
sequence of digits that encodes the path.


\begin{table}
\centerline{
\begin{tabular}{|c|c|l|l|} \hline
Iteration Number & Relation & Bottom-Up & Ordered Search \\ \hline
$0$ & $path$ 	& $\{ \}$ 			& $\{ \}$		\\
 & $m\_path$ 	& $\{ m\_p(1)\}$ 			& $\{ \}$ 		\\
 & $m\_path_{done}$ &				& $\{ \}$ 		\\
 & $Context$ 	&				& $m\_p(1)$	\\ \hline
$1$ & $path$ 	& $\{p(1,2,12), p(1,3,13)\}$	& $\{ p(1,2,12),p(1,3,13) \}$ \\
 & $m\_path$ 	& $\{ m\_p(1), m\_p(2), m\_p(3) \}$	& $\{ m\_p(1) \}$  	\\
 & $m\_path_{done}$ &				& $\{ \}$ \\
 & $Context$ 	& 				& $m\_p(1)^{\ast}, m\_p(2), 
	m\_p(3)$ \\ \hline
$2$ & $path$ 	& $\{p(1,2,12), p(1,3,13), p(2,4,24)$ &
						$\{ p(1,2,12),p(1,3,13),
			p(3,4,34)\}$ \\
 &              &   $ p(3,4,34) \} $		& 			\\
 & $m\_path$ 	& $\{ m\_p(1),m\_p(2),m\_p(3),m\_p(4)\}$& $\{ m\_p(1), m\_p(3) \}$  \\
 & $m\_path_{done}$ & & $\{ \}$ \\
 & $Context$ 	& 				& $m\_p(1)^{\ast}, m\_p(2),
					m\_p(3)^{\ast}, m\_p(4) $ \\ \hline
$3$ & $path$ 	& $\{ p(1,2,12), p(1,3,13), p(2,4,24)$  & $\{p(1,2,12),
					p(1,3,13), p(3,4,34), p(1,4,134) \} $\\
 &		& $ p(3,4,34), p(1,4,124), p(1,4,134)\}$ &	\\
 & $m\_path$ 	& $\{ m\_p(1), m\_p(2), m\_p(3), m\_p(4) \} $ &$\{ m\_p(1), m\_p(3),m\_p(4) \}$\\
 & $m\_path_{done}$ & & $ \{ \} $  	\\
 & $Context$ 	&				& $\{ m\_p(1)^{\ast},
					m\_p(2), m\_p(3)^{\ast}, m\_p(4)^{\ast} \}$\\ \hline
\end{tabular}
}
\caption{Evaluation of $\langle P^{mg},Q^{mg} \rangle$ 
using {\sf Ordered\_Search}}
\label{tbl:choice:ex4}
\end{table}

The evaluation terminates in Iteration 3 for the bottom-up 
technique as well as for {\sf Ordered\_Search}.
In addition, {\sf Ordered\_Search} has clearly computed fewer facts.
We can extend this example to make {\sf Ordered\_Search} do arbitrarily
better than bottom-up evaluation.
%%%%%%%%
% The converse is also possible, and therefore care should be exercised in
% using this feature, but there are many cases where it is clear that
% {\sf Ordered\_Search} will do better, and in such cases it may be used
% safely.
%%%%%%%%

Note that a top-down, tuple-at-a-time evaluation strategy, like Prolog, would
set up a query on $path$, and return when it found the first 
answer to $path$.
\end{example}

\eat{
%%%%%%%%%%%%%%%%%%%%
One (rather inefficient) possibility is to obtain the complete answer set 
to the query (or subquery), and then non-deterministically choose an answer.
However, that may not always be the best strategy, as the following
example demonstrates:

\begin{example}
Consider the following program\footnote{The $choice$ construct uses the 
LDL syntax.} $P$:
\logicprog{
\lrule {r1:} {q(1)} {p(Y), choice((),(Y))} \\
\lfact {r2:} {p(1)} \\
\lrule {r3:} {p(N+1)} {N > 0, p(N)} \\
\lquery {q(1)}
}
Clearly, if one sought to obtain the complete extension of $p$ 
(by repeatedly applying rules $r2$ and $r3$ until a fixpoint is reached)
before making a choice in the body of $r1$, the bottom-up evaluation would
not terminate.

Note that a top-down, tuple-at-a-time evaluation strategy, like Prolog, would 
set up a query on $p$ (while evaluating rule $r1$), and return when it 
found the first answer to $p$, in this case, $p(1)$. 
Since this fact can be used to satisfy the body of the rule, it can be used
to answer the query.
\end{example}
%%%%%%%%%%%%%%%%%%%%
}

%%%%%%%%%%%%%%%%%%%%%%%%
% RAGHU:  
% There are major problems with implementing propagation of
% alpha/beta values in alpha/beta search.  I don't think we can do it in
% any reasonable fashion using just ordered search.  So this section has
% been deleted.  : Sudarshan
%              &&&&&&&&&&&&&&&&&&& 
% \subsection{Alpha / Beta Pruning of Min/Max Search Trees}
% 
% Min/max search trees are used in game programs.
% The search tree is rooted at a board position, and each node has a 
% child for each possible next board position.
% Values are given for leaf nodes.
% The value of the root node is defined as the maximum of the values of its
% children.
% At alternate levels of the tree, the value of a node is defined as either
% the minimum of the values of the children or the maximum of the values of the
% children.
% Thus to compute the value of a node, we need the values of all its children,
% and ordered search provides us with a technique of acheiving this.
% 
% Alpha / Beta pruning is an optimization of min/max search.
% We can assign temporary values for nodes as we find values for 
% some of the children.
% Given the temporary value of the parent of a min-node, if some child of 
% node has a value smaller than the temporary value of the parent,
% there is no point searching other children of this node - the value of this
% node will never grow large enough to affect the value of the parent.
% This is known as alpha pruning.
% Beta pruning is similar in flavor and is a converse of alpha pruning.
% We do not go into details.
% 
% The most important point to note that results for one child of a node
% can help avoid a search of another child of the node.
% With bottom-up evaluation, all children of the node are searched in 
% parallel, which means that alpha/beta pruning is meaningless.
% On the other hand when ordered search does a depth first traversal
% (e.g. if the search tree has no repeated nodes) we do indeed search one 
% child of a node completely before switching to another child.
% Thus the alpha and beta values are available for pruning children.
% 
% An implementation of alpha/beta pruning will have to modify the evaluation
% algorithm to propagate the alpha/beta cutoffs.
% We do not go into details here, except to note that this is 
% possible.
% 
% \reminder{Short note in justification here, and possibly an example if 
% space allows.}
%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Ordered Search and Modules}

\reminder{Delete this section.  It doesn't fit in.}

The CORAL deductive programming language (\cite{rbss90:coral})
has a support for modules, as independent units of compilation.
Predicates defined in a module $M$ can be exported and can be queried by
other modules $N$.
The semantics of a query to an exported predicate in module $M$ is that 
all answers to the query are computed and returned to the calling module.
Consider now the case where a called module uses {\sf Ordered\_Search}.
In this case, {\sf Ordered\_Search} can be modified so that 
the queries in a call are inserted in the local $Context$ of the 
called module $M$.
Computation proceeds till all answers are generated, and then the call
returns.
Successive calls can be treated in {\em exactly\/} the same fashion,
if the relations local to the module are maintained across calls.
This property helps in the implementation of the {\em save\_module\/}
feature in CORAL that requires that the state of a module
be maintained across calls.


\section{Optimizations and Extensions of {\protect\sf Ordered\_Search}}
\label{sec:extn}

\subsection{Supplementary Magic Templates}

We presented our algorithms based on the Magic Templates rewriting.
Supplementary Magic Templates rewriting is a variant 
of Magic Templates rewriting, which essentially factors out 
sub-expressions that are common to a (modified) original rule and
all the magic rules derived from that rule.
The Supplementary predicates created correspond to successive increasing 
prefixes of the (modified) original rule.
As a result of this, we lose the direct connection
we had between the subgoals on the head of the rule and the subgoals
generated for the body literals.

To do an ordered search using Supplementary Magic
Templates, we need to store with each supplementary fact the subgoal on 
the rule head that resulted in the generation of the fact.
It is an easy modification to the ordered search algorithm to insert
this information for the first supplementary fact, and to propagate the
information along derivations of facts for supplementary
predicates further down the rule.
Further, duplicate elimination must not be done on supplementary 
facts, since it is possible for two different head subgoals to generate
the same supplementary fact, in which case we would end up storing 
just one of them, and lose dependency information for the other subgoal.

Given the two modifications described above, Procedure~{\sf Ordered\_Search}
can be used along with Supplementary Magic Templates rewriting,
and will not interfere with any other part of the 
ordered search evaluation.

\subsection{Not Maintaining $m\_p_{done}$ Relations}

In Procedure~{\sf Ordered\_Search},
the $ m\_p_{done} $ predicates serve two purposes.
First, they act as guards for negated $p$ literals in rule bodies, to 
ensure that facts are used in a negated literal only when the corresponding
subgoal has been completely evaluated.
Second, magic facts in the $m\_p_{done}$ relation are used in 
Procedure~{\sf Insert\_in\_Context} to check whether a newly generated
subgoal has been completely evaluated.
(A subgoal $ m\_p(\overline{t_1}) $  has been completely evaluated if it is 
an instance of a fact $ m\_p(\overline{t_2}) $ in the $m\_p_{done}$ relation.)

If there is any negated $p$ literal in the body of a rule,
our evaluation scheme needs to 
maintain the $m\_p_{done}$ relation.
However, if there is no occurrence of a negated literal for predicate $p$,
it is possible to avoid maintaining the $m\_p_{done}$ relation explicitly.
The only operation on such an $m\_p_{done}$ relation is 
checking whether a newly generated subgoal has been completely 
evaluated.
We have the following result: 

\begin{proposition}
\label{prop:mp:mpdone}
A magic fact is in the $m\_p_{done}$ relation iff it is in the differential
$m\_p$ relations, but not in $Context$.
\end{proposition}

We omit the proof of this result.
To check if a newly generated subgoal has been completely
evaluated, we merely check if there is a fact in the $m\_p$
relation that subsumes the newly generated subgoal, and which is not 
in $ Context$.

Procedure~{\sf Ordered\_Search} is useful in many contexts where they 
may not be any negation, for instance when one desires a single answer
to a query.
In such contexts, we can eliminate the $m\_p_{done}$ relations 
reducing the space requirements of evaluating the program.

%%%%%%%%%%%%%%
% Justification: 
% Recall that a subgoal (magic fact) $ m\_p(\overline{t_1}) $ is 
% in the differential relation $m\_p$ only if it had been marked in 
% $Context$ at some point in the {\sf Ordered\_Search} evaluation.
% Further, a subgoal is moved from $Context$ into the $m\_p_{done}$
% relation only when it has been completely evaluated.
% Since no duplicate elimination is done while inserting
% facts in the differential $m\_p$ relations (all duplicate elimination
% is done while inserting magic facts in $Context$), a fact
% is in the $m\_p_{done}$ relation iff it is in the differential
% $m\_p$ relations, but not on $Context$.
% Hence, a subgoal $ m\_p(\overline{t_1}) $ has been completely evaluated 
% iff there is some fact $ m\_p(\overline{t_2}) $ in the differential
% $m\_p$ relations which is not present in $Context$.
% 
% One can use this to check if a subgoal has been completely evaluated
% without explicitly maintaining the $m\_p_{done}$ relation.
% In an extreme case where there is are no negated literals in the program,
% alpha/beta pruning of search spaces, or obtaining a single 
% answer to a query), one can avoid maintaining $m\_p_{done}$ relations
% altogether.
%%%%%%%%

\subsection{Increasing Set-Orientedness of Evaluation}

Procedure {\sf Ordered\_Search} is not set-oriented in 
making generated subgoals available for further use (although it is 
set-oriented in generating subgoals and answers to subgoals).
The procedure can be made more set-oriented by marking a whole set of 
subgoals at a time (in Procedure {\sf Initialize\_SN\_Relations}), 
and collapsing the corresponding nodes in $Context$ together
(using Procedure {\sf Collapse\_Nodes}), so long as the dependencies 
between the subgoals are not critical.

For instance, in evaluating a program without negation, we could
make Procedure {\sf Ordered\_Search} as set-oriented as we desire.
In the extreme case, each unmarked subgoal on $Context$ can be marked
in {\sf Initialize\_SN\_Relations}, and all (marked) nodes can be
collapsed; the result is Basic Semi-Naive evaluation.
Thus, for programs without negation, Procedure {\sf Ordered\_Search} 
can be modified to get a range of different degrees of set-orientedness.

\reminder{Maybe dump the next discussion of nested evaluation.}

Again, in evaluating stratified logic programs, if the head of $Context$
contains an unmarked $m\_p$ subgoal, one can select consecutive
unmarked $m\_p$ subgoals from the head of $Context$ and collapse
the corresponding nodes.
Increasing set-orientedness in this fashion does not have any impact
on the correctness of the evaluation since, for stratified programs,
there is no ``negative'' dependency between two $m\_p$ subgoals.
Thus, for programs with stratified negation, Procedure 
{\sf Ordered\_Search} can be modified to achieve a high degree of
set-orientedness.

\eat{
%%%%%%%%%%%%%%%%%%%%
\subsection{Extending the Class of Programs Evaluated}

In Section~\ref{sec:o-s:results}, we established results about
Procedure {\sf Ordered\_Search} for the class of MTMS programs, 
i.e. the Magic Templates rewriting of left-to-right modularly
stratified programs, with left-to-right total sips.

We conjecture that our results extend naturally to the more general
class of logic programs with finite negation trees; every modularly 
stratified DATALOG program has finite negation trees, but the converse 
is not true~\cite{ross:modstrat:full}.
Intuitively, this is the class of programs that has no cycles (at 
the level of program facts) through negation.
%%%%%%%%%
% The order in which subgoals are maintained in 
% $Context$ by Procedure~{\sf Ordered\_Search} will reflect
% the dependency relation between subgoals for such programs too.
% Magic facts will be moved to the $m\_p_{done}$ relation only when
% they have been completely evaluated.
% Thus, the evaluation would still be sound, complete for DATALOG, and 
% have the non-repetition property.
%%%%%%%%%

Our results can be easily extended to deal with partial sips.
To establish a correspondence with the techniques discussed in
\cite{ross:modstrat:full}, we would have to consider only certain
kinds of rule prefixes (those corresponding to the sips chosen for
the rule), and extend Ross' results to cover this extended class of
programs and sips.
%%%%%%%%%%%%%%%%%%%%
}

%%%%%%%%%%%%%
}


\sections{Related Work}
\label{sec:rel:work}

In this section, we extend the discussion of related work in Section \ref{sec:intro}.
A variant of QSQR, {\em subquery completion}, was described in
Lefebvre~\cite{lef:agg} to deal with recursively defined aggregates.
It uses the dependencies between subgoals maintained by QSQR 
to handle a class of acyclic programs with
aggregation.
However, this technique does not deal with programs that have cycles in the
subgoal-dependency graph (even if the cyclic dependency is only 
between positive subgoals).
{\sf Ordered\_Search} allows positive cycles in the subgoal
dependency graph, and deals with them by collapsing nodes 
in the $Context$, and declaring all the facts in a collapsed node to
be completely evaluated once a fixpoint is reached.
There is no analogue to this step in the technique of \cite{lef:agg}.
Ross also describes how his approach can be used to adapt QSQR
to deal with modularly stratified negation.
In this case, as with bottom-up evaluation, Ross' approach needs to
maintain dependencies between subgoals transitively (which
is done implicitly by {\sf Ordered\_Search}).
The previous comparisons of our technique with Ross' technique also
apply to this case.
Bidoit and Legay~\cite{bl:well} describe an evaluation procedure
modifying QSQR, based on global SLS-resolution, to compute the 
well-founded model of a program.
However, even for modularly stratified programs, this program repeats
computation, and is considerably less efficient than our technique.

%%%%%%%%%%%%%
% \begin{proposition}
% If there are $n$ distinct subgoals set up in the computation, the
% computation tree set up by QSQR/QoSaQ can have $O(n^2)$ subgoal nodes.
% \end{proposition}
% 
% \reminder{Verify this!}
% 
% This is in contrast with our techniques which take $O(n)$ space
% to store subgoals (i.e., magic facts).
%%%%%%%%%%%%%


%%%%%%%%%%%
% \section{Future Work/Points to Note}
% SCCwise evaluation with ordered search.
% \\
% \\
% Set orientation is possible with ordered search.
% As long as the goals on top of context cannot have negative dependencies 
% between them, they can be marked and made visible together.
% Of course several of the ordering properties mentioned earlier will 
% no longer hold.
% \\
% Per-literal ordered search:
% \\
% 	- annotation per literal (perhaps if literal is negative).\\
% 	- Guards are set up on this literal similar to the guards for negative
% 	literals. \\
% 	- we require that calls be acyclic.
% 	-- All this is plain garbage since it cannot be done in a 
% 	semi-naive fashion - dependencies that are critical for negation
% 	may have been lost in the part of the computation that did not
% 	use ordered search.
%%%%%%%%%%%%%

\sections{Conclusions and Future Work}
\label{sec:concl}

We presented a memoing technique, {\sf Ordered\_Search}, that is a hybrid
between breadth-first and depth-first search.
This technique can be used to efficiently evaluate modularly 
stratified programs, as well as to compute single answers to a query
more efficiently than pure bottom-up evaluation.
Fully set-oriented computation causes problems for the
evaluation of modularly stratified programs, as illustrated by our
comparisons with Ross~\cite{ross:modstrat:full}---it can result in
an order of magnitude slow-down.
Hence, it is important to provide some of the benefits of tuple-at-a-time
computation with bottom-up evaluation, and {\sf Ordered\_Search} does just
this.

{\sf Ordered\_Search} can also be used for programs that
compute non-ground facts; details are presented in the full version 
of the paper.
Also, while our claims about correctness of {\sf Ordered\_Search}
have been made for the class of modularly stratified programs, we
conjecture that the method is correct whenever there is no negative
dependency within a strongly connected component of the subgoal dependency graph.
We believe that {\sf Ordered\_Search} is a versatile and very useful 
tool in the evaluation of queries on deductive databases.
We are in the process of implementing {\sf Ordered\_Search} in the 
CORAL system~\cite{rbss90:coral}.

An important direction of future research is to explore the possibility 
of increasing the set-orientedness of {\sf Ordered\_Search}, thereby
increasing efficiency of evaluation, while retaining its desirable 
properties for evaluating modularly stratified programs.
Another direction of research is to provide a finer grain of control 
in making subgoals available to the evaluation such that the 
technique can mimic Prolog more closely, providing further benefits for
queries requiring a single answer.

\section{Acknowledgements}

We would like to thank Alexandre Lefebvre for valuable discussions
regarding QSQR and EKS-V1, and pointing out some related work.

\bibliography{lib/bib/moredb,lib/bib/dbimp}

\appendix

\sections{Algorithms}
\label{sec:algs}

{\sf Ordered\_Search} below is applicable to programs with function
symbols that compute non-ground facts.

\algorithm{
\> Ordered\_Search($P^{mg}, Q^{mg}$) \+ \+ \\
Let $Context$ be a list of sets of (magic and supplementary)
	facts, initially containing $Q^{mg}$. \\
repeat \+ \\
repeat \+ \\
Initialize\_SN\_Relations($P^{mg}, Context$). \\
Apply\_Rules($P^{mg}$). \> \> \> \> \> /* Compute new facts */ \\
for each newly computed pair of magic/supplementary facts
	$\langle F_1, F_2 \rangle$ \\
\> Insert\_in\_Context($\langle F_1, F_2 \rangle, Context$) \\
end for \- \\
until (no new facts computed) \\
Remove\_Marked\_Subgoals($P^{mg}, Context$) \- \\
until ($Context$ is empty) \\
return answers to $Q^{mg}$. \- \\
end Ordered\_Search \-
}

{\sf Initialize\_SN\_Relations} below is used to maintain the
differential relations that are needed to ensure that derivations
are not repeated, i.e., to ensure the non-repetition property.
%%%%%%%%%
% The main thing to note about this procedure is the selection of 
% generated facts from $Context$ for further use.
% Once a fact is selected for use, it is marked, and the corresponding 
% node in $Context$ is also marked.
%%%%%%%%%

\algorithm{
\> Initialize\_SN\_Relations($P^{mg}, Context$) \+ \+ \\
Let $p_1, \ldots, p_n$ be the original program predicates defined 
    in $P^{mg}$. \\
Let $m\_p_1, \ldots, m\_p_n$ be the corresponding magic predicates. \\
Let $supp_1, \ldots, supp_k$ be the supplementary predicates in $P^{mg}$.
\\
for each predicate $p_i, 1 \leq i \leq n$, ~~ SN\_Update($p_i$). \\
for each predicate $m\_p_{i_{done}}, 1 \leq i \leq n$, ~~ 
	SN\_Update($m\_p_{i_{done}}$). \\
for each predicate $m\_p_i, 1 \leq i \leq n$ \+ \\
  $ m\_p_i^{old} := m\_p_i^{old} \sqcup \delta m\_p_i^{old} $. ~~
  $ \delta m\_p_i^{old} := \phi$. ~~
  $ \delta m\_p_i^{new} := \phi $. \- \\
end for \\
for each predicate $supp_i, 1 \leq i \leq k$ \+ \\
  $ supp_i^{old} :- supp_i^{old} \sqcup \delta supp_i^{old}$. ~~
  $ \delta supp_i^{old} := \phi$. ~~
  $ \delta supp_i^{new} := \phi$. \- \\
end for \\
Let $F_1$ be an unmarked fact in the head of $Context$; mark $F_1$. \\
if (head of $Context$ is unmarked) \+\\
    Mark head of $Context$. \\
    Link head of $Context$ with previous marked node. \\
    Set $number$ of head of $Context$ to $number$ of previous 
		marked node $+ 1$. \- \\
end if \\
Let $l$ be the predicate of $F_1$. \\
$\delta l^{old} := F_1$. \\
for each predicate $m\_p_i, 1 \leq i \leq n$, ~~
  $ m\_p_i := m\_p_i^{old} \sqcup \delta m\_p_i^{old}$. \\
for each predicate $supp_i, 1 \leq i \leq k$, ~~
  $ supp_i := supp_i^{old} \sqcup \delta supp_i^{old}$. \- \\
end Initialize\_SN\_Relations \-
}

{\sf Apply\_Rules} below is used to make new derivations.
In addition, it records which magic/supplementary fact was used to 
derive a newly generated magic/supplementary fact.
This is used to maintain dependency information within the $Context$.

\algorithm{
\> Apply\_Rules($P^{mg}$) \+ \+ \\
Let ${\cal R}$ be the rules of $P^{mg}$, and 
let ${\cal R}_{SN}$ be the semi-naive rules obtained from ${\cal R}$. \\
Apply each rule in ${\cal R}_{SN}$ once; when computing magic facts,\\
\> compute pairs $\langle F_1, F_2 \rangle$, where each of $F_1$ and $F_2$ 
    is either a magic fact or \\
\> a supplementary fact, and $F_2$ was used to compute $F_1$. \- \\
end Apply\_Rules \-
}

{\sf Insert\_in\_Context} below is used to insert newly generated
magic and supplementary facts into the $Context$, which maintains 
dependency information between magic facts.

\eat{
%%%%%%%%%%%%
the order in which magic facts are selected to be made available
for further use, and the order in which magic facts are 
inserted into the $m\_p_{done}$ relations reflects this dependency.

Since a goal $m\_p(1)$ could be after a marked goal
$m\_p(X)$ on $Context$, we do {\em not\/} maintain an 
irredundant set (irrset) representation of non-ground facts.
This could result in some redundant derivations being performed.

We need both the magic facts for purpose of dependency information,
just as Ross does.
A partial solution would be to maintain separate magic relations for
use in the magic rules and non-magic rules on $P^{mg}$.
%%%%%%%%%%%%
}

\algorithm{
\> Insert\_in\_Context($\langle F_1, F_2 \rangle, Context$) \+ \+ \\
/* $F_2$ was used to compute $F_1$. */ \\
Let $p_i$ be the predicate of $F_1$. \\
(a) if ($F_1$ is subsumed by a fact in the
	$m\_p_{i_{done}}$ relation) ~~~ /* completely solved */ \\
\>  	return \\
(b) else \+ \\
	(i) \> Add\_After($F_1, F_2, Context$).\\
	(ii) \> if ($F_1$ is subsumed by some $F_3$ that occurs after 
		$F_1$ in $Context$) \+ \+\\
	    	    Delete $F_1$ from $Context$. \- \- \\
	(iii) \> else \+ \+ \\
	    Delete occurrences $F_3$ earlier than $F_1$ in $Context$ that are\\
	    \> not marked and are subsumed by $F_1$. \\
	    Let $F_4$ be the earliest fact in $Context$ subsumed by $F_1$. \\
	    \> /* This fact is either marked, or is the fact $F_1$ itself. */ \\
	    Collapse\_Nodes($F_4, F_1, F_2, Context$).  \- \- \\
	(iv) \> end if \- \\
(c) end if \- \\
end Insert\_in\_Context \-
}

\eat{
%%%%%%%%%%%%
We intuitively explain the rationale behind some of the operations 
performed by {\sf Insert\_in\_Context}.
In Step (b)-(ii), we delete the new (unmarked) fact if it is subsumed 
by some fact that appears later in $Context$.
This step is  meaningful, since the later fact will be made available 
for use before the new fact is made available.
Answers to this later fact are also answers to the new fact.
Thus, the new fact is redundant and can be deleted.
The reason for the deletion of earlier unmarked subsumed facts
in Step (b)-(iii) is the same, since these earlier facts have
not been made available yet.

If a newly generated magic fact $F_1$ has not been completely 
evaluated yet, the fact $F_2$ that generated it will occur as a 
marked fact in $Context$.
(Marked facts are removed from $Context$ by {\sf Remove\_Marked\_Subgoals}
only after they are fully evaluated.)
%%%%%%%%%%%%
}

{\sf Add\_After} below is used to insert $F_1$ in $Context$, as the 
last unmarked fact generated from $F_2$.

\algorithm{
\> Add\_After($F_1, F_2, Context$) \+ \+ \\
(a) \> if ($F_2$ is in the last marked node in $Context$ ) \+ \\
    (i) \> Add a new node containing $F_1$ to head of $Context$. \- \\
(b) \> else \+ \\
    (i) \> Let $N$ be the earliest marked node after $F_2$ in $Context$. \\
    (ii) \> Add a new node containing $F_1$ immediately before $N$ 
	in $Context$. \- \\
(c) \> end if \\
(d) \> Set the $ parent $ of $F_1$ to be $F_2$. \- \\
end Add\_After \-
}

\eat{
%%%%%%%%%%%%%%%
The intuition behind the call to 
{\sf Collapse\_Nodes} in Step (b)-(iii) of {\sf Insert\_in\_Context}
is as follows.
Suppose a newly generated subgoal $ m\_p_i (\overline{t_1}) $ 
subsumes an earlier marked subgoal $ m\_p_i (\overline{t_4})$.
In this case, $ m\_p_i (\overline{t_4})$ depends on the 
$ m\_p_i (\overline{t_1}) $, since each marked subgoal depends on 
all later subgoals.
Also, $ m\_p_i (\overline{t_1}) $ subsumes (and hence depends on)
$ m\_p_i (\overline{t_4})$.
Thus, a cyclic dependency has been established.
%%%%%%%%%%%%%%%
}

\eat{
%%%%%%%%%%%
An attempt is made to eliminate facts from the magic relation,
when we know that more general facts will be made available subsequently.
This helps in avoiding some redundant inferences.
%%%%%%%%%%%
}

{\sf Collapse\_Nodes} below ensures that all magic facts which cyclically
depend on each other are kept together in a node in $Context$; these
magic facts will be declared fully evaluated, and moved into the 
corresponding $m\_p_{done}$ relations together.

\algorithm{
\> Collapse\_Nodes($F_4, F_1, F_2, Context$) \+ \+ \\
if ($F_4$ is marked) ~~~~
	/* $F_4$ is in a different node from $F_1$. */ \+ \\
    (a) \> (i) \> Remove all marked nodes in $Context$ marked between
		(not including) the node \\
	\> \> \> containing $F_4$ and (including) the node containing $F_2$. \\
        \> (ii) \> Set the $Subgoals$ set of the node of $F_4$ to the 
		union of its $Subgoals$\\
	\> \> \> set and the $Subgoals$ sets of all the removed 
		nodes. \\
        \> (iii) \> Set the $unmarkedSubgoals$ set of the node of
       		$F_4$ to the union of its \\
       	\> \> \> $unmarkedSubgoals$ set and the $unmarkedSubgoals$
       		sets of all \\
	\> \> \> the removed nodes. \\
    (b) \> Delete the (newly inserted) node containing $F_1$ from $Context$.\\
    (c) \> if ($F_1$ is not subsumed by $F_4$) \+ \+ \\
	    Add $F_1$ to the $Subgoals$ set as well as the $unmarkedSubgoals$ 
	    set of \\
	    \> the resultant node. \- \- \\
    (d) \> end if \- \\
end if \- \\
end Collapse\_Nodes \-
}

\eat{
%%%%%%%%%%%
\footnotetext{It is possible to delete from the 
differential relations for $m\_p_i$ all facts in the collapsed node 
that are subsumed by another fact in the collapsed node,
without adversely affecting any of our results.
Not deleting such facts could slow down the evaluation, though
it would not compromise soundness or completeness.
%%%%%%%%%
% In the deductive database system CORAL we do not delete such facts,
% since this makes it easier to maintain certain indices.
%%%%%%%%%
}
%%%%%%%%%%%
}

\eat{
%%%%%%%
Once a subgoal $m\_p(\overline{t})$ has been completely evaluated---this 
happens when no new subgoals or answers can be generated in the evaluation
and every subgoal that $m\_p(\overline{t})$ depends on has 
been completely solved---
%%%%%%%
}
{\sf Remove\_Marked\_Subgoals} below is used to remove facts from
$Context$ and insert magic facts into the $m\_p_{done}$ relations.

\algorithm{
\> Remove\_Marked\_Subgoals($P^{mg}, Context$) \+ \+ \\
while (all facts in head of $Context$ are marked) ~~~
    /* head of $Context$ is completely solved */ \\
\> Add all magic facts in head of $Context$ to the corresponding 
    $\delta m\_p_{done}^{new} $ relations. \\
\> Remove head of $Context$. \\
end while \- \\
end Remove\_Marked\_Subgoals \-
}

{\sf SN\_Update} below is used to update the differential relations.

\algorithm{
\> SN\_Update($ p_{i} $) \+ \+ \\
$ p_{i}^{old} := p_{i}^{old} \sqcup \delta p_{i}^{old} $. ~~~
	/* no duplicate elimination is done by $\sqcup$. */ \\
$ \delta p_{i}^{old} := \delta p_{i}^{new} - p_{i}^{old} $. ~~
$ \delta p_{i}^{new} := \phi $. ~~
$ p_i := p_i^{old} \sqcup \delta p_i^{old}$. \- \\
end SN\_Update \-
}

\end{document}


