\section{Hypothetical and Parametrical Judgments}
\label{aug}
\newcommand{\omicron}{\emph{ord}}
\renewcommand{\frac}{\ianc}

We aim to apply the transformation method to parametrical and
hypothetical judgments. This requires a non-trivial extension of the
horn technique, since we have to respect the underlying intuitionistic
logic. Our leading intuition is to preserve, under complementation,
the operational semantics of these judgments. Thus,in a first
approximation, the negation of $D \Imp G$ yields the attempt of
establishing $\Not G$ from the assumption $D$ and the negation of $\Pi
x:A.G$ is the attempt to establish $[a/x]\Not G$ for a new parameter
$a:A$. To make this more distinct we use $Not$ instead of $\neg$.
\beq
Not(D\Imp G) & = & D \Imp Not(G) \\
Not(\Pi x:A.G) & = & \Pi x:A. Not(G) 
\eneq

We then extend the $Not$ operation as expected to every other 
constructor in the extended language, since it 
will come handy to deal with the completion.
\beq
Not(P) & = & \neg P\\
Not(G_{1}\And G_{2}) & = & Not(G_{1}) \Or Not(G_{2}) \\
Not(G_{1}\Or G_{2}) & = & Not(G_{1}) \And  Not(G_{2}) \\
Not(\exists x:A.G) & = & \forall x: A. Not(G) \\
Not(P\If G) & = & \neg P\If Not(G)
\eneq

Therefore the complementation of a parametric clause does not entail 
the existential of the complement of the body as in Harland.  Moreover 
we will not pose the OWA restriction on implicational goals; that will 
allows us to treat self-recursive definitions.  In fact a thorough 
examinations of common examples of \ho programming in logical 
frameworks show that most of them are self-recursive.  Another common 
mark is that they have a typical pattern: self-recursive implications 
are ``covered'' by universals so as to, in a sense, reduce the 
structural complexity of the predicate to be assumed.  Indeed we may 
dare to say these are the only \ho self-recursive definitions which are
 sensibly complementable.

Therefore, we will restrict the class of programs closed under 
complementation to avoid inconsistencies during execution.  This 
reflects out intuition of goal-directed search and tends to exclude 
only definitions whose negative behavior is not clearly predictable.  
If one insists on unrestricted complementation, the standard technique 
would be elimination of implications through meta-interpretation as 
discussed in \ref{meta}.

Let us exemplify that:

\begin{Examplen}
Let \texttt{pf : o -> type} be an implementation of natural deduction 
and let us consider the rule for implication introduction and the 
corresponding clause in its proposed negation:
\beq
impI & : & pf\ (A \supset B) \If (pf\ A \Imp pf\ B)\\
\Not impI & : & \neg pf\ (A \supset B) \If (pf\ A \Imp \neg pf\ B)
\eneq
In the latter clause the structure of the head is not qualified enough so 
that the assumption of \texttt{pf\ A} may later contradict the evaluation of 
\texttt{$\neg$ pf\ B}. Consider instead a definition of when a lambda expression is 
closed:
\beq
clolam & :& closed\ (lam\ E) \If \Pi x : exp.\ (closed\ x) \Imp closed\ 
(E\ x)\\
\neg clolam & :& \neg closed\ (lam\ E) \If \Pi x : exp.\ (closed\ x) \Imp 
\neg closed\ (E\ x)
\eneq
In the latter case the assumption of \texttt{closed\ !x} is consistent with 
the rest of the negative program.
\end{Examplen}

We will therefore limit the application of complementation (and of 
completion) to those self recursive predicates which satisfy the above 
condition, which we formally define next.  We abuse the notation by 
mentioning $P$ instead of $functor(P)$.

\begin{Definition}[Dependence]
 Given a program $(P\If G)\cup\cP$, we say that $P$ 
% Given a clause $P\If G$, we say that $P$ 
\emph{depends positively [negatively] on $G$} 
iff
\begin{itemize}
\item $P$ depends positively on $P$ 
\item $P$ depends positively 
[negatively] on $\forall x :A.G$ iff $P$ depends positively 
[negatively] on $G$ 
\item $P$ depends positively [negatively] on 
$G_{1} \Imp G_{2}$ iff $P$ depends positively [negatively] on $ G_{2} 
$ or $P$ depends negatively [positively] on $G_{1}$.
\end{itemize}
\end{Definition}


Let $dep^{*}_{\pm}$ be the transitive closure of the above dependency 
relations (to accommodate  mutual recursion): 

\begin{Definition}[Recursive]
We say that a clause $P\If G$ is \emph{recursive} in $\cP$ if $P\ 
dep^{*}_{+} $ on $P$ in $\cP$: it is \emph{left recursive in $Q$} if 
$P\ dep^{*}_{-} $ on $P$ in $\cP$
\end{Definition}

Note that $P$ may depend both positively and negatively in a program 
and typically a left recursive clause is recursive as well.  If $P\ 
dep^{1}_{\pm} Q$ and $Q\ dep^{*}_{\pm} P$ we say that $P$ is 
(left) recursive \emph{thru $Q$}.

\begin{Definition}[Mode]
\ldots
\end{Definition}

\begin{Definition}[$\Pi$-Allowedness by subterm ordering]
  A (left) recursive clause $P\If G$ in $\cP$, with $mode(P) =\la
  +\Mm, *\Nn\ra$ is \emph{$\Pi$-allowed} iff $\Delta \prv G <_{\Pi} P$
  in the following judgment:
\[
\begin{array}{c}
\ianc{\Delta\prv 
  G_{2}<_{\Pi} P}{\Delta\prv G_{1}\Imp G_{2} <_{\Pi} P}{<_{\Pi}-\Imp} \\[2ex]
\ianc{\Delta, \Pi x: A\prv [a/x]G<_{\Pi} P}{\Delta\prv \Pi x: A.
  G<_{\Pi} P}{<_{\Pi}-\Pi}\\[2ex]
\ianc{p\ dep^{*}_{+ }q\qquad \Delta \prv +\Mm < *\Mm^{'}} {\Delta \prv
 (q\ +\Mm\ *\Nn) <_{\Pi} (p\ +\Mm^{'}\ *\Nn^{'})}{<_{\Pi}-P} 
\end{array}
\] where
$<$ is the lexicographical extension of \fo subterm ordering.
  \end{Definition}

The aim of this definition  is twofold: given an input-output 
relationship, first we restrict to terminating recursive programs; 
second we limit left recursion so that run-time assumptions shall not 
add contradictory premises.  Note also that for our application we do 
not(?) need \ho subterm ordering \cite{EP96,Vir96} since the left hand 
side of $<$ is always a ground term.

\begin{Observation}
A left-recursive clause $P\If G$ is \emph{$\Pi$-allowed} only if for 
every second-order input variable $E$ in $P$, $E$ occurs 
positively\footnote{define somewhere} in the scope of an universal 
quantifier in $G$.
\end{Observation}

Thus \texttt{impI} is not $\Pi$-allowed, whereas \texttt{clolam} is.  
Finally, a predicate is \emph{allowed} if so is every (left) recursive 
clause in its definition; a program is \emph{allowed} if so is every 
predicate definition in it.

\subsection{Metainterpreter for implication elimination}
\label{meta}
The usual Prolog metainterpreter for fohf, its partial evaluation \wrt 
the `trivial' clause
[Fill in]

\section{Completion}

To respect the operational semantics of left-recursive \ho programs 
we need a stronger notion of completion: first we need to establish a 
sort of normal form of parametrical judgments (under negation); only 
later we will be able to take the completion in the usual Clark 
sense.  We therefore distinguish two phase, \emph{augmentation} and 
\emph{completion}.  For pedagogical reasons we first treat the case 
of second-order unary predicates.

\subsection{Augmenting unary predicates}

We try to motivate the need for augmentation by examples: consider 
again judgments defining when a lambda term is closed or open:

\beq
clolam &: & closed\ (lam\ E) \If \Pi x : exp.\ (closed\ x) \Imp closed\ 
(E\ x)\\
 cloapp &: & closed\ (app\ E_{1} E_{2}) \If closed\ E_1 \And closed\ E_{2}\\
\skl
 oplam &: & open\ (lam\ E)  \If \Pi x : exp.\ open\ (E\ x)\\
opapp &: & open\ (app\ E_{1} E_{2}) \If open\ E_1 \Or open\ E_{2}
 \eneq 
It is apparent that both are total decision procedures and that they 
complement each one in the sense that, in a first approximation $\Gamma\prv 
\Pi E: exp.\  closed\ E \Or open\ E$.  Hence we should be able to derive 
one from the other and viceversa.  Let us concentrate only on the 
function case.

Taking Not(clolam) yields
\beq
\neg clolam &: & \neg closed\ (lam\ E) \If \Pi x : exp.\ closed\ x \Imp 
\neg closed\ (E\ x)
\eneq
which by renaming is the clause \texttt{openlam} with the additional 
$closed\ !x$.  It is clear that the former is immaterial \wrt 
derivability, \ie that this extension is conservative with respect to 
the signature of the source clause (see \ref{ppn:cons}).  On the 
other hand, Not(\texttt{openlam}) is clearly incomplete.  In this 
case we do need the additional assumption $\neg open\ !x$.  Since 
trying to add the appropriate assumption at completion time would be 
unwieldy, we do this in a separate phase we call \emph{augmentation} 
\beq 
aug(openlam) & : & open\ (lam\ E) \If \Pi x : exp.\ \neg open\ x 
\Imp open\ (E\ x) \eneq
 which leads to the required \beq \neg 
aug(openlam) & : & \neg open\ (lam\ E) \If \Pi x : exp.  \neg open\ x 
\Imp \neg open\ (E\ x) \eneq

Nevertheless, we have to exercise caution in augmenting only those 
clauses which need it. Consider for example a clause expressing 
natural deduction provability for universals:
\beq
allI &:& pf\ (all\ A) \If \Pi a : i.\ pf\ (A\ a)
\eneq

Here augmentation ought not to be applied.  We can discriminate these 
cases by requiring it only when the type of the parameter is 
\emph{less}, in a sense, of the source type of the recursive 
predicate.  This employs the idea of \emph{type subordination} 
introduced in \cite{RP96} to investigate mode and termination of \ho 
programs.

\begin{Definition}[Subordination]
Let $\leq : A \times A$ be a reflexive and transitive relation on simple 
types that satisfies \ldots
% for $i\in 1..n$:
%\[
%\frac{a \leq a_{i}}{a\leq c(a_{1}\mdots a_{n})}{S-c}
%\quad
%\frac{a\leq A_{1}}{a\leq A_{1}\Imp A_{2}}{S1-\Imp}
%\quad
%\frac{a\leq A_{2}}{a\leq A_{1}\Imp A_{2}}{S2-\Imp}
%\]
\end{Definition}

To sum up, we need to augment recursive non-left recursive 
parametrical clauses which satisfy the above invariant on types so as 
to yield a $\Pi$-allowed clause.

\begin{Definition}[Unary augmentation]
  For a program $\cP$ over a signature $\Sigma$, let $p$ be predicate
  defined recursively by structural induction, for $n,m,q \geq 0$:
 \beq
  m &:& p\ (\l \xn . (a\ (\ol{Y_m \xn}) \ (\ol{E_q \xn}))) \\
  & &\If \BAnd \limits^m_{j = 1} p\ (\l \xn .(Y_j \xn)) \\
  & & \If \BAnd \limits^q_{i = 1}(\Pi z_{i} : A_{i}.\  p\ (\l \xn.(E\ \xn\ z_{i}))) \\
& & \If G \eneq
such that:
 \bit
\item
 $a\in \Sigma\cup\xn$
% \item
% $m$ is a second-order $\Pi$-allowed recursive clause thru $q$ in $\cP$:
\item
 $\Ym : \ol{C_{m}}$ is a vector of first-order variables 
\item
 $\Ep : \ol{B_{q}}$ is a vector of second-order variables \ie $\omicron(B_{i}) = 2$
\item
$G$ is about predicates defined in a lower stratum then $m$
%  $def(p)$
\item
$A_{i}\leq B_{i},\ i\in 1..q$.
\enit
Then define 
\beq
aug(m) &:& p\ (\l \xn . (a\ (\ol{Y_m \xn}) \ (\ol{E_q \xn}))) \\ 
& &\If \BAnd \limits^m_{j = 1} p\ (\l \xn .(Y_j \xn)) \\
& & \If \BAnd \limits^q_{i = 1}(\Pi z_{i} : A_{i}.\  \neg p\ (\l \xn.z_{i})
 \Imp p\ (\l \xn.(E\ \xn\ z_{i}))) \\
 & & \If G
\eneq
Define $aug(def(p))$ and $aug(\cP)$ respectively as the augmentation of every clause
 in $def(p)$ and of every definition in $\cP$.
\end{Definition}

We can (and we will) make the conditions on the structure of $p$ less
stringent, by requiring only that the recursive calls are less, under
the subterm ordering, than the head of the clause. This is indeed
consistent with our intent to apply complementation only to
terminating programs.

\begin{Definition}[Completion]
Let $p$ be  a unary predicate and suppose there are $m$
clauses in its definition  in the underlying program, and  the
$i-th$ clause has the following form (without $\eta$ expansion
\footnote{agree on a uniform convention}
\beq
pi &:& p(M_{i}[\vY]) \leftarrow G_{i}[\vY]
\eneq
for each $i$, where all the variables occurring in the 
definition are taken from the set $\vY$.
Let
\beq
aug(pi) &:& p(M_{i}[\vY]) \leftarrow aug(G_{i}[\vY])
\eneq
where $aug(G_i)$ is a reminder of the augmentation in the body of $pi$.
Then its completion {\em comp(p)} is, for new $\Xn$
\beq
def(p) & :& \forall X .p(X) \Imp \BOr\limits^m_{i=1}
\exists \vY (X \ebe M_{i}[\vY]) \And aug(G_{i}[\vY])\\
Not(def(p)) & :&\forall X . Not(p(X))\If \BAnd\limits^m_{i=1}
\all \vY  (X \nebe M_{i}[\vY]) \And Not(aug(G_{i}[\vY])))
\eneq
where the latter can be simplified, by the definition of $Not$ into:
\beq
Not(def(p)) & :&\forall X . \neg p())\If \BAnd\limits^m_{i=1}
\all \vY  (X \nebe M_{i}[\vY]) \And Not(aug(G_{i}[\vY]))
\eneq
% which can be abbreviated in the definiens formula
% \beq
% dp & :& \forall X. p(X) \If D[\vx]\\
% not(dp) & :& Not(\forall X. p(X) \If Not(aug(D[\vx])))
% \eneq
\end{Definition}

Finally, we make the final transition $Not(def(p))\lead^{*} def(\neg p)$ by 
 application of the transformation  rules 
\texttt{lift,dnf,disunify} with the obvious control\footnote{Yes, 
right}, as described in chapter \ref{dis}. Note that 
we already consider applied \textrm{cp} and partial normalization \wrt 
negation\footnote{\ie a version of negation normal form which respects 
our operational semantics}.

 \subsubsection{Example: open and closed terms}
 \input{open}

\section{Results}

To prove our main result\footnote{for unary predicates without mutual 
recursion for now}, we need to keep track of the assumption of 
a predicate definition (called guards): those are the set of (parametric) goals 
occurring negatively in the body of each clause of the definition.

\begin{Definition}[Guards]
\end{Definition}
\[
\begin{array}{ll}
\GG(def(P)) = \bigcup\limits_{i} \GG(G_{i}) &  P\If G_{i}\in def(P)\\
\skl
\GG(G\Imp Q) = \GG(G)  & \mbox{$Q$ atomic}\\
\GG(G_{1}\Imp G_{2}) = \GG(G_{1})\Imp \GG(G_{2}) & \mbox{otherwise}\\
\GG(\Pi x:A. G) = \Pi x : A. \GG(G)
\end{array}
\]
Given a predicate definition and its complement, we use $\GG^{+}, 
\GG^{-}$ for the respective guards.

\begin{Definition}[Stratification]
A program $\cP$ is \emph{stratified} if it can be partitioned in $k$ 
strata $\cP_{1}\cup\dots\cup\cP_{k}$ s.t.\  a clause $P\If G$ is 
in $\cP_{i}$ iff every non-recursive head of $G$ is contained in 
$\bigcup\limits_{1\leq j < i}^{k}$
\end{Definition}

We denote with $S(P)$ the maximum stratum which contains $P$.  
Stratification is not unique and hence the following may seem to 
depend on the partition.  Nevertheless it is possible to make it
independent either considering equivalences classes on partitions or 
inducing a \emph{strict}, minimal partition from the dependency graph.

\begin{Theorem}[Partition Theorem]
\label{th:ppart}
For a decidable predicate definition $def(p)$ in $\cP$ over a 
stratification $S$ and and context $\GG$ and term $M$ on signature 
$\Sigma$
\begin{enumerate}
\item
(Exhaustivity) $\GG^{+}\prv p\ M$ or $\GG^{-}\prv \neg p\ M$
 \item
(Disjointness) It is not the case that $\GG^{+}\prv p\ M$ and 
$\GG^{-}\prv \neg p\ M$.
\end{enumerate}
\end{Theorem}
\begin{proof}
We give a proof by induction  (course-of-value and structural) on the 
lexicographically ordered pair $\la S(p),M\ra$  over $\Sigma$:

\bit
\item
 Base for $S(p)$: $p$ is defined at stratum 1: we show 
 $\GG^{+}\prv p\ M$ or $\GG^{-}\prv \neg p\ M$ by induction over $M$: 
 first observe that $p$ and $\neg p$ can depend only on its recursive 
 calls (for n-ary constructors):
 \bit
\item
Base for $M$: projection from $\xn$:
\ben
\item
 consider $p\ (\l\xn.x_{i})$; if $p\ (\l\xn.x_{i})\not\in 
 heads(def(p))$, then there is a clause in $def(p)$ of the form $\neg 
 p\ (\l\xn.x_{i})$.  Thus $1.$ holds trivially.  Otherwise $p\ 
 (\l\xn.x_{i})$ must match a fact, since $p$ cannot depend neither on 
 itself or on other predicates.  Hence $p\ (\l\xn.x_{i})$ holds and 
 thus $1.$
\item
 Suppose $p\ (\l\xn.x_{i})\And\neg p\ (\l\xn.x_{i})$ hold: then 
 $(\l\xn.x_{i}) \cap Not(\l\xn.x_{i}) \not=\eset$; but this is 
 impossible by the Partition lemma \ref{lemma:part} hence $2.$
Symmetrically for $\neg p\ (\l\xn.x_{i})$.
\newline
\noindent
 Analogously to projection for a unary  constructor.  
\enen
\item
Step for $M$: $n$-ary constructor:
 \ben
 \item % Exh
 the induction hypothesis is (pushing in the universals):
\beq
( \BAnd \limits^m_{j = 1} p\ (\l \xn .(Y_j \xn)) 
\And \BAnd \limits^q_{i = 1}\GG^{+} \Imp p\ (\l \xn.(E_i \  \xn\ 
z_{i}))) \Or\\
( \BOr \limits^m_{j = 1} \neg p\ (\l \xn .(Y_j \xn)) 
\Or \BOr \limits^q_{i = 1} \GG^{-} \Imp  \neg p\ (\l \xn.(E_i \  \xn\ 
z_{i})))
\eneq
By cases from IH:
\[
\begin{array}{ll}
(\BAnd \limits^m_{j = 1} p\ (\l \xn .(Y_j \xn)) \And 
\GG^{+} \Imp \BAnd \limits^q_{i = 1} p\ (\l \xn.(E_i \  \xn\ z_{i})))
& \mbox{first case}\\[2ex]
p\ (\l \xn . (a\ (\ol{Y_m \xn}) \ (\ol{E_q \xn})) 
& \mbox{inversion
% on $m$
}\\[2ex]
\GG^{+}\Imp p\ (\l \xn . (a\ (\ol{Y_m \xn}) \ (\ol{E_q \xn})) \Or 
\GG^{-}\Imp\neg p\ (\l \xn . (a\ (\ol{Y_m \xn}) \ (\ol{E_q \xn}))
& \mbox{weakening}
\\ \mbox{}\\
(\BOr \limits^m_{j = 1} \neg p\ (\l \xn .(Y_j \xn)) 
\Or \BOr \limits^q_{i = 1} \GG^{-} \Imp  \neg p\ (\l \xn.(E_i \  \xn\ 
z_{i}))) & \mbox{second case}\\[2ex]
\neg p\ (\l \xn . (a\ (\ol{Y_m \xn}) \ (\ol{E_q \xn})) 
& \mbox{inversion 
%on $\neg m$
}\\[2ex]
\GG^{+}\Imp p\ (\l \xn . (a\ (\ol{Y_m \xn}) \ (\ol{E_q \xn}))) \Or 
\GG^{-}\Imp\neg p\ (\l \xn . (a\ (\ol{Y_m \xn}) \ (\ol{E_q \xn})))
& \mbox{weakening}
\end{array}
\]

\item % Dsj
 the induction hypothesis is (pushing in the universals) 
\footnote{we use intuitionistic negation by 
falsehood to distinguish it here from the complement negation.}:
\beq
( (\BAnd \limits^m_{j = 1} p\ (\l \xn .(Y_j \xn)) 
\And \BAnd \limits^q_{i = 1}\GG^{+} \Imp p\ (\l \xn.(E_i \  \xn\ 
z_{i}))) \And\\
 (\BOr \limits^m_{j = 1} \neg p\ (\l \xn .(Y_j \xn)) 
\Or \BOr \limits^q_{i = 1} \GG^{-} \Imp  \neg p\ (\l \xn.(E_i \  \xn\ 
z_{i}))))  \\
\Imp \bot
\eneq

Again, suppose the negation of the thesis holds: but the result of applying 
inversion on both clauses $m$ and $\neg m$ contradicts the IH.

\enen % end of 1.2. for S=1.

\enit

\item
Step for $S(p)$: suppose $p$ is defined at stratum $i$ and every 
predicate in $G$ is defined at stratum $j < i$:
\ben
\item %Exh
Proceed as above, with the difference that if $p\ (\l \xn .  (a\ (\ol{Y_m \xn})
 \ (\ol{E_q \xn})))$ 
matches a clause $p\ N \If G$, we may use the induction hypothesis on 
$G$, since every predicate in the latter is defined at a lower stratum 
or is a recursive call on a smaller term. Hence infer $ \GG^+ (G) \prv 
G$ or $\GG^{-}(G) \prv\neg G$ and thus the thesis
\item %Disj
Again, suppose the negation of the thesis holds: but the result of applying 
inversion on both $m$ and $\neg m$ contradicts the IH which applies 
to $G$ and $\neg G$ as well to the recursive calls.

\enen %end 1.2 sor S>1
\enit
\end{proof}

\begin{Corollary}[Consistency]
If $def(p)$ is allowed, then $comp(dp)$ is consistent
\end{Corollary}

\bigskip We show that the augmentation is conservative \wrt the source 
language: indeed we need the following stronger (yet trivial) fact:

\begin{Definition}[Head]
 For every $G$ define $hd(\Pi\Xn:G_{n}.a) =a$\footnote{Put here?}
\end{Definition}

\begin{Lemma}
Let $m: P \If G$ and $m' : P \If (P_{1} \Imp G)$ s.t. $\neg(hd(G)\ 
dep\ P_{1})$ in $m$ \footnote{may just need $P_{1} \not\in \Sigma_{m}$}. Then
 ${\cP}\prv_{u} m >> Q$ iff ${\cP}\prv_{u} m' >> Q$, for every $Q,\cP$.
\end{Lemma}
\begin{proof}
Immediate
\end{proof}

 Since uniform provability is defined by two mutually 
recursive judgments, we generalize to the following statement; 
\begin{Ppn}
\label{ppn:cons}
\mbox{}
\begin{enumerate}
\item
${\cal D} :: \cP\prv G$ iff ${\cal D'} :: aug(\cP)\prv G$
%  for $\Sigma_{G} \subseteq \Sigma_{\cP}$
\item
${\cal I} :: \cP\prv m >> P$ iff ${\cal I'} :: \cP\prv aug(m) >> P$
\end{enumerate}
\end{Ppn}
\begin{proof}
Direction left-to-right follows immediately from weakening. Conversely 
we proceed by induction on $\cal D',I'$ using the above lemma
\end{proof}




