\section{On the completion}

In general a completion construction for \NF is an extension of a 
program, say $E(P)$ such that, in an opportune logic $L$ equipped with 
a provability and finite failure relation, say $\prv_{L}$ and 
$\nprv_{L}$ and a negation sign $\neg$ if, for any given goal $G$, it 
holds:
\ben
\item
If $\prv_{L} G$, then $E(P)\models_{L} G$
\item
If $\nprv_{L} G$, then $E(P)\models_{L} \neg G$ 
\enen 

In Horn logic, the Clark completion \cite{Cla78} is one of the most 
successful proof-theoretic and finitary explanation of \NF: the 
central idea is that clauses should be seen as an iff-definition, 
enforcing the closure condition of inductive definitions, which 
corresponds in model-theoretic terms to the minimality of the intended 
model.  The if-part states the condition to be in the inductive 
definition, while the only-if part excludes everything else, thus 
providing a computable approximation to the CWA. As observed first by 
Gabbay, the \emph{positive} logic of embedded implication is not 
classical but intuitionistic (actually minimal).  When coupled with 
negation as failure in its generality, the meta-logic fails to have 
some straightforward properties, as detailed in \ref{lamrelated}.  
While a completion construction is possible it does \emph{not} 
coincide with the adjoining of the only-if part of the program.  This 
is due to the operational semantic of failure: a goal $D\Imp G$ fails 
iff from the new assumption $D$ we have that $G$ fails.  When trying 
to mirror this kind of failure with negation, we get to the equation

\begin{equation}
\neg (D\Imp G) = D\Imp\neg G \label{eq:comp}
\end{equation}
that no standard logic of negation satisfies.  In particular, Clark's 
completion would require something like $\neg (D\Imp G) = D\And\neg G$ 
even using Nelson's strong negation, which is currently held as the 
logic of negation elimination in the Horn setting 
\cite{Gelfond90,Pearce?}.  
For example from the program consisting only of the clause $a \If 
(b\Imp c)$, $a$ fails and hence $\neg a$ should follow from the 
completion: still $a$ follows from the iff completion while $\neg a$ 
is logically independent exactly due to the failure of \ref{eq:comp}.
We explore in \ref{lamrelated} some ways this issue has been 
investigated in the literature. We just mention the following
\bit
\item
In the Horn setting, the iff completion is the preferred way to 
logically motivate the transformational approach to negation, as 
detailed in Section \ref{comparison}
\item
In \cite{Giordano98} the authors convincingly show that the 
unrestricted addition of \NF to N-Prolog requires the usage of 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.  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, that we will call 
\emph{assumption-complete} such that they extend the current database 
in a specific predictable way, preserving consistency of the latter at 
all time.  This will also defuse the non-monotonic nature of \NF. We 
argue next \ref{motif} 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{motif}

Embedded implications in in intuitionistic \lp have been successfully 
used in various areas in theoretical computer science: we can roughly 
divide those into:
\bit
\item
metaprogramming, namely specifying and implementing (the meta-theory) 
of deductive systems
\item
hypothetical reasoning in databases \cite{Gabbay84,Bonner89} or simulating 
imperative-style programming \cite{Bonner90}
\item
incorporating modules \cite{Miller89jlp,Giordano89tcs,Nad?} and state encapsulation 
\cite{HM90}.
\enit

We motivate now why the restriction of complementation to 
\emph{parametric implication}, \ie \emph{assumption-complete programs} 
\ref{} is pragmatically adequate.  
 
While implementing deductive systems embedded implications are 
coupled with \ho abstract syntax to represent \emph{contexts}: the latter are 
typically used to traverse scoping constructs 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{Pfenning1994un}. The only counter-example I am aware of is when using a 
meta-logic to design theorem-provers: here meta-logic contexts are 
used to manage object logic hypotheses.  We feel that this case in 
not typical; first of all it is questionable (and out of our scope) 
to complement recursive enumerable predicates as general provability.  
Even if we limit to decision procedures as propositional or 
de-modalized linear logic, we are in a sense asking for a 
self-referential use of implications as we wish to represent 
implications in the object logic with the same in the meta-logic, the 
two logic being the same.  In this case, though we have no formal 
proof of this, we think we have to use ad hoc techniques as explicit 
management of hypotheses say as lists.

Modules are usually \emph{closed} assumptions and I doubt 
complementation makes any sense (see, LateX \texttt{includeonly} 
command, though)\footnote{Object-oriented programming, no clue at the 
moment.}.

We contend that sometimes intertwined use of negation and 
non-parametric implication--thus out of the fragment we deal with--to 
simulate the usage of global variables can be resolved with a refined 
notion of context as the one available in linear \lp: 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{\lop}{-\circ}
\newcommand{\pol}{\circ-}
\newcommand{\enf}{ \setminus +}

This program enumerates every Hamiltonian circuit in a directed graph

\begin{Examplen}[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 
\rapp 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{Examplen}

The next example (modified from \cite{Giordano98}) is a non-stratified 
program to compute the parity of a relations encoded as $n$ entries of 
the form $r(X)$:

\begin{Examplen}[Parity]
\[\begin{array}{l}
even \If \enf odd\\
odd \If r(X), \enf mark(X), (mark(X) \Imp even)
\end{array}
\]
Again this can be written in the Horn fragment of \emph{Lolli} as 
\[\begin{array}{l}
even \pol r(X)\otimes  odd\\
even\\
odd \pol r(X)\otimes  even
\end{array}
\]
where the relation $r\hat X$ belongs to the linear context.
\end{Examplen}


