\chapter{Local Variables}

\section{The Trouble with Local Variables}
\label{local}
This section could also be entitled `What has universal 
quantification to 
do with the negation technique ?'


Answer: 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}\footnote{Why, you would ask, complicate 
one's life 
with a third argument: well the clue is: consider the (d) clause in 
flat 
programs.}:

\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}
This section is devoted to addressing the first one. 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}.

\section{Logic Programming and Universal Quantification}
\label{uquant}

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})\footnote{The trend is still going on, see Gabbay's 
chapter `Elements of Algorithmic Proof' in \cite{Gab94}.}; They all showed, as far as I am concerned, 
an amazing amount  of technicalities, restrictions,
lack of clear operational semantics and mostly the absence
of a programming language significance, which is the original
sin of all dead languages\footnote{To alleviate this, I have to 
mention that the impetus to develop NQ-Prolog was the attempt
to formalize the British Nationality Act; yet this hardly qualifies
as a development of programming languages feature.}.

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). This is connected with what 
has come to be known as the {\em universal query problem} 
\cite{Apt95,Kun87}, discussed in Chapter~\ref{defs}\footnote{This 
section must be updated: we need to consider also partial predicates 
\cite{Wag91}.}.
%\footnote{Note that we only introduce this distinction for 
%goals.}:

\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}

We will use the notation $\Pi$ for the latter, for reasons that will 
become apparent in the sequel. This dichotomy  is also characterized 
as the difference between the model and proof-theoretical approach.


There is a not so obvious relation\footnote{To be further discussed} 
with what we intend the domain
of computation to be (recall that in the \lp \, tradition this
is central to define the intended term model).

\begin{itemize}
\item
Closed Domain:\\
the signature is fixed once and for all as the one
underlying the program; this is enforced by the $DCA$, 
the  first-order approximation of the CWA

\item
Open Domain:\\
the signature is taken to be infinite; in operational
terms this means that it is free to expand during execution
 by parameters\footnote{I assume at this point that parameter 
introduction is consistent with $CET$. Everything should boil down to 
adding/dropping the $DCA$. Infinite languages and parameter 
introduction should be orthogonal.}.
\end{itemize}

This has some relevant model-theoretic consequences that
we may not pursue here (see Theorem 1 in \cite{Man88}). At the risk 
of being trivial we instead give the following:

\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}


Before rushing to declaring the intensional approach the obvious 
winner, let me point out the following:
\begin{enumerate}
\item
It does not seem at the Horn level to be a problem of classical versus 
constructive logic; the above derivations exists in the minimal 
predicative calculus with equality\footnote{More precisely with the 
congruence axiom for the mentioned predicates, see the $M1$ rule in 
Section~\ref{disunif}.} and $DCA$.  For finite signatures, it would 
be  a 
showing of  sophisticated taste not to take $DCA$ as a constructive principle.  Infinite 
ones do not arise because they conflict with the Closed Domain 
Assumption.  Even OWA signatures stay finite \wrt terminating 
computations
\item
The issue of choice of domain is strongly linked to (constructive) 
negation: going back to the first example above: a query of the type 
$\If \exists x .  \Not q(x)$ could succeed in the Open Domain with 
answer something like $x \not =b$, for a new parameter $b$.  Yet it is 
not fair to consider constructive negation in the Open Domain as 
something already given\footnote{In CWA the only answer would be 
$x \not =a$ for the only element domain $\{a\}$: to be further 
discussed: the OWA answer interctr with the UQP.} .
\end{enumerate}


There is no contest that intentional quantification has proved to be 
a really novel and useful language feature: Miller has made a 
convincing case for its usage to implement local declarations and 
abstract data types
in $\lambda$Prolog; furthermore the $\Pi$ operator  in Elf is the 
cornerstone of allowing hypothetical and parametrical judgments. 
Nevertheless
it seems that the only reasonable interpretation of universal
quantification originating from local variables is an extensional 
one\footnote{This interpretation may also be useful in a Datalog 
sense \cite{Llo84,Llo86}.}. 
\begin{sloppy}
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.

We will next quote the model-theoretic results which support this new 
kind of rule. We will also mention the stronger completeness result 
that can be achieved for \SLD \ and \NF.
We stress again that the reference theory we are using is the 
completion of the program plus $CET$ enriched of the $DCA$. Moreover
the latter can be shown to be  a conservative extension of Clark's 
completion w.r.t.\ 
universal positive queries.
