

\section{The Trouble with Local Variables}
\label{local}

 even starting with a Horn program, the transformed one
may contain universal quantification in the body, stemming from
local variables. Consider a program for (irreflexive) transitive 
closure of a relation, which keeps also track of the intermediate 
elements in the path construed, 
in the 
version of \cite{Bro90}

\begin{Examplen}
\label{path}

\[\begin{tt}\begin{tabular} {llll} 
path(X,Y) & \Ift & path3(X,Y,ZS)\\
path3(X,Y,[]) &\Ift & edge(X,Y). \\
path3(X,Y,Z.ZS)& \Ift & edge(X,Z), path3(Z,Y,ZS). \\ 
\\
edge(a,b).\\
edge(b,c).\\
\end{tabular}\end{tt} \]

The complement of the program follows:

\[\begin{tt}
\begin{tabular} {lll} 
nonpath(X,Y) &\Ift &  all ZS. nonpath3(X,Y,ZS). \\
nonpath3(X,Y,[]) & \Ift & nonedge(X,Y).\\
nonpath3(X,Y,Z.ZS) & \Ift & nonedge(X,Z).\\
nonpath3(X,Y,Z.ZS) & \Ift & nonpath3(Z,Y,ZS). \\ 
\\
%nonedge(b,a).\\
%nonedge(a,a).\\
nonedge(a,c).\\
nonedge(b,b).\\
nonedge(X,a).\\
nonedge(c,b).\\
nonedge(c,c). % c,X may coincide with X,a on c,a
\end{tabular}\end{tt} \]
\end{Examplen}


This raises several important questions:
\begin{enumerate}
\item
What is the operational reading of universal quantification
in this setting 
\item
How it mingles with generic judgments (discussed in 
Section~\ref{uquant}) ?
\item
How can this be reflected in the theory of inductive definitions
\cite{Acz77} (discussed in~\ref{ind}) ?
\end{enumerate}
 We  start 
asking the naive query $\If nonpath(c,c)$, with the intuitive reading 
that indeed it should succeed since the graph is irreflexive.  Thus 
the 
subgoal $\If \forall^e ZS. nonpath3(c,c,ZS)$ should eventually 
succeed.
Nevertheless a naive exhaustive search would loop, since there are 
infinite paths between $c $ and $c$ in the (cyclic) antigraph.

We thus turn to the literature \cite{Man88,Bro90,Har91a}.Similarly to  implication, several attempts
to allow universally quantification in  goals in a 
controlled way were proposed in the mid 80's (see NQ-Prolog
\cite{Gab84}, NI \cite{Gab86}, clausal intuitionistic logic
\cite{McC86}. A possible source of misunderstanding was perhaps the confusion
between what we now know as the {\em intensional} \cite{Mil91b} 
vs.\ {\em extensional} \cite{Bar90} interpretation of $\forall$, as 
well as the implicit assumption
of the Closed World Assumption (CWA).
\begin{itemize}
\item
Extensional:\\
$\forall^e x. G$ holds if for all closed terms $t, [t/x]G$ 
holds
\item
Intensional:\\
$\forall^i x. G$ holds if for a new parameter $a, [a/x]G$ holds.
\end{itemize}
\begin{Examplen}
\label{ex:psx}
Consider the ``program'' $q(a)$; the query $\forall^e x.q(x)$
follows logically from $P \cup DCA$ (in every normal model---this 
will be assumed from now on) and should accordingly succeed;
symmetrically $\Pi x.q(x)$ does not and it fails, as it should. Yet
take the slighter more complicated program:
\[\begin{array} {l}
 p(0)\\
 \forall x. p(s(x))
\end{array} \]
the query $\forall^e x.p(x)$ apparently fails to terminate even
it follows logically from $P \cup DCA$, yet every instance $p(s^n(0))$ 
is provable. The query $\Pi x.q(x)$ still fails.
\end{Examplen}
Coming back
to Example~\ref{path}, you may check that the intensional version
of $\If \Pi ZS. nonpath(X,Y,ZS)$ makes no sense.
\end{sloppy}
Note that we have so far  carefully avoided to discuss an interpreter 
for extensional quantification. This is not a coincidence. Barbuti's 
first solution is eminently operational, cryptic and 
incomplete too. Namely, for a predicate $q$ and its complement $q^c$, 
a query $\If \forall y q^c(x,y)$ succeeds 
whenever:
\begin{enumerate}
\item 
$\If q^c(x,y)$ is computed producing a candidate substitution $\q$
\item 
$\If q(\q x,z)$ fails finitely, for $z$ fresh.
\end{enumerate}
\begin{sloppy}
You may indeed check that the query $\If nonpath(c,c)$ succeeds, $\If 
nonpath(b,X)$ yield answers $X=a, X=b,X=b\ldots$ and $\If nonpath(a,c)$ fails.
\end{sloppy}
The idea seem to use the knowingly mistaken interpretation that \NF 
gives to quantifier in non-ground queries (see Introduction~\ref{}) 
to 
achieve the result. The source of incompleteness can be localized to 
the interaction between local variables and conjunction, namely the 
candidate substitution may be too general to yield the desired finite 
failure (see example at pp.\ 213--214 in \cite{Bar90}).  Indeed the 
procedure has to be further factorized as follows:
\bit
\item
If $\If q(\q x,z)$ has only finite failure derivations, then succeed
\item
otherwise further instantiate $\q x$ and go to the previous step.
\enit

This instantiation is achieved by a procedure  {\tt herbrand} which
enumerates the term model. Of course, when dealing with an infinite 
universe, the procedure always diverges, as admitted by the authors 
(pp.\ 226). Hence:
\begin{quote}
``\dots It is meaningless to talk about the finite failure of {\em 
SLDN}''
\end{quote}

Indeed, a clever usage of the $DCA$ may alleviate this problem as 
explained in \cite{Mom95} and reported in Section~\ref{mdca}.

Nevertheless,  we thus agree  w.r.t.\ regarding the overall 
unfeasibility of this approach, as unable to 
grant completeness. Therefore we
abandon this problematic generate-and-test
approach and turn to the refinement of  extensionality that goes 
under the name of {\em proof by case analysis}, shortened in 
$CASE$ \cite{Man88,Bro90}
(and somehow also  \cite{Har91a}), which is naturally suggested by 
the second program quoted in Example~\ref{ex:psx}.

\smallskip
$CASE$ is based on two pillars: the idea of   {\em term covering} 
\cite{Man88}, i.e.\ an intensional finite representation of all the 
ground instances of a term, and on the operational reading of an 
opportune instance of (an equivalent of) the $DCA$.

To give the idea away, the point is to prove a positive universal 
statement by proving a {\em finite} set of its instances which 
nevertheless constitute a {\em covering} of the original one.
\[
\begin{array}{lr}
P \vdash \forall x: \tau . G \ \mbox{iff } P \vdash \Pi [t_i/x]G \ 
\mbox{for } t_1\dots t_n /x & CASE
\end{array}
\]