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

Recently there has been some interest in combining {\em NF} with what 
is known as intuitionistic logic programming.  The underlying 
languages 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 generic 
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 the semantics (stable models \cite{Dung92}, monotonic 
Kripke-like models \cite{Har93}, 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.


\subsection{N-Prolog and the paradoxes of \NF}
Gabbay \cite{Gab85}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 even when dealing with normal 
clauses.

They can be summarized as follows (taken from \cite{Olivetti92}):
\ben
\item Failure of transitivity and  modus ponens (In our terms this 
amounts to saying that the cut rule in not eliminable)
\begin{Examplen}
Let $\cP$ be as follows
\[
\begin{array}{l}
a \If b, \neg c.\\
b \If c
\end{array}\]
Now,  $\cP\prv c\Imp b$ and $\cP\prv b\Imp a$ but $\cP\not\prv c\Imp 
a$. 
\end{Examplen}
\item
Failure of weakening
\begin{Examplen}
Let $\cP$ be as follows
\beq
b \If \neg a
\eneq
Then $\cP\prv b$ but $\cP\not\prv a\Imp b$
\end{Examplen}
\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{Har93}
\enit
Our position:
\ben
\item
our notion of assumable goal and probability from the empty context:
 in the above case the first two queries are not allowed , as $b$ and $c$ are not assumable.
\item as above
\item
this is the semantics of failure of hypothetical judgments
\item
the ``completion'' is indeed inconsistent and then the program is not complementable
\enen


\subsubsection{NF in Clausal Intuitionistic Logic}

We can regard Clausal Intuitionistic Logic as a close 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.  Hypothetical datalog and 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 
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 world.  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 (AUGENT) and elimination (BACKCHAIN) 
rule.  Moreover we do not want to treat arbitrary extensions.  The 
examples in the paper 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{Embedded implication as a modality}

This approach has been investigated first at the propositional level 
in \cite{Olivetti92} and then for first-order N-Prolog in \cite{Giordano98}.  ``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.  The main idea is 
that a computation of en embedded goal $D\Imp G$ from $\cP$ entails a 
shift to another world (in a Kripke sense) where $\cP\cup D$ holds.  
The authors propose a completion construction as an explanation of 
negation-as-failure: 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 generalize immediately to universally quantified 
goals: one possibility is to allow in the completion an `intentional 
only' universal quantifier which can be instantiated only to 
parameters.  The right kind of logic turns out to be a three-valued 
version of $K4$.  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$.  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{Mom93}. 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, if not 
exhaustive. This of course simplify the later development, 
unfortunately at the cost of irremediably 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 (or at best as strong 
negation) insofar as the negative completion is seen as $\neg (p\And 
\neg Body)$.  The classical attitude carries over to universal 
quantification, which is allowed to be only extensional.  Harland so 
misses the intrinsic connection between implication and parametric 
universal quantification.  Extensionality is achieved thru covering as 
in \cite{Mancarella88}, though the role of the DCA is not made explicit.  
Therefore Harland is not able to correlate extensional uniform proofs 
with with intuitionistic provability plus \emph{DCA}.  This is not 
surprising since its partition between complete and incomplete 
predicates restricts the AUGMANT 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}
\newcommand{\cD}{{\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 $a \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\footnote{\ie the standard but usually forgotten 
restriction that nothing else belongs to the (partial) inductive set.} 
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}. 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.
\enit

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 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.  For example the deduction of 
$path(b,a)\prv\bot$ eventually leads to the conjunctive goals 
$(edge(b,a)\prv \bot),(edge(b,Z)\And path(Z,a)\prv\bot)$, where both 
reduce to $\bot,\GG\prv\bot$.  On the other hand an 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 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.
%  The closure condition 
% is in a sense global and requires specific control every time the 
% antecedent of the goal is not empty.  On the other hand, 


% 
% % ref
% % \bibitem {SH92} p. S H. Cut-Elimination in logics with definitional 
% % reflection. In: D. Pearce\& H. Wansing (eds.) Non-Claiisical Logics 
% % and Information Processing, LNAI, Springer-Verlag 1992.
% % 
% % \bibitem {MacD97} R. MacDowell . Phd Thesis Upenn 1997.
% % \bibitem {Kre93} Per Kreuger. GCLA II. A Definitional Approach to 
% % Control. SICS research report R92:09
% % \bibitem {Aro93} M.  Aronson. Implementation issues in GCLA II. 
% %  A-Sufficiency and the Definiens Operation. SICS research report R93:02
