\subsection{Complementing \ho functions}

An useful alternative to the complementation procedure described in 
\ref{} is possible when dealing with \emph{total functional 
relations}.  % As a matter of fact
% we need not consider the completion at all, but only rely on 
% disunification.
The idea, inspired by a remark in \cite{Nai86}, is to implement 
negation through inequality.

\begin{Examplen}
Consider a substitution predicate on lambda terms
\beq
sub & : & (exp \Imp exp) \Imp exp \Imp exp \Imp type\\
\skl
subl &:& sub\ (\lx x) \ M\ M\\
subap &:& \ldots\\
subl &:& sub\ \lx (lam\ \l y(E\ x\ y))\ M\ (lam\ (\l y . N\ y) \If\\
 & &
\Pi z: exp. (\Pi M^{'}:exp. sub(\lx z\ M^{'}\ z) \Imp sub\ \lx (E\ x\ 
z)\ M\ (N\ z)
\eneq

\ignore{The standard method would yield (for the interesting case)
\beq
Not(subl) &:& \neg sub\ \lx (lam\ \l y. (E\ x\ y))\ M\ (lam\ (\l y . N\ y)) 
\If\\
& &
(\Pi z: exp. (\Pi M^{'} M^{''}:exp. \neg sub(\lx z\ M^{'}\ M^{''}) \If 
 M^{''} \nebe z))\\
 & & \Imp sub\ \lx (E\ x\ z)\ M\ (N\ z)
\eneq
}
\noindent
Still we may observe that $sub$ is a total function on the type 
$(exp\Imp exp)\Imp exp$, that is it can be called with mode $\la +,+,-\ra$. 
Thus me may define $\neg sub$ simply as:
\beq
Not(sub) &:& \neg sub\ F\ M\ N\If sub\ F\ M\ N^{'} \Imp  N\nebe N^{'}
\eneq
\end{Examplen}

More in general, consider  a functional relation $p$: we can specify 
its complement as 
\[
\forall \vX\exists\vY. \neg p(\vX,\vY) \Bimp p(\vX,\vZ)\And  \vY \nebe\vZ
\]
The correctness and completeness of this specification is proved as 
follows: consider the  axioms for existence and uniqueness for a 
functional relation $p$:
\beq
E & : & \forall\vX\exists \vY.p\ \vX\ \vY\\
U & : & \forall\vX\exists \vY\exists \vZ.p\ \vX\ \vY\And p\ \vX\ \vZ 
\Imp \vY\ebe\vZ
\eneq

\begin{Ppn}
$E,U\prv\forall \vX\exists\vY. \neg p(\vX,\vY) \Bimp \exists\vZ.
p(\vX,\vZ)\And  \vY \nebe\vZ$.
\end{Ppn}
\begin{proof}
Left-to-right employs existence: conversely assume $ \exists\vZ. 
p(\vX,\vZ)\And \vY \nebe\vZ$ and at the same time $p(\vX,\vY)$: by 
axiom $U$ we infer $\vY \ebe\vZ$, absurdum, hence $\forall 
\vX\exists\vY. \neg p(\vX,\vY)$.
\end{proof}

Predicates which, according to different moding, implement different 
types of functions yield differently negated functions accordingly.  
For instance the length function on lists $len : natlist \Imp 
nat\Imp type$ with moding $\la +,-\ra$ yields $\neg 
len1(+List,*Nat)$ and for $\la -,+\ra$ --which computes an 
incomplete list of length $N$, \ie $\neg len2(+Nat,*List)$.
  
The two requirements of cannot be dropped. 
\ben
\item Functionality: if a relation is not functional, we have then a 
vector of inequalities: as usual they cannot be computed 
independently, but they need to be combined either with the $\oplus$ 
operator or by considering the equational problem consisting in 
the (simultaneous) conjunction of the inequalities.
\item
Totality.  If a function is partial, its complement contains not only 
for which the function is false but also the ones where it is 
undefined.  In the latter case the call to the positive occurrence 
will fail.  Consider the typing example: $\neg of : exp \Imp tp\Imp 
type$ holds not only when a well-typed expression does not have a 
given type, but also for any ill-typed (in the object language) 
expression.  Still a call say to $\neg of\ (app\ (lam\ (\lx x)) (lam\ 
(\lx x)))\ nat$ will should be provable will fail, since its positive complement must fail as 
well.  Of course every partial function can be made total by adding a 
`catch-all' clause: but then we should add to the latter something 
like a cut, erasing the benefits of the transformational 
approach.
\ignore{Pragmatically, we can envision a system enforcing totality 
through annotations either given by the user or mechanically generated 
for programs satisfying some strict syntactical requirement}.
  \enen % 
% Let us compare the two approaches as far as computational efficiency
% is concerned: while for ground queries they are clearly equivalent, 
% for open queries the compiled one is superior as it computes 
% statically those explosions (in number proportional to the size of 
% input terms) that the run-time version is deemed to compute 
% dynamically. Nevertheless fold-unfold transformations make the two 
% approaches equivalent. 

The issue is now how to resolve inequalities: the possibilities are:
\ben
\item
Solving them inside the interpreter that would be equipped with a 
subset of the disunification rules.
\item
Synthesize for every type its \texttt{noncopy} program
\item
Eliminate them with fold-unfold transformations
\enen

Pros and cons:
\ben
\item
Though the disunification rules for complement problems are not too 
many, they still need some control. This goes against the CLP attitude 
that postpone hard problems. For open queries it would not suffice, on 
the other hand, to keep them as constraints, as there is in general no 
guarantee they would get sufficiently instantiated: they are after all 
the main goal of the computation.
\item
This entails going beyond second-order, even though for the 
\texttt{noncopy} program only. Showing the latter adequate would 
require the development of complementation in the algebraic form. The 
net gain would be only on total functions with local variables
\item
fold-unfold transformations notoriously require a degree of ingenuity. 
While describing a non-deterministic system seems feasible, turning it 
into a deterministic algorithm like complementation looks more 
problematic, though not impossible. Besides, prametrical programs 
still need to be augmented.
\enen

We exemplify the last method:

\begin{Examplen}
\[
\begin{array}{lll}
lnil &:& len (nil, 0).\\
lcons & : & len (X.XS, s(N)) \If len(XS ,N).\\
\mbox{}\\
nl & : & \neg len (L, M) \If len (L, N), N\neq M.
\end{array}
\]
By unfolding on $len$ we get
\[
\begin{array}{lll}
u(nl,lnil) &:& \neg len(nil, M) \If M \neq 0.\\
u(nl,lcons) &:&\neg len (X.XS, M) \If len (XS, N), s(N)\neq M.
\end{array}
\]
By computing  the two complement problems and dropping the useless 
body we have:
\[
\begin{array}{lll}
nlnil & : & \neg len(nil, s(N)).\\
nlcons1 & : & \neg len(X.XS, 0).\\
\end{array}
\]
By folding $u(nl,lcons)$ with $nl$ we get: 
\[
\begin{array}{lll}
nlcons2 & : & \neg len (X.XS, s(M)) \If \neg len(XS, M).
\end{array}
\]
\ie the same recursive program for $\neg len$ that the compile-time method provides
\end{Examplen} 

