\section{\NF in Intuitionistic Logic Programming}
\label{sec:lamrelated}

Recently there has been some interest in combining {\em NF} with what
is known as intuitionistic logic programming.  The underlying
languages, with the exception of \cite{Harland93}, are either version
of N-Prolog or clausal intuitionistic logic.  Due to the inherently
difficulty with universal quantification mentioned in \ref{nfs-neg},
the treatment is deprived of parametric goals.  The emphasis is not on
the transformational approach but to combine the non-monotonic nature
of \NF with the capability of embedded implication to dynamically
update the current program.  We will not detail here the proposed
semantics (stable models \cite{Dung92}, monotonic Kripke-like models
\cite{Harland89}, non-monotonic perfect \cite{Bonner90} or
three-valued \cite{Giordano98} models).
 
 
%   on Kunen's semantics and/or 
% Gabbay's modal interpretation of {\em NF} into {\em G}, the modal 
% logic of Peano arithmetic, another facet of negation in logic 
% programming that we cannot pursue here.


\medskip
Gabbay \cite{Gabbay85} pointed out that \NF with embedded implication seems to lead to 
curious paradoxes, at the point of making the whole enterprise not 
logically sound.  This problem arises already  when dealing with normal 
clauses.

They can be summarized as follows (taken from \cite{Olivetti92}).
\ben
\item Failure of transitivity or in other terms non-eliminability of the cut rule.
Let $\cP$ be:
\[
\begin{array}{l}
a \If b\And \neg c\\
b \If c
\end{array}\]
Now,  $\cP\prv c\Imp b$ and $\cP\prv b\Imp a$ but $\cP\nprv c\Imp 
a$. 

\item
Failure of weakening.
Let $\cP$ be:
\beq
b \If \neg a
\eneq
Then $\cP\prv b$ but $\cP\nprv a\Imp b$.
\item ``Pathology of negative information'', \ie $\cP\prv \neg(A\Imp
  B)$ iff $\cP\prv A\Imp\neg B$
% \item
% Classical inconsistency: given the program $a\If (b\Imp c)$, $\neg a$ is 
% provable but the two are inconsistent in classical logic
\enen
There are several 
solutions to this riddle:
\bit
\item A modal completion \cite{Giordano98}.
\item A syntactic distinction between arrows \cite{Bonner90}.
\item A syntactic distinction between predicates \cite{Harland93}.
\enit
Our position:
\ben
\item
Provability must take into account the context where the query is
attempted: in case $1.$ the first  query is  not allowed, since $b$
is a  predicate which must be called from an empty context.
\item Similarly, $a\Imp b$ is not a legitimate query as $b$ must be
  queried in the empty context.
\item
This is indeed the operational semantics of failure of hypothetical
judgments; the issue is giving a logical justification of that and the
challenge is to give it without changing the logic underneath.
%\item
%the ``completion'' is indeed inconsistent and then the program is not complementable
\enen


\subsection{\NF in Clausal Intuitionistic Logic}

We can regard Clausal Intuitionistic Logic as a close (but less
fortunate) cousin of 
uniform proofs independently developed by McCarty in the late eighties 
\cite{Mc88a,Mc88b}; unfortunately the amount of operational details  
makes the system fairly opaque. \NF  
in this setting has been investigated in Bonner's thesis \cite{Bonner91phd} 
and are summarized in \cite{Bonner94}.  The framework in \cite{Bonner90} is 
hypothetical datalog (with possibly infinite constants) and embedded implications.  
They assume a notion of negation-stratification and develop an awkward 
proof-theory parameterized by strata; a non-monotonic preferred Kripke 
model theory is presented and adequacy is demonstrated.  They offer 
the following solution to the aforementioned paradoxes: the 
implication sign is really two distinct connectives, one for clauses 
and one for goals.  Clause implication is interpreted classically and 
it is transitive, while goal implication is not and must be 
interpreted non-monotonically.  Indeed the latter has a \emph{modal} 
semantic which takes into account the extension of a context as a 
shift in worlds (in the Kripke sense).  While we favor a syntactic distinction between goals 
and clauses, the uniform proof approach views implication as logical 
(intuitionistic) implication whose different behavior is simply 
dictated by its introduction and elimination 
rule.  Moreover we do not aim to deal with arbitrary extensions. We have
hinted in the previous Section how to linear \lp can address examples in this paper
which are outside the fragment we are able to treat.  
% Still, we believe that some of them, as the Hamiltonian circuit 
% problem, can be addressed more declaratively in a \emph{linear} 
% negation-free framework.
 
\subsection{\NF and N-Prolog}

This approach has been investigated first at the propositional level 
in \cite{Olivetti92} and then for first-order N-Prolog in
\cite{Giordano98}:
\begin{quote}
  ``In order to understand N-Prolog computations with \NF, we must
  adopt a dynamic view of success and failure [\ldots] we cannot
  determine what goals succeeds or fail from a program unless we
  determine what goal succeeds or fail from
  \emph{arbitrary}\footnote{Italics is mine.} extension of the
  program'' \cite{Olivetti92} pp.\ 258
\end{quote}

The main idea is again that a computation of an implicational goal
$D\Imp G$ from $\cP$ entails a shift to another world where $\cP\cup
D$ holds.  The authors propose a completion construction as an
explanation of negation-as-failure.  The completion is formulated as a
infinite theory such that $comp_{n}(\cP)$ is used to evaluate a goal
$G$ roughly if we need $n$ extensions of the program to compute $G$:
for example for a clause $a \If (b\Imp c)$ then $a$ is provable iff
$comp(\cP\cup b)$ entails $c$ and $a$ is false iff $comp(\cP\cup b)$
entails $\neg c$.  Note that $comp(\cP\cup b)$ is different from
$comp(\cP) \cup b$ or $comp(\cP) \cup comp(b)$.  Moreover, due to the
possible non-monotonicity of arbitrary extensions the $comp(\cP)$ and
$comp(\cP\cup B)$ may be jointly inconsistent: the modality represents
then the shift of context.  The completion construction does not seem
to generalize immediately to universally quantified goals.  The right
kind of logic turns out to be a three-valued version of $K4$.  The
authors prove soundness and completeness of ESLDNF derivability \wrt a
Kripke-Kleene fixpoint construction for a notion of non-floundering
programs.  The three-valued approach allows not to restrict to
stratified programs.

\subsection{\NF in \fo Uniform Proofs}

Harland's thesis \cite{Harland91phd} is an attempted analysis of Uniform 
Proofs and {\em NF} at the first-order level. Unfortunately, his 
approach, though sound, is essentially useless, as we shall argue next.

Harland inherits the traditional `boolean' attitude \wrt the closed
world assumption: predicates are either \emph{completely defined}
(CWA), as in the \texttt{append} program, or incomplete (OWA); while
this distinction, he maintains, is essentially semantic and therefore
enforced by user declarations, the latter coincide with the programs
where temporary assumptions are made, \ie clauses with embedded
implications.  Thus {\em NF} would make sense only for the former,
since how, will you apply the CWA to something that is by definition
incomplete?  Therefore those programs would require some form of real
(say minimal) negation, much as in \cite{Momigliano92}. Technically,
this is achieved distinguishing, for all predicates occurring in the
signature, those which appears negatively versus positively in the
body of clauses. The two sets are required to be disjoint. This of
course simplify the later development, unfortunately at the cost of
irremediable trivializing the whole enterprise. In fact, if a
predicate which appears negatively, \ie it is assumed, cannot occur
positively, then it will never be used in the derivation. Its
assumption is totally irrelevant to the computation and may be
discarded from the program. The fragment studied by Harland then
collapses to normal programs with extensional quantification.

Then he shows how to formulate the completion as an object fohh
formulae so as to simulate {\em NF} as derivability in the uniform
proof system.  The executable completion is formulated through
contraposition.  Programs are assumed to be locally stratified, hence
the completion is consistent.  Thus Harland stumbles in the fallacy of
considering the completed programs as its iff-completion, though he
correctly has $\mnot(D\Imp G) = D\Imp \mnot (G)$.  This operational
interpretation of the \emph{augment} instruction \wrt negation is
nevertheless inconsistent with its formulation in the completion,
where negation is interpreted classically insofar as the negative
completion is seen as $\neg (p\And \neg Body)$.  The classical
attitude carries over to universal quantification, which is only
allowed to be extensional.  Harland so misses the intrinsic connection
between implication and parametric universal quantification.
Extensionality is achieved through covering as in \cite{Mancarella88},
though the role of the \emph{DCA} (Domain Closure Axiom) is not made explicit.  Therefore Harland is
not able to correlate extensional uniform proofs with intuitionistic
provability plus \emph{DCA}.  This is not surprising since its
partition between complete and incomplete predicates restricts the
AUGMENT rule so that its operational provability relations are not
conservative extensions of standard uniform provability: this makes
the usual proof-theoretic adequacy impossible.  Moreover no
operational semantic for coverings is described: not only the role of
free variables introduced by coverings is unclear, but the extensional
rules are totally non-deterministic \wrt the choice of the correct
covering.

An equality/inequality solver on the Herbrand universe is described 
and used to solve inequalities stemming from the completed 
definitions: this algorithm is different from the traditional 
\emph{uncover} algorithm as it does not return the most general 
solution but a possibly infinite enumeration of the latter; this 
permits not to left linearize the program.


\subsection{PID}
\label{gcla}
\renewcommand{\cD}{\mathbf{\cal D}}

\emph{Partial Inductive Definitions} (\cite{Halnass91}) are a 
generalization of inductive definitions \cite{Acz77} to definiens 
containing implications and (for a finitary version 
\cite{Eriksson93phd}) parametrical quantification: they also 
incorporate a proof-theoretical notion of closure somehow as in the 
CWA, but brought upon by the principle of \emph{definitional reflection}.  
In a logical setting, following \cite{SchroederHeister93lics}, we take 
an intuitionistic sequent calculus parameterized by a set of 
\emph{definitions}, \ie a finite set of clauses $b \Leftarrow G$.  For 
a definition $\cD$, we call $\cD(a) = \{\sigma G \mid b\Leftarrow G 
\in \cD, a=\sigma b\}$.  In the spirit of the ``clauses-as-rules'' 
paradigm \cite{Halnass90,Halnass91jlp} we add for every defined atom, 
the rules
\[
\ianc{\GG\prv G\quad G\in \cD(a)}{\GG\prv a}{\cD-R} \quad 
\ianc{ \{\sigma\GG,\sigma G \prv A : \sigma = mgu(a,b), b\Leftarrow 
G \in \cD \} }{\GG,a\prv A}{\cD-L}
\]
Call this $DR(\cD)$, for a given set of definitions $\cD$.
The first rule corresponds to backchaining on the definitional 
clauses, while the second, in its $\omega$-version, reflect the 
closure clause of (partial) inductive definitions.  They can be seen as right and 
left introduction rules for the non-logical symbol $a$: This feature 
is used in the programming language \emph{GCLA} \cite{Aronson91} which 
allows both functional and \lp style.  Search is conducted on sequents 
$\GG\prv G$ and it is clearly non-amenable of a uniform proof 
approach, since focusing is impossible as at any time each of the 
assumption in the antecedent may be expanded via $\cD-L$.  Indeed, 
without mentioning the issue of contraction, control in this setting 
has proven to be a major problem and this has lead to \emph{GCLA II}, 
which is a middle ground between a \lp language and a tactic theorem 
prover \cite{Kreuger92}.
 
One basic problem is the failure of cut-elimination: accordingly to 
the symmetry of the definitional rules, a reduction step can be 
performed by a local cut.  Global cut-elimination, however, is not 
possible in general, as discussed in \cite{SchroederHeister93lics}, since in order to 
reduce an atomic cut formula thru the $\cD-L/ \cD-R$ reduction we may 
generate a cut with a more complex definiens formula.  Definitions are 
called \emph{total} if they enjoy cut-elimination, otherwise they are 
\emph{partial}: classes of total definitions include:
\bit
\item Implication-free programs.
\item Contraction-conscious logics.
\item Stratified program \wrt negation.
\item Stratified program \wrt implication \cite{MacDowell98}.
\enit
 Here predicates 
are assigned \emph{levels}: the latter are then extended to formulae, 
so as to forbid recursion thru negative 
occurrences; the level of an implication is essentially the order of 
its type: definitions are allowed only if the level of the heads is 
strictly greater then the level of the body: for instance $a\Leftarrow b\Imp a$
is allowed while $a\Leftarrow a\Imp b$ is not. This excludes every
left-recursive definition.

Definitional reflection brings in a proof-theoretic notion of 
negation.  Intuitively, $\cD-L$ works as the only-if clause of the 
completion: a proof of $\prv \neg a$ is a proof of $a\prv\bot$.  This 
has been formalized by Schroeder-Heister who has proven \cite{SchroederHeister93lics} 
the equivalence between $comp(P)$ and $DR(P)\cup (x =x \Leftarrow 
\top)$, where the latter clause formalizes $CET$.  This result holds 
for any kind of definition and does not depend on cut-elimination.  
This has been hailed by the \emph{GCLA} group as a major benefit of 
allowing definitional reflection.  In fact negative goals are no 
different from others and therefore seem to compute answer 
substitutions.  This claim has some validity as far as normal 
stratified programs and ground goals are concerned: indeed they may yield only sequents 
such that if the antecedent is non-empty, it must be atomic and the 
consequent is $\bot$: then $\cD-L$ must be used to introduce a 
definiens from a lower stratum.  As mentioned above, search is here 
cut-free.  The equivalence with the completion holds irrespectively of 
the presence of local variables.  In this remark, then this approach 
would seem to have an edge on the transformational one since it does 
not need extensional quantification.  

\begin{Example}
Consider a graph $edge(a,b), edge(b,c)$: the deduction of 
$path(b,a)\prv\bot$  leads to the conjunctive goals 
$\{edge(b,a)\prv \bot),(edge(b,Z)\And path(Z,a)\prv\bot\}$, where
there is a computation which reduces to $\bot,\GG\prv\bot$.
\end{Example}

  On the other hand the usual issue 
with floundering arises when concerned with open queries.  When logic 
variables are allowed PID's give the usual unsound reading to 
existential queries and one is faced again with the question of 
\emph{failure substitutions}. 
For example the query $\vd\exists x\neg even(x)$ yields
$even(X)\vd\bot$; the rule $\cD-l$ will loop, being unable to compute
to what amounts, in out terms, to $\mnot(0)\cap\mnot(s(s(X)))$.

 % For
% example the deduction of $path(b,Y)\prv\bot$ eventually leads to the 
% conjunctive goals $(edge(c,Y)\prv \bot),(edge(c,Z)\And 
% path(Z,Y)\prv\bot)$, where it is not enough to know that 
% $\cD(edge(c,Z))= \bot$, but to provide an answer to the query we need 
% to instantiate $Z$ to a failing value to to proceed in the 
% computation: this is of course equivalent to use a covering. 
I an not aware of any implementation of the $\omega$-rule for the 
purpose of enhancing a logic language with negation.  As a 
matter of fact, the rule of definitional reflection used in 
\emph{GCLA} is the weaker `logical' version \cite{Aronson91} which does 
not imply in general the completion.


Notwithstanding the similarity, PID's give a striking different 
operational semantics to hhf.  Consider for example the definition $a 
\Leftarrow b \Imp c$: then the sequent $\prv \neg a$ has no cut-free 
proofs, while $\prv a$ is provable against our operational intuition:

\[
 \ianc{ \ianc{ \ianc{\bot\prv c}{b\prv c}{\cD-L}}{\prv b\Imp 
 c}{\Imp-R}} {\prv a}{\cD-R}
\]
Here, since $b$ has no definition, it is assumed to be false and hence 
entails anything.  This means that $\cD-L$ is not conservative \wrt 
the positive fragment, \ie the former rule may be used in proving 
positive atoms.  In the complementation approach instead, positive and 
negative fragments are disjoint and exclusive. This is no surprising 
since, as mentioned above, the equivalence with the iff completion 
induces an operational semantics of failure which is distinct from the 
one  typical of hhf.
Moreover definitional reflection does not match well with parametric
judgments:
\bmeta Elaborate \emeta
\renewcommand{\cD}{{\cal D}}
\newpage












