\section{Aim}

The aim of this thesis\footnote{This section comes from my 1994 
proposal and need serious updating} is to develop a framework for the 
synthesis of the negation of (logic) programs in logical frameworks 
such as LambdaProlog, $L_{\l}$ , \cite{NM88,Mil91b,HM93} and set 
the basis for the type-theoretic programming languages Elf, Twelf and
possibly their linear refinment as Lolli or \emph{LLF}. 
\cite{Pfe91a,CP96,SP98}.  % and in general in higher-order logic.
 This has an immediate practical 
relevance in programming in those languages, since it relieves the 
programmer from the burden of explicitly encoding negative information 
in the form of  clauses which express the condition for a predicate
not to hold.  The main point 
is to avoid resorting to an operational interpretation of 
negation-as-failure, {\em NF}, whose ultimately troublesome semantics 
is a serious threat to the implementation, verificationand 
automatization  of the 
meta-theory of deductive systems
% , which is one of the ultimate 
% objectives of logical frameworks such as LF \cite{Har93} or Hereditary 
% Harrop formulae (hhf) \cite{Mil91b}
.  We will have plenty to say on why \NF is an abosoultely inadequate
way to address the issues of negation in alogical framework.
Lret us mention here the basic issue of \emph{proof-terms}: s8uch a
framework must deilver evidence of what a proof is of a certaing
judgment. The most popular way, since the Automath project
\cite{DeBruijn80} is to to see derivations as lambda terms inhabiting
theorems seen as types. It is not clear how to represent, in a
faithfull fashio how to associate a prrof-terms to a `derivation' by
negation-as-failure. This is not a mere notational problem.
\smallskip{}
The approach to negation that we shall investigate is {\em
  transformational}, also known as \emph{intensional negation}, sketched 
in \cite{Sat84} and developed in Pisa
\cite{Barbuti87,Bar90,Bruscoli94}.  Roughly, given a  program with occurrences of negated predicates, the aim 
is to derive a new program where the former have been replaced by new 
positive predicates which correspond to their complement (in a 
way to be clarified below).

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 appraches in  
\ref{related}), 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
disappointing results in Harland's 
thesis \cite{Har91a}.

Intuitionistic type theories from the simply typed $\lambda$-calculus 
on, say, to Martin-L\"{o}f's Type Theory implement negative types 
under the Curry-Howard isomorphism as expected, i.e.\ $\Not A \equiv A 
\Imp \perp$, where $\perp$ denotes the empty type and DSL is an 
elimination rule.  Thus negative types have no special status, since 
the emphasis is on functional programs extraction, rather that giving 
a search (logic programming-like) operational reading to types.

Under the latter interpretation of dependent function types this would 
correspond to including explicit negative information in the program.  
Although this is entirely consistent with the procedural 
interpretation of function types (hypothetical judgments), it has, 
beyond the aforementioned obvious disadvantage, some additional ones, 
as we shall argue next.

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 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{Las91}.
\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.  Hence most of the effort is to try 
and show that it also satisfies the other criteria Lassez et al.  
pointed out.  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{Gab86}:
\end{quote}

Our answer to this plea, will be to show 
that, paradoxically, the best way to deal with negation in the \lp 
setting (but see \ref{el-rel} for more) is to eliminate it through 
transformation.

Now, let us see more concretely what it means to us; this reduces to 
the two intertwined questions: {\em why a language as Twelf}
%  \footnote{It may be 
% argued that this is more of relevance to Elf seen as a LP language 
% rather that to LF as a specification metatheory; yet the operational 
% interpretation of LF signatures is independent from the idea of 
% synthesizing negative types
% % : e.g.  the specification of LF into LF 
% % itself would greatly benefit from that.
}?  and {\em why adding 
negation}?

\begin{enumerate}
\item
{\bf Twelf}: its main edge is the easiness to formalize and 
{\em verify} the metatheory of deductive systems: Martin-L\"{o}f's idea of judgments-as-types and 
proof checking as type checking has revolutionized the otherwise 
painful task of programming proof-checkers. 
%  Moreover Twelf's idea of 
% verification of metaproof as programming can be safely  
% compared to Kowalski's motto (Algorithms = Logic + Control).  
Also the analogy with the difference between the success of logic 
programming and the unsatisfactory results of general theorem proving 
may be enlightening.  There is perhaps a reasonable middle way between 
Poincare's derision to the logicist approach:
\begin{quote}
``If you need 27 steps to prove that one is a natural number, how many 
will you need for a real theorem?''.
\end{quote}
and Wos' ambition to have solved with OTTER real mathematical open 
questions (see \cite{Wos91} for a (distressing) list of them).

\item
{\bf Negation}: Twelf is one of the purest, hence poorest by design in terms of 
programming language features, systems around; of course this is a 
conscious design decision to achieve the possibility of expressing, 
verifying and eventually automating the meta-theory of deductive 
systems.  Indeed, every enlargement of the expressive power of the 
language has to be carefully crafted, in a declarative way (i.e.\ 
without spoiling its inductive character), as in the case of 
refinement types \cite{Pfe93} or otherwise expressed as an outside 
argument (schema-checking \cite{Pfe92}).  More explicitly, this 
amounts to show that every extension is {\em conservative} on the 
operational and declarative semantics of Twelf.  
% In our case the 
% obligation is to show that the transformation is the identity function 
% on positive signatures and that no new queries involving only positive 
% types can be successful from the transformed program.

An appropriate negation operator may have a rather dramatic effect on 
the possibility of implementing (i.e.\ {\em programming}) topics that 
would prove to be too unwieldy to deal with otherwise.  Automating the 
negation of predicates as say {\em typable, well-formed, canonical 
form} etc.\ will increase the amount of meta-theory that can be 
checked.  Moreover providing negative definitions seems to be 
particularly error-prone, repetitive and not particularly interesting, 
thus a good candidate to mechanization.  Following this trend a good 
analogy is the use of higher-order abstract syntax \cite{Pfe88}: 
although it may seem unintuitive at the beginning w.r.t.\ ``named'' 
syntax, it does  make 
the difference between being able to master meta-proofs and spending 
enormous amounts of time in implementing low-level (and tedious) 
features such as renaming or substitution.  To bring this to the 
extreme, of course, everything can be expressed eventually in 
first-order logic and ideally proved-checked or even demonstrated by, 
say, 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.  And this is the bottom line: adding another 
(practically) essential tool to Twelf\footnote{Naturally, there is 
always the problem of enhancing the metalanguage so much that it 
actually overkills the object level it is trying to specify.  Even if 
the proposed framework is conservative over more manageable systems, 
we run the risk of having to deal with a overwhelmingly complicated 
metatheory of the framework for suspicious gains.}.
\end{enumerate}

This has an analogy with  developments in the eraly $90$'s in the design of 
``standard'' Prolog-like languages; for external reasons, namely, 
program transformation, there has been a trend in ``logicizing'' here 
at a first-order level built-in predicates such as term comparison, 
arithmetic, metalogical predicates (see \cite{Hil94}). 
%  The limit of this 
% process is perhaps Lloyd's G\"{o}del language \cite{Hil94} where 
% everything is supposedly declarative
% 
% \footnote{This has very recently 
% allowed the construction of a self-applicable partial evaluator for 
% the whole language.}.

Hence the motto seems to be: add features, keep them logical (and 
constructive).

\subsection{Which logical framework}
% \newcommand{\ll}{$L\l$}

Why we use \lll, if we use it at all.  Mention \ho patterns and the CLP 
approach to hard \ho unification problems and lack of quantification 
over propositions in LF.

