\documentstyle[a4]{article}
\pagestyle{headings}
\pagenumbering{arabic}
\include{com}
\begin{document}
\title{The Transformational Approach to Negation in
Higher-Order and Type-Theoretic Logic Programming Languages \\ 
{\normalsize Thesis Proposal}}

\author{Alberto Momigliano \\
Department of Philosophy \\
Carnegie Mellon University\\
15213 Pittsburgh PA, USA \\ 
{\tt mobile@lcl.cmu.edu}}
\maketitle

\section{Introduction}

The aim of this thesis is to develop a framework for the synthesis of 
the negation of (logic) programs in type-theoretic programming 
languages such as Elf \cite{Pfe91a} 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 type families (higher-order 
clauses). 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 and verification 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}. As 
hinted in the title, the approach that we shall investigate is 
{\em transformational}, started in \cite{Sat84} and refined in 
\cite{Bar90}. Roughly, given an Elf (hhf) program  with occurrences
of negated types (predicates), the aim is to derive a new program 
where the former
have been replaced by new positive types (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 review in Section \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 can be found 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\footnote{Note  that the double 
negation interpretation
has been investigated in the context of computational irrelevance.},
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: to quote from \cite{Las91}:
\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''.
\end{quote}

The reason why {\em NF} is so popular in the logic programming (LP) 
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: 
quoting from \cite{Gab86}
\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''.
\end{quote}

Without going overboard,  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 Elf} \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 Elf}: its main edge seems to me the easiness to formalize and
{\em verify} the metatheory of deductive systems: without mentioning
the pedagogical value, 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 Elf's
idea of verification of metaproof as programming can be safely
(perhaps) 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 (but I cannot elaborate on that here).
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}:  Elf is one of the purest, hence poorest
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 Elf. 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,
notwithstanding the Nuprl group \cite{Con86}, 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 Elf\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. This is, in  my opinion,
the case of the usage of framework based on full linear logic,
for contexts where the manipulation of resources is not so vital.}.
\end{enumerate}

This has an analogy with recent developments 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  and so on. 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, if possible).

\medskip

The rest of this proposal is organized as follows: Section \ref{nt}
contains the core of the proposed work: after a brief delineation of 
an improved version of the transformational 
approach to first-order logic programs in \cite{Bar90} (\ref{bar}),
we describe the bulk of our contribution, namely, extension to

\begin{enumerate}
\item
Higher-order terms (patterns) (\ref{hop})
\item
Implicational goals (\ref{imp})
\item
Generic goals (\ref{uquant})
\end{enumerate}

In Section \ref{ext} we list some related topics that we would
like to investigate; in particular the connection with inductive
definitions (\ref{ind}), the possibility of using regular tree
languages to escape some of the known limitations of the
method (\ref{reg}) and other more general types of higher-order
program transformations (\ref{tran}). Section \ref{related} tries to 
situate our work in an historical perspective and lists some
of the alternative approaches to negation in LP. Eventually
in Section \ref{out} I summarize what appears to me as the
essential ingredients of the proposed work and present a
potential time frame.

\section{Synthesis of Negative Types}
\label{nt}
\subsection{Background}

For the sake of this document we assume familiarity with
the basic notion and properties of logic programming (classical 
references are \cite{Llo87} and \cite{Apt90}), hhf and uniform proofs 
\cite{Mil91b}, LF and Elf. We shall instead spend a few words on 
negation (see \cite{Apt94} for a recent survey).

The idea of a proof under the {\em NF} (meta)rule is a very natural 
one: suppose you have a set of axioms and 
some kind of inference mechanism which produces a recursively 
enumerable set of theorems, and 
that you are asked to verify the truth of a negative conjecture   
$\Not C$ under {\em NF}; then you try to prove $C$ from your theory; 
if you succeed, then  
$  \Not C$  does not hold, while if you realize (in a finite time) 
that $C$ is not provable, then you are 
entitled to assert that  
$  \Not C$  holds. {\em NF} is a computational approximation to the 
Closed World Assumption (CWA) \cite{Rei78}. Its basic idea is  to 
state that a goal is false if we are able to prove that it cannot be 
proved by the program. We answer no to a 
goal because our attempt to say yes failed, so we say no because we 
cannot say yes.  

Differently from 
other kind of negation, {\em NF}  (\cite{Gab86} p.\  8)
\begin{quote}
`` ... does  not follow from some constructive   knowledge, but from 
lack of knowledge.'' 
\end{quote} 

That motivates two specific features of {\em NF}: its inability of 
finding instantiations for the variables of the  goals and its 
non-monotonicity.
In logic programming, {\em NF} works this way (\cite{Llo87}  p.\  
87):  

\begin{quote}
``The basic idea is to use \SLD-resolution 
augmented by {\em NF} rule. When a positive literal is selected, we 
use essentially \SLD-derivation to derive 
a new goal. However, when a ground negative literal is selected, the  
goal answering process is 
entered recursively in order to try to establish the negative subgoal 
\dots   Having selected ground negative literal  $ \Not A$ in some 
goal, an attempt is made to 
construct a finitely failed $SLDNF$ tree with root  
$\leftarrow A$  before continuing with the remainder of the 
computation. If such a tree is constructed, then 
the subgoal  
$ \Not A$  succeeds. Otherwise, if a $SLDNF$-refutation is found for  
$  \Not A,$  then the subgoal fails''.
\end{quote}

The {\em completion of a program} $comp(P)$ \cite{Cla78} is the most 
well-known
way to motivate the usage of {\em NF}, which is otherwise unsound 
w.r.t.\ the classical notion of logical consequence:
when a negative goal succeeds from $P$, it can be shown to follow 
from $comp(P)$  (see Section \ref{related} for a refinement of that). 
Completeness is instead a whole different issue: it can be achieved 
only for restricted classes of programs or by switching to 
many-valued models \cite{She88}, \cite{Kun87}. In this thesis we 
shall opt
for the former alternative and take the notion of completion as the 
intended meaning of the given program. Briefly it consists of 
extending the latter with its only-if side (the closure condition in 
inductive
definitions, see \ref{ind}).

\begin{Def}
Let p be a $n$-ary relation symbol; we assume that it is defined by 
$n$ clauses whose head has the form $p(\dots)$ and the $i$-th clause 
has $n_i$ literals in its body, i.e.\ has the form
\beq
p(t_{i,1}\dots t_{i,n}) \leftarrow L_{i,1}\dots L_{i,n_i}
\eneq

The {\em completion} of $p$ is the following axiom:

\beq
\forall \overline{x} (p(\overline{x}) \Bimp \bigvee\limits^n_{i=1}
\exists \overline{y} (\overline{x}=\overline{t_i} \And
\bigwedge\limits^{n_i}_{k=1} L_{i,k}))\\
\eneq
where $\overline{x}$ is an array of $n$
of new variables, whereas $\overline{y_i}$ are those appearing in the 
$i$-th clause.

\begin{Example} Consider the usual program for membership in lists:

\\

\[\begin{array} {l} 
member(X,X.XS). \\
member(X,Y.YS) \leftarrow member(X,YS). \\ 
\end{array} \]

\\

Its completion is
\beq
\forall z, zs ( member(z,zs) \Bimp \exists x,y,xs,ys, (zs = x.xs \And 
x = z) \Or  (zs = y.ys \And y = z \And member(x,ys)))
\eneq
\end{Example}

Another ingredient is {\em Clark's equational theory} (CET) 
\cite{Cla78}, which is required to proof-theoretically simulate 
unification: those axioms force equations introduced by the 
completion to be interpreted as the identity relation 
on the domain of interpretation. This (infinite) equational theory, 
also
known as $E_{FT}$, completely axiomatizes the algebra of finite
trees under an infinite signature \cite{Kun87}. When the signature is 
finite
we need an addition to CET in the form of the {\em Domain Closure 
Axiom} (DCA) \cite{Mah88}: for a signature $\Sigma = 
\{f_1,\dots,f_n\}$ the axiom states:
\beq
\forall x(\bigvee\limits^n_{i=1}
\exists \overline{y} (x=f_i(\overline{y})))
\eneq
\end{Def}

This amounts to saying that every model is {\em reachable}, i.e.\  
every
element is denoted by at least a term construed out of the signature. 
For the above example it asserts (glossing over typing for the time 
being -- we remedy this in the next section):

\beq
\forall x(\exists y,ys (x= nil \Or x = y.ys))
\eneq

Finally, we recall how to express the (relative) complement problem
as an elementary equational formula \cite{Las87} \cite{Com91}. Let 
$[t]$ denotes the set of ground instances of a term $t$. The problem 
is to compute $[t] / [u_1, \dots , u_n]$. Assuming that 
$\overline{z}$ are the free variables of $t$ disjoint from 
$\overline{y}$, i.e.\ the free variables of $u_1, \dots, u_n$, 
everything boils down to 
solving:

\begin{center}
$\exists \overline{z} \forall \overline{y} (x = t \And
\bigwedge\limits^{m}_{i=1} x \not = u_{i})$
\end{center}


\subsection{The Transformational Approach in Normal LP}
\label{bar}
Here we give a brief summary (and a slight improvement) of Barbuti's 
approach \cite{Bar90};
see \ref{cn} for a comparison with others, in particular 
\ref{stat-rel} for a more close scrutiny of the relationship with 
Sato's.
This is the starting point since we wish to improve this in several 
ways, generalizing through what will occur as a natural hierarchy.

Proceeding bottom-up, the first thing is to define a complement 
operation on terms ({\em Not}). Informally an open (left-linear, see 
below) term can be seen as a  representation of the set of its ground 
instances; hence its complement should represent the set-theoretic 
complement of such a set. An algorithm for first-order terms is given 
in \cite{Bar90} which specializes \cite{Las87}
 
Standard Prolog is not typed: that means that a straightforward {\em 
Not} operation will produce a lot of irrelevant results (this has 
some analogy with the proposal in \cite{Foo88}). For example, towards 
the synthesis of the {\em nonmember} operations on list of numerals
the result of $Not(0)$ contains not only $s(x)$ as expected, but also 
$nil, 0.nil \ldots$ This is going to increase exponentially with the 
size of the signature. A type discipline would solve this problem.

\begin{Def}
Let $C$ be a Church simple typing for a finitary signature $\Sigma$. 
We define $Not(t^\tau)$ by structural induction, where we assume that 
$t_i$ has type $\tau_i$:

\[ \begin{array} {ll}

Not(x^\tau) =  \{\} \\
Not(f(t_1,\dots,t_n)^\tau) = \\
 \{g(x_1,\dots,x_n)^\tau \suchthat g \in \Sigma, 
g \not = f\} \cup \{f(x_1,\dots,x_{i-1},\overline{t},x_{i+1}, 
\dots,x_n)^\tau \suchthat i \in [1,n], \overline{t} \in 
Not(t_i)^{\tau_i} \}

\\
\end{array} \]

\begin{Example}
Given $\Sigma = \{0^{nat},nil^{nlist},s^{nat \Imp nat},.^{nat \Imp 
nlist 
\Imp nlist}\}$ 
\begin{center} 
Not($s(x).nil$) = $\{nil,0.nil,y.z.xs\}$

\end{center}
This corresponds to the solution of the formula
\begin{center}
$\exists z \forall x . z=w \And z \not = s(x).nil$
\end{center}
\end{Example}
At this level of details, the transformation on predicates is better 
described in words: basically for every clause $p(\overline{t}) 
\leftarrow \Gamma$ in the predicate definition $A$, a table of facts 
$nonp(\overline{t}^c)$ is created for $\overline{t}^c = 
Not(\overline{t} )$, plus a new clause derived by the
disjunction of the literals in the original body $\Gamma$, 
introducing universal quantifiers for (distinct) local variables. 
Eventually the
``negative'' contribution of each clause is merged through unification
to yield the new predicate definition (hereafter denoted with 
$nonA$). The process is iterated for
every predicate occurring negatively in the original program.


The algorithm asks for a specific format in the input program: 
clauses should be left-linear,
 i.e.\  multiple occurrences of the same variable in the
head are disallowed, and every local variable must have a single 
occurrence within a literal in the body; since left-linearization is 
always possible by introducing
unification constraint on the right \cite{Sti88} with a new 
predicate, say, {\em eq}, and localization by introducing new 
predicates, in this document we shall leave those steps implicit; yet 
see \ref{reg} for ways to lift the former restriction on terms. The
possibility of this pre-transformation could, nevertheless, be 
deceiving, since it actually induces a shift from pure Horn LP 
towards {\em Constraint Logic Programming} (CLP) \cite{Stu91} on the 
Herbrand Universe. A 
possibility would be to restrict to classes of programs that satisfy
the aforementioned conditions; on the other hand, similarly to the 
case of {\em allowed} programs to avoid {\em floundering} 
\cite{She85}, this fragment is too limited to be of practical utility.
Moreover the complement operation takes care of disunification,
as explained in more details in (\ref{stat-rel}). Eventually,
a departure from pure Horn logic is unavoidable, as shown in example
\ref{path}.


\begin{Example} 
Given the above program for membership in lists, its negation is 
synthesized as expected:

\\

\[\begin{array} {l} 
nonmember(X,nil). \\
nonmember(X,Y.YS) \leftarrow noneq(X,Y), nonmember(X,YS). \\ 
\end{array} \]

\\

\end{Example}

Note that, even starting with a Horn program, the transformed one
may contain universal quantification in the body, stemming from
local variables. Consider a program for (irreflexive) transitive 
closure of a relation:

\begin{Example}
\label{path}
\\

\[\begin{array} {l} 
path(X,Y) \leftarrow edge(X,Y). \\
path(X,Y) \leftarrow edge(X,Z), path(Z,Y). \\ 
\\
edge(a,b).\\
edge(b,c).\\
\end{array} \]

\\
The complement of the program follows:
\\

\[\begin{array} {l} 
nonpath(X,Y) \leftarrow nonedge(X,Y),\forall Z. nonpath3(X,Y,Z). \\
nonpath3(X,Y,Z) \leftarrow nonedge(X,Z); nonpath(Z,Y). \\ 
\\
nonedge(a,a).\\
nonedge(a,c).\\
nonedge(b,a).\\
nonedge(b,b).\\
nonedge(c,a).\\
nonedge(c,b).\\
nonedge(c,c).\\

\end{array} \]

\\

\end{Example}

This raises two important questions:
\begin{enumerate}
\item
What is the operational reading of universal quantification
in this setting and how it mingles with generic judgments 
(discussed in \ref{uquant}) ?
\item
How can this be reflected in the theory of inductive definitions
\cite{Acz77} (discussed in \ref{ind}) ?
\end{enumerate}

The soundness and completeness of the transformation w.r.t.\ the 
completion of $P$ and (an extension) of \SLD-refutation
is proved in \cite{Bar90}.

Assuming that we have a good understanding of the technique
at this level, the real work starts with the extension to hhf/LF.

\subsection{Two Words on hhf/LF.}

For the sake of simplicity, all the examples in this document will be 
hhf. Without further ado, we recall the syntax and the operational 
semantics, where for atoms we assume the usual backchaining rule and 
$A_r$ is a rigid atom:

\[
\begin{array} {l}
\\
D ::= A_r | G \supset D| \forall xD| D_1 \And D_2|  \\ 
G::= A   | G_1 \And G_2 | G_1 \lor G_2 | \forall xG | \exists xG | 
D \supset G 

\\
\end{array}
\]

\begin{quote} 
    AND:  $P \prv G_1 \And G_2$  only if $P  \prv G_1$ and $P  \prv 
G_2$	  \\
  OR:  $P  \prv  G_1 \Or G_2$  only if $P  \prv G_1$ or $P  \prv 
G_2$  \\
  INSTANCE: $P \prv  \exists xG$  only if there is a term t s.t. $P  
\prv [t/x]G$ \\
  AUGMENT:  $P \prv  D \supset G$  only if $D,P \prv G$ \\
  GENERIC:  $P  \prv \forall xG$  only if $P  \prv [a/x]G$ for a 
eigenvariable 'a'  \\

\\

\end{quote}

At first sight LF (Elf) can be seen as the type-theoretic version
of hhf ($\lambda$Prolog) and thus answers suited to the latter
could be transferred to the former. Moreover translation
of dependent function types into higher-order logic, namely into HOL 
\cite{Jac93} or hhf \cite{Fel91}, have been explored. Unfortunately,
these translations use the familiar idea of sending (dependent) types
into predicates, similarly as the case of many-sorted into 
first-order logic, 
whereas the main idea  in the Martin-L\"{o}f's tradition is exactly
the opposite, namely squeezing  the most of information inside
the type discipline. Hence we shall come back to the translation 
approach (and if any to Felty's \cite{Fel91}, due to its parenthood 
with Elf)
only as a last resort, in case everything else fails. Moreover
this entails compiling a carefully orchestrated property as 
the decidability of type-checking in LF into a undecidable
one such as theorem proving. Besides the
operational interpretation given respectively in Elf and 
($\lambda$Prolog) to $\Pi$ and $\forall$ is strikingly
different; while the latter is used exclusively to introduce
new names, the former, as well known, subsumes function types:
this may turn out to be connected to the difference between
$static$ and $dynamic$ type families in Elf. Operationally,
we are hopeful that most of the techniques developed for
Elf would apply to higher-order logic and vice versa. Nevertheless, 
to minimize
risks we shall investigate universal quantification and implication 
separately.

Finally, we may wonder whether there is a use of {\em NF}
at the meta-level, i.e.\ in the formalization of meta-proofs.
Although there is plenty of ``negative'' theorems around of
the form ``given $A$ there is no $B$ such that...'' that are in the
scope of systems such as Elf, it is clear
that the notion of negation involved is intuitionistic (if not 
minimal).  While it is entirely feasible to incorporate this line
of reasoning into the framework, much in the sense of \cite{Har91a},
\cite{Mom92}, it is unlikely that {\em NF} may turn out to be useful
at this level; indeed, more than a way of proving, it is a license
to {\em assume} $\Not C$, when every attempt to prove $C$ have
failed: hence, this concept is relative to a particular inference
system in the background, and this cannot exhaust in any way our
ability to prove $C$. For example, the current failure to prove 
Goldbach's conjecture does not allow us to assume its falsity. 
In conclusion {\em NF} seems applicable at the level of 
``proposition-as-types'', rather than ``judgments-as-types''.


\subsection{Higher-Order Terms (Patterns)}
\label{hop}

The first extension we shall pursue is higher-order Horn logic: once
we succeed in formulating a satisfactory notion of completion, the
major point is computing the complement of lambda-terms. In 
\cite{Las91} some examples are given regarding functional programs,
but the treatment is strictly first-order. Since the (relative) 
complement problem is an instance of the more general issue of {\em 
disunification} \cite{Com91}, this seems to amount to searching for
cases for which higher-order disunification is decidable. 
Reasoning by analogy, fragments for which unification is tractable
are good candidates. The most well-studied one is {\em higher-order
patterns} \cite{Mil91a} which have a unary (and linear) unification 
problem. Patterns are lambda-terms such that all variables occurring 
in the scope of a free variable are bound and distinct.

Indeed, unpublished work by Lugiez \cite{Lug94} uses a method of 
quantifier elimination
to achieve disunification of higher-order patterns. An extension to a 
fragment of second-order lambda-terms is achieved using regular tree 
languages, yet the linearity constraint is retained. 

On the other hand, experience has shown that the undecidability of
higher-order (dis)unification is very rarely of practical significance
and should not prevent us to try to devise procedure for undecidable
fragments. Of course this entails the Elf philosophy of keeping
(dis)unification problems as constraints which may not be solved
and in the end returned in some normal form.


\subsection{Embedded Implication}
\label{imp}
One of the few extensions to Horn logic that has proved successful
is allowing implicational goals. This was mildly started in NProlog
\cite{Gab84} and was fully developed in the theory of hhf 
\cite{Mil91b}. The possibility of hypothetical judgments has proven
very useful especially to express declaratively the meta-theory
of deductive system \cite{Pfe9?} and it is mandatory to 
preserve it.

The obvious extension of the transformational approach seems to be 
working in most cases.

\begin{Example}
Given $\Sigma = \{ all^{(i \rightarrow o) \rightarrow o}, imp^{o 
\rightarrow o \rightarrow o },
and^{o \rightarrow o \rightarrow o }\}$, the following defines the 
property
of being a Horn clause, where we assume suitable predicates for
``term'', ``atom'' and ``conjunction''

\[\begin{array} {l}
horn (all(C)) \leftarrow \forall x. (term(x) \supset horn (C \ x)).\\
horn(imp(G, A)) \leftarrow  atom(A), conjunction (G)\\
horn(A) \leftarrow atom(A).\\
\end{array} \]

\\ 

This yield the following, where some, but not all redundancies
(see the last clause) have been eliminated and we presuppose the
negation of the other (horn) predicates:

\[\begin{array} {l}
nonhorn (all (C)) \leftarrow \forall x. (term(x) \supset nonhorn (C \ 
x)).\\
nonhorn(imp  (G, A)) \leftarrow  nonatom(A); nonconjunction (G)\\
nonhorn(and (A ,B)) \leftarrow nonatom(and (A, B)).\\
\end{array} \]

\end{Example}

Unfortunately, this does not seem to be general enough, perhaps 
depending on the difference between predicates under the Closed vs.\ 
Open World Assumption. Namely, predicates occurring negatively
in an implication are taken to be open, since they are going to 
dynamically join the program and thus cannot be completed \`{a} la
Clark. In the former example ``term'' is such a predicate. This seems
to rule out {\em non-stratified} implications in the sense of 
\cite{Apt88}.

Consider the
following definition of a predicate which holds if the consequent
of an implication directly appears in the antecedent:

\begin{Example}

\beq
trivial(A \Imp B) \leftarrow trivial(A) \supset trivial(B)
\eneq
\end{Example}

It seems that the only 
thing left is to describe a general technique to eliminate
implications. The obvious answer is to introduce a new predicate
that keeps assumptions explicit, instead of relying
on the interpreter, yielding:

\begin{Example}

\[\begin{array} {l}
trivial(A \Imp B) \leftarrow  trivial2(A,B)\\
trivial2(A,A).\\
trivial2(C,A \Imp B) \leftarrow trivial2(C,B);trivial2(A,B).
\end{array} \]
\end{Example}

The proof obligations is as follows:
\begin{Theorem}
Let $\epsilon$ be the transformation. Then $P \prv G $
iff $\epsilon(P) \prv  \epsilon(G)$
\end{Theorem}

While it is fairly clear how to describe the transformation, the
real challenge is to make it efficient, i.e.\ to use it sparingly
and to minimize the amount of explicit assumptions.
For non-recursive predicates it is maybe possible to eliminate
implications through an extension of the idea of {\em unfolding} 
\cite{Llo91}. This
does not work in general since recursive calls allow self-unfolding.

One way to reduce the amount of predicates which are to
be moved in the list of explicit assumptions is to modify
the notion of {\em stratification} to reflect hypothetical 
dependencies rather than negative ones.


\subsection{Generic Goals}
\label{uquant}

Similarly to  implication, several attempts
to allow universally quantification in  goals in a 
controlled way were proposed in the mid 80's (see NQ-Prolog
\cite{Gab84}, NI \cite{Gab86}, clausal intuitionistic logic
\cite{McC86}). They all showed, as far as I am concerned, an amazing 
amount  of technicalities, restrictions,
lack of clear operational semantics and mostly the absence
of a programming language significance, which is the original
sin of all dead languages\footnote{To alleviate this, I have to 
mention that the impetus to develop NQ-Prolog was the attempt
to formalize the British Nationality Act; yet this hardly qualifies
as a development of programming languages feature as for 
instance $\lambda$Prolog has achieved.}.

A possible source of misunderstanding was perhaps the confusion
between what we now know as the {\em intensional} \cite{Mil91b} vs. 
{\em extensional} \cite{Bar90} interpretation of $\forall$, as well 
as the implicit assumption
of the CWA.  More formally:

\begin{itemize}
\item
Extensional:\\
$\forall^e x. G$ holds if for all closed terms $t, [t/x]G$ 
holds\footnote{Note that we only introduce this distinction for 
goals.}

\item
Intensional:\\
$\forall^i x. G$ holds if for a parameter $a, [a/x]G$ holds
\end{itemize}


There is an obvious relation with what we intend the domain
of computation to be (recall that in the LP tradition this
is central to define the intended term model).

\begin{itemize}
\item
Closed Domain:\\
the signature is fixed once and for all as the one
underlying the program; this can be enforced by the CWA
or an approximation as the DCA.

\item
Open Domain:\\
the signature has no restriction; in operational
terms this means that it is free to expand during execution
 by parameters.
\end{itemize}

This has some relevant model-theoretic consequences that
we may not pursue here. At the risk of being trivial
we instead give the following:

\begin{Example}
Consider the ``program'' $q(a)$; the query $\forall^e x.q(x)$
follows logically from $P + DCA$ and accordingly succeeds;
symmetrically $\forall^i x.q(x)$ fails, as it should. Yet
take the slighter more complicated program:
\[\begin{array} {l}
 p(0)\\
 \forall x. p(s(x))
\end{array} \]
the query $\forall^e x.p(x)$ apparently fails to terminate even
it follows logically from $P + DCA$. $\forall^i x.q(x)$ still fails.
\end{Example}

Before declaring the intensional approach the obvious winner, let me
point out the following
\begin{enumerate}
\item
It does not seem entirely to be  a problem of classical versus 
constructive
logic; the above derivations exists in the minimal predicative
calculus with equality and DCA. For finite signatures, it is a
question of taste to take DCA as a constructive principle. Infinite 
ones
do not arise because they conflict with the Closed Domain Assumption.
\item
The issue of choice of domain is strongly linked to
(constructive) negation: going back to the first example above: 
a query of the type $\exists x . \Not q(x)$ succeeds in the Open
Domain with answer something like $x \not =a$. Moreover,
it seems that only reasonable interpretation of universal
quantification originating from local variables. Coming back
to Example \ref{path}, you may check that the intensional version
of $\forall Z. nonpath(X,Y,Z)$
makes no sense, while, for instance $nonpath(b,X)$ succeeds with
$X=b, X=a$ and $nonpath(a,c)$ fails.

\item
Abandoning the problematic generate-and-test
approach in \cite{Bar90}, extensionality
can be refined to {\em proof by case analysis} \cite{Man88}
and \cite{Har91a} for fohh.
The idea is to use  a $covering$ \cite{Las91}, i.e.\ a finite 
representation of the underlying signature, on whose
members new goals are generated and tested.
\end{enumerate}

\begin{Def}
Given a signature $\Sigma$ and a type $\tau$ hereby declared, a set 
of terms $S=\{t_1,\dots,t_n\}$ is a
{\em covering} for $\tau$ iff for all ground $t^\tau$ there is $i \in 
[1,n]$ and a substitution $\q$
s.t.\ $t = \q t_i$. A {\em minimal} covering set is a covering set 
such that no proper subset is a covering set. A {\em covering for a 
signature} is a covering for all the declared types.
\end{Def}
\begin{Example}
$\{0,s(y)\}$ is a minimal covering for the signature of numerals, 
where
$y$ is a new free variable.
\end{Example}

The soundness of the proof by case analysis (a sort of inversion) can 
be proven; roughly
if a formula  is provable from $P+CET+DCA$ for every choice in the 
covering, then its universalization is provable from the same 
assumptions.

This has to be extended to higher-order terms, but I do not foresee
particular problems.

\medskip 

Of course, proof by case analysis must not be confused with 
induction\footnote{Although there is some connection (still to be 
understood) with the usage of the $\omega$-rule for cut-elimination 
in arithmetic.}:

\begin{Example}
\[\begin{array} {l}
 p(0)\\
 \forall x. p(s(x)) \leftarrow p(x)
\end{array} \]
the query $\forall^e x.p(x)$ fails, since an inductive step is 
required.
\end{Example}

What about parametricity? It seems that intensional
quantification is preserved under the negative transformation,
(see the ``horn'' example)
though one would have to keep track of the extension
of the signature. There is an obvious  tension between
OWA and CWA that could turn out to be problematic.
Hopefully, we shall use case analysis for $\forall^e$
and the GENERIC operation for $\forall^i$. 
\section{Extensions/Related Topics}
\label{ext}

\subsection{On Inductive Definitions}
\label{ind}

It is remarkable how much the LP community has ignored the
connection between Horn logic and inductive definitions (ID) as 
codified in \cite{Acz77} (up to \cite{Hal91a} \cite{Jgr91}and 
\cite{St93}). Most of
the (fixpoint) semantics developed in \cite{Apt82} is a literal 
transliteration of the basic ideas of ID in terms of term models.
Namely given an ID $P$, $ID(P)$ defined as
the intersection of all $P$-closed sets is nothing else than $M_P$,
the minimum model of $P$ seen as a set of clauses. Moreover the 
completion of a program can be seen as syntactic way of enforcing the 
minimality of $ID(P)$, which now turns out to be the only model
(up to isomorphic copies). Similarly the theory of $T_P$ is just
a transcription of the (monotonic) operator $\phi$ associated to
$P$.  Some of the work on intended
models for normal clauses (see Section \ref{related}) can be 
reformulated for non-monotonic $\phi$. For instance an extension of 
the
notion of $P$-closedness leads to the idea of stable models.

Apart from the polemics, what I think can be a interesting problems
by itself is:
\begin{quote}
If, given an ID $P$, its inductive set $ID(P)$ is uniquely determined
in some universe $U$, are there any non-trivial conditions on $P$ or
more easily on $\phi$ such that taking the complement $U - ID(P) 
 =_{def} (ID(P)^C)$ yield a dual inductive definition $P^c$, i.e.\  
the complement is an homorphism: $ID(P^c) = (ID(P)^C)$.
\end{quote}

Of course there some trivial answers, as when $P$ is a decidable 
property in a recursive universe: moreover some remarks in 
\cite{Apt82} on the convergence among the least and greatest fixpoint 
of 
$T_P$ may be relevant.

What I find worth investigating are the limits of Horn-definability:
for example the complement of the definition of transitive closure
is not Horn anymore: hence it should not be in the form of an 
inductive
definition. Yet, from a logic programming point of view the problem
seem to depend from the presence of local variables, whose relevance
in the theory of ID's is not clear (to me). Things are going to get 
nastier once we step to hhf, where, among other things,  classical 
and minimal provability differ, which was not 
an issue for Horn logic. 

It is very likely that the theory of {\em partial inductive 
definitions} \cite{Hal91a} (PID) is the right framework. Here 
(partial) inductive definitions are allowed to be construed by 
iteration on the arrow
in the body of the definition. By analogy, since the closure 
condition of ID corresponds to the completion of Horn programs, it is 
possible  that a suitable restriction of (finite) PID could provide a 
semantics for the negative transformation of hhf programs. 

As remarked below \ref{pt-rel}, PID  are currently
being tested as a basis of a programming language which 
extends languages founded on hhf, but at a very high price in terms
of control. More is discussed in \ref{pt-rel}
%\subsection{Complement in the Lattice of linear higher-order 
patterns}

\subsection{Regular Tree Languages}
\label{reg}
Regular tree languages \cite{Gec84} have been intensively studied and 
adopted,
among others, 
to provide a type discipline to standard Prolog \cite{Mis84} 
\cite{Yar91} 
\cite{Dar92} \cite{Hei92}. Their 
usefulness lies in the fact that they provide a generalization of 
regular languages, without losing their nice closure properties. In 
particular, languages described by non-deterministic grammars are 
closed under complement: this means that there are algorithms to 
compute the negation of
types described by those languages. It is also known (see
 \cite{Lug94} for results and references) that sometimes
the set of (dis)unifiers of lambda-terms can be seen as a word in a 
regular language.  The move to regular tree languages provides 
additional decidability results, although the linearity condition, 
i.e.\ the disallowance of multiple occurrence of the same variable in 
terms, is retained.

Indeed this approach can be used to break the chains of
left-linearization in terms.

\begin{Example}
Given the usual signature for triples of numerals a representation of 
\linebreak
$\{(u,0,v)\}/\{(u,0,u)\}$ is
$\{(s(u),0,0), (0,0,s(u)), (s(u),0,s(v)) \leftarrow (u,0,v)\}$. 
\end{Example}

This can be used to compute the complement of the {\em sum} program 
without requiring the introduction of constraints. 

\subsection{Program Transformation in Higher-Order Logic Programming}
\label{tran}
At the best of my knowledge, program transformation of higher-order 
logic programs has not been investigated per se. The negative
transformation as well as the elimination of implications
can provide insights for more general questions. Both seem
to have strong ties with {\em partial evaluation} \cite{Llo91}:
this essentially consists of two steps: {\em specialization} and {\em 
unfolding}. Without stretching  the connection too much,
the negative transformation in a sense is a form of specialization
since it makes (negative) information explicit  that is left implicit
in the original program. Moreover the target program may contain
redundancies that can be optimized through partial evaluation. As 
mentioned above elimination of implications can be sometimes
achieved via unfolding. Hence a procedure for partial evaluation
in higher-order logic programming would be a welcome side-effect
of this enterprise. Again the problem is not so trivial, since all
three extensions to Horn logic carry some complications. If we
do not want to restrict ourselves to patterns, the notion of 
higher-order
uniform proof on which partial evaluation works will have to be 
extended to take into account possibly infinite unifiers. Similarly
there is an obvious problem in pre-evaluating universal goals whose 
only aim is to introduce new names. The implicational 
fragment seems the less problematic, since it essentially requires
a compile-time version of the deduction theorem.

\section{Related Work}
\label{related}

The history of LP coincides in a large part with the attempt to 
extend the expressive power of Horn logic without incurring in
 computational inefficiencies or declarative nonsense. {\em NF} is 
probably the most common
keyword in this paradigm. What is problematic here is well known and 
let me refer to \cite{Apt90} and
\cite{Apt94}. We list the mainstream  achievements in the following

\medskip

{\bf Brief Chronology}

\begin{itemize}
\item
1970 Hill/Kowalski/Kuehner: \SLD-resolution
\item
1972 Kowalski/Colmerauer: Prolog, with control
\item
1976 Kowalski \& Van Emden: $T_P$-fix-point semantics = minimum model 
semantics for Horn logic
\item
1977 (Tarnlund) Computational adequacy of definite programs
\item
1978 Reiter \cite{Rei78}: Formulation of the CWA 
\item
1978 Clark \cite{Cla78}: Introduction of NF. Contains 
\begin{enumerate}
\item
 	the first (unfounded) def. of \SLDNF-resolution
\item
 	restriction to safe computation rules
\item
 	notion of completion (no reference to inductive definitions)
\item
 	introduction of the free equational theory and statement (proven in 
\cite{Llo87} of two crucial lemmata relating it to unification
\item
 	proof-theoretical soundness, i.e.\  outline of how to transform a 
\SLDNF-refutation in a (classical) derivation somewhere. Shepherdson 
(\cite{She85}) observes it is Intuitionistic, St\"{a}rk \cite{St92a} 
(and me \cite{Mom92}) that it is actually minimal
\item
 	conjecture of a completeness result for hierarchical (i.e.\  
terminating) programs.
\end{enumerate}
\item
1982 \cite{Apt82} Refinement of fix-point semantics to the 
completion, the actual beginning of the Herbrand semantics frenzy: 
everybody forgets that $T_P$ is just generalized Modus Ponens. 

\item
1982 \cite{Min82} First attempt to give a Herbrand semantics to 
non-Horn programs, known as the Generalized CWA in terms of minimal  
models: this has been endlessly refined (actually weakened) and ended 
it up under the label of Disjunctive LP \cite{Min91}
\item
1982 Bowen: first conservative extension of LP to first-order logic, 
as a sequent calculus + unification 
\item
1982 IC-Prolog (Clark) Prolog with non-ground computation rule for 
{\em NF}: given $? \Not A$ open, proceeds either if $?A$ fails or if 
$?A$ succeeds without binding the free variables of $A$, now known
as ESLDNF-resolution. 
\item
1983 \cite{Jaf83} Completeness result for {\em NF} and Horn logic: if 
$\Not A$ follows from $comp(P)$ than $P \cup \{A\}$ fails finitely. 
\item
1984 \cite{Las84} Finite failure semantics for {\em NF}, fair rule 
and connection with greatest fix points of $T_P$.
\end{itemize}

From now on things tend to become rather unwieldy: we then proceed 
analyzing trends in parallel. 

\subsection{Elaboration of the Herbrand Semantics for {\em NF}}

 We  heavily borrow from 
\cite{Har92}, to whom we refer also for references. We start with the 
canonical model approach, where a particular model is constructed and 
identified as the meaning of the program, as $M_P$ for $P$ Horn.

\begin{itemize}
\item
Perfect Models (Przymusinski) : minimal under a preference order 
relation. 
\item
Stable Models (Gelfond). Take interpretation $M$ and $P$ and act as 
follows: for each non Horn clause $C \in P$ and literals $\Not A$ in 
the body of $C$:
\begin{itemize}
\item[i.]
	if $A \in M$, delete  $C$
\item[ii.]
	else delete $\Not A$ in  $C$

\end{itemize}
The resulting program $P^*$ is Horn. If $M_{P^*} = M$, then $M$ is 
stable. So the construction of the model mimics \SLDNF  computations. 
Note that stable models need not exist nor be unique.
\item
Well-Founded Models (van Gelder) 
\item
FixComp Models (Dung): unfold the (instances of the) clauses of $P$ 
until only negative literals appearing it. Take the completion of it 
(which may either be infinite or inconsistent). 

\item
Three(Four)-Valued Models (Kunen/Fitting): probably the more 
reasonable approach (as in \cite{Kun87} \cite {St92a}  and eventually 
in \cite{Stu91}). Every $P$ has a unique Three-Valued minimum Model. 
\end{itemize}

\subsection{Connection to Non-monotonic Logic}

The relationship lies in the way in which semantics for non-monotonic 
logics tend to be in some sense minimal. For instance a model of a 
circumscription of a predicate $q$ is selected in so far it minimizes 
the extension of $q$. Under certain restriction logic programs can be 
shown to be semantically equivalents to well-known non-monotonic 
formalisms as circumscriptions, default theories or autoepistemic 
logic. Again let me refer to \cite{Apt94} for references.

\subsection{Constructive Negation}
\label{cn}
{\em Constructive Negation} is an attempt to devise methods capable 
to provide logically justified answers to non-ground 
negative queries, in analogy with the witnessing property of 
constructive logics \cite{Tro88}. 
Formally, for a suitable 
derivability relation, this property holds when if $ \prv \exists x 
p(x)$ then there is a term $t$ s.t. $\prv  p(t)$ . Accordingly, it is 
suggested that from $ \prv \exists x \Not p(x)$ the same property 
infers a term $t$ s.t. $ \prv \Not p(t)$. We can roughly distinguish 
two approaches
\begin{itemize}
\item[i.]
Program Transformation: \cite{Sat84}, \cite{Foo88}, \cite{Bar90}.  
\item[ii.]
Negation by Constraints: \cite{Wal87} for datalog programs, 
\cite{Cha88} \cite{Cha89} and extended to CLP in \cite{Stu91}; 
Fail Substitutions: \cite{She89} \cite{Mal89}. 
\end{itemize}


Historically, the original attempt to deal with negation was simply
to try avoiding the floundering phenomenon: given that the latter is
in general undecidable, one possibility is to try to make sure that 
when a negative literal is called it has already been grounded: there
 are basically three possibilities:

\begin{enumerate}
\item
 Satisfy the syntactical, though very restrictive, conditions on 
allowed computations \cite{She85}, which essentially reduces 
evaluation to {\em ground} evaluation.
\item
Try to achieve grounding by delaying as in {\em [M]NU-Prolog} or {\em 
Sicstus}, where a goal may be declared to be ``frozen'' and is 
evaluated only 
when it reaches a sufficient degree of instantiation. This is 
obviously only a partial solution, since at run-time there is no 
guarantee to eventually ground the problematic query. A further
improvement is offered by the computation rules of {\em IC-Prolog}
 (see \cite{Nai85}, for a comprehensive analysis and references).
\item
Covering the open negative query with a generator of values for the 
relevant variables.
\end{enumerate}

\subsubsection{Static Approaches}
\label{stat-rel}
If we are dealing with 
datalog programs, i.e.\  with finite Herbrand Universe $U_P$, the 
naive approach would be 
to instantiate  all the rules with potentially 
troublesome goal with terms from $U_P$ \cite{Apt88}, say through 
propagation in every 
negative literal in the program.
This is clearly infeasible, since it may result in an intractable 
numbers of rules, proportional to all the permutation of arguments 
over $U_P$; besides, this may return many undesired 
(untypable) answers.

A sophistication of this idea can be found in \cite{Foo88}: the 
proposal is to automatically infer a `type' for the problematic 
variables and transform the original program into one where 
grounding is ensured by coverage from those types. Then useless 
answers originating from general instantiation would be excluded by 
the typing discipline. The idea is therefore to transform the program 
into a typed one, where a type is a set of facts, say $t(q,j,c)$, 
where 
$q$ is a predicate name of arity $n, j$ ranges over the natural 
numbers and $c$ is in $U_P$. Although it can be shown that the new 
program is equivalent to the 
old one, this cannot be extended to full Prolog: function symbols 
make the type infinite  and non-ground facts would undermine the 
instantiation capability of 
the type. What is required is a generator for infinite $U_P$, instead 
of a table of facts. 


The transformational approach has a fairly long history -- see 
\cite{Nai85},for a survey of the early 80's. The idea is to implement 
negation using inequalities, so that  the negation of any predicate 
occurring negatively in the original 
program $P$ is synthesized so as to obtain an equivalent definite 
program $P^c$ (in the sense of $F_P=M_{P^c}$).  This was first 
proposed in \cite{Sat84}. In this seminal paper it is shown how to 
massage
the completion so that the derived program mimics failed computation 
of the original one. The technique consists essentially
in taking the contrapositive of the completion, putting the RHS in 
dnf and eliminating the universal quantified inequalities by 
introducing a `nonunifiable' predicate. From the simplification
of those constraints and by regarding the negated predicate as
a new name and through the many-sorted discipline the new definition 
is obtained. 

 Two interrelated problems are involved in this simple transformation:
\begin{enumerate}
\item
We need an explicit way to solve the aforementioned inequalities: 
this was first suggested in \cite{Las87} in the general 
context of explicit representation of generalization and refined
in \cite{Las91}; there it is shown that the {\em uncover} algorithm 
may
simplify those constraints into canonical forms but also that
this elimination is not achievable in general.  Another version, 
specifically calibrated to
the negation issue in its being {\em incremental} is given in
 \cite{Har91a}.
\item
The presence of local variables, i.e.\ variables that appear in the 
body but not in the head is problematic, as they turnout to be 
universally quantified. 
\end{enumerate}

There have been several partial solution to the above problem:
\cite{Sat84}  proposes to use a more general fold/unfold
transformation system.
In \cite{Bar90} instead it is proposed to compute the set-theoretic 
complement of the terms in the negative predicate compiling away the 
inequalities. 

In the light of the analysis in \cite{Las91}, it is worthwhile to 
compare the two approaches:

1. Sato/Tamaki:
\begin{itemize}
\item
locally stratified many-sorted programs
\item
no local variables
\item
may be non-left linear
\item
no explicit mechanism to handle inequalities
\item
sketch of proof of  $F_P=M_{P^c}$
\end{itemize}

2. Barbuti and co.
\begin{itemize}
\item
left-linear non-stratified programs with no shared local variable in 
the body, thus
reducing the complexity of extensional universal quantification
(see below).
\item
local variables yield non-Horn programs with extensional universal 
quantification
\item
left linearization reintroduces inequalities motivating the
move to CLP in \cite{Lev92}
\item
operational interpretation of $\forall$
\end{itemize}

Hence the following, where $SS_P$ is the success set of $P$:

\begin{Theorem}
Let $\beta$ and $\sigma$ respectively Barbuti's and Sato's 
transformations, and $P$ be left-linear: then $SS_{\beta(P)}
=SS_{\sigma(P)}$
\end{Theorem}


The main idea (actually a lemma) is as follows: by Theorem 5 in 
\cite{Las91} the substitution
formulae in $\sigma(P)$ have a finite representation that
can be computed by {\em uncover}; analogously the latter computes
the complement of terms in  $\beta(P)$ with the same result.


This should carry over to the general case: left-linearization in 
$\sigma(P)$ produces 
inequalities which by the same theorem are not eliminable
and are equivalent to the canonical forms of those coming
from $\beta(P)$.


\subsubsection{Dynamic Approaches}

Chan \cite{Cha88} is acknowledged to be the inventor of the term 
'constructive' negation; his approach can be roughly characterized as 
a mix of {\em NF} 
with a constraints-solving attitude. In essence it consists in taking 
a negative goal, calling the positive version and negating the answer 
obtained. As in the $CLP$ family of languages, unification and 
disunification are 
kept explicit and returned as solutions. The key observation is that 
if $G$ is a goal and $A_1,..., A_n$ the answer substitutions (treated 
as atoms), $G 
\Bimp A_1 \Or \dots \Or A_n$ is a logical consequence of the 
completed database. Therefore the constructive negation rule is 
simply 
$\Not G \Bimp \Not (A_1 \Or \dots \Or A_n)$, i. e. the answer to 
$\Not G$ is 
the negation of answers to $G$. Of course, there is some work to do in
 keeping the (in)equalities tidy (normalized answers) and there are 
some obvious problems when dealing with computations that have 
infinite answers, fixed in \cite{Cha89}, by quantifying over the 
answer
substitutions. No proof of completeness is offered.
A generalization to constraint logic programming over 
arbitrary structures is offered in \cite{Stu91}; it turns
out to be sound and complete w.r.t. the three-valued models
of the completion.

\medskip
$(E)SLDNF-S$ (\cite{She89}) The finite failure case 
in the definition of $SLDNF$-resolution is modified as 
follows: given the goal $?(\Gamma, \Not A)$, then it has a child
$?\q\Gamma$, if there is a finitely failed-tree for $?\q A$, 
where $dom( \q ) \in vars(A)$. So {\em NF} instantiates 
under success, i.e.\  negative goals directly return substitutions: 
given $P$ and $G$ the aim is to look for a (fail) substitution  $\q$
  s. t.\  $P 
\cup \{\q G \}$ has a finitely failed tree; then by the soundness of 
the {\em NF} rule $\forall \q \Not G$ is a consequence of $comp(P)$ 
and thus  $\q$  is an 
a.s. for the query  $?\Not G$. This seems very costly, since it 
entails enumerating (guessing) every fail substitution. 

This is refined in \cite{Mal89}, where it is shown how to avoid to 
generate all possible substitutions in lieu of a maximal general fail 
substitution. Moreover, the improvement w.r.t.\  Chan's work lies in 
the feature of always including some positive bindings for the 
variable in the negated goal. If the $SLD$-tree is infinite, the 
method, similarly  to what dappwna eo - as
{\ enumerates the set of fail substitutions; this corresponds to 
the fact that in general negative queries cannot be represented by 
finite positive information alone (connected to \cite{Las88}). Note
anyway that $(E)SLDNF-S$ turns out to be complete for a three-valued 
possible world semantics of $comp(P)$.

\subsection{Non-Failure Driven Negation} 
\label{nfs-neg}

During the years ways of incorporating other more logical forms of 
negation than NF have appeared. Since most of the time this gives 
back full non clausal-logic, most of them are catalogued as ATP's. In 
all these accounts, 
negative information has to be provided explicitly and specific rules 
are offered to deal with that. Sometimes it is possible to mix OWA 
and CWA predicates safely. For a more detailed account and 
bibliography, let us refer to \cite{Mom92}.
\begin{itemize}
\item
{\em N(Q)Prolog} \cite{Gab84} and {\em Negation as Inconsistency} 
(\cite{Gab84}): the former is a complete implementation of positive 
intuitionistic logic. 
By defining 
disjunction classically and allowing a restart rule, Gabbay shows it 
to be complete for full classical logic as well. The latter evaluates 
a query against an ordered pair $ \la P,N \ra $, where $P$ is a Horn 
program and $N$ a set of queries that are required {\em not} to 
succeed; this is logically equivalent to adding to the program the 
negation of all the members of $N$, and permits importing negative 
facts and rules. Both systems have a very 
awkward first-order version.

\item
Stickel's $PTTP$, supplementing \SLD-resolution with the model 
elimination rule. This 
entails 
keeping track of the ancestors of the goal, loosing one of the key 
feature of 
Prolog, namely input resolution. Moreover, due to the directionality 
of $SLD$-resolution it 
requires the 
inclusion of the contrapositives of the clauses, causing a notable 
increase in 
the size of the theory.

\item
Loveland's $nHProlog$  incorporating case 
analysis in \SLD-resolution demands each time the invocation of a 
restart rule, until the stack of unsolved (disjunctive) heads is 
empty. Without requiring contrapositives it simulates case analysis 
with different runs of essentially the Prolog engine. 
Unfortunately naive nH-Prolog is incomplete and 
the new 
versions (Progressive nH and Inheritance nH) have  a less natural 
and convincing description. 

\item
Plaisted \cite{Pla88} instead is concerned with a 
difficult attempt to use sequent-based logic programming with a 
version of the cut rule which operates backwards leading 
to a problematic guessing of its premises. For a comparison, see 
\cite{Ree92}.

\item
Another close relative goes under the name of {\em disjunctive logic 
programming} (see \cite{Min91} and references therein). It aims to 
deal with full clausal logic by extending the machinery for Horn 
Logic. In particular the procedural semantic, called 
$SLO$-resolution, extends the $SLD$-step by having the selection 
function 
choose a clause in the current goal (a sequence of clauses) and 
trying to find a clause whose 
head subsumes it; if successful, the goal is incremented by the body, 
without deleting the selected clause. 
\end{itemize}

\subsection{Proof-Theoretic Approaches to Negation and {\em NF}}
\label{pt-rel}

Lately we have participated in an attempt to tie LP to proof-theory, 
where it belongs: and this has brought new insights, particularly 
on {\em NF}.

The first step is to view Horn clauses positively as rules and goals 
as 
existentially closed conjunctions of atoms to be proved by the 
former. 
Historically this can probably be dated back to Gabbay  
and  Reyle  \cite{Gab84}.  We can distinguish 
among two approaches: 
\begin{itemize}
\item[1.]
Clauses as axioms (programs as theories) and some form of Gentzen 
sequent calculus to infer goals, as it is very clearly expressed in a 
series of 
papers by Miller et al.  \cite{Mil91b}. 
This approach is also motivated by 
the enlarged language in consideration (hhf), 
where 
every connective and quantifier is allowed by the syntax, though not 
arbitrarily. 

\item [2.]
 Clauses as rules  \cite{Hal90}:  Horn (and beyond) programs should 
be seen as set of inference rules for the  derivation of (not 
necessarily 
ground) atoms. This view is coherent with the idea of programs 
defining a 
continuos mapping on the lattice of Herbrand interpretations: then 
logic programs can be seen as inductive definitions of such 
interpretations. A 
formal system $C(P)$  is associated to a program $P$ consisting of 
rules. They define a specialized calculus, called  
{\em linear derivation}, which proves pairs of the form  $\la 
G,\theta \ra$,   
and demonstrate it to be sound and complete w.r.t.\  $C(P)$. A linear 
derivation is 
essentially a $SLD$-derivation upside-down, in a structure-sharing, 
forward 
chaining style, i.e.\  where substitutions are split from goals.  
Moreover, Elf itself \cite{Pfe91a} can be seen under this perspective.
\end{itemize}
\\

This has the following relation with negation:
\begin{itemize}
\item[1.]
Minimal, intuitionistic and classical negation can
be superimposed over Uniform Proofs
\cite{Mil89}, \cite{Har91a}, \cite{Mom92}: 
Minimal negation, being camouflaged implication, is executed 
through the 
$AUGMENT/backchain$  operation ; the evaluation of  $ 
\Not   D$ consists in 
the assumption of $D$ and in the attempt to prove $\perp$ from 
the enlarged theory. The Duns Scoto Law and Reductio ad Absurdum for 
atoms formalize the latter, preserving the feature of abstract 
logic programming languages \cite{Mil91b}.
\item[2.]
GCLA \cite{Aro91}  is based on the rule-based definitional
approach to LP: it has intuitionistic negation
built-in, originating when the {\em definiens} operator $D$ returns
an empty set of atoms.
The calculus $D(P)$ \cite{Hal91b} is obtained by adding a 
definitional rule to $C(P)$ 
(see 
\cite{Aro91} for a richer set of rules and the programming language 
$GCLA$ 
based on them). Note that although $G$ is derived in $D(P)$ using 
$(P\prv)$, the former 
may not be 
a logical consequence of the program, nor of any standard extension 
known 
in the literature like $comp(P)$ or $CWA(P)$. Indeed the system does 
not 
need a logical language at all and has, as a semantics, the theory of 
{\em 
partial 
inductive definitions} \cite{Hal91a}. The only relationship with {\em 
NF} of which I am aware of  the possibility of showing the 
containment of the $SLDNF$-resolution into $D(P)$, under the proviso 
of {\em A-sufficiency}. Let me refer to \cite{Mom94a} for  more 
details and the proof.
\end{itemize}

\medskip 

W.r.t.\ negation-as-failure St\"{a}rk \cite{St92a} has  given a 
sequent 
calculus $NF(P)$  consisting of

\begin{itemize}

\item
Clark's equality and freeness axioms
\item
Negation rules (see below $\Not \ - R$)
\item
cut rules, where $\Sigma$ is a set of equations and $\Gamma$ of 
literals.

\unitlength1cm
\begin {picture}(14,1.3)
\put(0,0.7){$\Sigma \prv s=t  \;,\;\; \ s=t,\Gamma \prv \Delta$}
\put(0,0.4){\line(1,0){4.4}}
\put(0.9,0){$\Sigma,\Gamma\prv \Delta$}

\put(6,0.7){$ \Sigma \prv A \;,\;\;\;  A,\Gamma \prv $}
\put(6,0.4){\line(1,0){2.7}}
\put(6.8,0){$\Sigma, \Gamma \prv $}
\end {picture}
\\
\item
Program rules from $P$, divided into positive and negative 
introduction.  For example, given the non-stratified program for 
$even$ we have:

\unitlength1cm
\begin {picture}(14,1.3)
\put(0,0.7){$\Sigma \prv t=0 $}
\put(0,0.4){\line(1,0){2}}
\put(0.0,0){$\Sigma \prv even(t)$}

\put(6,0.7){$ \Sigma \prv t=s(X) \;\;\;  \Sigma \prv \Not even(X) $}
\put(6,0.4){\line(1,0){4.9}}
\put(7.1,0){$\Sigma \prv even(t)$}
\end {picture}

\unitlength1cm
\begin {picture}(10,1.3)
\put(0,0.7){$t=0, \Gamma\prv \;\;\; t=s(X), \Not even(X), \Gamma \prv 
$}
\put(0,0.4){\line(1,0){6.5}}
\put(2,0){$even(t),\Gamma\prv $}
\end {picture}
\end{itemize}
\\

Much more is however contained in St\"{a}rk's thesis; to quote a few, 
he shows 
that a sequent is provable in $NF(P)$ iff it is true in all 3-valued 
model of the completion. Furthermore a completeness result is proved 
w.r.t  $SLDNF$-
resolution for program satisfying the cut-property 
\cite{St92b}.

\subsection{NF in Intuitionistic Logic Programming}

Recently there has been some interest in combining {\em NF}
with what is known as intuitionistic logic programming
\cite{Bon90} \cite{Gio92} \cite{Oli92}. Unfortunately,
the underlying languages are either version of N-Prolog or
clausal intuitionistic logic. Due to the inherently difficulty
with universal quantification mentioned in \ref{nfs-neg}, the
treatment is either propositional or deprived of generic goals.
Moreover the emphasis is 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

Harland \cite{Har92}  instead proposes a sequent calculus based 
on intuitionisic logic that directly incorporates {\em NF} without 
referring to the completion. The usual rules, 
restricted to deal with Horn logic, induce a {\em positive} 
derivability 
relation; furthermore, he introduces a 
{\em negative} system of {\em disprovability}, denoted by $\prv^-$ 
with 
judgments of the type:  if a conjunction fails then so does one of 
the 
conjuncts and so forth.  The two systems are interlinked by the rules 
for 
{\em NF}.

\\

\unitlength1cm
\begin {picture}(14,1.3)
\put(0,0.7){$\Gamma \prv^-  F$}
\put(0,0.4){\line(1,0){1.6}}
\put(1.7,0.4){($\Not-R+$)}
\put(0.0,0){$\Gamma \prv \Not F$}

\put(4,0.7){$ \Gamma \prv F$}
\put(4,0.4){\line(1,0){1.7}}
\put(5.8,0.4){($\Not-R-$)}
\put(4.0,0){$\Gamma \prv^- \Not F$}
\end {picture}
\\

Structural rules have a paramount importance in this calculus:
 due to the nonmonotonic nature of {\em NF}, weakening in the 
positive fragment 
is restricted to introduce only already 
provable formulae on the left, resulting in a dual to contraction. 
In the negative system structural rules, cut included, are not 
eliminable.  This is not strictly a calculus of {\em finite} failure, 
since sequents of the form $p\leftarrow p \prv^- p$ are provable, 
although with the essential use of weakening. Of course, due to the 
recursion-theoretic complexity of unprovability, every such an 
axiomatic formulation is bound to be incomplete. Moreover the 
boundary seems fuzzy, as, for example, $p$ is independent from the 
program $p\leftarrow q, q \leftarrow p$. The calculus without 
structural rules is shown \cite{Har91a} to be
sound and complete w.r.t. finite failure and $SLDNF$-resolution
(extended to first-order hereditary Harrop formulae).
Having to model the operational behavior of {\em NF}, both the 
positive and the negative system make explicit references to 
unification, Skolem functions 
and so forth. Still, the system is not meant for proof search
and requires a relative complement algorithm to provide answers to 
open negative queries.

\medskip

Harland's thesis \cite{Har91a} is an in-depth analysis of Uniform 
Proofs and {\em NF} at the first-order level. Distinguishing between 
CWA and OWA predicates, {\em NF} makes sense only for the 
former, since they exclude everything else, while the latter requires 
some form of 
real (say minimal) negation, much as in \cite{Mom93}. The distinction 
is enforced by user declarations.


Eventually, he shows how to formulate the completion as an object 
fohh 
formulae so as to simulate {\em NF} as derivability in the uniform 
proof 
system. This entails giving a completion procedure for fohh clauses; 
note that only CWA predicates are completed. Programs are assumed 
to be locally stratified, hence the completion is consistent. An 
equality/inequality solver on $U_P$ is described. The executable 
completion is formulated through contraposition, much as in my 
thesis \cite{Mom93}, though in a more detailed and convoluted way. A 
completeness result is proven w.r.t.\ failure, which is 
conservative over Horn clauses; the treatment of implicational goals 
is somehow ad hoc.



\subsection{My Previous Work}

It is worthwhile to review very briefly my past work on the subject:
\cite{Mom89} is essentially an expository survey of {\em NF} from the 
usual semantic point of view. In \cite{Mom92} and more
fully developed in \cite{Mom93} negation in the context of fohh
is investigated much (though independently) in the sense of
\cite{Har92}. In \cite{Mom94a} a proof-theoretic
approach to LP based on the notion of {\em axiom-application
rule} and $regularity$ is developed. This is refined and applied to
constructive negation in \cite{Mom94b} through the idea of {\em
regular splitting}, a manipulation of the completion so as to
achieve the same properties of \SLD-resolution.

\subsection{Complement Problems and Elimination of Negation in Term 
Algebrae}
\label{el-rel}

Complement problems and elimination of negation are not restricted to 
LP, but has some
other relevant application in computer science. Actually the more 
general question
of {\em disunification} has become a fast growing field in its own 
which
is impossible to summarize here. 
Extension of disunification in order-sorted signatures is under 
research as well as in the presence of equational theories, 
inequalities ($\leq$) and symbolic constraints. Let me refer
to \cite{Las91} and \cite{Com91} for more details and references. 

More specifically, complement problems and variants of the {\em 
uncover} algorithm have been used in several ways:
\begin{itemize}
\item
 To determine whether the definition of a function by pattern
matching in functional programming is exhaustive and disjunct and
to take into account the assumed sequential application of the rules 
for compilation.
\item
Its
connection with the notion of {\em ground reducibility} in term
rewriting makes it a candidate to check whether an algebraic 
(equational) specification is sufficiently complete. 
\item
In term rewriting systems describing infinite transition systems,
the complement of LHS returns the states from which no transition is
achievable, giving thus a tool for the temporal analysis of 
communicating processes.
\item
Applications
to inductive theorem proving have also been investigated. 
\end {itemize}

\section{Thesis Outline}
\label{out}

The fundamental ingredients are as follows

\begin{itemize}
\item
Sato-Barbuti's synthesis technique for the complement of first-order 
logic programs
\item
Harland's notion of completion for fohh 
\item
Lassez-Lugiez's disunification technique for handling inequalities
stemming from the completion.
\end{itemize}

What's left to do is mix them together and lift it to hhf/LF and 
voila'! More seriously, an ideal approach goes like this: the 
transformational approach is rooted in the notion of completion for 
Horn logic.
Its extension to higher-order Horn logic and LF's Horn fragment has 
not been
investigated so far and may turn out to be an interesting subject
in its own. In particular, we need to understand the higher-order 
version of CET and the DCA and their connection with the induction 
principle and the algebra of higher-order terms. This is not only 
vital to give a semantics to a suitably generalization of the idea of 
proof by cases to the
higher-order case, but it also  seems to recur in other sectors of 
Elf theory (i.e.\ 
open vs.\ closed terms and the (im)possibility of implementing
metaproofs such as strong normalization (cut-elimination) for PA 
which are not formalizable in first-order arithmetic).


Once this has been accomplished, Lugiez's disunification
technique should give us a first approximation to negating 
$L_\lambda$ programs \cite{Mil91a}. To deal with full higher-order 
Horn clauses we still need to
analyze the use of regular term languages to incorporate
non-patterns. Moreover we have to be aware that perhaps the best 
choice to deal with non non-left linear programs is to switch to an 
explicit CLP, which is also consistent with Elf approach to 
unification.

It is entirely possible that already at this level we may have to 
restrict ourselves to certain (hopefully syntactically defined)
classes of programs to achieve first a sensible behavior and 
eventually completeness. Note that the latter is a front-line research
topic \cite{Apt94}, where wider and wider classes of programs are 
explored. Nonetheless, given the emphasis on practicality of this 
thesis, we shall probably have to restrict to narrower, more 
understood fragments that make sense in the higher-order setting.

\\

Next, following Harland's notion of completion for fohh, we
ought to re-introduce intensional quantification and embedded
implication in the picture. As already mentioned, this in turn leads 
to several questions:
\begin{enumerate}
\item
The interaction between intensional and extensional quantification
and the related assumptions on the domain of computation is very
delicate and has not been adequately investigated. Moreover,
its extension to LF's $\Pi$ operator is still shrouded in mystery.
\item
Non-stratified implications may have to be eliminated in a judicious 
way, or at least
brought to some sort of normal form to be dealt with by
the proposed approach.
\end{enumerate}

Eventually (and ideally) we would like to come up with a broad,
neatly defined and useful class of higher-order programs amenable 
to the transformational idea and at the same time shed some light on 
the notion of negation-as-failure in the higher-order setting.

\medskip

Time Plan:

\begin{enumerate}
\item
Higher-order terms (patterns): 4 months
\item
Implicational goals: 4 months
\item
Generic goals: 4 months
\item
Write-up: 3 months
\end{enumerate}

Exploring related topics and/or an implementation could add
6 -- 9  additional months.


\include{thref}

\end{document}


