\chapter{Conclusions and Future Work}
\label{ch:end}
\renewcommand{\lf}{logical framework}

%\label{sec:concl}
The importance of \ho \lf s and logic programming languages that
depend on intuitionistic logic, open-world assumptions (changing
contexts), and lambda-abstractions is becoming more apparent and their
use more widespread. Recent research is attempting to increase their
expressivity, while preserving the conciseness and elegance of their
representation techniques. The issue of negation has to be appreciated
in that context.  A good understanding of negation in such settings
will significantly enhance the expressive strengths of such
specification languages.

In this dissertation we have presented a solution to this
long-standing issue in \lf s endowed with a \lp interpretation.  The
solution offered by our approach has the net (and neat) effect that
negation and its problems are \emph{eliminated}, \ie we avoid any
extension to the (meta) language.
%  In fact, extending a \lf\ requires
% special care, since we have also to fulfill the \emph{proof
% obligation} that the proposed negative definition does behave as the
% complement (of its positive counterpart).

Although the transformational approach to negation has been
investigated in traditional logic programming, this is a novel approach
to addressing negative information in the  higher-order intuitionistic
setting.  Many of the techniques from Horn programs do not carry over
directly, so creative solutions had to be found to adapt the idea to
the higher-order setting. In particular, we had to:

\begin{enumerate}
\item Formulate a strict $\l$-calculus to obtain  closure under term
  complement of the source language.
\item Find a notion of negation normal forms which is compatible with
  the operational semantics required by Hereditary Harrop Formulae (HHF).
\item Introduce the \emph{Regular World Assumption} (RWA) as a way to reconcile the intrinsic tension
  between the \emph{Closed World Assumption}, associated with
  negation, and the \emph{Open World Assumption} typical of languages
  with embedded implication.
\end{enumerate}

Elimination of negation is particularly tuned to \lf s: although the
problems connected with negation  are analogous in \lf 
s and logic programming,  the
solution does not need to be the same. In this sense our approach is
not a panacea. For example, it is definitely non appropriate in
presence of even a small database of facts. Although the typing
discipline goes a long way to limit the combinatorial explosion of
negative facts, often a different approach is more fruitful; consider
a small database recording the age of some people. It would be painful
to negate say \texttt{age k s$^{34}$(0)} by inferring \texttt{non-age k 0}\dots
\texttt{non-age k s$^{33}$(0), non-age k s$^{35}$(X)}. In this case the use
of some form of \emph{constructive} negation is preferable, possibly
in the form of disequations, \ie \texttt{non-age k Z $\If$ Z $\neqd$
s$^{34}$(0)}. This area, to date, has not been explored at all in the \ho case.
%On the other hand, this does not happen frequently in \lf
%applications.

\smallskip Before discussing how to extend our approach beyond some of
the current limitations, we take on again the main technical
restriction\footnote{We discuss the issue of local variables later,
  see Subsection~\ref{ssec:local}.}, \ie to \emph{complementable}
programs as defined in Figure~\ref{fig:compl}.  As we have argued, the
key to a successful and implementable pairing of negation and
hypothetical judgments is to keep separate at any time static and
dynamic information in a program.  We have achieved this by requiring
every assumption to be parametric, a property which is preserved by
the negative program. The eigenvariable condition enforced by the
operational semantics of HHF together with the rigidity restriction
does the rest. We have argued that this restriction is a most natural
one \wrt the intended application; in our experience, it covers the
overwhelming majority of actual Twelf and $\l$Prolog code. This of
course does not mean that there are no useful programs which lie
outside of this class; it is indeed entirely possible to use
hypothetical judgments in isolation from parametric ones. We have
noted in Section \ref{sec:motiv} how sometimes this can be avoided by
resorting to a finer notion of context such as the one offered in
linear logic. Otherwise, it is always possible to eliminate the
offending implications by introducing an explicit management of
contexts. For instance, we can revisit Example \ref{ex:nd} and
transform \beq impi & : & nd(A\ imp\ B)\If (nd(A) \Imp nd(B)).  \eneq
into: \beq
impi'&:& nd(A\ imp\ B) \leftarrow  nd2(A,B).\\
impi1&:& nd2(A,A).\\
impi2 & : & nd2(C,A\ imp\ B) \leftarrow nd2(C,B).\\
impi3 & : & nd2(C,A\ imp\ B) \leftarrow nd2(A,B).  \eneq 
Although this
goes against the spirit of \lf s based on intuitionistic \lp which
owes part of its success to the capability of representing
object-logics contexts via the meta-level scoping mechanism of
embedded implication, this is not unheard of, and it is actually
proposed (for different reasons) in \cite{McDowell97lics}. Besides, this transformation will
of course be localized only to those predicates we need to complement.


\section{Lifting Restrictions}
\label{sec:lift}
We now address some of the restrictions which can in fact be lifted;
in doing so, we will consider an example which is not currently treated:
\begin{Example}
Consider the following extension of the \texttt{copy} clauses to a
third and fourth order constructs, respectively \texttt{callcc} and
\texttt{reset}: 

\beq
%exp : \prop.
%lam : (exp \Imp exp) \Imp exp.
%app : exp \Imp exp \Imp exp.
callcc&:&((exp \Imp exp) \Imp exp) \Imp exp.\\
reset &:&(((exp \Imp exp) \Imp exp) \Imp exp) \Imp exp\\
%cp&:&exp \Imp exp \Imp \prop.
% cpapp&:&cp\ E1\  F1 \Imp cp\ E2\ F2 \Imp cp\ (app E1\  E2) (app F1\ F2).
% cplam&:&({x:exp}  cp\ x x \Imp cp\ (E\ x) (F\ x)) 
%           \Imp cp\ (lam [x:exp] E\ x) (lam [y:exp] F\ y).
cpcallcc &:&  cp\ (callcc\ \lamb{c}{exp \Imp exp} E\ c) \  
(callcc\ \lamb{d}{exp \Imp exp} F\ d)\\
&&\qquad\If (\PI{c}{exp \Imp exp} \\
 &&\qquad\qquad            (\PI{x}{exp}\PI{y}{exp} cp\ (c\ x) \ (c\
 y)\If  cp\ x\ y) \\ 
  &&\qquad\qquad\qquad            \Imp cp\ (E\ c) \  (F\ c)).\\             
cpreset  &:&  cp\ (reset\ \lamb{f}{ (exp \Imp exp) \Imp exp} E\ f) \  
                (reset\ \lamb{g}{ (exp \Imp exp) \Imp exp} F\ g)\\
&&\qquad\If(\PI{f}{ (exp \Imp exp) \Imp exp} \\
  &&\qquad\qquad            (\PI{c,d}{ exp \Imp exp} \\
 &&\qquad\qquad \qquad         cp\ (f\ c) \  (f\ d))\\
 &&\qquad\qquad \qquad\qquad     \If (\PI{x,y}{ exp}  cp\ x\ y \Imp 
cp\ (c\   x) \  (d\ y))\\
 &&\qquad\qquad \qquad\qquad \qquad               \Imp cp\ (E\ f) \  (F\ f))
\eneq
\end{Example}


\subsection{Parameters Restrictions} 
The restriction to parameters of base type seems to be the less
complicated to  lift, if we still require them to occur only in
\emph{head} position. We thus would redefine the class of Shallow
Parameter Expressions (\emph{SPE\/}) as:
\[ \begin{array}{rrcl}
\mbox{\textit{SPE}}& e_x &  \bnfas & x\hastype A\bnfalt\lx e_x\bnfalt (e_x\ M)^k
\end{array}
\]
This will allow to complement the
third-order \emph{cpcallcc} clause:
\beq
\lefteqn{c\oftp exp\Imp exp\vd\mnota(\PI{x,y}{exp} cp\ (c\ x) \ (c\
  y)\If  cp\ x\ y)=}\\
&&  \Pi(\neg cp\ (c\ x)\ (lam\ E)\And \neg cp\ (c\ x)\ (app\ E_1 \ E_2)\And\mbox{} \\
&& \neg cp\  (lam\ F)\ (c\ y)\And \neg cp\  (app\ F_1\ F_2) \ (c\ y)\And\mbox{} \\
&&  \neg  cp\  (c\ x) \ (c\ y)\If \neg cp\ x\ y).
\eneq

% Here we can introduce the appropriate disequations as before, thus
% yielding:
% \beq
% \neg  cpcallcc &:&  \neg cp\ (callcc\ \lamb{c}{exp \Imp exp} E\ c) \  
% (callcc\ \lamb{d}{exp \Imp exp} F\ d)\\
% &&\qquad\If (\PI{c}{exp \Imp exp} \\
%  &&\qquad\qquad(\PI{x}{exp}\PI{Z_1}{exp\Imp exp} \neg cp\ Z_1 \ (c\ x)\If Z_1\neqd (c\
% x)\And\mbox{} \\
% &&\qquad\qquad \PI{Z_2}{exp\Imp exp} \neg cp\  (c\ x) \ Z_2\If Z_2\neqd (c\ x)\And\mbox{}\\
% && \qquad\qquad\neg  cp\ (c\ x) \ (c\ x)\If \neg cp\ x\ x)\\
%   &&\qquad\qquad\qquad            \Imp\neg cp\ (E\ c) \  (F\ c)).\\   
% \eneq



The condition for parameter to occur at head position instead is
orthogonal, since it is a sufficient condition for maintaining
non-overlapping between dynamic and static clauses; that is, of
course, the main technical idea behind the exclusivity proof. A clause
can indeed be \emph{complementable}, \ie every assumption is
parametric, but if the eigenvariable does not occur in head position
in the assumption, then the non-overlapping requirement may not be
immediately verifiable. If we can detect by static program analysis or
by any other means that no overlapping will result, then those clauses
too can be promoted.


\subsection{Extension to Any Order} 
\label{ssec:anyorder}
We currently treat only the third-order case, that is we allow HHF
which only make Horn assumptions. In this way, generally speaking,
judgments on goals are only trivially recursive with the ones on
clauses, since the latter would not make any new assumption. Allowing
arbitrary assumptions requires instead this recursion to be unbounded.
In general, most of the times we simply need to modify those
judgments by passing around their contexts. To be concrete, let
us consider for instance the issue of  \emph{schema extraction}; in the $n$-ary case,
schemata ought to be \emph{hereditarely closed}. In fact, if a HHF
belongs to a schema, the latter ought to take into account any further
assumption that the former may yield.  The aforementioned  modifications of the
extraction judgments in Figure~\ref{fig:schema} will do the trick:
\[
\begin{array}{c}
\ibnc{\ga\vd G\yg \cS_1}{\ga\vd D\yd \cS_2} {\ga\vd(G\Imp  D)\yd \cS_1\mbar
  \cS_2}{ \yd\Imp}
\vsk
\dots
\vsk
\ibnc{ \GG;(\cD\And D)\vd G\yg \cS_1}{\GG;\cD\vd D\yd \cS_2}{
  \ga \vd   D\Imp G\yg \cS_1\mbar \cS_2}{ \yg\Imp}
\end{array}
\]
% At the moment we do not know whether this
% can be achieved with the current data structure or the latter must be
% modified to account for arbitrary scoping of dynamic assumptions.
For example we can extract the following schema from the extended definition of \texttt{cp}:
\beq
 \defp(cp)& \yd &  x \hastype exp; cp\ x\ x\mbar\mbox{}\\
&&   c \hastype exp \Imp exp;
                         (\PI{x,y}{exp}  cp\ x\ y \Imp cp\ (c\ x) \ (c\   y))\mbar\mbox{} \\
&&   f\hastype (exp \Imp exp) \Imp exp;
                          (\PI{c,d}{ exp \Imp exp} cp\ (f\ c) \ (f\ d)
                          \If\\
&& \qquad\qquad\qquad\qquad\qquad\qquad\qquad
                            (\PI{x,y} {exp} cp\ x\ y \Imp cp\ (c\ x) \ (c\ y)))
\eneq
%\end{document}
In this case only the schema alternative induced by the
\texttt{cpreset} clause needs to be hereditarely closed with 
\texttt{x:exp;cp x x}; but this is already provided by the (schema
extracted from the) \texttt{cplam} clause.

% Schema satisfaction needs not to be changed; in particular, the $\dsat$
% judgment does not need to pass around the context, since all the work
% is done by the \emph{instance} relation which fires when blocks are
% already assembled.
Similar changes apply to the other judgments; in particular,
augmentation is generalized, so that goals which can make dynamic
assumptions will be recursively augmented as well. Formally:
\[
\begin{array}{c}
\ibnc{\GG;\cD\vd\ald(D)=D^a}{\GG;(\cD\And
D)\vd\alg(G)=G^a}{\ga\vd\alg(D\Imp  G)=D^a\Imp G^a}{\alg\Imp}
\end{array}
\]
We can therefore complement a fourth-order clause such as
\texttt{cpreset}, where, for the sake of readability, we have not
expanded the calls to $\mnota(D)$:
\beq
\neg cpreset  &:& \neg cp\ (reset\ \lamb{f}{ (exp \Imp exp) \Imp exp} E\ f) \  
                (reset\ \lamb{g}{ (exp \Imp exp) \Imp exp} F\ g)\\
&&\qquad\If(\PI{f}{ (exp \Imp exp) \Imp exp} \\
  &&\qquad\qquad            (\PI{c,d}{ exp \Imp exp} \\
 &&\qquad\qquad \qquad              (\PI{x,y}{ exp}  cp\ x\
 y\And\mnota(cp\ x\ y)
 \Imp \neg cp\ (c\ x) \  (d\ y))\\
 &&\qquad\qquad \qquad\qquad              \Imp \neg cp\ (f\ c) \  
(f\  d)\And\mnota(cp\ (f\ c) \  (f\ d) \\
 &&\qquad\qquad \qquad\qquad \qquad               \Imp \neg cp\ (E\ f) \  (F f))
\eneq


\subsection{Open Queries}
\newcommand{\mode}{\mbox{\textrm{mode}}}
\newcommand{\Tn}{\overline{T_n}}
\newcommand{\xm}{\overline{x_m}}
One of the more widespread criticism to negation-as-failure
(\emph{NF\/}) is that it cannot return 
answer substitutions; in fact, if it is not restricted to ground goals,
it may return unsound solutions, as detailed in Section \ref{sec:nf}.
On the other hand, one of the bright spots of elimination of negation
is the \emph{positivization} of negative information, which can now
be queried as regular (HHF) clauses. In particular, negative open
queries are simply positive queries to the complement program and thus
will return a witness if one exists. However, open queries are not
accounted for in the theory we have developed so far. Indeed, we have
used programs just as \emph{decision procedures}, \ie such that for
every ground goal only yes/no answers can be returned. This does not
need to be the case; open queries can be allowed in so far as 
enough `directionality' is retained in the query. In fact, if we can
split the arguments of  a query in an \emph{input} and \emph{output}
sequence so that termination (in the input elements) can still be
determined, the proof of exclusivity will  go through, provided
that the no-overlapping requirement  holds. However, this is
almost infallibly the case, because parameters tend to occur in input
position; in fact, as we have already remarked, parametric judgments
are typically used to traverse scoping constructs and most of the
times termination can be proven \wrt those terms. 

The idea is to give \emph{modes} to predicate definitions: let
$q\hastype A_1\Imp\dots\Imp A_n\Imp\prop$ and $\mode(q)=m_1\mdots m_n$
be a \emph{mode} for $q$, where each $m_i$ is either $+$ (input) or
$-$ (output) \cite{Rohwedder96esop}. More complex moding systems have
been proposed in the literature on traditional logic programming, but
this one may be pragmatically adequate for our purposes. 
%  An atom $q\ \Tn$ \emph{satisfies}
% a mode $m_q=\mode(q)$ if for every $1\leq i\leq n$:
% \beq
% m_i= + & \mbox{iff} & T_i \mbox{ is ground}\\
% m_i= - & \mbox{iff} & T_i \mbox{ is flex}
% \eneq
Now, given $m_q$ consisting of a sequence of $m\geq 1$ +'s and $n\geq 0$
-'s, if we can show that $\defp(q)$ is terminating \wrt $m_q$ and, in case it
is a non-Horn definition, if  $\defp(q)$ is parametric in at least one
position $i$ such that $1\leq i\leq m$, then the query $\forall
\xm.\,\exists \yn.\, q\ \xm\ \yn$ is allowed. This can be recursively
extended as usual to any goal (and clause).
To make the discussion more concrete, let us return to the
\texttt{copy} example. The results in Chapter \ref{ch:cc} guarantees
the following, for an appropriate context schema $\ga$:
\begin{itemize}
\item $\PI{x}{exp} \forall y\!:\! exp$ either $\ga\vd cp\ x\ y$ or $\ga\vd
  \neg cp\ x \ y$.
\item $\PI{x}{exp} \forall y\!:\! exp$ it is not the case $\ga\vd cp\
  x\ y$ and $\ga\vd   \neg cp\ x \ y$.
\end{itemize}
But of course we may be interested in \emph{finding} a $y$ such that
the above holds. By noting that \texttt{copy} can be shown to be
terminating  only with one term instantiated, we can consider say $x$
as input and $y$ as output. Additionally, we can check that the
non-overlapping condition still holds in this case; thus we can
establish: 
\begin{itemize}
\item $\forall x\!:\! exp$ either $\exists y\!:\! exp$ such that $\ga\vd cp\
  x\ y$ or $\ga\vd  \neg cp\ x \ y$.
\item $\forall x\!:\! exp$ it not the case that $\exists y\!:\! exp$
  such that $\ga\vd cp\ x\ y$ and $\ga\vd  \neg cp\ x \ y$.
\end{itemize}




\subsection{Local Variables Revisited}
\label{ssec:local}
Allowing non-ground queries has sometimes the side-effect of
overcoming the strict restriction to programs without local variables.
In certain cases, in fact, we can lift the local variable to the head
of the clause (and possibly embed it in a constructor); thus, the
variable is no
more (intrinsically) existentially quantified in the body and will not cause any problem
during complementation; moreover, we do not change the arity of the
predicate definition, although the latter too is possible. If we can
still prove the program terminating, that is the local variable plays
no role in the termination argument,
then we can use that  predicate definition leaving the ex-local
variable as an output value only. For example, we can revisit the
program for type-checking in the simply typed calculus; if we change
application to allow the type of the argument to the function, that
is:
\beq
app & : & exp\Imp exp\Imp tp\Imp exp.\\
ofapp & : &  of\ (app\ E_1\ E_2\ T_1) \ T_2\\
&&\qquad \If of\ E_1\ (arrow\ T_1\ T_2)\\
&&\qquad \If of\ E_2\ T_1\\
oflam &:&  of\ (lam\ E) \  (arrow\ T_1\ T_2)\\
& & \qquad\If( \PI{x}{exp} of\ x\ T_1 \Imp  of\ (E\ x) \ T_2).
\eneq
Then we can apply (a slight modification of) our complement algorithm,
yielding: 
\beq
\neg app1 & : &  \neg of\ (app\ E_1\ E_2\ T_1) \ T_2\\
&&\qquad \If \neg of\ E_1\ (arrow\ T_1\ T_2).\\
\neg app2 & : &  \neg of\ (app\ E_1\ E_2\ T_1) \ T_2\\
&&\qquad \If  of\ E_1\ (arrow\ T_1\ T_2)\\
&&\qquad \If \neg of\ E_2\ T_1.\\
\neg \ald(oflam) &:&\neg of\ (lam\ E) \ (arrow\ T_1\ T_2)\\
& & \qquad \If(\PI{x}{exp} of\ x\ T_1 \Imp\\
& &\qquad\qquad (\PI{T}{tp} \neg of\ x\ T\If T\neqd T_1)\Imp\\
&&\qquad\qquad\qquad  \neg of\ (E\ x) \ T_2).
\eneq

Of course, this lifting of local variables  is not sound in general; in the
former case, it is doable because $T_1$ remains  in output position,
as (possibly higher-order) mode analysis guarantees. On the other hand, for
example, it will not work for predicates as graph reachability:
\[\begin{array} {l} 
path(X,Y) \If edge(X,Y). \\
path(X,Y)\If edge(X,Z)\And path(Z,Y). \\ 
\end{array} \]
Here, the local variable $Z$ becomes an input argument to the
recursive call for \texttt{path}. It is our opinion that the issue of
local variables during complementation does not have a universal
solution.  Approaches which embrace the extensional nature of
universal quantification brought in by the negation of existential
quantifiers \cite{Bar90, Brogi90} are not satisfactory and robust
enough to carry over to logical frameworks with intensional universal
quantification.  On the other end of the spectrum, the idea to simply
keep those universally quantified predicates as constraints, such as
in \cite{Bruscoli94} will pay some run-time overhead.  We instead
conjecture that (sound) variable lifting may be enough for a
sufficiently interesting class of programs \wrt our intended
application. In fact, it goes along well with the rigidity restriction
we have already to enforce to obtain exclusivity of complementation.

\section{Extensions}
\label{sec:extend}
The techniques we have described in this dissertation applies to a
framework such as $L_{\l}$; we briefly comment on how to extend
elimination of negation to richer languages.

\subsection{Beyond Patterns}
Term complementation and intersection require \ho patterns; both
$\l$Prolog and Twelf allow any (well-typed) terms, although they are
dealt with differently. Since we have (dis)equations in our language,
we can apply an idea analogous to normalization of input variables
\ref{ssec:inputnormal} and  replace occurrence of non-patterns with
fresh variables in 
those predicates we intend to complement, and constrain those variable
to be equal to the replaced term. This is close to what happens in the
Twelf implementation  and allow the constraints handling mechanism to
work its magic. If the framework is not constraint-oriented, it is
well-known how to compile away the offending non-pattern occurrence
via appropriate substitution predicates implemented through the
\texttt{copy} clauses \cite{Liang95}.


\subsection{Richer Type Theories}

The approach we have chosen is tailored to satisfy the requirements of
more complex \lf s than $L_{\l}$; thus, we now mark some
observations on how elimination of negation can be extended to richer
type theories.



\subsubsection{Polymorphism}

Different degrees (in the $\l$-cube) of polymorphism have been
advocated as a feature in \lf s. Of course, the more expressive the
type theory, the more complicated its meta-theory. Pfenning has given
an algorithm for patterns unification and generalization in the
{Calculus} of {Constructions} \cite{Pfenning91lics}. Even if we stick
to the fully applied case, term complementation may be fairly
difficult to achieve in general.  Languages such as $\l$Prolog instead
offer the more manageable prenex (ML-like) polymorphism. In this case,
a version of term complementation able to deal with polymorphic
constructors, such as a polymorphic \emph{cons}, should be
feasible. In many ways, the problems are analogous to negation in
presence of predicate quantification (see next entry \ref{sss:P}),
namely the tension between a static operation as complementation and
the possible instantiations offered by polymorphism.
%  in
% particular we need to extend the complement rules so that the
% complement of a rigid term at base type $a$ will include those
% polymorphic constants of type $\forall \alpha.\, A$ such that there
% exists a well-given type $B$ for which rng$([B/ \alpha]A)=a$. Is seems
% that it will be necessary to put some restrictions on $B$ to make this
% viable. One drastic possibility is to require $B$ to be monomorphic.

\subsubsection{Dependent Types}

Almost all the design decisions we have taken while addressing the
issue of negation in a \lf\ have been motivated by the ease to extend
the latter to a framework as LF/ \emph{Twelf}. The very idea to allow
negation by elimination owes to the requirment to preserve the adequacy
of the extraordinary representation power of dependent types, while at
the same time avoid to interfering with the underlying \lp engine,
which makes \emph{Twelf} a unique unified meta-language for the theory
and meta-theory of deductive systems. While we fall short in this
dissertation to addressing dependent types directly, we believe that
the machinery we have developed is robust enough for this extension.
One novel problem that we can already foresee is related to the
interaction between term complementation and \emph{empty} types.  In
the simply-typed fragment we can assume every type to be inhabited,
but this property is obviously undecidable in the more powerful
setting. This turns out to be problematic when complementing
variables; at first sight, it not clear what the complement of $\GG\vd
\mnot(E\ \xn)\hastype a\ M$ would be. One possibility is to restrict
variable complementation at type $a\ M$, perhaps such that $M$ has no
internal structure at all, \ie it is empty or just a term variable;
this would cover all the examples in this dissertation. Another one
could be `approximating' complementation in the simply-typed fragment
and then sift out the resulting complement set, in view of
dependencies.

\subsection{Predicate Quantification}
\label{sss:P}
  
In the \lp community the term `higher-order' is usually identified
with the possibility of quantifying on predicates, in the effort to
simulate the first-class functions capability of functional
programming languages. This is a sometimes a source of
misunderstandings (let me mention \emph{Hilog} \cite{Chen93} which has
a higher-order syntax and allows arbitrary terms to appear in places
where predicates, functions and atomic formulas occur in predicate
calculus, but whose semantics is strictly first-order) and it may be
overrated, at least as far as \lf s are concerned, as the success of
frameworks such as those based on LF testify. Nevertheless, this is a
useful, though not essential, feature and has been utilized for
example in implementation of proof-carrying code with $\l$Prolog
\cite{Appel99iclp}. Although we have not investigated the issue in
depth, it seems that clause complementation can be sometimes applied
in this extended sense. For instance, let \texttt{some} be a predicate
of type $(nat\Imp\prop) \Imp natlist\Imp \prop$, which selects the
first element in a list of numbers for which a given predicate 
$P\hastype nat\Imp\prop$ holds:
 \beq
shd&:& some\ (\lamb{x}{nat} P\ x) \ (cons\ Y\ Ys) \\
&&\qquad \If (P\ Y).\\
stl&:& some\ (\lamb{x}{nat} P\ x) \ (cons\ Y\ Ys) \\
&&\qquad \If some\ (\lamb{x}{nat} P\ x) \ Ys.  \eneq 
The application
of our algorithm would yield: \beq
\neg snil&:& \neg some\ (\lamb{x}{nat} P\ x) \ nil \\
\neg  stl&:& \neg some\ (\lamb{x}{nat} P\ x) \ (cons\ Y\ Ys) \\
&&\qquad \If \mnotg(P\ Y)\And \neg some\ (\lamb{x}{nat} P\ x) \ Ys.
\eneq Since we cannot foresee the structure of the goal $ (P\ Y)$ at
compile-time, we delay the computation of $\mnotg( P\ Y)$ until the
instantiation is known. Of course, we cannot allow unrestricted
instantiations, but we need to restrict $P$ to conform to the possible
context schema. This will prevent goals such as $some\ (\lamb{x}{nat}
\neg even(x)\Imp even(s(s(x)))\ (cons\ 0\ nil)$, which will destroy
exclusivity.
  
Of course, the above example is too simple-minded in at least one
respect; we did not define term complementation on terms with some
internal logical structure. The only reason the \texttt{some}
predicate was complementable is because the predicate occurring inside
a term is simply a variable, making term complement trivial. In the
general case, clause heads can contain arbitrary complex terms of type
$\prop$. The approach we have developed so far does not seem to
capture those phenomena except  in the  simplest form.
 
% it would seem necessary to make it  recursive to clause complementation


\section{Implementation Issues}
\label{sec:iissues}
A strict logical framework can be directly implemented with very minor
adaptations of well-known techniques used for its linear cousins such
as \emph{Lolli} \cite{Hodas94phd, Cervesato97tcs} and \emph{LLF}
\cite{Cervesato96phd}. Although we argue that strictness is a useful
and ubiquitous concept which deserves to be offered as a
\emph{primitive} notion in a logical framework, this is not the only
choice.

In fact, Girard would be quick to point out that it is not
necessary to take strictness as a primitive  at all, since linear logic
is flexible enough to express the notion of `must occur' already.
Indeed, strict implication can be embedded into linear logic by simply
defining $A\RImp B$ as $A\lop A\Imp B$. This is of course true, but
notice that while this translation will indeed retain provability, it
not faithful to the
structure of proofs.  Since in a logical framework as LF we are also
concerned with the structure of terms, this embedding is not adequate.
% does not preserve the structure we need.  
For example, the strict term $\l x^1.\, c\ x^1\
x^1$ corresponds to both  $\l x^g \l y^u. c\ x^g \ y^u$ and $\l x^g \l
y^u. c\  y^u \ x^g$, where the $( \_ )^g$ notation refers to linear
abstraction and application.
%\x \y. c y x
Even if we are just considering proof search (and not terms) there are
too many distinct derivations of $A\lop A\Imp B$ when compared to
$A\RImp B$. So when we take a theorem in strict logic, embed it, and run
a \lf such as \emph{LLF}, we incur into a fair amount of additional
non-determinism.  On the other hand, the strict $\l$-calculus captures
exactly the right properties in an elegant way and can be developed
from first principles.  In summary, the linear $\lambda$-calculus here does not
apply; even though it is clearly possible to compile strict functions
to linear ones, this compilation preserves only truth, but not the
structure of proofs.

Moreover, as far as negation is concerned, we can safely remain in an
intuitionistic setting.  The drawback is that we have to
decorate source programs whose  clause heads (hereditarely) contain
partially applied terms with appropriate occurrences of the
\texttt{vacuous} predicate we have mentioned in Section \ref{sec:nfa}.
The latter, under negation, is transformed in the \texttt{strict}
one.  Strict unification does not need to be considered, since every term
remains in the fully-applied fragment.

For example, if we are encoding a term say $\rep{\Lambda x.\, e}$ with
the side condition that $x\not\in FV(e)$, we usually represent $e$
with a pattern variable $E$, which does \emph{not} depend on $x$.  For
example, reconsider clause \texttt{linxap1}:
\beq
linxap1& : & linx(\lx app\ (E_1\ x) \ E_2) \If  linx(\lx E_1\ x).\\
\eneq
The latter may be rewritten as:
\beq
linxap1'& : & linx(\lx app\ (E_1\ x) \ (E_2\ x)) \If  vacuous(\lx E_2\
x)\And linx(\lx E_1\ x).
\eneq
where $vacuos(\lx E_2\ x)$ enforces that $x$ does not occur in $E_2\ x$.
The negation transformation will convert those annotations in (pre-compiled)
\texttt{strict} ones. Pursuing further this example, the complement of
\texttt{linxap1'} will include:
\beq
  \mnotd( linxap1)& : & \neg linx(\lx app\ (E_1\ x) \ (E_2\ x) )\If
  strict(\lx E_2\ x)\Or \neg  linx(\lx  E_1\ x).
\eneq

This kind of decoration of programs is a relatively small price to pay
compared to the hassle of implementing a strict calculus, only for the
purpose of allowing full clause complementation; consider for example
the lack so far of a crucial ingredient such as the type
reconstruction algorithm (although one for a related calculus is
presented in Wright's dissertation \cite{Wright92}).  Moreover, for
every signature, the definition of the predicate \texttt{vacuous} is
completely trivial, while the one for \texttt{strict} is type-directed
and may be automatically inferred, in the style of Miller's
\texttt{copy} clause \cite{Miller91elp}. On the other hand, this
approach is less workable when lifting the restriction to
\emph{ground} goals; in the presence of open queries, in fact, those
annotations would induce an undesirable `generate-and-test'
operational semantics: for example, the \texttt{vacuous} predicate
would generate vacuous terms to be then checked for, in this case,
linearity.  It may be possible to internalize the strictness
annotations as \emph{boolean constraints} \cite{Harland97cade}, in
analogy to the linear case; if so, that would work very well with \lf
s such as \emph{Twelf(X)} \cite{Virga99phd} which have a declarative
notion of constraints.


\section{Additional Topics}
\label{sec:additional}
\subsection{Higher-Order Program Algebra}

Several authors have investigated the algebra of logic programs to address
modularity and meta-level issues \cite{OKeefe85,MP88,Sannella92}.
In particular in \cite{MP90} the authors describe a program algebra
for Horn clauses without local variables under clause complement, set
union and intersection.  Since they interpret negation as finite
failure, exhaustivity does not hold. In fact, what they call a
``constructive version of a boolean algebra'' is exactly what Rasiowa
\cite{Rasiowa57} 
calls ``quasi pseudo Boolean algebras'', that is distributive lattices
which satisfy the axioms of strong negation restricted to Horn logic. 

We can extend the idea of a logic program algebra to a significant
fragment of (third-order) HHF. In our case we take equality ($\simeq$)
as operational equivalence under appropriate run-time contexts
\cite{Harland92iclp}; for every program $\cP_1,\cP_2$ (seen as
conjunction of predicate definitions) which satisfy a common context
schema $\cS$, for every run-time context $\ga\ins\cS$ and for every
ground $G$: \beq \cP_1\simeq \cP_2 & \mbox{iff} & (\ga\vd_{\!\cP_1}G
\mbox{ iff } \ga\vd_{\!\cP_2} G) \eneq Then we can organize the set of
(finite) programs into a boolean algebra under union `$\And$' (lub),
intersection `$\Or$' (glb), complement `$\mnotd$', empty program
`$\top$' (zero) and universal program `$\perp$' (one).  Corollary
\ref{co:ccbool} confirms that negation is boolean.  Moreover, the
rules for $\mnotg,\mnotd$ have been engineered to respect De Morgan's
laws.

It could be interesting to study the applicability of those
ideas to modularity of \ho logic programs, in particular to the
modular construction of knowledge-based systems; for example a user
could collect in a module $\cP_1$ all the positive knowledge about a
predicate and in another, say $\cP_2$, all the negative ones (that is, the
cases where the predicate does not hold). This is useful when
dealing with defaults and exceptions. The system would be able to
compose those modules via boolean manipulations.


%\subsection{Strictness and Explicit Substitutions}
\subsection{Strict and Vacuous Variables}

It is our contention that the strict $\l$-calculus that we have
introduced to formulate term complementation has an independent
interest in the investigation of sub-structural logics. Not only our
types system is simpler and (we claim) more elegant of the ones
presented in the literature (reviewed in Section \ref{sec:relstrict}),
but the introduction of the notion of \emph{vacuous} variables can be
useful in a variety of contexts, beyond strictness analysis.  In fact,
Pfenning \cite{Pfenning00saig} has suggested some unexpected usage of
those variables in type theory; in particular, if we equip a linear
$\l$-calculus with vacuous variables, this will permit more programs
under type assignment. For example consider the function $\lx\ly
x\otimes (\l w\, . \, y)\ x$, which is traditionally considered \emph{not}
linear, since $x$ appears twice; nevertheless, the second occurrence
is vacuous since it is the argument of a constant function. By
accounting for the latter, we can give it the linear type $A\lop B\lop
(A\otimes B)$. This carries over to the study of \emph{explicit
  substitutions} \cite{Abadi91} in resource-conscious $\l$-calculi:
for example, in \cite{Ghani98} and refined in \cite{Cervesato99lfm},
the authors propose a system of explicit substitutions for
intuitionistic linear logic over unit, lollipop, tensor and bang,
where variables can either be linear or intuitionistic. The calculus
is not optimal for several reasons, to start with the need for
commutative conversions. One technical issue which could be improved
is the substitution ``extension operator'' which accounts for term to
be substituted and comes in three flavors: intuitionistic, linear and
`used' linear, to mark a term which has already been linearly
substituted.  More in general vacuous (or \emph{hidden}) variables go
together with the modality of \emph{hidden types}, $M\hastype [A]$, ``
$M$ is a \emph{past} term of type $A$'' \cite{Davies00jacm}, which as
the adjoint operation of the traditional $S4$ necessity operator, is a
promising tool in the study of staged computation \cite{Davies00jacm}
and computational irrelevance. We plan to develop such a calculus and
verify its usefulness in those areas.














