\section{Introduction to HHF Complementation}
\label{sec:intro5}


\newcommand{\Mtwo}{\mathcal{M}_2}
\newcommand{\foldn}{FO\lambda^{\Delta I\!\!N}}


Consider the following judgment to check whether a lambda terms is 
\emph{linear}\footnote{Do not confuse this notion with the one which
  refers to a term not having repeated occurrences of the same
  existential variable.}, if every functional subterm uses each of its
arguments exactly once:
 \newcommand{\lin}{\mbox{ linear}}
\newcommand{\linx}{\mbox{ linear in }x }
\renewcommand{\lx}{\Lambda x \,.\, }
\renewcommand{\ly}{\Lambda y \,.\,}
\bca
%\phj{x\lin}{u}{ x \lin}{\linear\atm}\qquad
\ibnc{ e_1 \lin}{e_2\lin}{  (e_1\ e_2) \lin}{\lin\cdot}
\vsk
\ibnc{ \begin{array}{c}\vsk\vsk \lx e\linx\end{array}}{\begin{array}{c}
                        \ianc{}{x\lin}{u}\\
                         \vdots\\
                        e\lin\end{array}}
                         {\lx e\lin}{\lin\l^{x,u}}
\vsk\vsk
\ianc{}{  \lx x\linx}{ \l}
\qquad
\ianc{ \lx e\linx}{ \lx \ly e\linx}{ \l^y}
\vsk 
\ianc{  \lx e_1\linx}{ \lx (e_1 \ e_2)\linx}{ _1\cdot} 
\qquad
\ianc{  \lx e_2\linx}{ \lx (e_1 \ e_2)\linx}{ _2\cdot} 
\eca

Intuitively, we check for linearity of a function making sure that
the it is linear in its first argument (judgment `$\lx e\linx$')
and then recurring on the rest of the expression. Note the rule
`$\lin\l^{x,u}$' is {\em hypothetical\/} in $u$ and {\em parametric} in $x$;
rule $ \l^y$ is instead only parametric in $x$.

\renewcommand{\lx}{\lambda x\,.\,}
\renewcommand{\ly}{\lambda y\,.\,}
Frameworks based on HHF provide an ideal syntax to represent these
judgments; namely, via the usual encoding introduced in Example \ref{ex:lam}:
\begin{Example}
\label{ex:linear}
\beq
linlam& : & linear(lam\ \lx E\ x)\\
& & \qquad\If  linx( \lx E\ x)\\
& & \qquad \If (\PI{x}{exp} linear(x)\Imp linear(E\ x)).\\
linapp & : & linear(app\ E_1\ E_2)\\
& & \qquad\If  linear(E_1)\\
& & \qquad \If linear(E_2).
\vsk
linxx& : & linx(\lx x).\\
linxap1& : & linx(\lx app\ (E_1\ x) \ E_2)\\
& & \qquad\If  linx(\lx E_1\ x).\\
linxap2& : & linx(\lx app\ E_1\ (E_2\ x))\\
& & \qquad\If  linx(\lx E_2\ x).\\
linxlm& : &linx(\lx lam(\ly E\ x\ y))\\
& & \qquad\If (\PI{y}{exp} linx (\lx E\ x\ y)).
\eneq
\end{Example}
The judgment and its implementation is clearly a decision procedure.
It does make sense to ask ourselves what is its complement. An
expression is {\em not\/} linear if there is some function which
either does not use its argument or uses it more than once.  We
first observe that, since \texttt{linear} is a relation defined via
exhaustive and exclusive patterns term
complementation does not play a role. Then, the complement of {\tt
  linapp} does not pose any problem, as it is a Horn clause: an
application in not linear if either the first element or the second in
not linear.  
\beq
\neg linapp & : & \neg linear(app\ E_1\ E_2)\\
& & \qquad\If  \neg linear(E_1)\Or\neg linear(E_2).  
\eneq 
A lambda expression in not linear
in two cases: first it is not linear in its first argument:
 \beq
\neg linlam1& : & \neg linear(lam( \lx E\ x))\\
& & \qquad\If \neg linx(\lx E\ x).  
\eneq

Secondly, 
if its body is not linear. Now, this poses  new problems, as we have
to negate a hypothetical and parametric clause. Let us follow our nose and reason by example: suppose we are
given, in the empty context
a goal $linear(lam(\lx lam(\ly x)))$, which is unprovable, since the
second lambda term is not linear in $y$; the proof tree yields the
failure leaf  $linx(\lx z)$, for a new parameter
$z$, in the context $z\oftp exp;linear(z)$. Our guiding intuition is that
we want to mimic a failure derivation so as to provide a successful
derivation from the  negative definition, \ie
 a proof of $\neg linx(\lx z)$ from $z\oftp exp;linear(z)$; this shows one prominent feature of
complementation of an HHF formula: negation `skips' over $\Pi$ and
$\Imp$, since it needs to mirror failure {\em from\/} assumptions. 

Let
us turn to complementing the judgment $` \linx$'.  A first point to note in that, by
encoding an object expression `e' with a pattern variable, we must make sure that in clause
{\tt linxap1,linxap2} the variable $x$ {\em does\/} not occur in the
argument which 
is not checked. We thus embed the clause in the strict $\l$-calculus
and `$E$' in the simple term `$E\ x^0$'. For the sake of
readability we do this only for the two aforementioned clause and we
also hide $()^u$ annotations.  
\pagebreak
\beq
linxap1& : & linx(\lx app\ (E_1\ x) \ (E_2\ x^0))\\
& & \qquad\If  linx(\lx E_1\ x).\\
linxap2& : & linx(\lx app\ (E_1\ x^0) \ (E_2\ x))\\
& & \qquad\If linx(\lx E_2\ x). 
 \eneq 
Via term complementation and intersection in the
strict $\l$-calculus we obtain, among others:
 \beq
\neg linxap0& :& \neg linx(\lx app\ (E_1\ x^1) \ (E_2\ x^1)).
%\neg linx2& :& \neg linx(\lx app\ (E_1\ x^1) \ (E_2\ x)). 
\eneq
Moreover, as in the case of top-level application, the complement of
{\tt linxap$_i$} holds if the body does not hold: 
\beq
\neg linxap1& : & \neg linx(\lx app\ (E_1\ x) \ (E_2\ x^0))\\
& & \qquad\If  \neg linx(\lx E_1\ x)\\
\neg linxap2& : & \neg linx(\lx app\ (E_1\ x^0) \ (E_2\ x))\\
& & \qquad\If \neg linx(\lx E_2\ x).  
\eneq 
Now, let us examine clause
{\tt linxlm} and let us reconsider the failure leaf $ linx(\lx z)$
from the context $z\oftp
exp;linear(z)$. In a first attempt, let us consider
what the complement would be  according to the idea above: 
\beq
\stackrel{?}{\neg} linxlm& : &\neg linx(\lx lam(\ly E\ x\ y))\\
& & \qquad\If (\PI{y}{exp} \neg linx (\lx E\ x\ y)).
\eneq 

However, there is no way to obtain a proof of $ \neg linx(\lx z)$ from
the current context. Indeed, the {\tt linxlm} clause does not carry 
enough information by itself so that its complement can mimic the
failure proof. In a sense that we will make precise, the clause, and
in turn its predicate definition is not {\em assumption-complete\/}:
once it has introduced a new parameter, the clause only specifies how
to use it in a positive context. It is up to us to synthesize its
dynamic negative definition, in this case exactly $\neg linx(\lx z)$.  More
generally, it is a characteristic of HHF that the negation of a clause
is not enough to determine the behavior of a program under
complementation.  We will have to insert (via a source-to-source
transformation) additional structure in a predicate definition in order
to completely determine the provability and failure of goals which
mention \emph{parameters}. By observing the structure of all possible
assumption that a predicate definition can make, we will {\em
  augment\/} those assumptions with their negative definition.  In
particular, we first augment the clause \texttt{linxlm}: 
\beq
\ald(linxlm)& : &linx(\lx lam(\ly E\ x\ y))\\
& & \qquad\If (\PI{y}{exp} \neg linx(\lx y)\Imp linx (\lx E\ x\ y)).
\eneq so that, by complementation, we obtain \beq
\neg \ald(linxlm)& : &\neg linx(\lx lam(\ly E\ x\ y))\\
& & \qquad\If (\PI{y}{exp} \neg linx(\lx y)\Imp \neg linx (\lx E\ x\ 
y)).  \eneq
Moreover, we need to do the same with the \texttt{linlam} clause,
since the \texttt{linx} predicate may occur as a subgoal:
\beq
\ald(linlam)& : &  linear(lam( \lx E\ x))\\
& & \qquad\If   linx( \lx E\ x)\\
& & \qquad \If(\PI{x}{exp} (\neg linx(\ly x) \And
linear(x))\Imp \neg linear(E\ x)).\\ 
\eneq

 In summary the negative program is: 
\pagebreak
\beq
\neg linapp & : & \neg linear(app\ E_1\ E_2)\\
& & \qquad\If  \neg linear(E_1)\Or\neg linear(E_2).\\
\neg linlam1& : & \neg linear(lam( \lx E\ x))\\
& & \qquad\If  \neg linx( \lx E\ x)\\
& & \qquad \mbox{}\Or(\PI{x}{exp} (\neg linx(\ly x) \And
linear(x))\Imp \neg linear(E\ x)).\\ 
\vsk
\neg linxap0& :& \neg linx(\lx app\ (E_1\ x^1) \ (E_2\ x^1)).\\
%\neg linx2& :& \neg linx(\lx app\ (E_1\ x^1) \ (E_2\ x)).\\
\neg linxap1& : & \neg linx(\lx app\ (E_1\ x) \ (E_2\ x^0))\\
& & \qquad\If  \neg linx(\lx E_1\ x).\\
\neg linxap2& : & \neg linx(\lx app\ (E_1\ x^0) \ (E_2\ x))\\
& & \qquad\If  \neg linx(\lx E_2\ x).\\
\neg linxap3& : & \neg linx(\lx app\ (E_1\ x) \  (E_2\ x))\If \neg linx(\lx
  E_1\ x)\And  \neg linx(\lx E_2\ x).\\
\neg linxlm& : &\neg linx(\lx lam(\ly E\ x\ y))\\
& & \qquad\If (\PI{y}{exp} \neg linx(\lx y)\Imp \neg linx (\lx E\ x\ 
y)).  \eneq 

While it is not impossible\footnote{For what is worth, the first three
  versions of such a program I wrote were mistaken.} to manually come
up with this program by writing predicate definitions formalizing when
terms are {\em strict} (that is, variable arguments occur at least
once) and {\em vacuous}(that is, arguments are guaranteed not to
occur) and then by merging them in the correct fashion, it would be
better to have this done automatically, especially considering changes
or extensions of the original program.

\smallskip

Unfortunately the procedure we have outlined is not possible in general.
Consider a clause encoding the introduction rule for implication in
natural deduction, which can be used to check whether an implicational
formula trivially holds:

\begin{Example}
\beq
\label{ex:nd}
 form&: & type\\
 imp&: & form\Imp form\Imp form\\
 a&: &
form\\
b&: & form\\
impi & : & nd(A\ imp\ B)\If (nd(A) \Imp nd(B)).
\eneq
Following our earlier remark its complement would be:
\beq
\neg impi1& : & \neg nd(a)\\
\neg impi2& : & \neg nd(b)\\
%\neg impi3& : & \neg nd(c)\\
\stackrel{?}{\neg} impi& : &\neg nd(A\ imp\  B)\If (nd(A) \Imp \neg nd(B)).
\eneq
\end{Example}

Apparently, this specification is  incorrect since both $nd
(a\ imp\  a)$ and $\neg nd(a\ imp\  a)$ are derivable from the empty
context. We can isolate one major problem: in clause {\tt impi}, the
assumption $nd(A)$ that is dynamically added to the (static)
definition of the {\tt nd} predicate {\em overlaps\/} with the head of
the clause. A symmetrical problem can occur when dynamic and static
clauses do differ but their complements do not. Suppose we 
introduce a predicate which checks if a number is even and non zero as
follows:
\beq
e & : & ev(s(s(N)))\If (ev(0)\Imp ev(N)).
\eneq
Again, our naive algorithm would incorrectly yield:
\beq
\neg e1 & : & \neg ev(0).\\
\neg e2& : &\neg ev(s(0)).\\
\stackrel{?}{\neg} e & : & \neg ev(s(s(N)))\If (\PI{M}{nat}\neg ev(s(M))\Imp \neg ev(N)). 
\eneq
Thus  both $ev (s(s(0)))$ and $\neg ev (s(s(0)))$ are incorrectly
provable. The problem here is the overlapping between the
of assumption $ev(0)$ and the {\em complement\/} of the head of the
{\tt e} clause.
\smallskip

We have thus isolated two main issues:
\ben
\item Exhaustivity: we need to enrich clauses so that
every (ground) goal or its negation is provable.
\item Exclusivity:  we need to isolate a significant fragment where
it is not the case that both a goal and its negation are provable.
\enen

We will describe in Section \ref{sec:aug} a procedure that we call
{\em augmentation}, which, by enriching the program with  the complement of
assumptions will, will achieve exhaustivity (Section~\ref{sec:exh});
moreover, we will achieve exclusivity with the restriction to
{\em complementable\/} programs, formally introduced in Figure
\ref{fig:compl}. To anticipate the idea, a clause is complementable if
every assumption is {\em parametric\/} in some eigenvariable. We will
try to motivate in Section \ref{sec:motiv} why this fragment is
adequate to the practice of logical frameworks. Section
\ref{sec:lamrelated} reviews some related work in the area of \NF and
embedded implication.


\section{Background}
\label{sec:completion}
\newcommand{\ff}{\dashv\!\!\!\prv_L}
Traditionally, a completion construction for the \NF rule is an extension of a 
program, say $E(P)$ such that, in  a logic $L$ equipped with 
a provability and finite failure relation, say $\prv_{L}$ and 
$\ff$ and a negation sign $\neg$, for any given goal $G$ and a
consequence relation $\models_{L}$, (ideally) it 
holds:
\ben
\item
 $\prv_{L} G$ iff $E(P)\models_{L} G$.
\item
 $\ff G$ iff $E(P)\models_{L} \neg G$ .
\enen 

Many such constructions have been proposed for Horn logic, starting
from the \emph{Closed World Assumption} (CWA) \cite{Reiter78}.  The
Clark completion \cite{Cla78} is perhaps the most successful
proof-theoretic and finitary explanation of \emph{NF\/}: the main idea is that
clauses in a predicate definition should be seen as an
\emph{iff-definition}, thus enforcing the minimality condition of its
inductive definition; this would correspond, in model-theoretic terms,
to the existence of a least  intended model.  The if-part states the
condition to belong to the inductive definition, while the only-if
part excludes everything else, thus providing a computable
approximation to the CWA.  This is well understood and agreed as far as
Horn logic is concerned and confirmed by the completeness of finite
failure \wrt the completion \cite{Apt90}.

As observed first by Gabbay \cite{Gabbay85}, the \emph{positive} logic
of embedded implication is not classical but intuitionistic (actually
minimal).  When coupled with negation as failure in all its
generality, its meta-logic fails to have some straightforward logic
properties, as detailed in Section \ref{sec:lamrelated}.  The key
difference lies in the constructive interpretation of implication and
its delicate interplay with negation.  While a completion construction
is possible, it is \emph{not} equivalent to the adjoining of the
only-if part of the program.  This is intrinsically due not only to the non-monotonic nature of such definitions, but also  to the operational semantic
of failure: a goal $D\Imp G$ fails iff from the (scoped) assumption
$D$ we have that $G$ fails.  
Let us try to mirror this with a logical connective:
\beq
\label{eq:comp}
\neg (D\Imp G) &\stackrel{?}{=} &D\Imp\neg G
\eneq
Similarly for parametric judgments:
\beq
\label{eq:comp2}
\neg (\PIXA G )& \stackrel{?}{=}& \PIXA\neg G
\eneq
No standard logic of negation satisfies the above rules. In
particular, it is erroneous to formulate Clark's
completion  using Nelson's strong negation \cite{Nelson49}, 
which is currently held as the
meta-logic of negation elimination in the Horn setting
\cite{Gelfond90,Pearce?}. Indeed, strong negation brings too much duality to
intuitionistic logic as it is pushed in through connectives and
quantifiers; in particular if $\sim$ denotes strong negation the
following holds:
\beq
\sim(D\Imp G) & \Bimp & D\And\sim G\\
\sim(\PIXA G) & \Bimp & \exa\sim G
\eneq

Strong negation may be ``the logic of information structures''
\cite{Wansing93}, as far as Horn logic is concerned, but it is
definitely \emph{not} the meta-logic of negation elimination in
logical frameworks based on HHF.  It is not simply a question to endow
intuitionism with a semi-classical notion of negation, while preserving
the disjunction and existential property. The hard point is not
negation in itself, but its interaction with a more operational
Brower-Heyting-Kolmogorov interpretation of implication.

 
\begin{Example}
Consider the program consisting 
only of the clause $a \If (b\Imp c)$; the standard completion would be 
$$a\Bimp (b\Imp c)\And\neg b\And \neg c.$$
Now, $`a$' fails and hence
$`\neg a$' should follow from the iff-completion: still $`a$'
intuitionisticallly (yet not minimally) follows, while $`\neg a$' is
logically independent exactly due to the failure of Equation
(\ref{eq:comp}).
\end{Example}
We explore in Section \ref{sec:lamrelated} how this issue has been
investigated in the literature.  This is relevant to our enterprise
because: 
\bit
\item
In the Horn setting, the iff-completion has been the preferred way to 
logically motivate the transformational approach to negation, as 
we have seen in Section \ref{sec:what}.
\item
In \cite{Giordano98} the authors persuasively argue that the 
unrestricted addition of \NF to languages such as 
N-Prolog requires the switch to a 
(three-valued) modal logic. 
\enit 

Since we need to express the negation of a predicate in the same
language where the predicate is formulated, we choose to restrict the
set of programs we deem complementable in a novel and extensive way.
This will help to close the gap between the two poles usually
associated to classic and intuitionistic logic programming, \ie the
closed versus open world assumption.  We will define a class of
programs which extend the current database in a specific regular way,
by ensuring that static and dynamic clauses never overlap. This
property extends \wrt the complement program and thus has the side
effect of guaranteeing the consistency of the completion.  Finally we will require every goal to conform to such a \emph{schema context}. We call this approach the \emph{Regular World Assumption} (RWA). We argue
next (Section \ref{sec:motiv}) that this class of programs is just what
the doctor ordered for logical frameworks.
%  Moreover we may also contend 
% that the usage of \NF in Prolog-like language \wrt programming tasks 
% which exclude formalization of default situations is intrinsically 
% monotonic, as a cursory look to any Prolog manual can confirm


\section{Motivation}
\label{sec:motiv}

Embedded implication  in intuitionistic \lp has been successfully 
used in various areas of logic programming; we can roughly 
divide those into:
\bit
\item Meta-programming, namely specifying and implementing (the
  meta-theory of) deductive systems.
\item Hypothetical reasoning in databases \cite{Gabbay84,Bonner89,Bonner94} or
  simulating imperative-style programming \cite{Bonner90}.
\item Incorporating modules and local predicate definitions
  \cite{Miller89jlp,Giordano92,Kwon93} and state encapsulation in
  object-oriented programming \cite{HM90}.  
\enit
  
We now try to motivate  why the restriction of complementation to 
\emph{parametric implication} (formally defined in 
Section \ref{sec:cc}) is pragmatically adequate for our intended application.  
 
While implementing deductive systems embedded implication is usually
coupled with \ho abstract syntax to represent \emph{scoping
  constructs}: the latter are typically used to traverse operators
like abstractions, quantification and, more pervasively, to represent
rules with hypothetical premises.  In this application implications
are typically `covered' by an intensional universal quantifier which
express the parametricity of the assumption. Dozens of examples can be
found for instance in \cite{Pfenning94un}. One counter-example I am
aware of is when using a logic framework to encode derivability in an
object logic: here meta-logic contexts are used to manage object logic
hypotheses, as in Example \ref{ex:nd}.  We feel that this case in not
typical; first of all it is questionable (and out of the scope of a
logical framework) to complement recursive enumerable predicates such
as general provability.  Even if we limit ourselves to decision
procedures as propositional logic, we are in a sense asking for a
self-referential use of implication as we wish to represent
implications in the object logic with the same in the meta-logic.  In
this case, though we have no formal proof of this, we think we have to
use ad hoc techniques such as explicit management of hypotheses say as
lists; a similar approach is taken in \cite{MacDowell97lics}.

Modules are usually \emph{closed} assumptions and I doubt negation is
useful at this level. Local definitions, as an auxiliary
\texttt{reverse3} procedure hidden inside the naive \texttt{reverse}
procedure are typical only in \ho\lp languages as $\lambda$Prolog, and
require full predicate quantification. We conjecture that some of
those programs can be complemented if there is no overlap between
static and dynamic clauses. As far as object-oriented programming is
concerned, more recent research \cite{Bugliesi00} has now moved on to
linear logic programming languages.
%  (see, LaTeX \texttt{includeonly} command, though)


The possibility to simulate the availability of global variables in
\lp has been advocated \cite{Giordano98} as the main motivation of the
intertwined and unrestricted use of negation and embedded
implication.  We contend that sometimes that can be resolved with a
refined notion of context as the one available in linear logic
programming: this has also the side-effect of by-passing the issue of
non-stratification.

We now exemplify how to eliminate negation from non-stratified 
N-Prolog programs.  We cannot say at the moment whether this 
transformation can be generalized and eventually mechanized.
\newcommand{\enf}{ \setminus\! +}
% The following program enumerates every Hamiltonian circuit in a
% directed graph, where we use $\enf$ to denote \nf:
% \begin{Example}[Hamiltonian circuit]
% \[\begin{array}{l}
% yes \If select(X), (mark(X) -> path(X))\\
%  path(X) \If edge(X,Y), node(Y) (mark(Y) -> path(Y))\\
%  path(X) \If \enf someleft\\
%  someleft \If \enf select(X)\\
%  select(X) \If node(X), \enf mark(X)
% \end{array}
% \]
% This can be written (as suggested by I.~Cervesato, personal 
% communication) in the Horn fragment of \emph{Lolli} by 
% representing each node $n$ with a \emph{linear} assumption $node_n 
% \hat{:} node n$ and each edge from $n1$ to $n2$ as an 
% \emph{intuitionistic} assumption $ edge_{n1-n2} : edge\ n1\ n2.$
% \[\begin{array}{l}
%         nodeName : type.\\
%         node : nodeName -> type.\\
%         edge : nodeName -> nodeName -> type.\\
%         path : nodeName -> type.\\
%         hamilton : type.\\
% \vsk
%         yes : hamilton
%                 o- node X
%                 o- path X.\\
% \vsk
%         path_go : path X
%                 o- edge X Y
%                 o- node Y
%                 o- path Y.\\
%         path-stop : path X.
% \end{array}
% \]
% The clause "path-go" is applicable till there is some linear assumption 
% $node_n \rapp node\ n$ in the context.  Only when they have all been 
% consumed is "path-stop" applicable.
% \end{Example}
The following example (taken from \cite{Giordano98}) is a non-stratified 
program to compute the parity of a relation encoded as $n$ entries of 
the form $r(X)$, where `$\enf$' denotes negation-as-failure:

\begin{Example}[Parity]
\[\begin{array}{l}
even \If \enf odd.\\
odd \If r(X), \enf mark(X), (mark(X) \Imp even).
\end{array}
\]
We can write a \emph{Lolli} program \cite{Hodas94ic} based on the same
algorithm, where the linear context contains the entries of the
relation and the initial token \texttt{off}; let $-\!\circ$ and
$\otimes$ denote linear implication and conjunction:
\[\begin{array}{l}
even \pol\ r(X)\otimes\ off\ \otimes(on\ \lop\  odd).\\
even\pol\ off.\\
odd \pol\ r(X)\otimes\ on\ \otimes( off\ \lop\  even).\\
odd\pol\ on.
\end{array}
\]
The tensors consume the relation and turn on or off the switch
accordingly to the parity of the relation.
\end{Example}

We can make a similar remark about the relative pronoun gap parsing example in
Categorical Grammars \cite{Pareschi90} which in  \cite{Bonner90} is
treated with intuitionistic implication plus \NF. Hodas
\cite{Hodas94phd} has shown  how this can be dealt  with much more
elegantly again with linear implication.


\section{Related Work}
\label{sec:lamrelated}

In the 90's 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 versions
of N-Prolog or clausal intuitionistic logic.  Due to the inherently
difficulty with universal quantification mentioned in Subsection \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 coupled 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
(propositional) normal clauses.
They can be summarized as follows (taken from \cite{Olivetti92}).
\ben
\item Failure of transitivity, or, in other words, non-eliminability of the cut rule.
Let $\cP$ be:
\[
\begin{array}{l}
a \If b\And \enf c.\\
b \If c.
\end{array}\]
Now,  $\cP\prv c\Imp b$ and $\cP\prv b\Imp a$, as $c$ is undefined,  but $c\Imp 
a$ is not provable from $\cP$.
\item
Failure of weakening.
Let $\cP$ be:
\beq
b \If \enf a.
\eneq
Then $\cP\prv b$ but $ a\Imp b$ is not provable from $\cP$.
\item ``Pathology of negative information'', \ie $\cP\prv \enf(A\Imp
  B)$ iff $\cP\prv A\Imp\enf 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 implications \cite{Bonner90}.
\item A syntactic distinction between predicates \cite{Harland93}.
\enit
We detail the latter next, but let us state, for the record, 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 cousin of
uniform proofs independently developed by McCarthy in the late eighties
\cite{Mc88a,Mc88b}. \NF in this setting has been investigated in
Bonner's thesis \cite{Bonner91phd} and is 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 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 succeed or fail from a program unless we
  determine what goal succeeds or fail from
  \emph{arbitrary}\footnote{Emphasis 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 an
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  $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 {\em ESLDNF} derivability \wrt a
Kripke-Kleene fixpoint construction for a notion of non-floundering
programs.  The three-valued approach avoids the restriction to
stratified programs.

\subsection{\NF in First-Order Uniform Proofs}

Harland's thesis \cite{Harland91phd} is an in-depth analysis of
Uniform Proofs and {\em NF} at the first-order level. Unfortunately,
his approach, though sound, is not adequate to our purposes, 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{Miller89jlp,Momigliano92}.  Technically, this is achieved by
distinguishing, for all predicates occurring in the signature, those
which appear negatively versus positively in the body of clauses. The
two sets are required to be disjoint.  This of course simplifies the
later development, but, 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. This fragment therefore collapses to
normal programs with extensional quantification.  While it is possible
to enforce differently the distinction between complete and incomplete
predicates, we are indeed interested to apply negation to incomplete
predicates, although in a restricted fashion.

Then Harland shows how to formulate the completion as a \fo HHF
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
identifies the completed program with its iff-completion, though he
correctly has $\neg(D\Imp G) = D\Imp \neg 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 of $Q\If G$ is seen as $\neg (Q\And \neg G)$; again this holds only
because \nf cannot be applied to incomplete predicates.  The classical
attitude carries over to universal quantification, which is only
allowed to be extensional.  Harland so does not stress 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 semantics for coverings
is described: not only is the role of free variables introduced by
coverings 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{Partial Inductive Definitions}
\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 in a finitary version
(\cite{Eriksson93phd}) of parametric 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$,
where $b$ ranges over atomic predicates possibly with free variables.  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 $a$, 
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 atomic proposition $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 not 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 global 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}, in order to 
reduce an atomic cut formula through 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-free logics.
\item Stratified program \wrt negation.
\item Stratified program \wrt implication \cite{MacDowell97lics}.
\enit

In the latter case, predicates are assigned \emph{levels}: the latter
are then extended to formulae, so as to forbid recursion through 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 than 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 has been claimed to bring in a proof-theoretic
notion of negation, although it would be more accurate to say that it
allows a \emph{meta-level} notion of closure.  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, thanks to definitional reflection, suffices
to define free equality.  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 so far as negative goals are simply a special case of
implicational ones and therefore should be able 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.  Thus for example, $\neg even(s(0))$ is
provable as follows, suppressing here any mention of the (empty)
parameter context:
$$\ianc{ \ianc{}{\defp(even),even(s(0))\vd\bot}{\cD-L}}{\defp(even)\vd
  even(s(0))\Imp\bot}{\Imp R}$$
since the definiens of $even(s(0))$ is empty.

 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 $Z$ is a local
  logic variable; then there is a computation which reduces to
  $\bot\dots\prv\bot$.
\end{Example}

On the other hand, some of the familiar  problems with negative goals 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 $\defp(even)\vd\exists x\neg even(x)$ yields $\defp(even),even(X)\vd\bot$; the rule
$\cD-L$ will loop, being unable to compute to what amounts, in our
terms, to $\mnot(0)\cap\mnot(s(s(Y)))$. In other terms, definitional
reflection uses unification to consider the given definition as a
minimal inductive definition, but this does not allow to compute
values that lies outside this very definition,

 % 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 am 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 the operational intuition
of HHF:
\[
 \ianc{ \ianc{ \ianc{}{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 not 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. Consider a goal $\cdot;\defp(even)\vd \neg open\ lam(\lx
x)$, which is clearly unprovable: a naive \lp interpreter augmented
with definitional reflection will eventually yield the goal
$\cdot;\defp(even),\PI{x}{exp} open\ x\vd\bot$. In the failed
derivation of the same
positive goal, a goal-oriented strategy would introduce a new
parameter and try the goal $y\oftp exp;\defp(even)\vd open\ y$. Yet,
the same idea does not work when definitional reflection is allowed as
now the universal in on the left and we can only do (inverted)
universal elimination.

The main confusion, in general, lies in attempting to give a naive
goal-oriented reading to a sequent calculus augmented with the
definitional reflection rule. The latter is instead a meta-level
closure operator; this is indeed how it is used in meta-logics as
$\Mtwo$ \cite{Schurmann98cade} and $\foldn$ \cite{McDowell97lics}.
If we try to use it as a \lp engine for HHF with negation, \ie we add
introduce logical variables and dynamic assumptions, it breaks down
and reveal its meta-theoretic nature. We also remark that adopting our
restriction to \emph{complementable} programs ( formally introduced in
Figure~\ref{fig:compl}) would not help, as far as \lp is concerned.
Instead, we conjecture that the proof of cut-elimination given in
\cite{McDowell00} can be extended to those programs,
allowing to enhance the range of  $\foldn$ significantly.

\renewcommand{\cD}{{\cal D}} 






















