
%%%%% Let's begin

Suppose we are giving a formal definition of a programming language in
the style of natural semantics \cite{KAHN87}; after we have specified
the abstract syntax, the type system ($e\hastype \tau$) and a small
step evaluation semantics ($e\mapsto e'$), it is time to check their
consistency via a proof of type soundness. We may start by attempting
the \emph{Progress} lemma, which will eventually guarantee that
well-typed expressions cannot go wrong; in symbols, this could go like
this: for every expressions $e$ such that $e\hastype\tau$ and $e$ is
\emph{not} a value, there exists an expression $e'$ such that
$e\mapsto e'$. Now, imagine that our language is fairly sophisticated
and our funding agency requires a machine-checkable
 verification of our results.
Thus, we decide to use an automated reasoning tool, possibly an
interactive one. A proof of progress is a rather trivial structural
induction for a human, but in order to be machine checked, it needs to
be spelled out in every detail. We may have implemented judgments
defining expressions, values, typing and evaluation: but what about
the notion of \emph{not} being a value? We may try to reason in a
strictly intuitionistic way and view $\neg value(e)$ as the derivation
of a contradiction $\perp$ from the assumption $value(e)$. This is
possible, but certainly not in the spirit of the proof; $\neg
value(e)$ is just a test, a way to sift out expressions that are
already fully evaluated.  What we really need is a \emph{positive}
(inductive) definition of ``not being a value'', say $nonvalue(e)$;
indeed, this should be possible, since non-values are exactly those
expressions which are not values.  Nevertheless, manually coding this
notion may be tedious and error-prone, especially considering
evolution of our initial specification. Moreover, we will also have
the obligation of \emph{proving}, at least to our satisfaction, that
the explicit definition of `non-value' coincides with the negation of
`value'. Lacking this, our formal verification cannot be entirely
trusted.



\smallskip For another example consider a simple instance of reasoning
about process algebra, such as Peterson's algorithm for mutual
exclusion \cite{Peterson81}. The problem here is to ensure that two processes
can never be simultaneously in their critical section. A process can be
in several (possibly many) states, such as \texttt{sleeping, trying,
  critical}; a transition relation describes how the system moves from
a state to another, according to whether a process is allowed to change
its status.  Suppose we want to verify some property of the system such as
\emph{safety}: for any possible sequence of transitions if the initial
state is \emph{safe},  so is the final one. Now, from the description of
the problem, it is apparent that a state is safe if both process are
\emph{not} in their critical section.  It would benefit the
verification attempt to have a \emph{positive} explicit specification
of being a safe state, rather than working with an implicit negative
one. Not only the number of states can be  fairly large, but consider
the natural extension of the same problem to $n$-processes: a
hand-written positive specification of a state being safe can be incomplete or
plain wrong. Again, over time, the number of states will increase or
possibly decrease and the safety specification needs to evolve
accordingly.


\smallskip

The bottom line is that negation is a very common connective in a
specification -- and rightly so, since it is one of the most basic
logic operators. Formalizations that use negation are often sharper and
more concise. Nevertheless, not every automated reasoning tool
available nowadays is able to provide an appropriate handling of this
connective. This is particularly problematic for \emph{logical
  frameworks} based on \ho logic or type-theory with a \lp interpretation, such as
\emph{Twelf}~\cite{Schurmann98cade} and $\l$Prolog
\cite{Nadathur88,Miller91elp}.  While the latter provide a very
advanced unified environment for the specification, implementation and
verification of deductive systems, they inherit the traditional
problems with negation, which Prolog has struggled with since its
inception. These problems are further augmented by some of their more
beneficial features; namely by being `higher-order' and being based on
intuitionistic provability. Those characteristics are the main key
elements of the success of those frameworks and should be preserved
under every extension. This dissertation presents an approach to
endow those languages with a logically sound notion of negation
without sacrifying any part of their representation power.




\section{Logical Frameworks}

A \emph{logical framework} \cite{Pfenning99handbook} is a
meta-language for the specification, implementation and verification
of deductive systems and their meta-theory. Deductive systems consist
of axioms and rules defining derivable judgments; they can be used to
specify logics and aspects of programming languages such as
operational semantics, type systems, abstract machines and
compilation.  

Logical frameworks offer a bridge between the success of declarative
programming languages (logic and functional) and the unsatisfactory
results of general theorem proving.  There is
perhaps a reasonable middle way between Poincare's derision to the
logicist approach:
\begin{quote}
  ``If you need twenty-seven equations to prove that $1$ is a natural
  number, how many will you need to prove a real
  theorem?''\footnote{Les dernieres efforts des logiciens, in Science
    et Methode, p.~193.}.
\end{quote}
and Wos' claim to have solved with OTTER real mathematical open
questions (see \cite{Wos91} for a depressing list).

Many \lf\  have been proposed in the
literature (see \cite{Pfenning99handbook} for an overview) and many
extensions are also under consideration. However, we must carefully
balance the benefits that any proposed extension can bring against the
complications its meta-theory would incur.
We have two main issues to consider:

\begin{enumerate}
\item It is been argued that logical frameworks should be by design as
  weak as possible \cite{DeBruijn91lf}, in order to:
  \begin{itemize}
  \item Simplify proofs of adequacy of encodings.
  \item Allow effective checking of the validity of derivations.
  \item Reduce the complexity of proof-search.
  \item Inherit a treatable  unification problem.
  \end{itemize}
  
\item At the same time \lf s must provide powerful tools to support the
  design process of deductive systems. Experience has shown that the
  strength of a \lf\ is proportional to the ease it makes encodings
  simple and concise.  The more direct is the encoding, the easier is
  to reason about it.  One well known example is higher-order abstract
  syntax~\cite{Pfenning88pldi}, which moves renaming and substitution
  principles to the meta-language; this avoids the explicit programming
  and proving of  a large series of low-level results about those trivial
  but ubiquitous concepts.  Another example is the reification of
  derivations as proof terms in type-theoretic languages, which
  reduces run-time check for correctness of derivations to
  type-checking in the meta-language.
\end{enumerate}




The approach taken in the \emph{Twelf} project is a ``pay as you go''
one. In other words, every extension is carefully crafted so as to
be {\em conservative} on the operational and declarative semantics of
the core language. Examples are the \emph{linear} extension
\cite{Cervesato96lics} or refinement types \cite{Pfenning93types}.




% However, we
% must carefully balance the benefits that any proposed extension can
% bring against the complications its meta-theory would incur.

\section{Negation}

The aim of this thesis is to develop a framework for the synthesis of
the negation of logic programs in logical frameworks 
such as hereditary Harrop formulae (HHF) \cite{Miller91apal} and its
implementation in $\lambda$Prolog \cite{Nadathur88}. We intend this to
 set the basis for  type-theoretic frameworks such as LF
\cite{Harper93jacm} and its implementation \emph{Twelf}
\cite{Schurmann98cade} and possibly their linear refinement as
Lolli~\cite{Hodas94ic} and \emph{LLF}~\cite{Cervesato96lics}.  This
approach could also be useful for generic theorem proving systems,
especially ones based on \ho logic such as Isabelle~\cite{Isabelle}.

Those systems (Isabelle excluded) do not provide a \emph{primitive} negation operator.
Indeed, constructive logics usually implement negative information as
$\Not A \equiv A \Imp \perp$, where $\perp$ denotes absurdity and the
Duns Scoto Law is the elimination rule.  Thus negative predicates have
no special status; that would correspond to explicitly coding negative
information in a program, which is entirely consistent with the
procedural interpretation of hypothetical judgments available in \lf s
with a \lp interpretation. However, this would not only significantly
complicate goal-oriented proof search (as it is manifested in the
difficulty of implementing, for example, the full logic of \emph{Forum}
\cite{Miller94}), but providing negative
definitions seems to be particularly error-prone, repetitive and not
particularly interesting; more importantly, in a \lf\ we have also to
fulfill the \emph{proof obligation} that the proposed negative
definition does behave as the complement (of its positive counterpart).


Providing a viable negation operator has an immediate practical
relevance in programming in those languages, since it relieves the
user from the burden of explicitly encoding negative information in
the form of clauses which express the condition for a predicate not to
hold.  Automating the synthesis of negative information has not only
a clear benefit in the \lp sense, but it may also
have a rather dramatic effect on the possibility of implementing
deductive systems that would prove to be too unwieldy to deal with
otherwise.  The synthesis of the negation of predicates such as {\em
  typable, well-formed, canonical form, subsort, value} etc.--as well
as Prolog-like predicates such as equality, set membership and the
like--will increase the amount of meta-theory that can be formalized.

Of course, the addition of negation does not change the
recursion-theoretic expressive power of a language, but we claim that
it does make a difference at the representation level.
To bring this to the extreme, deductive systems can
be expressed eventually in, say, \fo Horn logic and ideally
proved-checked or even demonstrated by a resolution theorem
prover or more likely by an interactive one.  In practice, this has
turned out to be very problematic, if not a total failure; hence the
refinement of the tools to higher-order logic and type-theory. 

Traditionally, negation-as-failure (\emph{NF}) \cite{Cla78} has been
the overwhelmingly used approach in \lp (see \cite{Apt94} for a recent
survey): that is, infer $\neg A$ if every proof of $A$ fails finitely.
The operational nature of this rule and its ultimately troublesome
logical status is a serious threat to the \lf s' endeavor.  We will
return on the topic of why \NF is an absolutely inadequate way to
address the issues of negation in a such a  framework in
Section~\ref{sec:nf}.


While the topic of negation has been pursued to the extreme in
first-order logic programming (we shall try a small review of closely
related approaches in Section~\ref{sec:history}), the field is almost virgin
as far as higher-order logic and type theory is concerned: languages
such as $\lambda$Prolog implement {\em NF} with the usual cut-fail
combination: a logical reconstruction for the first order fragment has
been attempted, with somewhat disappointing results, in Harland's
thesis \cite{Harland91phd}.



\smallskip
Though the impetus of this enterprise may seem at first sight mainly 
pragmatic, it should not be underrated.  In short, we are trying to 
design a reasonable notion of negation, a basic building block of any 
logic under severe computational constraints: 
\begin{quote}
``The problem is difficult because it seeks a notion of negation which 
is simultaneously semantically elegant and computationally feasible: 
in both execution and mathematical/logical semantics the extended 
language should cleanly extend the definite clause language'' \cite{Lassez91}.
\end{quote}

The reason why {\em NF} is so popular in the logic programming
paradigm is that it essentially requires no modification to the search
structure of an \lp interpreter.  The real question is whether it also
satisfies the other aforementioned criteria.  Nonetheless this is just
a part of it:

\begin{quote}
  ``...  this notion [{\em NF\/}] is a basic logical notion, a notion of
  value to pure logic (as studied since the Ancient Greeks) of equal
  importance and theoretical standing as notion like Possibility,
  Deduction, Axiom and the like.  The role of negation by
  failure in \lp in only a special case: one manifestation of its role
  in logic'' \cite{Gabbay91elp}.
\end{quote}

Our answer to this plea will be to show that, paradoxically, the best
way to deal with negation in the \lp setting is to eliminate it
through transformation.

%here .
It is a basic fact of classical propositional logic that connectives
are inter-definable; more precisely, a sufficiently expressive
set of sentential operators can  provide, by definition, the missing
ones, as  an immediate consequence of their truth-value semantics.  It
is therefore customary and economically convenient to assume as
primitive only this basis and define the others operators in terms of
the former.  In almost every definition negation is taken as
primitive, paired either with conjunction, disjunction or implication;
even those more succinct presentations based on a singleton connective
as {\em nand} retain an implicit flavor of negation.
% The same remark applies 
% to a notion of negation defined via a propositional constant for 
% falsehood. This provably goes back to Kolmogorov and it is 
% motivated by what Girard \ref{Gir91} likes to call the Heyting 
% semantics.  

There is yet another way to address negation which 
%is peculiar to classical negation and
is related to the transformational approach we are interested in.
This is known as {\em negation normal form} and it is used for example
in Tait's concise proof of cut-elimination for classical logic.  For
every atomic predicate symbol $p$ we also have a symbol denoting the
opposite, say $\ol{p}$.  Then, with the essential usage of double
negation elimination and De Morgan's laws, negation is \emph{defined}
as follows:
\beq
\neg p& \eqdef &  \ol{p} \\
\neg \ol{p}&\eqdef&  p \\
\neg \neg  p& \eqdef & p \\
\neg (A \And B)& \eqdef&  \neg A \Or \neg B\\
 \neg (A \Or B) &\eqdef & \neg A \And \neg B
\eneq
Thus, as far as the classical propositional structure is concerned, 
negation can be accomplished simply  by renaming. Consistency is then achieved by 
adding axioms that specifies that is it inconsistent to hold both $p$ 
and $\ol{p}$, namely $p \Bimp \neg \ol{p}$ an  $\neg p \Bimp  \ol{p}$.

This is another way to look at the approach to negation that we shall
investigate, that is the  {\em transformational} one, also known as \emph{intensional
  negation}, initiated in \cite{Sato84} and developed in Pisa for Horn
logic~\cite{Barbuti87,Bar90,Bruscoli94}.  Roughly, given a clause with
occurrences of negated predicates, say $Q\If G, \neg P, G'$, where $P$
is an already defined atom, the aim is to derive a \emph{positive}
predicate, say $non\_P$, which implements the complement of $P$,
preserving operational equivalence; then, it is merely a question of
replacement, yielding the negation-less clause $Q\If G, non\_P,G'$.
This has the neat effect that negation and its problems are
\emph{eliminated}, \ie we avoid any extension to the (meta) language.
Technically, we can achieve this by transforming a Horn program into
negation normal form and then by negating atoms via complementing
terms, a problem first addressed in \cite{Lassez87} for \fo terms.  To
mention the simplest example possible, suppose we have a procedure
\texttt{p} that calls somewhere a check for a number not to be
\texttt{even}, where the latter is already defined:
\[
\begin{array}{l}
p(X) \If \dots \neg even(X) \dots
\vsk
even(0).\\
even(s(s(Y))) \If even(Y).
\end{array}
\]
The goal is to obtain a definition for \texttt{p}, where the negative
occurrence of \texttt{even(X)} is replaced by a positive call to its
complement, say \texttt{non\_even(X)}. This involves the
\emph{synthesis} of the \texttt{non\_even} predicate from its positive
definition:
\[
\begin{array}{l}
p(X) \If \dots non\_even(X) \dots
\vsk
non\_even(s(0)).\\
non\_even(s(s(Y))) \If non\_even(Y).
\end{array}
\]

Thus where is our contribution?  The problem is that this does not
carry immediately over to every computational logics, where the notion
of negation normal form may be in itself problematic.  The issue was
not apparent in the existing literature because of the identification
of \lp with Horn programming.
%\smallskip
For accident or necessity (though we now lean for the former) Horn
logic imposed itself as {\em the} format in logic programming.
Because of its restricted syntax classical and intuitionistic
provability coincide in this fragment. This entails that classical
equivalences preserve the intended operational semantics of the source
program. Thus negation normal forms do work here, as we explain in
Chapter~\ref{ch:hornelim}


Nevertheless, this approach does not scale immediately to more
expressive languages.
 Once
we go beyond Horn logic, the intuitionistic (or `search-like')
interpretation becomes crucial to ensure the existence of what is
commonly agreed as a reasonable interpreter for a \lp language.
Our endeavor can be paraphrased as the search for a notion of negation
normal form for a significantly fragment of \ho intuitionistic logic
which is compatible with a \lp interpretation.

It must be remarked that the issue of negation in constructivism is by
no means new, but it has been considered by many problematic. One
sticky point lies in the Heyting semantics of $\neg A$, seen as a short
for $A\Imp\bot$; many have expressed doubts about the epistemological
status of a construction which yields the absurdum. A discussion can
be found in Wansing's monography \cite{Wansing93}. Already in its
textbook \cite{Heyting56} Heyting mentions Griss' attempt to formalize
a notion of negation-less mathematics. The most well-known approach to
marry a first-class notion of negation with constructivism is Nelson's
\emph{strong negation} \cite{Nelson49}.  As we will argue in Section
\ref{sec:completion}, the interaction between strong negation and
implication is inadequate to support the operational interpretation of
HHF we are interested in.

Additionally, elimination of negation does not scale immediately to \lf s such as HHF,
for two other  reasons:
\begin{enumerate}
\item The simply-typed $\l$-calculus is not closed under term
  complement.
\item There is an intrinsic tension between the \emph{Closed World
    Assumption} (CWA) \cite{Reiter78}, which is associated with negation,
  and the \emph{Open World Assumption} (OWA) typical of languages with
  embedded implication.
\end{enumerate}

Differently from the \fo case, the complement of a lambda term cannot,
in general, be described by a pattern, or even by a finite set of
patterns.  We can isolate one basic difficulty: a pattern such as
$\lambda x\ldot E\ x$ for an existential variable $E$ matches any term
of appropriate type, while $\lambda x\ldot E$ matches precisely those
terms $\lambda x\ldot M$ where $M$ does not depend on $x$.  The
complement then consists of all terms $\lambda x\ldot M$ such that $M$
\emph{does} depend on $x$.  However, this set cannot be described by a
pattern, or even a finite set of patterns. This formulation of the
problem suggests that we should consider a calculus with an
internal notion of \emph{strictness} so that we can directly express
that a term must depend on a given variable.
We will  therefore introduce a \emph{strict} $\l$-calculus where term complement in the
simply typed $\l$-calculus can be embedded and performed. 

The second issue is rooted again in the fundamental difference between
Horn and HHF formulae: as well known, a Horn predicate definition can
be seen as an inductive definition of the same predicate. The
\emph{minimality} condition of inductive definitions excludes anything
else which is not allowed by the base and step case(s). This
corresponds in Horn logic to the existence of the least model and to
the consistency of the CWA and its finitary approximation, the
\emph{completion} of a program \cite{Cla78}: every atom which is not
provable from a program is assumed to be false.  Languages which
provide embedded implication and universal quantification are instead
\emph{open-ended} and thus require the OWA; in fact, dynamic
assumptions may, at run-time, extend the current signature and program
in a totally unpredictable way. This makes it in general impossible to
talk about the closure of such a program.  In the literature  (reviewed
in detail in Section~\ref{sec:lamrelated})  the issue
has been addressed in essentially three ways:
\begin{enumerate}
\item By enforcing a strict distinction between CWA and OWA predicates
  and applying \NF only to the former \cite{Harland91phd}, where the
  latter would require   minimal negation,   as in \cite{Momigliano92}.
\item By switching to a modal logic, which is able to take into
  account \emph{arbitrary extensions} of the program as possible
  worlds (see the completion construction in
  \cite{Giordano98} for N-Prolog and \cite{Bonner94} for
  Hypothetical Datalog).
\item By embracing the idea of \emph{partiality} in inductive
  definitions and using the rule of  \emph{definitional
    reflection} to  incorporate a proof-theoretical notion of
  closure analogous to the completion~\cite{SchroederHeister93lics,McDowell97lics}.
\end{enumerate}

None of those approaches are satisfactory for our purposes: most of
the predicates we want to negate are open-ended; similarly,
definitional reflection is not well-behaved (for example cut is not
eliminable) for that very class of programs we are interested in.
Moreover, we need to express the negation of a predicate in the same
language where the predicate is formulated.  Our solution is to
restrict the set of programs we deem deniable in a novel way, so as to
enforce a \emph{Regular Word Assumption} (RWA): we define a class of
programs whose dynamic assumptions extend the current database in a
specific regular way. This constitutes a reasonable middle ground
between the CWA which allows no dynamic assumption but is amenable to
negation and the OWA, where assumptions are totally unpredictable. The
RWA is also a promising tool in the study of the meta-logical
frameworks \cite{Schurmann00phd}.  Technically, this regularity under
dynamic extension is calibrated so as to ensure that static and
dynamic clauses never \emph{overlap}. This property extends to the
negative program; in a sense, we maintain a distinction between static
and dynamic information, but at a much finer level, \ie \emph{inside}
the definition of a predicate. The resulting fragment is very rich, as
it captures the essence of the usage of hypothetical and parametric
judgments in a \lf; namely, that they are intrinsically combined to
represent \emph{scoping} constructs in the object language. This is
why we contend that this class of programs is adequate for the
practice of logical frameworks.


\subsection{What is Failure (in a Logical Framework)?}

A minimal requirement for a negation operator `$\neg$' is that if a set of
assumption $\GG$ is
consistent, it is the case that $\GG\vd A$ iff \emph{not} $\GG\vd\neg
A$. It is a key issue how to interpret the notion of non-existence of a
proof. In the \lp tradition this has been identified with the idea of
\emph{finite failure}: the \lp interpreter is run by querying a given
program $\cP$ with a goal $G$; the halting of the query without a
derivation is evidence enough to assert the negation of $G$.  This
idea actually traces back to the same principle in the deductive
database context, where the decision problem has a positive answer.
Indeed, in this setting, the \emph{Closed World Assumption} is a most
natural one, since, given the large number of entries in a database,
the only reasonable way to encode negation is by absence. The transfer
of this idea to full \lp \cite{Shepherdson85} has been not exactly
worry-free, as the enormous literature on the subject testifies.
Luckily, our requirements are somewhat different from general logic
programming; in fact, in a \lf, negation refers not to finite failure
but to unprovability tout court, as we refrain from negating programs
whose negation is not recursively axiomatizable: the adequacy of the
representation will break down, since there would be functions which cannot
be captured by the framework.  We will therefore deal only with
terminating programs; this is why we identify negation with a
\emph{complement} operation. This restriction, far from being an easy
way out, gives us the additional burden to prove that termination is
preserved under every manipulation of programs.


It is clear that elimination of negation makes sense only when
negation is \emph{stratified} \cite{Apt88}, \ie the negative
predicates ultimately refers (in the call graph) to a positive one.
%In \lp stratified programs are well-known to have a
We will informally adopt the generally accepted weaker notion of
\emph{local stratification}  \cite{Apt94}, when the positive
dependency relies not simply on predicate names, but on ground
instantiations of literals.
While there may be a place in \lp for non-stratified negation, as the
emerging \emph{answer set programming} paradigm \cite{Marek99}
testifies, the latter seems to be circumscribed to solving mainly
combinatorial problems.  This does not seem to be  a concern for a \lf.



\subsection{Which Logical Framework?}
% \newcommand{\ll}{$L\l$}

In this dissertation we work with the pattern fragment of third-order
HHF; thus our results apply to the same fragment of  \lll 
\cite{Miller91jlc}, although every design decision has been influenced
by the possibility to extend it to the richer language of LF and to
its implementation in \emph{Twelf}. We comment on this in the
conclusions (Chapter~\ref{ch:end}). \emph{Twelf} can be seen as a
dependently-typed CLP-oriented enhancement of \lll. Both share
unification restricted to the pattern fragment, as well as the lack of
predicate quantification.  For convenience reasons we take the liberty
of decorating HHF clauses with labels that can be thought of as
names. This allows us to be more concise when applying program
transformations. Even though they resemble the same notation in
\emph{Twelf}, they lack any intrinsic meaning and will not be used as
proof-terms. 

Furthermore,  we restrict ourselves to HHF without \emph{local}
variables. If we look in the usual \lp fashion at an implicational
clause as a rule where the consequent is the `head' and the antecedent
the `body', a local variable is an essentially existential one which
occurs in the body but not in the head. This restriction is customary in the
literature on elimination of negation \cite{Sato84,MP90}.  For example the following clause for typing application
cannot be allowed, in this format.
\pagebreak
\beq
ofapp & : & \PI{E_1,E_2}{exp}\PI{T_1,T_2}{tp}\\
&& of\ (app\ E_1\ E_2) \ T_2\\
&&\qquad \If of\ E_1\ (arrow\ T_1\ T_2)\\
&&\qquad \If of\ E_2\ T_1.
\eneq

% \[\begin{array} {l} 
% path(X,Y) \If edge(X,Y). \\
% path(X,Y)\If edge(X,Z)\And path(Z,Y). 
% \end{array} \]
The problem is that  Horn clauses
with local variables are already \emph{not} closed under complementation; in
fact,  elimination of negation will transform those into \emph{extensionally}
universally quantified variables. It is a whole new topic to give an
operational reading of universal quantification in this setting and to
mingle it with parametric judgments.  It is our feeling that the issue of
local variables during complementation does not have a simple general
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, except when dealing with \emph{finite} domains. 

While it is well-known that every computable function can be expressed
by a Horn programs \emph{without} local variables, we cannot hide that
this is a somewhat severe restriction. We offer some ideas on how to
partially overcome it in the conclusion (Subsection~\ref{ssec:local}).




















