\documentclass[runningheads,oribibl]{llncs}
\authorrunning{Alberto Momigliano}%alti
\titlerunning{Elimination of Negation in a Logical Framework}%alti
\pagestyle{headings}%alti
\usepackage{amsfonts}
 
\usepackage{amsty}
\title{Elimination of Negation in a Logical Framework}

\author{Alberto Momigliano}

\institute{Department of Philosophy,
           Carnegie Mellon University,
%         5000 Forbes Ave.\\
           Pittsburgh, PA 15213, U.S.A.
%          Tel.\ +1\ 412\ 268-3074\\
%          Fax\ +1\ 412\ 269-1440\\[1ex]
  \email{mobile@cs.cmu.edu}}
\bibliographystyle{abbrv}


\begin{document}
\setcounter{page}{410} %alti
%\pagestyle{empty}

\maketitle


\begin{abstract}
  Logical frameworks with a \lp interpretation such as hereditary
  Harrop formulae (HHF) \cite{Miller91apal} cannot express directly
  negative information, although negation is a useful specification
  tool.  Since negation-as-failure does not fit well in a \lf,
  especially one endowed with hypothetical and parametric judgments,
  we adapt the idea of \emph{elimination} of negation introduced in
  \cite{Sato84} for Horn logic to a fragment of higher-order HHF. This
  entails finding a middle ground between the Closed World Assumption
  usually associated with negation and the Open World Assumption
  typical of \lf s; the main technical idea is to isolate a set of
  programs where static and dynamic clauses do not overlap.
\end{abstract}

% \begin{keyword} Logical frameworks, elimination of negation,
%   hypothetical and parametric judgments, Regular World
%   Assumption.
% \end{keyword}



\section{Introduction}
\label{sec:intro}

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 or type systems. A \emph{logical framework} is a
meta-language for the specification, implementation and verification
 of  deductive systems and possibly their meta-theory. 
A \lf\  must provide tools which make encodings  as simple and
direct  as possible. One well known example is higher-order abstract
syntax, which moves renaming and substitution principles to the
meta-language.
% avoiding to explicitly program and  prove a huge
%series of low-level results about the former. 
% 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. 
Logical frameworks should be by design    as weak  as
possible to simplify proofs of adequacy of encodings,
effective checking of the validity of derivations and proof-search as
well as unification.  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.

This paper discusses the introduction of a logically justified notion
of \emph{negation} in logical frameworks with a \lp interpretation
such as hereditary Harrop formulae (HHF) \cite{Miller91apal} and its
implementation in $\lambda$Prolog \cite{Nadathur88}. We intend this to
form 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 or \emph{LLF}.
%\cite{Cervesato96lics,Hodas94ic}.  
Those systems 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 code 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, 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).
 Automating the synthesis of
negative information has not only an immediate practical relevance 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.

Traditionally,  negation-as-failure  (\emph{NF}) \cite{Cla78} has been the
overwhelmingly used approach in \lp (see \cite{Apt94} for a recent
survey):
%this rule may be seen as a sort of proof by consistency: we
%are allowed to 
that is, infer $\neg A$ if every proof of $A$  fails finitely. The operational
nature of this rule motivates the lack of a unique semantics and some
of its related troublesome features: possible unsoundness,
incompleteness and floundering. Furthermore, even if we manage to isolate a
well-behaved logical fragment, such as acyclic normal programs,
%  for which completeness \wrt to the most widely held
% semantics holds, we must remark that a logical framework, even one
% which can be given an operational interpretation, radically differs
% from a \lp language. 
allowing \NF in a \lf\ would make adequacy theorems more difficult to
prove, as both provability and unprovability must now be
considered. The situation is even further complicated when we step to
frameworks with hypothetical judgments; as recognized first by Gabbay
\cite{Gabbay85}, the unrestricted combination of \NF and embedded implication 
is particularly problematic, since it leads to the failure of basic
logic principles such as cut-elimination.

The approach to negation that we adopt is
\emph{transformational}, also known as \emph{intensional negation},
initiated in \cite{Sato84} and developed in Pisa \cite{Bar90} for Horn
logic with negation.
% and later extended to constraint \lp \cite{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.  A final issue, which we do not tackle here, is dealing
with \emph{local} variables, which, during the transformation, become
(extensionally) universally quantified \cite{Brogi90}.

Unfortunately, this approach does not scale immediately to \lf s such as HHF,
for three main reasons:
\begin{enumerate}
\item The simply-typed $\l$-calculus is not closed under term
  complement.
\item Negation normal forms are incompatible with the operational
  semantics required by HHF.
\item There is an intrinsic tension between the \emph{Closed World
    Assumption} (CWA), which is associated with negation,
  and the \emph{Open World Assumption} (OWA) typical of languages with
  embedded implication.
\end{enumerate}

The first problem has been solved in \cite{Momigliano99}, by
introducing a \emph{strict} $\l$-calculus where term complement in the
simply typed $\l$-calculus can be embedded and performed. The second issue
is orthogonal and requires an operational notion of normal form.  The
third one is rooted 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.
% This problem has been first recognized by
% Gabbay \cite{Gabbay85}, who pointed out that \NF coupled to embedded
% implication seems to lead to curious paradoxes, as non-eliminability
% of the cut rule or failure of weakening.
 In the literature 
 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{McDowell97lics}.
%  \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.

It is clear that elimination of negation makes sense only when negation
is \emph{stratified}, \ie the negative predicates
ultimately refers (in the call graph) to a positive one. While there
may be a place in \lp for non-stratified negation,
% see the\emph{answer set programming} paradigm \cite{Marek99},
this does not seem to be the case for a \lf. Another difference from
traditional \lp is that negation applies only to \emph{terminating}
programs; thus it  refers not to finite failure but to
unprovability tout court, as we refrain from negating programs whose
negation is not recursively axiomatizable. We will thus identify
negation with a \emph{complement} operation.

The rest of the paper is organized as follow: in Sect.~\ref{sec:ex}
we give an informal view of the complement algorithm by means of
examples, while Sect.~\ref{sec:termin} introduces the language.
Section~\ref{sec:cc} describe term and clause complementation.  We
conclude in Sect.~\ref{sec:end} with some remarks on future work. We
refer to \cite{Momigliano00phd} for more details and proofs omitted
here for reasons of space.

\section{A Motivating Example}
\label{sec:ex}

Consider the expressions of the untyped $\l$-calculus:
\beq
e & \bnfas & x \bnfalt \Lambda x \, .\,  e \bnfalt e_1\, e_2
\eneq We encode these expressions as terms in (labeled) HHF via the usual techniques of higher-order abstract
syntax  as canonical forms over the following signature:
\beq
\Sigma  & = & exp\hastype \mbox{\textrm{type}}, lam\hastype (exp\Imp 
exp)\Imp exp, app \hastype exp \Imp (exp\Imp exp)
\eneq
The representation function is given by:
\[
\rep{x} = x\qquad
\rep{\Lambda x\,.\, e} = lam\ (\lamb{x}{exp} \rep{e})\qquad
\rep{e_1\ e_2} =app\ \rep{e_1}\ \rep{e_2}
\]
A term is \emph{linear} if every functional subterm uses
each  argument  exactly once: in particular, we check for linearity of a
function making sure that the latter is linear in its first argument
and then recurring on the rest of the expression.
%\[\begin{array}{lcr}
%\begin{small}
\beq
linapp & : & linear(app\ E_1\ E_2) \If linear(E_1)\And linear(E_2).\\
linlam& : & linear(lam( \lx E\ x))\\
& & \qquad \If linx( \lx E\ x)\And  (\PI{y}{exp}
linear(y)\Imp linear(E\ y)). 
\vsk
linxx& : & linx(\lx x).\\
linxap1& : & linx(\lx app\ (E_1\ x) \ E_2) \If  linx(\lx E_1\ x).\\
linxap2& : & linx(\lx app\ E_1\ (E_2\ x)) \If  linx(\lx E_2\ x).\\
linxlm& : &linx(\lx lam(\ly E\ x\ y)) \If (\PI{y}{exp} linx (\lx E\ x\ y)).
\eneq
%\end{small}
% \beq
% linapp & : & linear(app\ E_1\ E_2)\\
% & & \qquad \If linear(E_1)\And linear(E_2).\\
% %& & \qquad \If linear(E_2).\\
% linlam& : & linear(lam\ \lx E\ x)\\
% & & \qquad \If linx( \lx E\ x)\And  (\PI{x}{exp}
% linear(x)\Imp linear(E\ x)). 
% %& & \qquad \If (\PI{x}{exp} linear(x)\Imp linear(E\ x)).
% \vsk
% linxx& : & linx(\lx x).\\
% linxap1& : & linx(\lx app\ (E_1\ x) \ E_2)\\
% & & \qquad \If  linx(\lx E_1\ x).\\
% linxap2& : & linx(\lx app\ E_1\ (E_2\ x))\\
% & & \qquad \If  linx(\lx E_2\ x).\\
% linxlm& : &linx(\lx lam(\ly E\ x\ y))\\
% & & \qquad \If (\PI{y}{exp} linx (\lx E\ x\ y)).
% \eneq
% \end{small}
%\end{array}\]
This is clearly a decision procedure, which can be complemented; an
expression is {\em not\/} linear if there is some function which
either does not use its argument or uses it more than once.
%We first observe that, since $linear$ is a total relation, term
%complementation does not play a role. Secondly, 
First, the complement of {\tt linapp} does not pose any problem, as it is a
Horn clause: an application is not linear if either the first element
or the second is not linear.
% \beq
% \neg linapp & : & \neg linear(app\ E_1\ E_2)\\
% & & \qquad \If  \neg linear(E_1)\Or\\
% & & \qquad \If  \neg linear(E_2).
% \eneq
Next, a lambda expression is not linear in two cases: one, if it is
not linear in its first argument:
\beq
\neg linlam1& : & \neg linear(lam\ \lx E\ x)\If  \neg linx( \lx E\ x).
\eneq
Secondly, if its body is not linear. Now, this poses a new problem, as
we have to negate a hypothetical and parametric goal. Let us reason
by example and suppose we are given, in the empty context, a goal
$linear(lam(\lx lam(\ly x)))$, which is unprovable, since the second
lambda term is not linear in $y$; the proof tree yields the failure
leaf $linx(\lx z)$, for a new parameter $z$, in the context $z\oftp
exp;linear(z)$. Our guiding intuition is that we want to mimic a
failure derivation so as to provide a successful derivation from the
negative definition, \ie a proof of $\neg linx(\lx z)$ from $z\oftp
exp;linear(z)$; this shows one prominent feature of complementation of
an \mbox{HHF} formula: negation `skips' over $\Pi$ and $\Imp$, since
it needs to mirror failure {\em from\/} assumptions.
% Let
% us turn to complementing \texttt{linx}.
% A first point to note in that in clause {\tt linxap1} $x$
% {\em does\/} not occur in the argument which is not checked;
% symmetrically for \texttt{linxap2}.
% We use the  annotation $()^0$, whose semantics is established in
% \cite{Momigliano99}:
% \beq
% linxap1& : & linx(\lx app\ (E_1\ x) \ (E_2\ x^0))\\
% & & \qquad \If  linx(\lx E_1\ x).\\
% linxap2& : & linx(\lx app\ (E_1\ x^0) \ (E_2\ x))\\
% & & \qquad \If  linx(\lx E_2\ x).
% \eneq
% The negation of the head of the clause is computed by  complementing its argument;
% we thus obtain, among others:
% \beq
% \neg linxap1& :& \neg linx(\lx app\ (E_1\ x) \ (E_2\ x^1)).
% \eneq
% Moreover, as in the case of top-level application, the complement of
% {\tt linxap1,linxap2} hold if the body does not hold.
% % \beq
% % \neg linxap1& : & \neg linx(\lx app\ (E_1\ x) \ (E_2\ x^0))\\
% % & & \qquad \If  \neg linx(\lx E_1\ x)\\
% % \eneq
 Now, let us examine clause {\tt
linxlm} and reconsider the above failure leaf; in a first attempt,
according to the idea above, the complement would be:
\beq
\stackrel{?}{\neg} linxlm& : &\neg linx(\lx lam(\ly E\ x\ y))\If 
(\PI{y}{exp} \neg linx (\lx E\ x\ y)).
\eneq
However, there is no way to obtain a proof of $\neg linx(\lx z)$ from
the current context. Indeed, the {\tt linxlm} clause does not carry
enough information so that its complement can mimic the failure proof.
In a sense, the clause is not {\em assumption-complete\/}: once it has
introduced a new parameter, the clause only specifies how to use it in
a positive context. It is up to us to synthesize its dynamic negative
definition, in this case simply $\PI{y}{exp}\neg linx(\lx y)$.  More in general,
it is a characteristic of HHF that the negation of a clause is not strong
enough to determine the behavior of a program under complementation.
We will have to insert  (via a source-to-source transformation)
additional structure in a predicate definition, in order to completely
determine the provability or failure of goals which mention
\emph{parameters}. By observing the structure of all possible
assumption that a predicate definition can make, we will {\em
  augment\/} those assumptions with their negative definition. In
particular, we first augment the clause \texttt{linxlm}: 
\beq
\ald(linxlm)& : &linx(\lx lam(\ly E\ x\ y))\\
& & \qquad\If (\PI{y}{exp} \neg linx(\lx y)\Imp linx (\lx E\ x\ y)).
\eneq so that, by complementation, we obtain: \beq
\neg \ald(linxlm)& : &\neg linx(\lx lam(\ly E\ x\ y))\\
& & \qquad\If (\PI{y}{exp} \neg linx(\lx y)\Imp \neg linx (\lx E\ x\ 
y)).  
\eneq 
Unfortunately, the procedure we have outlined is not
possible in general.  Consider a clause encoding the introduction rule
for implication in natural deduction, which can be used to check
whether an implicational formula trivially holds:
%\begin{example}
\beq
\label{ex:nd}
\Sigma & = & form\hastype type, imp\hastype form\Imp (form\Imp form), a\hastype
form,b\hastype form,c\hastype form\\
impi & : & nd(A\ imp\ B)\If (nd(A) \Imp nd(B)).
\eneq
Following our earlier remark its complement would be:
%\begin{small}
\beq
\neg impi1& : & \neg nd(a).\\
\neg impi2& : & \neg nd(b).\\
\neg impi3& : & \neg nd(c).\\
\stackrel{?}{\neg} impi& : &\neg nd(A\ imp\  B)\If (nd(A) \Imp \neg nd(B)).
\eneq
%\end{small}
%\end{example}
This specification is clearly incorrect since both $nd (a\ imp\ 
  a)$ \textbf{and} $\neg nd(a\ imp\ a)$ are derivable from the
empty context. We can isolate one major problem: in clause {\tt impi}
the assumption $nd(A)$ which is dynamically added to the (static)
definition of the {\tt nd} predicate {\em overlaps\/} with the head of
the clause. A symmetrical problem can occur when dynamic and static
clause do differ but their complements do not.
% Suppose we 
% want to have a predicate which check is a number is even and non zero:
% \beq
% e & : & ev(s(s(N))\If ev(0)\Imp ev(N)
% \eneq
% Again, our naive algorithm would incorrectly yield:
% \beq
% \neg e1 & : & \neg ev(0)\\
% \stackrel{?}{\neg} e2& : &\neg ev(s(N))\\
% \neg e & : & \neg ev(s(s(N))\If ev(0)\Imp \neg ev(N)
% \eneq
% And incorrectly both $ev (s(s(O)))$ and $\neg ev (s(s(O)))$ are
% provable. The problem here is the overlapping between the
% of assumption $ev(0)$ and the {\em complement\/} of the head of the
% {\tt e} clause.
% \smallskip
We have thus isolated two main issues:
\ben
\item Exhaustivity: we need to enrich clauses so that
every (ground) goal or its negation is provable.
\item Exclusivity:  we need to isolate a significant fragment where
it is not the case that both a goal and its negation are provable.
\enen
We will achieve exhaustivity (Theorem \ref{thm:exh}) by {\em
  augmenting} the program with  the complement of
assumptions; moreover, we will achieve exclusivity (Theorem
\ref{thm:exclu}) with the restriction to {\em complementable\/}
programs. To anticipate the idea, a clause is complementable if every
assumption  contains  some eigenvariable at execution time.

\section{Provability and Unprovability}
\label{sec:termin}

We will use the following somewhat unusual language:

\[ \begin{array}{rrcl}
 \mbox{\textit{Simple Types}} & A & \bnfas & a \bnfalt A_1 \Imp A_2 \\
 \mbox{\textit{Terms}} & M & \bnfas & c \bnfalt x \bnfalt \lam x\oftp
A\ldot M \bnfalt M_1\ M_2 \\
\mbox{\textit{Atoms}}& Q & \bnfas & q\ \vM \bnfalt \neg q\ \vM \\
\mbox{\textit{Clauses}}& D & \bnfas & \top\bnfalt\perp\bnfalt Q \If
G\bnfalt D_{1}\And D_{2}\bnfalt D_{1}\tensor D_{2}\bnfalt\PIXA D\\
\mbox{\textit{Goals}}& G & \bnfas & Q \bnfalt \top\bnfalt \perp\bnfalt
\vM \eqd \vN\bnfalt \vM \neqd \vN\bnfalt\\
& & & G_{1}\And G_{2}\bnfalt
G_{1}\Or G_{2}\bnfalt D\Imp G\bnfalt\PIXA G\\
 \mbox{\textit{Signatures}} & \Sigma & \bnfas & \cdot \bnfalt \Sigma, a
\oftp \mbox{type} \bnfalt \Sigma, c\oftp A \\
\mbox{\textit{Parameter Contexts}}& \GG & \bnfas &\cdot\bnfalt\GG,
 \xoa\\
\mbox{\textit{Assumptions}}& \cD & \bnfas &\top\bnfalt\cD\And D
\end{array}
\]
There is a distinguished type $\prop$ for propositions which can occur
only as the target of some $A$. We remark that `$\neg$' is \emph{not} a
connective, but a name constructor for atomic formulae; `facts' are
represented, for convenience, by $ Q\If \top$, although in examples we
will omit to mention $\top$.
% We use $\vM,\vN$ for sequences of terms of fixed length $n$. 
We assume that existential variables occur only
once in the head of program clauses (\ie clauses are
\emph{left-linear}); this can always be achieved by introducing
disequations in the body.
% By $\df(q,\cP)$ we denote the conjunction of
%clauses in $\cP$ whose head is $q$.  
In this paper we restrict ourselves to  programs such that all
assumptions are Horn and which can be proven to be terminating under some
well-founded ordering.
%, specifically to programs which make only Horn assumptions.
We introduce the uniform proofs system \cite{Miller91apal} for
(immediate) provability and denial in Fig.~\ref{fig:sf}.  For
terminating programs, we can prove that the failure to achieve a proof
of $G$ translates into (a derivation of) the denial of $G$.  Note also
that due to the presence of disjunction as a clause constructor,
uniform proofs are \emph{not} complete for our language. We will
remedy this situation in Sect.~\ref{sec:cc}.
\[
\begin{array}{ll}
\ga\sp G & \mbox{Program $\cP$ and assumption $\cD$ uniformly entail
  $G$.}\\
\ga\fp G & \mbox{Program $\cP$  and assumption $\cD$ uniformly deny $G$.}\\
\ga\sp D \imm Q & \mbox{Clause  $D$ from $\cP$ and $\cD$ immediately entails atom $Q$.}\\
\ga\fp D \imm Q & \mbox{Clause  $D$ from $\cP$ and $\cD$ immediately denies atom $Q$.}
\end{array}
\]

\begin{figure}
%\begin{small}
\[
\begin{array}{c}
% |-
 \ianc{}{\ga\sp\top}{\vd\top}\qquad\ianc{}{\gna\fp \perp}{{\nprv}_\perp}\vsk
%\ianc{\vM = \vN}{\ga\sp \vM \eqd \vN}{{\prv\eqd}}\qquad
%\ianc{\vM \not = \vN}{\ga\fp \vM \eqd \vN}{{\nprv\eqd}}\vsk
%\ianc{\vM \not = \vN}{\ga\sp \vM \neqd \vN}{{\prv\neqd}}\qquad
%\ianc{\vM  = \vN}{\ga\fp \vM \neqd \vN}{{\nprv\neqd}}\vsk
\ibnc{\ga\sp G_1}{\ga\sp G_{2}}{\ga\sp G_{1}\And G_{2}}{{\prv}\And}
\qquad
\ibnc{\ga\fp G_1}{\ga\fp G_{2}}{\ga\fp G_{1}\Or G_{2}}{{\nprv}\Or}
\vsk
\ianc{\ga\sp G_i}{\ga\sp G_{1}\Or G_{2}}{{\prv\Or_i}}
\qquad
\ianc{\ga\fp G_i}{\ga\fp G_{1}\And G_{2}}{{\nprv\And_i}}
\vsk
%\ianc{\ga\sp G_2}{\ga\sp G_{1}\Or G_{2}}{{\prv\Or_2}}
%\qquad
%\ianc{\ga\fp G_2}{\ga\fp G_{1}\And G_{2}}{{\nprv\And_2}}
%\qquad
\ianc{\ga\sp[t/x]G}{\ga\sp\exa G}{\vd\exists}
\qquad
\ianc{\mbox{\rm for all $n$ }\gna\fp[n/x] G}{\gna\fp\exa G}{\nvd\exists}
\vsk
% HORN --> HHF
 \ianc{\GG;(\cD\And D) \sp G}{\ga\sp D \Imp G}{{\prv} \Imp}
\qquad
\ianc{\GG;(\cD\And D )\fp G}{\ga\fp D \Imp G}{{\nprv} \Imp}
\vsk
\ianc{(\GG,y\oftp A);\cD\sp[y/x]G}{\ga\sp \PIXA G}{{\prv} \Pi^y}
\qquad
\ianc{(\GG,y\oftp A);\cD\fp[y/x]G}{\ga\fp \PIXA G}{{\nprv} \Pi^y}\vsk
\ianc{\ga\sp (\cP\And\cD) \imm Q}{\ga\sp Q}{\vd\atm}
\qquad
\ianc{\gna\fp (\cP\And\cD) \nimm Q}{\ga\fp Q}{\nprv\atm}
\vsk
\ianc{}{\ga\sp\perp\imm  Q}{\imm\perp}\qquad
\ianc{}{\ga\fp \top\nimm Q}{\notimm \top}\vsk
\ianc{ \ga\sp  [t/x]D \imm  Q}{\ga\sp \PIXA D \imm Q}{\imm\Pi}\qquad
\ianc{\mbox{for all $n$ }\ga\fp [n/x]D \nimm
  Q}{\ga\fp \PIXA D \nimm Q}{\notimm\Pi}\vsk
\ianc{\ga\sp D_{i}\imm Q}{\ga\sp D_{1}\And D_{2}\imm Q}{\imm{\And_i}}\qquad
\ianc{\ga\fp D_{i}\nimm Q}{\ga\fp D_{1}\tensor D_{2}\nimm
  Q}{\notimm{\tensor_i}}\vsk
\ibnc{\ga\sp D_{1}\imm Q}{ \ga\sp D_{2}\imm Q}{\ga\sp D_{1}\tensor D_{2}\imm 
Q}{\imm\tensor}\vsk
\ibnc{\ga\fp D_{1}\nimm Q}{\ga\fp D_{2}\nimm Q}{\ga\fp D_{1}\And D_{2}\nimm
Q}{\notimm\And}\vsk
\ibnc{\vN=\vM}{\ga\sp G}{ \ga\sp ( q\  \vN\If G) \imm q\
  \vM}{\imm\Imp}
\vsk
\ianc{ \vN\not=\vM}{\ga\fp (q\ \vN\If G) \nimm q\
  \vM}{\not\imm{\Imp_1}}
\qquad
\ibnc{ \vN=\vM}{\ga\fp G} {\ga\fp (q\ \vN\If G) \nimm q\ \vM}{\not\imm{\Imp_2}}


% \ibnc{\ga\sp D\imm Q}{\ga\sp  G}{\ga\sp  D\If G \nimm 
%   Q}{\imm\Imp}\vsk
% \ianc{\ga\fp D\imm Q}{\ga\fp  D\If G \nimm 
%   Q}{\notimm{\Imp_1}}\qquad
% \ianc{\ga\fp G}{\ga\fp  D\If G \nimm 
%   Q}{\notimm{\Imp_2}}
\end{array}
\]
%\end{small}
\caption{(Immediate) Provability and Denial}
\label{fig:sf}
\end{figure}

Some brief comments are in order: the (in)equalities rules simply
mirror the object logic symbols $\eqd,\neqd$ as meta-level
(in)equalities and are omitted. $\notimm\Pi$ and $\nvd\exists$ are
infinitary rules, given the meta-linguistic extensional universal
quantification on all terms.  Rules $\vd\Pi,\nvd\Pi$ are instead
parametric in $y$, where the $()^y$ superscript reminds us of the
eigenvariable condition.  The denial rules for implication and
universal quantification reflect the operational semantics of
unprovability that we have discussed earlier.

% , For the sake of conciseness we will often use in this thesis
% the following rule schema, where $\cJ(X,R)$ is a judgment involving a
% token $X$ ranging over a set $\cT$ and a relation $R$:
% $$\ianc{X\in \cT}{\cJ(X,R)}{R\ X}$$

We start by putting every program in a \emph{normalized} format \wrt
assumptions, so that every goal in the scope of an universal quantifier
is guaranteed to depend on some assumption, possibly the trivial clause $\top$. This
has also the effect of `localizing' the trivial assumption to its
atom, a property will be central while complementing assumptions; for
example we re-write \texttt{linxlm} as follows:
\beq
linxlm&:&   linx\ (\lx lam(\ly  E\ x\ y))  \\
& & \qquad \If (\PI{x}{exp} \top_{linx}\Imp linx\ (\lx E\ x\ z)).
\eneq 
For the sake of this paper, we also need to modify the source program
so that every  term in a clause head is \emph{fully applied}, \ie it
is a lambda term where 
every variable mentioned in the binder occurs in the matrix; 
this makes term complementation (Sect.~\ref{sec:cc}) much
simpler. For example clause \texttt{linxap1} is rewritten as:
\beq
linxap1& : & linx(\lx app\ (E_1\ x) \ (E_2\ x)) \If  linx(\lx E_1\
x)\And vac(\lx E_2\ x).
\eneq
where $vac(\lx E_2\ x)$ enforces that $x$ does not occur in $E_2\ x$.  Its
definition is type-directed, but we
have shown in \cite{Momigliano99} how to internalize these occurrence
constraints in a strict type theory, so that this further
transformation is not needed.

\smallskip
We  now discuss context schemata.
%\footnote{This
 % section is inspired by Sch\"{u}rmann's treatment of similar material in
 % his forthcoming dissertation \cite{}.}. 
% Hereditary Harrop formulae differ form Horn clauses in that they may
% dynamically extend the current signature and program; this is
% reflected in the provability (and denial) relation which is
% parameterized by a run-time context $\ga$.
As we have argued  in Sect.~\ref{sec:ex}, we cannot obtain
closure under clause complementation for the full logic of HHF, but we
have to restrict ourselves to a smaller (but significant)
fragment. This in turn 
entails that we have to make sure that during execution, whenever an
assumption is made, it remains in the fragment we have isolated.
Technically, we proceed as follows:
\begin{itemize}
\item We extract from the static definition of a predicate the general
  `template' of a legal assumption.
\item We require dynamic assumptions to conform to this template.
\end{itemize}
We thus introduce the notion of \emph{schema satisfaction}, which uses
the following data structure: a \emph{context schema} abstracts over
all possible instantiations of a context during execution. To account
for that, we introduce a quantifier-like operator, say $\some{\Phi}
\cD$, which takes a clause and existentially bounds its free
variables, if any, \ie $\Phi=FV(\cD)$. The double bar `$\bar$', not to
be confused with the BNF `$\mid$' that we informally use in the
meta-language, denotes schema alternatives, while `$\ecs$' stands for
the empty context schema.
% This is
% achieved by the following reification of schemata. Do not confuse
% `$\bar$', which is used to represent schema alternatives in the object
% language with `$\bnfalt$' which does the same in our informal
% meta-language.
\[ \begin{array}{rrcl}
\mbox{\textit{ Contexts Schemata}}& \cS & \bnfas &
\ecs\bnfalt\cS\bar(\GG;\some{\Phi} \cD)
\end{array}\]
The {\tt linear} predicate yields this (degenerate)
example of  context schema:
\beq
\cS_{linear} & = & \ecs\bnfalt\cS_{linear}\bar x\oftp exp;linear(x)\bnfalt\cS_{linear}\bar 
x\oftp exp;\top_{linx} 
\eneq
%\end{example}

We extract a context schema by collecting all negative occurrences in
a goal; this is achieved by simulating execution until an atomic goal
is reached and the current list of parameters and assumptions is
returned, with their correct existential binding. Different clauses
may contribute different schema alternatives for a given predicate
definition. A \emph{run-time} context consists of a set of
\emph{blocks}, each of which is an instance of the context schema, for
example:
$$y_1\oftp exp,y_2\oftp exp,x_1\oftp exp;\top_{linx}\And
\top_{linx}\And linear(x_1)$$
We will need to disambiguate blocks in run-time contexts; overlapping
may indeed happen when the alternatives in a context schema are not
disjoint.  Intuitively, a block is complete when an atomic conclusion
is reached during the deduction.  Any bracketing convention will do:
$$\block{y_1\oftp exp},\block{y_2\oftp exp},\block{x_1\oftp
exp};\block{\top_{linx}}\And\block{ \top_{linx}}\And
\block{linear(x_1)}$$ We then define when a formula satisfies a
schema.  We start by saying that a completed block \emph{belongs} to a
schema when the block is an alphabetic variant of some instantiation
of one of the alternatives of the schema.  Then, the empty run-time
context is an \emph{instance} of every schema. Secondly, if $\GG'$ and
$\cD'$ are completed blocks which belong to $\cS$, and $\ga$ in
an instance of $\cS$, then $(\GG,\block{\GG'});(\cD\And\block{\cD'})$
is an \emph{instance} of $ \cS$, provided that $\cD'$ is a valid
clause. The latter holds when each of its subgoals satisfies the
schema. This is achieved by mimicking the construction on the run-time
schema until in the base case we check whether the resulting context
is an instance of the given schema.

We can prove that if a  context schema is extracted from a program, then
any instance of the latter satisfies the former.
Moreover,  execution preserves contexts, \ie every
subgoal which arises in any given successful or  failed (immediate and
non-immediate) sub-derivation satisfies the context schema.
See \cite{Momigliano00phd} for the formal development.

\section{Clause Complementation}
\label{sec:cc}
We restrict ourselves to programs with:
\bit
\item Goals where every assumption is parametric, \ie it is in the
  scope of a positive occurrence of a universal quantifier and the
  corresponding parameter occurs in head position in the assumption.
\item Clauses $Q\If G$ such that the head of every term in $Q$ is
  rigid.
%\item Parameters of base type and occurring only in \emph{head}
%  position.  
\enit 
Note that the rigidity restriction applies only to
non-Horn predicate definitions and can be significantly relaxed; see
\cite{Momigliano00phd} for a detailed account.

% \begin{figure}
% \renewcommand{\ga}{\GG}
% \newcommand{\vda}{\vd}
%   \label{fig:notass}
%     \[
%     \begin{array}{c}
%        \ianc{}{\ga\vda\mnota (\perp_Q)  =  \top_Q}{\mnota\perp}\vsk
%        \ianc{}{\ga\vda\mnota (\top_Q)  = \BAnd_{x\in dom(\GG)}^{x\in
%           Q_{\mid_i}}\mnotxi(\top_Q)}{\mnota\top}\vsk
%            \ianc{\vdf\mnotg(G) = G'}{\ga\vda\mnota( Q\If G) =\BAnd_{x\in dom(\GG)}^{x\in
%           Q_{\mid_i}}\mnotxi(Q) \And ( \neg Q\If G')}{\mnota\If}\vsk
%          \ianc{\ga\vda\mnota( D)=D'}{\ga\vda\mnota (\PI{x}{A}D)  =  \PI{x}{A}D'}{\mnota\Pi}\vsk
%         \ibnc{\ga\vda\mnota (D_{1})= D_1'}{\ga\vda\mnota (D_{2})= D_2'}{\ga\vda\mnota
%         ( D_{1}\And D_{2})=D_1'\tensor D_2'}{\mnot\And}\vsk
%        \ibnc{\ga\vda\mnota (D_{1})= D_1'}{\ga\vda\mnota (D_{2})= D_2'}{\ga\vda\mnota
%         ( D_{1}\tensor D_{2})=D_1'\And D_2'}{\mnot\tensor}
% \vsk
% \ibnc{\Sigma(q)=A_1\Imp\cdots \Imp A_n\Imp\prop}{\cdot\vd sh(x,A_i)=\ex}
% {\gfq\mnotxi(\top_q)  =
%       \PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\ Z_1\dots Z_{i-1}\ \ex\
%       Z_{i+1}\dots Z_n\If \top}{\mnotxi\top}\vsk
%     \ibnc{\Sigma(q)=A_1\Imp\cdots \Imp A_n\Imp\prop}{\cdot\vd
%       sh(x,A_i)=\ex}
% {\gfq\mnotxi  (q\ \Mn)=
%     \BAnd_{1\leq j\leq n}^{j\not = i}(\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n}
%      \neg q\ \ol{Z^i_{\ex}}\If M_j\neqd Z_j)}{\mnotxi\atm}
% \vsk
% \ianc{}{\gvd sh(x,P)=x}{\ex\atm}
% \qquad
% \ianc{\GG,y\oftp A\vd sh(x,B)=\ex}{\GG\vd sh(x,A\Imp B)=\lamb{y}{A}\ex}{\ex\Imp}
% % \ianc{\Sigma(q)=A_1\Imp\cdots \Imp A_n\Imp\prop}{\gfq\mnotxi(\top_q)  =
% %       \PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg q\ Z_1\dots Z_{i-1}\ x\
% %       Z_{i+1}\dots Z_n}{\mnotxi\top}\vsk
% %     \ianc{\Sigma(q)=A_1\Imp\cdots \Imp A_n\Imp\prop}{\gfq\mnotxi  (q\ \Mn)=
% %     \BAnd_{1\leq j\leq n}^{j\not = i}(\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n}
% %      \neg q\ \ol{Z^i_x}\If M_j\neqd Z_j)}{\mnotxi\atm}
%  \end{array}\]
%     \caption{Assumption Complementation: $\ga\vda\mnota(D)=D'$}
% \end{figure}
\smallskip
The first ingredient is \emph{\ho pattern} complement, $\mnot(M)$,
investigated in the general case in \cite{Momigliano99}; we give here the rules
for complementing fully applied patterns:
\pagebreak
\begin{small}
\[
\begin{array}{c}
\ianc{} {\GG\prv \mnot(E\ \xn)\blip \emptyset} {\mnot\_Flx}
\vsk
\ianc{\GG, x\oftp A \prv \mnot(M) \blip  N \hastype B} {\GG \prv \mnot(\lxa M)  \blip \lxa N \hastype A\Imp B}{\mnot\_Lam}
\vsk
\ianc{g\in\Sigma\cup\GG, g \hastype A_{1}\Imp\dots\Imp A_{m}\Imp 
a, m\geq 0,h \not\equiv g} 
{\GG\prv  \mnot (h\ \Mn) \blip 
g\ (Z_{1} \GG)\dots (Z_{m}\GG) \hastype a} {\mnot\_App^1}
\vsk
\ianc{\exists i: 1\leq i\leq n
\qquad\GG\prv \mnot( M_i) \blip N \hastype } 
{\GG\prv  \mnot (h\ \Mn) \blip 
h\ (Z_{1}\GG)\dots (Z_{i-1}\GG) \ N\ 
(Z_{i+1}\GG)\dots (Z_{n}\GG) \hastype a} {\mnot\_App^{2}}
\end{array}
\]
\end{small}
where the $Z$'s are fresh variables which may depend on the domain of
$\GG$, $h\in\Sigma\cup\GG$, and $\GG\prv h\hastype A_{1}\Imp\dots\Imp
A_{n}\Imp a$.  $\GG\vd\mnot(M)= \cN\hastype A$ iff $\cN=\{N\mid\GG\prv
\mnot(M)\blip N\hastype A\}$. For example:
%\begin{example}
$$\cdot\vd\mnot(\lx x) = \{\lx lam(\ly E\ x\ y), \lx app\ (E_1\ x) \ (E_2\ 
x)\}$$
%\end{example}
If we write $\GG \prv M\in\| N\| \hastype A$ when $M$ is a
ground instance of a pattern $N$ at type $A$, we can show that $\mnot$
behaves as the complement on sets of ground terms, \ie
%\begin{lemma}
%\label{le:part}
%For a fixed signature $\Sigma$, let $\GG\vd N \hastype A$ be a linear
%term.  Then:
\ben
\item (Exclusivity)  Not ($\GG\prv M\in \| N
  \|\hastype A$ and $\GG\prv M\in \| \mnot(N) \|\hastype A$).
\item (Exhaustivity) Either $\GG\prv
  M\in \| N \| \hastype A$ or $\GG\prv M\in \| \mnot(N) \|\hastype
  A$.  
\enen
%\end{lemma}


Complementing goals 
%(Fig.~\ref{fig:notgoal}) 
is immediate: we just put the latter in negation normal form,
respecting the operational semantics of failure.

%\begin{figure}
%\renewcommand{\ga}{\GG;\cD}
  \begin{small}
    \[
    \begin{array}{c}
      \ianc{}{\mnotg (\top)  =  \perp}{\mnotg\top}\qquad
        \ianc{}{\mnotg (\perp)  =  \top}{\mnotg\perp}\qquad
        \ianc{}{\mnotg (Q) =  \neg Q}{\mnotg At}\vsk
      \ianc{}{\mnotg(\vM \eqd \vN)= (\vM \neqd \vN)}{\mnot\eqd}\qquad
      \ianc{}{\mnotg(\vM \neqd \vN)= (\vM \eqd \vN)}{\mnot\neqd}\vsk
        %   \ianc{(\GG,y\oftp A);\cD\vd\mnotg([y/x]G)=[y/x]G'}{\mnotg
        %(\PI{x}{A}G)  =  \PI{x}{A}G'}{\mnotg\Pi^*}\vsk
      \ianc{\mnotg(G)=G'}{\mnotg
        (\PI{x}{A}G)  =  \PI{x}{A}G'}{\mnotg\Pi}\qquad
        \ianc{\mnotg(G) = G'}{\mnotg( D \Imp G) = D\Imp   G'}{\mnotg\Imp}\vsk
        \ibnc{\mnotg (G_{1})= G_1'}{\mnotg (G_{2})= G_2'}{\mnotg
        ( G_{1}\And G_{2})=G_1'\Or G_2'}{\mnot\And}\vsk
       \ibnc{\mnotg (G_{1})= G_1'}{\mnotg (G_{2})= G_2'}{\mnotg
        ( G_{1}\Or G_{2})= G_1'\And G_2'}{\mnot\Or}
    \end{array}\]
    \end{small}
 %   \caption{Goal Complementation: $\mnotg(G)=G'$}
%  \label{fig:notgoal}
%\end{figure}

%\smallskip We now introduce in Figure \ref{fig:notclause} and Figure
%\ref{fig:notass} the rules for static and dynamic clause
%complementation.  


Clause complementation is instead more delicate: given a rule $q\ 
\vM\If G$, its complement must contain a `factual' part motivating
failure due to clash with the head; the remainder $\mnotg (G)$
expresses failure in the body, if any.  Clause complementation must
discriminate whether (the head of) a  rule belongs to the static or dynamic
definition of a predicate.  In the first case
%(Fig.~\ref{fig:notclause}) 
all the relevant information is already
present in the head of the clause and we can use the term
complementation algorithm. This is accomplished by the rule
$\mnotd\Imp$, where a set of negative facts is built via term
complementation $\mnot (\vM)$, namely $\BAnd_{\vN\in\mnot(\vM)}\Pi(
\neg q\ \vN\If\top)$, whose fresh free variables are universally
closed; moreover the negative counterpart of the source clause is
obtained via complementation of the body. The original quantification
is retained thanks to rule $\mnotd\Pi$.
%\begin{figure}
  \begin{small}
    \[
    \begin{array}{c}
    %  \ianc{\gf \mnota(\top_{Q})=\neg D}{\ga\vd\mnotd (\top_Q)  = \neg 
     % D}{\mnota\top}\vsk
%       \ianc{}{\cdot;\top\vd\mnotd (\top)  = 
           \ianc{}{\mnotd (\top)  =       \perp}{\mnotd\top}\qquad
        \ianc{}{\mnotd (\perp)  =  \top}{\mnotd\perp}\vsk
    %( q\ \vM\If G)\in\cP
    \ianc{\mnotg(G) =  G'}{\mnotd( q\ \vM\If G) =
(\BAnd_{\vN\in\mnot(\vM)}\Pi( \neg (q\ \vN)\If\top)) \And ( \neg q\ \vM\If G')}{\mnotd\If}\vsk
         \ianc{\mnotd( D)=D'}{\mnotd (\PI{x}{A}D)  =  \PI{x}{A}D'}{\mnotd\Pi}\vsk
        \ibnc{\mnotd (D_{1})= D_1'}{\mnotd (D_{2})= D_2'}{\mnotd
        ( D_{1}\And D_{2})=D_1'\tensor D_2'}{\mnot\And}\vsk
       \ibnc{\mnotd (D_{1})= D_1'}{\mnotd (D_{2})= D_2'}{\mnotd
        ( D_{1}\tensor D_{2})=D_1'\And D_2'}{\mnot\tensor}
     %  \ibnc{
% %( q\ \vM\If G)\in\cD
% }{\gf\mnota( q\ \vM)=\neg D\quad\vd\mnotg(G) = G'}{\ga\vd\mnotd( 
%       q\ \vM\If G) =\neg D\And ( \neg q\ \vM\If G')}{\mnota\If}\vsk
      \end{array}\]
      \end{small}
  %    \caption{Clause Complementation: $\mnotd(D)=D'$}
 % \label{fig:notclause}
%\end{figure}
\begin{sloppypar}
Otherwise, we can think of the complement of an atomic assumption $(q\
M_1\dots x\ \dots M_n)$, which is
by definition parametric in some $x$, as static clause complementation
\wrt $x$, \ie $\mnotd( q_x\ M_1\dots M_{i-1}\ M_{i+1}\dots M_n)$.
However, most of  those $M_i$, which at compile-time are
variables, will be instantiated at run-time: therefore it would be
incorrect to compute their complement as empty. Since we cannot
foresee this instantiation, we achieve clause complementation via
the introduction of disequations. This is realized by the judgment
$\gf\mnota(D)$. We need the following notion: a parameter $x\oftp a$ is 
\emph{relevant} to a predicate symbol $q$ (denoted $ xR^{i}q$) if
$\Sigma(q)=A_1\Imp\cdots \Imp A_n\Imp\prop$ and for some $1\leq i\leq n$ the
target type of $A_i$ is $a$.
\end{sloppypar}
\begin{small}
 \[
    \begin{array}{c}
%       \ianc{}{\GG\vd\mnota (\perp_q)  =  \top_q}{\mnota\perp}\vsk
       \ianc{}{\GG\vd\mnota (\top_q)  = \BAnd_{x\in dom(\GG)}(
\BAnd_{xR^{i}q}\mnotxi(\top_q))}{\mnota\top}\vsk\\
           \ianc{\mnotg(G) = G'}{\GG\vd\mnota( Q\If G) =(\BAnd_{x\in dom(\GG)}(\BAnd_{xR^{i}q}\mnotxi(Q))) \And ( \neg Q\If G')}{\mnota\If}
      \end{array}
\]
\end{small}
Both rules refer to an auxiliary judgment $\mnotxi(D)$:
\begin{small}
\[
\begin{array}{c}
\ibnc{\Sigma(q)=A_1\Imp\cdots \Imp A_n\Imp\prop}{\cdot\vd sh(x,A_i)=\ex}
{\gfq\mnotxi(\top_q)  =
      \PI{Z_1}{A_1}\dots\PI{Z_n}{A_n} \neg (q\ \ol{Z^i_{\ex}})\If \top}{\mnotxi\top}\vsk
    \ibnc{\Sigma(q)=A_1\Imp\cdots \Imp A_n\Imp\prop}{\cdot\vd
      sh(x,A_i)=\ex}
{\gfq\mnotxi  (q\ \Mn)=
    \BAnd_{1\leq j\leq n,j\not = i}(\PI{Z_1}{A_1}\dots\PI{Z_n}{A_n}
     \neg (q\ \ol{Z^i_{\ex}})\If M_j\neqd Z_j)}{\mnotxi\atm}
\end{array}
\]
\end{small}
The idea
is to:
 \begin{itemize}
    \item Pivot on $x\oftp a\in\GG$. 
%relevant to $q$.
    \item Locate a type $A_i$ such that $x\oftp a$ is relevant to $q$ at $i$.
    \item Complement $D$ \wrt $x$ and $i$.
    \item Repeat for every $A_i$ and for every $x$.
%    \item Special case: if no $x$ is relevant, the trivial program is
%      returned.
\end{itemize}

The rest of the rules for $\GG\vd\mnota(D)$ are completely analogous
to the ones for $\mnotd(D)$ and are omitted. Both simply recur on the
program respecting the duality of conjunction and disjunction \wrt
negation.  Notice the different treatment of the trivial clause $\top$
by rules $\mnotd\top$ and $\mnota\top$: if no parameter has been
assumed, then $\top$ truly stands for the empty predicate definition
and its complement is the universal definition $\perp$.  If, on the
other hand $\GG$ is \emph{not} empty, it means that $\top_q$ has been
introduced during the $\top$-normalization preprocessing phase and has
been localized to the predicate $q$.  The rule $\mnotxi\top$ allows to
build a new negative assumption \wrt $q,x,i$ in case $\top_q$ is the
only dynamic definition of $q$. As $\top_q$ carries no information at
all concerning $q$, the most general negative assumption is added; the
notation $\ol{Z^i_{\ex}}$ abridges $ Z_1\dots Z_{i-1}\ \ex\ 
Z_{i+1}\dots Z_n$, where the $Z$'s are fresh logic variables and $\ex$
is a term built prefixing a parameter $x$ by an appropriate number of
lambda's, according to the type of its position; this is specified by the
$\GG\vd sh(x,A)$ judgment, omitted here (but see it in action in
Example \ref{ex:copy}).

Now that we have discussed how to perform clause, assumption and goal
complementation, we synchronize them together in a phase we call
\emph{augmentation}, which simply inserts the correct assumption
complementation into a goal and in turn into a clause. This is achieved by
a judgment $\gfald(D)$, again  omitted here for reasons of space.
% We give
% one judgment to augment a program, $\gfald(D)$ merely
% recurs on the structure of clauses until it calls goal augmentation,
% $\ga\vdfg\alg(G)$. The latter traverses a goal collecting
% parameters in $\GG$ and assumptions in $\cD$. When it reaches an atom,
% either it stops, as no parameter has been introduced, or it passes
% $\GG,\cD$ to assumption complementation.
% Finally the  complementation of a
% program is taken
% \emph{predicate definition-wise} rather that \emph{clause-wise}. The
% same remark applies to the `dynamic' program $\cD$. Formally, 
% fixed a signature $\Sigma_{\cP}$ and given a program $\cP$:
% \beq
% \mnotd(\cP) & = &  \BAnd_{q\in\Sigma_{\cP}} \mnotd (\defp(q,\cP))
% \eneq
% Similarly for a conjunction of dynamic assumptions $\cD$:
% \beq
% \mnota(\cD) & = &  \BAnd_{q\in\Sigma_{\cP}} \mnota (\defp(q,\cD))
% \eneq
%\begin{example}

For example, consider the \texttt{copy} clause on $\l$-terms:
\beq
\label{ex:copy}
% cpapp &:& \PI{E_1,E_2,F_1,F_2}{exp}\\
% & & cp\ (app\ E_{1}E_{2}) \ (app\ F_{1}F_{2})\\
% && \qquad\If  copy\ (E_{1}F_{1})\\ 
% && \qquad\If copy\ (E_{2}F_{2})\\
cplam &:& 
%\PI{E}{exp\Imp exp}\PI{F}{exp\Imp exp} \\
 copy\ (lam\ E) \ (lam\ F)\\
& & \qquad\If (\PI{x} {exp} copy\ x\ x\Imp copy\ (E\ x) \ (F\ x)).
\eneq
The augmentation procedure collects $x\oftp exp; copy\ x\ x$ and 
 calls $x\oftp exp\vd \mnota( copy\ x\ x)$.
%, glossing over the context $\Phi$ which
%is not active in this case. 
First
$ \mnot^x_1(copy\ x\ x)= (\PI{E'}{exp} \neg copy\ E'\ x\If
x\neqd E')$, secondly $
 \mnot^x_2(copy\ x\ x)= (\PI{F'}{exp} \neg copy\ x\ F'\If x\neqd F')$, yielding:
%\begin{small}
\beq
\ald(cplam)&:&
% \PI{E}{exp\Imp exp}\PI{F}{exp\Imp exp} \\
  copy\ (lam\ E) \ (lam\ F) \\
& & \qquad \If (\PI{x}{ exp}\\
& & \qquad\qquad (\PI{E'}{exp} \neg copy\ E'\ x\If x\neqd E')\And\\
& & \qquad\qquad (\PI{F'}{exp} \neg copy\ x\ F'\If x\neqd F')\Imp\\
&& \qquad\qquad\qquad
 (copy\ x\ x \Imp copy\ (E\ x) \ (F\ x))).
\eneq
%\end{small}
%while of course, $\ald(copyapp)=cpapp$, as enforced by $\alg \atm\top$.
Let us see how rule $\mnotxi\top$ enters the picture; recall the 
normalized \texttt{linxlm}  clause.
% \beq
% linxlam &: & \PI{ E}{ exp\Imp exp\Imp exp} \\
% & & linx\ (\lx lam(\ly  E\ x\ y))  \If\\
% & & \qquad  \PI {z} {exp} \top_{linx}\Imp linx\ (\lx E\ x\ z)
% \eneq
From $\cdot\vd sh(y,exp\Imp exp)=\lx y$
we have $\mnot^y_1(\top_{linx})= \neg linx\ (\lx y)$:
\beq
\ald(linxlam)&:&   linx\ (\lx lam(\ly  E\ x\ y)) \\
& & \qquad \If (\PI {y } {exp} \neg linx\ (\lx y)\Imp linx\ (\lx E\ x\ y)).
\eneq
%\end{example}

%\begin{example}
Let us apply the complement algorithm to the \texttt{linx} predicate
definition. The \texttt{strict} predicate is simply the complement
of the \texttt{vac} predicate previously introduced. Again, these
annotations can be internalized in a strict type theory 
\cite{Momigliano99}.
\pagebreak
%\begin{small}
\beq
\lefteqn{\mnotd(def(linx))=}\\
\lefteqn{ \mnotd(linxx)\tensor\mnotd(linxap1)\tensor\mnotd(linxap2)\tensor\mnotd(linxlm)=}\\
  && (\neg linx(\lx app\ (E_1\ x) \ (E_2\ x))\And \neg linx(\lx lam( \ly (E\ x\
y))))\tensor\mbox{}\\ 
  && (\neg linx(\lx x)\And  \neg linx(\lx lam( \ly (E\ x\ y)))\And\mbox{}\\
&& \neg linx(\lx app\ (E_1\ x) \ (E_2\ x) )\If strict(\lx E_2\ x)\\
&& \mbox{}\And\neg linx(\lx app\ (E_1\ x) \ (E_2\ x) )\If\neg linx(\lx E_1\ x))\tensor\mbox{}\\
  &&( \neg linx(\lx x)\And  \neg linx(\lx lam( \ly (E\ x\ y)))\And\mbox{}\\
&& \neg linx(\lx app\ (E_1\ x) \ (E_2\ x ))\If
strict(\lx E_1\ x)\\
 &&  \mbox{}\And\neg linx(\lx app\ (E_1\ x) \ (E_2\ x))\If \neg linx(\lx E_2\ x))\tensor\mbox{}\\
  && (\neg linx(\lx x)\And \neg linx(\lx app\ (E_1\ x) \ (E_2\ x)) \\
 &&\mbox{}\And\neg   linx (\lx lam(\ly (E\ x\ y) ))\If (\PI{y}{exp} \neg linx(\lx
y)\Imp \neg linx (\lx E\ x\ y ))).
\eneq
%\end{small}
%\end{example}

% \smallskip
% We can prove that augmentation guarantees that 
% static and dynamic clauses are closed under complementation.

% \begin{theorem}[Closure under Complementation]
%   If $\dsat D$,\\ then $\dsat\mnotd(\ald(D))$.
% \end{theorem}

\renewcommand{\ga}{\Gamma;\cD }
\renewcommand{\gna}{ \Gamma;\cD }
\renewcommand{\sn}{\vd_{\!\cP^-}}
\renewcommand{\spp}{\vd_{\!\cP}}
\renewcommand{\sp}{\vd_{\!\cP}}
\renewcommand{\snp}{\vd_{\!\cP^-} \mnotg}

We can now establish exclusivity and exhaustivity of clause
complementation. Let $\mnotd(\cP)=\cP^-$:
\begin{theorem}[Exclusivity] 
\label{thm:exclu}
For every run-time context $\ga$  instance of a schema $\csa$ 
extracted from an augmented program $\cP$:
\ben
\item It is not the case that $ \ga\spp G$ and $ \gna\snp ( G)$.
\item It is not the case that $ \ga\spp (\cP\And\cD) \imm Q$ and $
  \gna\sn (\cP^-\And\cD) \imm \neg Q$.  
\enen
\end{theorem}
\begin{proof} (Sketch)
  By mutual induction on the structure of the derivation of $\ga\spp
  G$ and $ \ga\spp (\cP\And\cD) \imm Q$. The proof goes through as
  there is no `bad' interaction between the static and dynamic
  definition of a predicate; namely there is no overlap between a
  clause from $\cP$ and from $\cD$ since in every atomic
  assumption there must be an occurrence of an eigenvariable \emph{and}
  every corresponding term in a program clause head must start with a
  constructor. If both clauses are dynamic, it holds because an
  appropriate disequation is present; this approximates what happens
  in the static case, which is based on term exclusivity.
\end{proof}

 The denial system comes in handy in the following proof.
%  of exhaustivity; here we
% make an essential use of the restriction to terminating programs, \ie
% such that for every goal either $\ga\sp G$ or $\ga\fpp G$.
\begin{theorem}[Exhaustivity]
\label{thm:exh}
\renewcommand{\ga}{\Gamma;[\q]\cD }
\renewcommand{\gna}{ \Gamma;[\s]\cD }
\renewcommand{\snp}{\vd_{\!\cP^{-}} [\s] \mnotg}
For every substitution $\q,\s$   and  run-time
context $\ga$ instance of a schema $\csa$  extracted from an augmented
program $\cP$:
\ben
\item
If   $\foq   \ga\fpp [\q] G$, then there is a  $\s$ such that  
 $  \gna\snp (G)$.
\item[2.1]
If, for all  $\q$
$  \ga\fpp [\q] \cP  \nimm [\q] Q$, then here is a $\s$ such that 
$  \gna\sn [\s] \mnotd(D) \imm [\s] \neg Q$.
\item[2.2]
If, for all  $\q$ 
$  \ga\fpp [\q] \cD  \nimm [\q] Q$, then here is a $\s$ such that 
$  \gna\sn [\s] \mnota(D) \imm [\s] \neg Q$.
\enen
\end{theorem}
The proof is by mutual induction on the structure of the given
derivations. As a corollary, we are guaranteed that clause
complementation satisfies the boolean rules of negation.

% Moreover, if we consider classes of equivalence of clauses under
% operational  equivalence, we can organize them in a boolean algebra.
% \smallskip 

Finally, we show how to eliminate from clauses the `$\tensor$'
operator stemming from the complementation of conjunctions, while
preserving provability; this will recover uniformity in proof-search.

 The key observation is that in this context `$\tensor$' can
be restricted to a program constructor \emph{inside} a predicate
definition; therefore it can be eliminated by simulating unification
in the definition, that is
% We generalize the approach in
%\cite{Bar90}, which defined 
$ (Q_{1}\If G_{1}) \tensor (Q_{2}\If
G_{2})\equiv \q(Q_{1}\If G_1\And G_2)$, where $\q = mgu(Q_{1},Q_{2})$.
% As we remarked earlier the `$\tensor$'
% operator in clauses was introduced to preserve the duality between
% conjunction and disjunction.  Its use is limited to clauses in the
% same predicate definition and 

However, the (strict) \ho unification problem is quite complex, even
more so due to the mixed quantifier structure of HHF; since we have
already parameter (dis)equations introduced by the augmentation
procedure, as well as variable-variable (dis)equations stemming from
left-linearization, we first compile clauses in an intermediate
language which keeps the unification problems explicit and then we
perform constraint simplification as in \emph{Twelf}.
% Note that only those (in)equalities which contain a parameter cannot
% be immediately solved and must be postponed as constraints.
Continuing with our example and simplifying the constraints:
\beq
 \lefteqn{\mnotd(linxx)\tensor\mnotd(linxap1)=}\\
&& \neg linx(\lx app\ (E_1\ x) \ (E_2\ x)) \If strict(\lx E_2\ x)
\And\mbox{}\\ 
&&
\neg linx(\lx app\ (E_1\ x) \ (E_2\ x))\If  \neg linx(\lx E_1\ x)
\And\mbox{}
\\ && \neg linx(\lx lam(\ly E\ x\ y)).
\eneq
% \beq
%  \lefteqn{\mnotd(linxx)\tensor\mnotd(linxap1)=}\\
% & \neg linx(\lx app\ (E_1\ x) \ (E_2\ x)) \If (\lx app\ (E_1\ x) \
% (E_2\ x)) \eqd (\lx app\ (E_1\ x) \ (E_2\ x^0)) \And\mbox{}\\
% &
% \neg linx(\lx app\ (E_1\ x) \ (E_2\ x))\If (\lx app\ (E_1\ x) \ (E_2\
% x)) \eqd (\lx app\ (E_1\ x) \ E_2 ) \And \neg linx(\lx E_1\ x))
% \eneq
The final definition of \texttt{$\neg$linear} and in turn \texttt{$\neg$linx} is:
%\begin{small}
  \beq
  \neg linapp & : & \neg linear(app\ E_1\ E_2)\\
  & & \qquad \If \neg linear(E_1)\Or \neg linear(E_2).\\
  \neg linlam1& : & \neg linear(lam(\lx E\ x))\\
  & & \qquad \If\neg linx(\lx E\ x)\\
& & \qquad\mbox{}\Or (\PI{y}{exp} (\neg linx(\lx y)\And linear(y))\Imp
  \neg
  linear(E\ y)).\\
  \neg linxap0& :& \neg linx(\lx app\ (E_1\ x) \ (E_2\ x))\If strict(\lx
  E_1\ x) \And strict(\lx E_2\ x).\\ 
%  \neg linx2& :& \neg linx(\lx app\ (E_1\ x) \ (E_2\ x))\If strict(\lx E_1\ x).\\
  \neg linxap1& : & \neg linx(\lx app\ (E_1\ x) \ (E_2\ x) )\If strict(\lx E_2\ x) \And \neg  linx(\lx  E_1\ x).\\
  \neg linxap2& : & \neg linx(\lx app\ (E_1\ x) \  (E_2\ x))\If strict(\lx E_1\ x) \And 
\neg linx(\lx  E_2\ x).\\
  \neg linxap3& : & \neg linx(\lx app\ (E_1\ x) \  (E_2\ x))\If \neg linx(\lx
  E_1\ x)\And  \neg linx(\lx E_2\ x).\\
  \neg linxlm& : &\neg linx(\lx lam(\ly E\ x\ y))\\
  & & \qquad\If (\PI{y}{exp} \neg linx(\lx y)\Imp \neg linx (\lx E\ x\ 
  y)).  \eneq
%\end{small}
%\end{example}


\section{Conclusions and Future Work}
\label{sec:end}
We have presented elimination of negation in a fragment of
higher-order HHF; our next task is to overcome some of the current
restrictions, to begin with the extension to \emph{any} order, which
requires a more refined notion of context.
%; accordingly, lifting the
%requirement for parameters to be of base type and in head position is a
%matter of descending into the parameter expression until we find the
%correct eigenvariable to pivot on.
The issue of local variables is instead more challenging. The proposal
in \cite{Brogi90} is not satisfactory and robust enough to carry over
to logical frameworks with intensional universal quantification. Our
approach will be again to \emph{synthesize} a HHF definition for the
clauses with local variables which during the transformations has
became \emph{extensionally} quantified.
%: the issue of \emph{extensionality} is of independent interest in the the theory of
%logical frameworks
Our final goal is to achieve negation elimination in LF.  

\smallskip
\noindent
\textbf{Acknowledgments.} I would like to thank  Frank
Pfenning for  his continuous help and guidance. The notion of
context schema is inspired by Sch\"{u}rmann's treatment of analogous
material in \cite{Schurmann00phd}.
\begin{small}
\bibliography{am}
\end{small}
\end{document}
