\subsection{Complementing \ho functions}

An useful optimization of the completion procedure 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 is inspired by a remark in \cite{Nai86}

\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

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

Still we may observe that $sub$ is a total function on the type 
$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\ P\ M\ N\If sub\ P\ M\ N^{'} \Imp \neqeb N N^{'}
\eneq
where the latter inequalities is computed through disunification. 
\end{Examplen}

To prove the correctness and completeness of this approach we extend 
$CET^{*}_{=_{\beta\eta}}$ with the axiom for existence and uniqueness 
for a functional relation $p$ and denoted the resulting theory 
$CET^{+}$:
\[
\forall\vX\exists !\vY:p\ \vX\ \vY
\]
\begin{Ppn}
$\forall \vX\vY: \neg p(\vX,vY) \Bimp \exists\vZ: 
p(\vX,\vZ)\And\neqeb \vY \vZ$
\end{Ppn}
\begin{proof}
Left-to-right employs existence: conversely use uniqueness.
\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$-- $\neg len2(+Nat,*List)$.
  
The requirement of totality cannot be dropped. 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 fail, since 
its positive complement must fail as well. 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.

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. We exemplify this phenomenon for the \fo horn 
case, since \ho program transformations have not been investigated yet.

\begin{Examplen}
\[
\begin{array}{l}
len (nil, 0).\\
len (X.XS, s(N)) :- len(XS ,N).\\
\mbox{}\\
\neg len (X.XS, M) :- len (XS, N), N\neq M.
\end{array}
\]
By unfolding on $len$ we get

\[
\begin{array}{l}
\neg len(nil, M) :- M \neq 0.\\
\neg len (X.XS, M) :- len (XS, N), s(N)\neq M.
\end{array}
\]
By computing sequentially the two disunification problems we have:
\[
\begin{array}{l}
\neg len(nil, s(_)).\\
\neg len(X.XS, 0).\\
\neg len (X.XS, M) :- len(XS, N), N\neq M.
\end{array}
\]
By folding the last clause we obtain the same recursive program for 
$\neg len$ that the compile-time method provide, \ie:
\[
\begin{array}{l}
\neg len (nil, s(N)).\\
\neg len (X.XS,0).\\
\neg len (X.XS, s(M)) :- \neg len(XS, M).
\end{array}
\]
\end{Examplen} 

This shows that for total function we may use directly disunification 
to the original program without going through the completion.
