\chapter{The Relative  Complement Problem}
\label{ch:el-rel}  



An open term $t$  in a given signature can be seen as the intensional
representation of the set of its ground instances, say $\| t \|$.
According to this interpretation, the {\em complement} of $t$ is the
set of ground terms which are \emph{not} instances of $t$, \ie are in
the set-theoretic complement of $\| t \|$.  It is natural to
generalize this to the notion of {\em relative} complement; this
corresponds to computing a suitable representation of all the ground
instances of a given (finite) set of terms which are not instances of
another given one, in symbols:
\[ \| t_1 \mdots t_n \| - \| u_1 \mdots u_m \| \] 
where dots 
represent (set theoretic) union\footnote{Another equivalent notation 
found in the literature is $ t_1 \Or \cdots \Or t_n \setminus u_1 \Or 
\cdots \Or u_m$ \cite{Lassez87}, or a mixture of the two.}.  More 
properly:
 \[ \| t_1 \mdots t_n \| \eqdef \bigcup^{n}_{i=1} \|t_i\| \] 
Let $FV(t_1 \mdots t_n) = \vx$ disjoint from $FV(u_1 \mdots u_m) = \vy$.  Then the relative 
complement problem can be also expressed by the following (restricted) form
of \emph{equational problem} \cite{Comon91}, where the $z_i$'s are
free variables.  
\[ \exists \vx 
\forall \vy : \BAnd^{n}_{i=1} z_i = t_i \And \bigwedge^{m}_{i=1} z_i 
\nq u_{i} \]
% With no loss of generality we will take $n=1$.
%  indeed: \[ 
% \| t_1 \mdots t_n \| - \| u_1 \mdots u_m \| = \bigcup^{n}_{i=1}(\|t_i 
% \| - \| u_1 \mdots u_m \| ) \] which corresponds to 
% \[ 
% \BAnd^{n}_{i=1}(\exists \vx_i \forall \vy : z_i = t_i \And 
% \bigwedge^{m}_{j=1} z_i \nq u_{j}) \]

\begin{Example}
Consider the signature containing the usual declarations for $0,s,+$.
The following rules define integer addition modulo $2$.  
\beq
\label{ex:mod2}
s(s(0)) & \Lmap & 0\\
y+0 & \Lmap & y\\
0+y & \Lmap & y\\
y+y & \Lmap & 0 \eneq 

The following relative complement problem expresses the question of sufficient completeness (in this case yielding a 
positive answer) of the rewrite rules:
\[
\| x_1 + x_2\| - \|s(s(0)),0+y,y+0,y+y \|
\]
which corresponds to
\[
\exists x_1x_2\forall y : (z= x_1 + x_2) \And (z \nq s(s(0)))\And (z \nq
y+0)\And (z \nq 0+y)\And (z \nq y+y)
\]
\end{Example}

Then, since a variable stands for the universe of discourse, a {\em
complement problem} is representable merely by $$ \| z\| - \| u_1
\mdots u_m \|$$ or a simpler ($\exists$-degenerate)  equational
problem:
\[ 
\forall \vy : \bigwedge\limits^{m}_{i=1} z \nq u_{i}
\]

Now we turn to review solutions to the relative complement problem in
\fo languages.

\section{The  Not  Algorithm}
\label{sec:bnot}

We start with the `\mnot' algorithm for first-order terms that
specializes the  prototypical {\em 
uncover} algorithm proposed in \cite{Lassez87} as a first attempt to 
solve the the problem and is at the heart of Barbuti et al.'s
approach \cite{Bar90}.  We present it in a many-sorted framework,
differently from the uni-sorted original version. We call (in this
chapter) a term \emph{linear} if it does not contain repeated
occurrences of a free variable.

\begin{Definition}
\label{def:focompl}
Consider a many-sorted  signature $\Sigma$ and a linear term 
$t: \tau$.  We define $\mnot(t)$ by structural induction, where we 
suppose that $t_i$ has sort $\tau_i$ and the $z$'s are new free
variables of appropriate typing:
\[ \begin{array} {lll}
\mnot(z \hastype \tau) & =   \emptyset \\
\mnot(f(\tn) \hastype \tau) & = & \\
 & \{g(\ol{z_m}) \hastype \tau \mid g \in \Sigma, g\not\equiv f, g\hastype \ol{\tau_m}\Imp\tau\} \cup \mbox{} 
\\
& \{f(z_1 \mdots z_{i-1},s,z_{i+1}, \dots,z_n) \hastype \tau \mid
s\in\mnot(t_{i}), 1\leq i n \}
\end{array} \]
\end{Definition} 

%Standard Prolog is not typed: this means that
The uni-sorted version of this function tends to produce a lot of
irrelevant outcomes.  For example, $\mnot(cons(s(x),nil))$ does not yield only
the desired $\{nil,cons(0,nil),cons(y,cons(z,xs))\}$ in the informal signature of lists
of numerals but also $\{0,s(x),\dots\}$.  On the other hand, fixing
$$\Sigma = \{0 \hastype nat , nil \hastype nlist , s \hastype nat \Imp nat, cons \hastype nat * nlist \Imp nlist \}$$
we get the desired result.  This problem may
tend to increase dramatically with the size of the signature. It can
be argued that the notion of complementation itself without an
underlying type discipline makes little sense, not only from a
complexity standpoint, but also in intellectual terms.  Moreover, more
refined type theories, as dependent types and\slash or sub-typing will
further constrain the result of the evaluation of $\mnot$.

\smallskip
A complement operator must satisfy the following desiderata: \ben
\item Exclusivity: it is not the case that $s$ is both a ground
instance of $t$ and of $\mnot(t)$.
\item Exhaustivity: $s$ is a ground instance of $t$ or $s$ is a
ground instance of $\mnot(t)$.  \enen

% \label{t:bar}
% Let $\vt$ be linear, $\mnot(\vt) = \{ \vt^c_1 \mdots 
% \vt^c_n\}$ and $\vx$ a tuple of fresh variables.  Then
% $E_{\Sigma T\cup DCA} \models \forall \vx(\forall(\vx \neq \vt) 
% \Bimp \BOr^n_{i=1} \exists (\vx =\vt^c_i))$.
% \end{Theorem}
%\end{sloppypar}
% This equivalence is crucial, inasmuch it allows to substitute a 
% complement problems with a set of positive terms.  This is actually 
% nothing more than a Corollary of Theorem \ref{thm:LM}, that we discuss 
% now.  
% % Reconsidering Example~\ref{eqb: odd},
% Considering the equational problem $\forall y: z \neq 0 \And z \neq 
% s(s(y))$ you would expect first to compute $\mnot(0) = \{s(x)\}$, then 
% $\mnot(s(s(y))) = \{0,s(0)\}$ and eventually somehow `anding' the result 
% to come up with the expected outcome $s(0)$.  This computation is 
% instead executed sequentially inside the transformation technique, as 
% discussed in Section~\ref{comparison}, and for some good reasons.
That is, the \mnot\ algorithm ought to behave as a the complement
operation on sets of ground terms. This cannot be achieved in all
generality.  In other words, intensional representations of terms are
not closed under complementation.  One canonical example is as
follows:
\begin{Example}
\label{ex:fyy}
Consider the signature $\{a:i, f: (i * i) \Imp i\}$: intuitively the
complement of $f(y,y)$ should be: \beq
\label{fxx}
\| z \| - \|f(y,y)\|& =& \{a\} \cup \{ f(x,z) \mid x \nq z \} \eneq
Instead, the $\mnot$ algorithm would incorrectly yield:
\[
\mnot(f(y,y)) \stackrel{?}{=} \{a\}
\]
\end{Example}
In fact, Lassez \& Marriot \cite{Lassez87} have been the first to
point out that this complement algorithm is correct only for {\em linear}
terms: complement of non-linear ones do not have a straightforward
finite representation. More sophisticated representation, such as
\emph{constrained terms} \cite{Comon88} have been investigated,
but are not suitable to our applications.

% THINK about unrestricted

% \begin{Theorem}[\cite{Lassez87}] 
% \label{thm:LM}
% There is an explicit representations of $\| t\| -
% \|t_1\mdots t_n\|$ iff the signature is finite and $t_1\mdots t_n$
% are unrestricted \wrt $t$. In particular, let $\q_i$ be the mgu of 
% $t$ and $t_i$: then there is a $\cal U$ so that ${\cal U} 
% \approx_{\Sigma(T)} {\cal P}_{t;t_1 \mdots t_n}$ iff there is $\phi_i 
% t$ such that $\| \phi_i t\| =\|\q_i t\|$ and $\phi_i t$ is 
% unrestricted \wrt $t$ for $i \in [1,n]$.
% \end{Theorem}
%This has been further generalized by Comon \cite{Comon89}.
% 
% \begin{Corollary}
% \label{claim:uncover}
% Let ${\cal U} \approx {\cal P}_{t;t_1 \mdots t_n}$ and let $\exists 
% \vx \forall \vy : \BAnd^{n}_{i=1} z_i = t_i \And 
% \bigwedge^{m}_{i=1} z_i \nq u_{i}$ rewrite to the unification 
% solved form $\exists \vx : P^*$. Then ${\cal S(U)= S}(\exists \vx : 
% P^*)$
% \end{Corollary}

%\smallskip
Moreover, as well known, the restriction to linearity seems to be almost
immaterial in \lp thanks to the idea of {\em left-linearization}
introduced by Plaisted and used first by Stickel \cite{Stickel88} to
avoid unnecessary occur checks testing.  It simply consists of a
source-to-source transformation which replaces repeated occurrence of
the same variable in a clause head with new variables which are
then constrained in the body by a new predicate, say $eq$, whose definition
is simply $eq(x,x)$; unification will then provide the other
properties of equality.  For example, continuing Example \ref{ex:fyy},
a clause such as $\forall y\,.\, p(y,y)\If G$ would be replaced by $\forall
z_1.\,\forall z_2\,.\, p(z_1,z_2)\If eq(z_1,z_2)\And G$.  As a matter of fact,
this approach is less innocent as it looks at first sight, since it
opens the road to a CLP attitude; moreover, $eq$ as a predicate is
\emph{not} linear in itself and required an ad hoc treatment in the
transformational approach to negation \cite{Bar90}.  Miller
\cite{Miller89iclp} has shown how to automatically infer the equality
predicate (the so-called \texttt{copy} clause) for any type. However,
for any order greater than the first, this clauses are not Horn
and their negation is itself problematic. One of the result in this
dissertation is to apply elimination of negation to predicates such as
\texttt{copy}.

\smallskip

Once we have a way to solve complement problems, it is easy to pair
it to intersection, seen as unification \cite{Plotkin71}, to have a
solution to relative complements as well, \ie

\beq 
\| t_1 \| - \| u_1 \mdots u_m \|& \eqdef &
\|t_1\|\cap\|\mnot(u_1)\|\cap\dots\cap\|\mnot(u_m) \| 
\eneq 

Another more general approach is possible. As we have seen in the
beginning, it is possible to express the (relative) complement problem
on terms as an equational problem.  This is the basis to solve
complement problems with disunification, as we sketch next.

\section{Disunification}
\label{sec:disunif}
Disunification is devoted to solving {\em arbitrary} first order
formulae whose only predicate symbol is equality, call them {\em
  equational formulae}.  The definition of what a {\em solution} is
differs on the application at hand. We may be interested only in the
overall validity or in the possible assignments that make the formula
valid.  As we have seen, complement problems can be seen as systems of
disequations with universally quantified variables. 
Thus a disunification algorithm (over \fo terms) will solve 
these problems, possibly providing values for free 
variables.


From an historic perspective this field became defined when it was
realized by Martelli \& Montanari \cite{Martelli82}, if not by Herbrand
(see the Appendix in \cite{Snyder91}) that \fo unification can be seen
as a transformation on sets of equations.  On the other hand the work
of Mal'cev \cite{Mal71} on the decidability and the possibility to
give complete axiomatization of the theory of equational algebras
qualifies as an ancestor.  The definition of Prolog-II introduced
first-class disequations. Indeed Colmerauer \cite{Col84} showed them
to have solutions in the algebra of rational trees.  Next Lassez \&
Marriot \cite{Lassez87} proposed the seminal (although awkward) {\em
  uncover} algorithm for computing relative complements.  Kirchner and
Lescanne first unified those previous papers in the framework of
equational problems and proposed a set of transformational rules,
though without a completeness proof \cite{Kir87}.  Maher introduced
the unification community to Mal'cev's results \cite{Maher88}. Comon
and Lescanne were the first one to present an adequate set of rules
\cite{Comon88,CL89} and the former surveyed the field \cite{Comon91}.

\smallskip

How to go on to derive a disunification procedure can  vary 
from the syntax and semantics we are concerned with, but 
nevertheless it entails the following steps:
\bit
\item Provide a set of axioms $\cal T$ that hold in the model we
  consider.
\item Design a set of rules $\cal R$ for the transformation of
  equational formulae that can be proven correct w.r.t.\ $\cal T$.
\item Design a control $C$ on $\cal R$ such that the application of
  rules satisfying $C$ terminates: irreducible formulae are in
  solved form and have the same set of solutions as the original
  problem.
\item If arbitrary formulae are allowed and solved forms are trivially
  decidable, this entails the decidability and completeness of $\cal
  T$.  
\enit

The simplest example is unification of finite (first-order) terms: 
\bit
\item $\cal T$ is Clark's free equality theory \cite{Cla78}.
\item ${\cal R}$ are, say, the Martelli-Montanari rules; correctness
  corresponds to the preservation of solutions under rule application.
\item Solved forms yield idempotent substitutions and control
  restricts the application of variable elimination. Completeness (of
  the theory) is established for example as in \cite{Maher88}.  
\enit

The disunification rewrite rules are divided into three big classes:
\bit
\item Equality rules, \ie rules which are correct for any equational
  algebra
\item Rules for finite trees over any signature
\item Rules for finite trees over a finite signature.  
\enit

We will not present the complete set of rules with logical provisos
and control.  We just mention that the first group contains
Replacement, Universal Quantifier Elimination, Existential Quantifier
Elimination and Elimination of Disjunctions.  The second batch contain
Clash, Decomposition, Occur check. The third section would contain
rules which are sensitive to the cardinality of the signature. Here we
mention only the Explosion rule (E), which is motivated by the domain
closure axiom (\emph{DCA}) \cite{Mancarella88}.  We list in
Figure~\ref{fig:fo-disunif} the rules relevant to the following
example in their barest form, \ie with only soundness and no
termination condition:


\begin{figure}
\[
\fbox{$\vspace{2em}
\begin{array} {lllll}
R & : & w=t \And P[w] & \Lmap & w=t \And [t/w]P\\
M1 & : & w=t \And w\not=u & \Lmap & w=t \And t\not = u\\
UE1 & : & \forall \vy,y \,.\, P \And y \neq t & \Lmap & \bot\\
% % UE2 & : & \forall \vy,y   \,.\, P \Or y \neq t & \Lmap & \forall \vy  \,.\, 
% [t/y] P\footnote{Used?}
% \\
Clh(T) & : & f(\tn) \nq g(\sm) & \Lmap & \top\\
Clh(F) & : & f(\tn) = g(\sm) & \Lmap & \bot\\
Dec1 & : & f(\tn) \neq f(\un) & \Lmap & \BOr\limits^{n}_{i=1} t_i \neq 
u_i\\
Dec2 & : & f(\tn) = f(\un) & \Lmap & \BAnd\limits^{n}_{i=1} t_i = 
u_i\\
E & : & \forall \vy \,.\, P & \Lmap & \BOr\limits_{f \in \Sigma} (\exists 
\vx \forall \vy \,.\, P \And w  = f(\vx))
\end{array}
$}
\]
In  rule $R$ $w \not \in Var(t)$, in  $E$, $P$ contains a 
(dis)equation with LHS $w$ and RHS $u$, where the latter is not a 
variable and contains a universally quantified variable.
\caption{Some disunification rules}
\label{fig:fo-disunif}
\end{figure}


\smallskip

We now give an example of disunification on the numerals signature,
which is required in the synthesis of the {\tt odd} program (see
Figure~\ref{fig:comp_even}). It consists in solving:
\begin{eqnarray}
\label{eqb: odd}
\forall y:z \not= 0 \And  z \not= ssy
\end{eqnarray}
The intuitive solution of (\ref{eqb: odd}) is $z = s(0)$.  We will use
the rules in Figure~\ref{fig:fo-disunif} and gloss over normalization
steps as well as elimination of trivial (dis)equations.  Branches stemming
from the explosion rule are numbered and pursued separately (keeping
in mind that they form a disjunction, \ie a finitely branching tree
from a search standpoint).  $R(x)$ denote application of the rule $R$
on variable $x$. The computation is traced in Figure~\ref{ex:num}.

\begin{figure}
\[ \begin{array} {ll}
\fbox{$\forall y: z \not= 0 \And z \not= ssy$}\\
\Lmap_{E(z)(1,2)}\\
& (1) \ \forall y: z \not= 0 \And z \not= ssy \And z=0\\
\Lmap_{M1(z)}\\
& \forall y: 0 \not= 0 \And 0 \not= ssy \And z=0\\
\Lmap ^*_{Clh(F)} \fbox{$\bot$}\\
& (2) \ \exists x \forall y: z \not= 0 \And z \not= ssy \And z=sx\\
\Lmap_{M1(z)}\\
& \exists x   \forall y: sx \not= 0 \And sx \not= ssy \And z=sx\\
\Lmap^*_{Dec,Clh(T)}\\
& \exists x \forall y: x \not= sy \And z=sx\\
\Lmap_{E(x)(2.1,2.2)}\\
&(2.1) \ \exists  x \forall y: x \not= sy \And z=sx 
\And x =0\\
\Lmap_{M1(z)}\\
&  \exists  x \forall y: 0 \not= sy \And z=s(0) 
\And x =0\\
\Lmap^*_{Clh(T)} \fbox{$z=s(0)$}\\
& (2.2)  \ \exists x_1 x \forall y: x \not= sy \And z=sx \And x 
=sx_1 \\
\Lmap^*_{M1(x),Dec1} \\
& \exists x_1 x \forall y: x_{1} \not= y \And z=sx \And x 
=sx_1 \\
\Lmap^*_{UE_1(y)}  \fbox{$\bot$}
\end{array} \]
\caption{Computation of $\forall y:z \not= 0 \And  z \not= ssy$}
\label{ex:num}
\end{figure}

Note that disunification nicely overcomes the difference between {\em linear}
and {\em non-linear\/} terms with  different notions of  solved
forms, namely {\em unification} solved form versus  solved form with
disequations \cite{Comon91}.  This may be interpreted as evidence of
the opportunity of rephrasing unrestricted relative complements as
disunification problems. We, on the other hand, maintain that this
approach is unnecessarily general for this purpose.
Implementing disunification entails managing the non-deterministic
application of a few dozen rules which eventually turns a given
problem into a solved form.  Though a reduction to a significant
subset of the disunification rules as the one depicted in
Figure~\ref{fig:fo-disunif} is likely to be attainable for complement
problems, control is a major problem. 
%We argue that using disunification for this purpose is unnecessarily general. 
 Moreover
the \ho case results in additional complications, such as restrictions
on the occurrences of bound variables, which fall outside an otherwise
clean framework.  As we show in this dissertation, this must not
necessarily be the case.  We believe that our techniques for the \ho
case can also be applied to analyze disunification, although we have
not investigated this possibility at present.


%\input{shortdis}
% Anyway, this is not the only road that can be traveled. We may be 
% using: 
% \bit
% \item
% {\em Regular tree languages} to describe (unary) types 
% \cite{Gec84,Pfe92b}.
% \item
%  {\em Constrained terms} \cite{Comon88,Com91b}
% \item
% Complement operations based on  disunification.
% \enit

% Both the first and second approaches\footnote{which are not disjoint, 
% if we wish to use as in \cite{Comon91b} (order) sorted signatures, as 
% the latter are identified with finite bottom-up tree automata, where 
% the sorts are the states and the function symbols are the terminal 
% alphabet.  More details in the cited report.} enjoy closure under 
% complementation.  The last one seems to have the required amount of 
% elegance and generality at the cost of an increased technical 
% complexity.


\section{Other Applications}
\label{sec:others-compl}

Complement problems and elimination of negation are not restricted to 
logic programming, but have some other relevant application in theoretical computer 
science.  Let me refer to \cite{Lassez91} and \cite{Comon91} for issues 
impossible to detail here and for complete references.

In fact, complement problems and variants of the  {\em 
uncover} algorithm  \cite{Lassez87} as a first attempt to 
solve the former, have been studied and tentatively applied in several 
ways:
\begin{itemize}
\item In functional programming, to determine, modulo pattern
  matching, whether the program clauses describing a function are
  exhaustive and disjoint, even further to produce a non-ambiguous set
  of patterns.  Moreover, it is possible to take advantage of the given
  sequential application of the rules to provide an improved compiled
  code.  Indeed, if, say, the second rule applies, it means the first
  one does not: hence the terms reducible by the second rule are in
  the complement of the LHS of the first.
\item The connection of complementation to the notion of {\em ground
    reducibility} in term rewriting systems makes it a candidate as a
  checker for {\em sufficient completeness} \cite{GH78} of an
  algebraic (equational) specification.  If the latter fails to be
  complete, the transformation rules my lead to recover the missing
  cases---hence the motto in \cite{Thiel84}:
\begin{quote}
``Stop losing sleep over incomplete specifications''
\end{quote}
Here we are looking for counter-examples: if a function is not
sufficiently complete, there is a term, built from the constructors in
the signature, which is different from any LHS, thus irreducible (see
Example~\ref{ex:mod2}).
\item In term rewriting systems describing infinite transition
  systems, the complement of a LHS returns the states from which no
  transition is achievable, providing thusly a tool for the temporal
  analysis of communicating processes.
\item In machine learning, a concept can be captured by a term with
  some (finite) exceptions: the computation of this structure, which
  is a relative complement, coincides with the search for an explicit
  representation of the cited concept.
\item Finally, applications to inductive theorem proving under the
  slogan {\em induction-less induction} or \emph{proof by consistency}
  \cite{Comon98} are under scrutiny.  This is connected to the idea of
  the so-called \emph{inductive reducibility} property.  
% Roughly,
%   given a rewrite system, a term $t$ is inductively irreducible, \ie
%   its set of irreducible instances is obtained by computing the
%   complement of the latter into the LHS of the system.
 \end {itemize}

We now switch gears and discuss the extension of the relative
complement problem to the \ho case; as usual, we restrict ourselves
to a specific class of $\l$-terms.


\section{Complementing Higher-Order Patterns}
\label{sec:hocomplement}
\renewcommand{\S}{\Sigma}

In most functional and logic programming languages the notion of a
pattern, together with the requisite algorithms for matching or
unification, play an important role in the operational semantics.  And,
of course, patterns form the left-hand sides of rewrite rules and are
thus critical to the study of rewrite systems.  Consequently, analysis
of the structure of patterns is an important task in the implementation
of programming languages and more abstract studies of rewriting systems
and their properties.

Perhaps the most fundamental problems are matching and unification,
but other questions such as generalization also arise frequently.
Here, we are concerned with the problem of pattern complement in a
setting were patterns may contain binding operators, so-called
\emph{higher-order patterns} \cite{Miller91jlc,Nipkow91lics}. A term
possibly containing some existential variables is called a
\emph{pattern} if each occurrence of an existential variable has the
form $E\ x_1\ldots x_n$, where the arguments $x_i$ are distinct
occurrences of free or bound variables (but not existential
variables).  Higher-order patterns have found applications in logic
programming \cite{Miller91jlc,Pfenning91lf,Michaylov93}, logical
frameworks \cite{Despeyroux97}, term rewriting~\cite{Nipkow93tlca},
and functional logic programming~\cite{Hanus96RTA}.  Higher-order
patterns inherit many pleasant properties from the first-order case.
In particular, most general unifiers~\cite{Miller91jlc} and least
general generalizations~\cite{Pfenning91lics} exist, even for complex
type theories.

In this section we discuss some of the preliminary issues towards a
generalization to the complement algorithm to \ho patterns.  We assume
the following: \bit
\item All terms are linear, \ie existential variables occurs only once.  
\item Types do not contain occurrences of the primitive type $\prop$.
  We thus complement only terms with no inner logical structure. 
% Note of course that this is the restriction
%  intrinsic in the \emph{LF} type theory \cite{Harper93jacm}.  
\enit

% \begin{Definition}[Higher-Order Pattern]
% A term $M$ in canonical form is a \emph{\ho pattern} if every free 
% occurrence of a variable $F$ is in a subterm $F(\xn)$ of $M$ such 
% that $\xn$ is a list of distinct bound variables.
% \end{Definition}

The main difference \wrt the \fo case is twofold: first, the 
second-order (relative) complement  problem is not semi-decidable, but
higher-order disunification on \ho patterns is decidable \cite{Lugiez94}.
 
Secondly, as we will see, the class of patterns is \emph{not} closed
under complement, although a special subclass is.  We call a canonical
pattern $\Gamma \vd M \hastype A$ \emph{fully applied} if each
occurrence of an existential variable $E$ under binders
$y_1,\ldots,y_m$ is applied to some permutation of the variables in
$\Gamma$ and $y_1,\ldots,y_m$.  This is formally defined in
Figure~\ref{fig:fa}.  Fully applied patterns play an important role in
functional logic programming and rewriting~\cite{Hanus96RTA} because
any fully applied existential variable $\Gamma \vd E\ x_1\ldots x_n$
denotes all canonical terms with free variables from $\Gamma$.  It is
this property which makes complementation particularly simple. In
fact, the main difference with the \fo case is that we need to
carefully keep track of bound variables: those are collected in a
context $\GG$, so that the complement of a rigid term is taken \wrt
both the signature and the current context.  In the case the term is
\emph{not} fully applied, the complement has to take into account
whether some of the variables mentioned in a lambda binder do appear
in the matrix; we discuss this in the next Section \ref{sec:nfa}.  We
first analyze the simpler case.


\begin{figure}
\[
\begin{array}{c}
\ianc{\ol{y_{\pi(n)}}=\dom(\GG)}{\GG\prvs  F\ \yn \fa }{\mbox{\tt faPat}} 
\qquad 
\ianc{ \GG,\of{x}{A}\prvs  M \fa }{\GG\prvs \lxa M \fa }
{\mbox{\tt faLam}}\vsk
\ianc{ h \in\Gamma\cup\Sigma \qquad \GG\prvs  N_{1} \fa
\cdots \GG\prvs  N_{n} \fa}
{\GG\prvs h\  \Nn \fa } {\mbox{\tt faApp}}
\end{array}
\]
\caption{$M$ is a fully applied pattern: $\GG\prvs  M \fa$}
\label{fig:fa}  
\end{figure}


\medskip

The language of the simply-typed $\l$-calculus is as follows, where we
use $a$  for atomic types (different from the type of proposition \prop), $c$ for term-level constants, and 
$x$ for term-level variables, while $h$ will stand for a constant
\emph{or} a variable.

\[ \begin{array}{rrcl}
 \mbox{\textit{Simple Types}} & A & \bnfas & a \bnfalt A_1 \arrow A_2 \\
 \mbox{\textit{Terms}} & M & \bnfas & c \bnfalt x \bnfalt \lam x\oftp
A\ldot M \bnfalt M_1\ M_2 \\
 \mbox{\textit{Signatures}} & \Sigma & \bnfas & \cdot \bnfalt \Sigma, a
\oftp \mbox{type} \bnfalt \Sigma, c\oftp A \\
 \mbox{\textit{Contexts}} & \Gamma & \bnfas & \cdot \bnfalt \Gamma, x\oftp A
\end{array} \]

We require that signatures and contexts declare each constant or
variable at most once so that, for example, when we write $\Gamma,
x\oftp A$, $x$ may not already be declared in $\Gamma$.  Furthermore, we
identify contexts which differ only in their order, in other words,
contexts are treated as sets of declarations for distinct variables. We promote ``,'' to 
denote \emph{disjoint} set union.  As usual we identify
terms which differ only in the names of their bound variables.  We
restrict attention to well-typed terms, omitting the standard typing
rules.

In applications such a logic programming or logical frameworks,
$\lambda$-abstraction is used to represent binding operators in some
object language.  In such a situation the most  normal
forms are long $\beta\eta$-normal forms (which we call \emph{canonical
forms}), since the canonical forms are almost always the terms in
bijective correspondence with the objects we are trying to represent.
Every well-typed term in the simply-typed $\lambda$-calculus has a
unique canonical form---a property which persists in the strict
$\lambda$-calculus introduced in Chapter \ref{cap:strict}.  See that
chapter for further discussion and an inductive definition of
canonical forms.

We denote existential variables of type $A$ (also called logical
variables, meta-variables, or pattern variables) by $E_A$, although we
mostly omit the type $A$ when it is clear from the context.  We think of
existential variables as syntactically distinct from bound variables or
free variables declared in a context.  

Semantically, an existential variable $E_A$ stands for all canonical
terms $M$ of type $A$ in the \textrm{empty} context with respect to a
given signature.  We extend this to arbitrary well-typed terms in the
usual way, and write $\| M\|$ for the set of canonical ground instances
of a term $M$ possibly containing existential variables (see
Figure~\ref{fig:grinst}).  In this setting,
unification of two patterns corresponds to an intersection of the set of
terms they denote~\cite{Miller91jlc,Pfenning91lics}.  This set is always
either empty, or can be expressed again as the set of instances of a
single pattern.  That is, patterns admit most general unifiers.


% Alternative example
% red(all(\l x^u. P x^0, P x^0)
% equiv(all(\l x^u. or(A x^u, B x^0)), or(all(\l x^u A x^u), B))
% \begin{example}
% Suppose we want to model predicates on the signature of the 
% implicational-universal fragment of \fo logic.
%  We introduce the following signature, which 
% declares constants of well-known meaning and type (see 
% \cite{Miller91jlc}).
% \beq
% \Sigma  & \bnfas & term\oftp \mbox{\textrm{type}},form\oftp \mbox{\textrm{type}},
%  all\oftp (exp\Imp 
% exp)\Imp exp, imp \oftp exp \Imp exp\Imp exp\\
% E & \bnfas & x \mid all\ (\lx E) \mid imp \ E_{1} E_{2}
% \eneq
% As usual with \ho abstract syntax \cite{Pfenning88pldi}, we identify the name of 
% (bound) variables in both languages.  \ignore{It is maybe worthwhile 
% to stress that we have three layers: the object language, the 
% (untyped) $\l$-calculus, the meta-language, our \ho logic or type 
% theory (whose variables are called \emph{logical} variables) and the 
% meta-meta language, the informal mathematical one used to describe the 
% former.   The adequacy of the encoding (proved for in 
% \cite{Hansell92jacm}) bijectively relates $\alpha$-equivalence classes 
% of object-level terms with $\beta\eta$-equivalence classes at the 
% meta-level.}  
% The term $\lamb{x} {term} imp \ (E_{1}\ x) (E_{2}\ x)$ represents the set
% of all unary functions which return an implication (in the object language).
% Its complement, in the given signature consists therefore in the
% identity function plus the sets of all unary functions returning
% an universal formula. In symbols:
% 
% \[
% \mmnot(\lamb{x} {term} imp \ (E_{1}\ x) (E_{2}\ x))= 
% \{ \lamb{x}{term} x, \lamb{x}{term}all \ (\lamb {y}{term}  (E\  x)\ y)\}
%  \]
% \end{example}






\renewcommand{\ng}{\GG\vd\mnot}
\newcommand{\diff}{\mbox{\textrm{diff}}}
\begin{Definition}[Fully applied \ho pattern complement]
\label{def:fa-compl}
Fix a signature $\Sigma$.  For a fully applied \ho linear pattern in canonical 
form $M$, define $\ng(M\hastype  A)$ as:

% \newcommand{\diff}{{\textrm diff}}

\[\begin{array}{lll}
\ng(E\ \xn \hastype  a) & = & \eset \\ %& \mbox{\rm if $$ is fully applied} 
\ng (h\ M_{1}\dots M_{m}\hastype  a) & = & \diff_{\GG}(h\hastype \ol{A_{m}}\Imp a) \cup 
\mbox{}\\
& &
\{h\ (Z_{1}\GG)\dots (Z_{i-1}\GG) \ N\ (Z_{i+1}\GG)\dots (Z_{m}\GG)\mid 
\\
& & N\in\ng(M_{i}\hastype A_{i}), 1\leq i\leq m \} \\
\ng(\lxa M\hastype A\Imp B) &  = & \{ \lxa N \mid N\in (\GG,x\hastype A\prv \mnot(M\hastype B)) \}
\end{array}\]
where  $m\geq 0$,
$(Z\ \GG)$ denotes that a fresh variable $Z$  of
appropriate typing may depend from the every variables in $\dom(\GG)$  and
\beq 
\diff_{\GG}(h\hastype \ol{A_{m}}\Imp a) & = & \{g\ (Z_{1} \GG)\dots (Z_{n}\GG) \mid 
g\in\Sigma\cup\GG, g \hastype  \ol{A_{n}} \Imp a, n\geq 0,h \not\equiv g \}
\eneq
\end{Definition} 
Note that the definition makes an essential use of the fact that 
$M$ is canonical and thus its matrix has atomic type $a$.

\begin{Remark}
For $h\in\GG\cup\Sigma,  \ng(h\hastype a) = \diff_{\GG}(h\hastype a)$.
\end{Remark}
\begin{proof}
Consider the $0$-ary application case.
\end{proof}

We will suppress mention of the type in $\ng(M\hastype A)$ when it can be 
inferred from the context.


\begin{Example}
\label{ex:lam}
Consider the untyped $\l$-calculus\footnote{We use $\Lambda$ for
  lambda abstraction in the object-calculus, not to be confused with
  $\l$ in the meta-language.}.
\beq
e & \bnfas & x \mid \Lambda x.\, e \mid e_1\, e_2
\eneq
We encode these expressions using the usual techniques of higher-order abstract
syntax (see, for example, \cite{Michaylov91}) as canonical forms
over the following signature $\Sigma_{lam} $.
\beq
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:
\beq
\rep{x} & = & x\hastype exp\\
\rep{\Lambda x.\, e} & = & lam\ (\lamb{x}{exp} \rep{e})\\
\rep{e_1\ e_2} & = & app\ \rep{e_1}\ \rep{e_2}
\eneq
As usual with \ho abstract syntax \cite{Pfenning88pldi}, we identify the name of 
(bound) variables in both languages.  The adequacy of the encoding
bijectively relates $\alpha$-equivalence classes  
of object-level terms with $\beta\eta$-equivalence classes at the 
meta-level. Now, suppose we want to negate the identity predicate on unary 
function types:
\[
id(\lamb{x}{exp} x).
\]
The intuitive answer is as follows:
\[
\begin{array}{l}
\neg id(\lamb{x}{exp}app \ (E_1\  x) (E_2\ x)).\\
\neg id(\lamb{x}{exp} lam \ (\lamb{y}{exp} (E\  x \ y)).
\end{array}
\]
This follows from the computation of $\cdot\prv\mnot(\lamb{x}{exp} 
x)$:
\beq
\cdot\prv\mnot(\lamb{x}{exp}  x) & = & \{\lamb{x}{exp} Z\mid Z\in (x\oftp exp\prv\mnot(x))\}\\
& = & \{\lamb{x}{exp} Z\mid Z\in \diff_{x\oftp exp}(x\oftp exp))\}\\
& = &  \{\lamb{x}{exp} Z\mid Z\in \{app \ (E_{1} x) (E_{2} x),lam \
(\lamb{y} {exp} (E\ x\ y)) \} \}\\
& = & \{ \lamb{x}{exp} app \ (E_{1} \ x) (E_{2} \ x) , \lamb{x}{exp} lam \ (\l y .\ (E\
x \ y))\}
\eneq


For another illustration, consider the representation of an
object-language $\beta$-redex:
\beq
\rep{ (\Lambda x.\, e)\ f} & = & app\ (lam\  (\lamb{x}{exp} \rep{e}))\ \rep{f}
\eneq
where $\rep{e}$ my have free occurrences of $x$.  When written as a pattern
with variables $E_{exp \arrow exp}$ and $F_{exp}$ ranging over \emph{closed}
terms, this is expressed as $app\ (lam\ (\lamb{x}{exp} (E\ x))\
F)$. Consider the predicate:
$$betardx(app\ (lam\ (\lamb{x}{exp} E\ x))\ F)$$
The complement of the
arguments in the empty context contains every top-level
$\lambda$-abstraction plus every application where the first argument
is not an abstraction:
\[
\cdot\vd\mnot(app\ (lam\ (\lamb{x}{exp} (E\ x))\ F))= 
\{ lam\ (\lamb{x}{exp} Z\ x), app\ (app\ Z_{1}\ Z_{2})\ Z_{3}\}
 \]
Thus the negation of the  \texttt{betardx} predicate is:
\[\begin{array}{l}
\neg betardx(lam\ (\lamb{x}{exp} Z\ x))\\
\neg betardx( app\ (app\ Z_{1}\ Z_{2})\ Z_3)
\end{array}\]
\end{Example}

If the term to complement is complex, we need to call the \mnot\
algorithm recursively as many times as its depth.  Let us see another
slightly more complicated example.


\newcommand{\lfn}{\lamb{f}{n\Imp n} }
\begin{Example}
Consider the signature of numerals 
% \beq
% n  &\bnfas & 0 \mid s(n)
% \eneq
and the problem $\cdot\prv\mnot(\lfn  f\  0)$.  
\beq
\cdot\prv\mnot(\lfn  f\  0) & = & \{\lfn Z\mid Z\in (\of{f}{n\Imp n}\prv\mnot(f\ 
0))\}\\
& = &   \{\lfn Z\mid Z\in \diff_{f}(f)\cup  \{f\ Z'\mid Z'\in 
(\of{f}{n\Imp n}\prv\mnot(0)) \} \}\\
& = &   \{\lfn Z\mid Z\in \{0,s(Z_{1}\ f)\} \cup \{ f\ Z' \mid N'\in \{f(Z_{2}\ f),s(N_3\ 
f)\} \}\\
& = &   \{\lfn 0,\lfn s(Z_{1}\ f), \lfn f(f(Z_{2}\ f)), \lfn f(s(Z_{3}\ f))\}
\eneq
\end{Example}


\section{Partially Applied Terms}
\label{sec:nfa} 


Consider a predicate on the signature $\Sigma_{lam}$ true if a unary
function $\rep{\Lambda x.\, e}$ does not depend on its argument. This
can be encoded using a pattern variable $E_{exp}$ which does not
depend on $x$.

\begin{equation}
\label{eq:vac}
vacous(\lamb{x}{exp} E).
\end{equation}
Intuitively, the complement should be a predicate, say
\texttt{strict}, true when the function \emph{does} use its arguments. Note
that there is no finite set of patterns which has as its ground
instances exactly those terms $M$ which depend on a given variable
$x$.
One way to express it is
as follows:
\[
\begin{array}{l}
strict(\lamb{x}{exp}  x).\\
strict(\lamb{x}{exp}  app\ (E_{1} \ x) (E_{2} \ x)) 
   \\\qquad\qquad\If  strict(\lamb{x}{exp}  E_{1} \  x) .\\
strict(\lamb{x}{exp}  app\ (E_{1} \ x) (E_{2}\ x)) 
   \\\qquad\qquad\If   strict(\lamb{x}{exp}  E_{2} \ x).\\
strict(\lamb{x}{exp}  lam\ (\lamb{y}{exp} (E\ x\ y)))\\
 \qquad\qquad\If  (\PI {z} {
  exp}  strict(\lamb{x}{exp}  (E\ x\ z))).
\end{array}
\]
Hence the complement of a fact, whose terms are partially applied
patterns, would lead to possibly hypothetical and
parametric clauses.  

\begin{Example}
\label{ex:etardx}
The encoding of an $\eta$-redex takes the form:
\beq
\rep{\Lambda x.\, e\ x} & = & lam(\lamb{x}{exp} app\ \rep{e}\ x)
\eneq
 where $\rep{e}$ may contain no free occurrence of $x$.  The side condition
is again expressed in a pattern by introducing an existential variable $E_{exp}$
which {\em does not} depend on $x$.  Hence, its complement with respect to
the empty context should contain, among others, also all terms
 \[ lam\ (\lamb{x}{exp} app\ (E\  x)\ x) \]
where $E$ {\em does} depend on $x$.
\end{Example}

More generally, we would have to decorate
programs with predicates discriminating when a pattern is fully
applied or not.  It is clear that the simply typed $\l$-calculus, or,
for that matter, every other intuitionistic type theory is not strong
enough to represent the complement of partially applied patterns.
This failure of closure under complementation cannot be avoided
similarly to the way in which left-linearization bypasses the
limitation to linear terms and it needs to be addressed directly.

One approach is taken by Lugiez \cite{Lug95}: he modifies the language 
of terms to promote constraints to first-class objects, similarly in 
spirit to explicit substitutions.  For example $\l xyz.\, M\{1,3\}$ 
would denote a function which depends on its first and third argument.  
The technical handling of those objects then becomes awkward as they 
require specialized rules which are foreign to the issues of 
complementation.

We can instead internalize the (in)dependence constraints in a type
theory which explicitly take into account the occurrence issue. Since
our underlying $\lambda$-calculus is typed, we use typing to express
that a function \emph{must} or \emph{must not} depend on its argument.
Following standard terminology, we call such terms \emph{strict in
  $x$} and the corresponding function $\lamb{x}{A} M$ a \emph{strict
  function}.  The natural choice is a calculus of strict types and is
formalized in Section \ref{sec:strict}.  We first give an informal
presentation.

We can introduce a strict application primitive constructor, 
say $F\rapp x$, which express the fact that $F$
\emph{must} use an argument $x$ mentioned in the context.  Thus for
example:
 $$\cdot\vd\mnot(\lamb{e}{exp}E) = \lamb{x}{exp}F\rapp x$$
Therefore, the complement of (\ref{eq:vac}) would be:
\[
\neg vacous(\lamb{x}{exp}  F\rapp x).
\]  


\ignore{We can go farther and recover the above definition of \texttt{strict} 
by `partially evaluating' $E$ against its signature:
\beq
\lefteqn{\cdot\prv\mnot(\lx E)  \Lmap}  \\
% & \lx x \Or \lx app\ (F_{1} \rapp x) (F_{2} x) \Or \lx app\ (F_{3} x) 
% (F_{4}\rapp x) \Or \lx lam\ (\l y.  (F\rapp x)y).
& \{\lx x,   \lx app\ (F_{1} \rapp x) (F_{2}\ x),   \lx app\ (F_{3} \ x) 
(F_{4}\rapp x),   \lx lam\ (\l y.  F\rapp x\ y)\}.
\eneq
thus yielding:
\[
\begin{array}{l}
\neg vacous(\lx x).\\
\neg vacous(\lx app\ (F_{1}\rapp  x) (F_{2}\ x)). \\
\neg vacous(\lx app\ (F_{3}\ x) (F_{4}\rapp x)). \\
\neg vacous(\lx lam\ (\l y. F\rapp x\ y)).
\end{array}
\]
}

Conversely, taking the complement of terms where arguments \emph{must} occur 
yields terms where some argument \emph{must not} occur: for example
\beq 
\cdot\prv\mnot(\lamb{x}{exp}\lamb{y}{exp}  E \rapp y \rapp x) & = &
\{\lamb{x}{exp}\lamb{y}{exp} F,\lamb{x}{exp}\lamb{y}{exp} F_{1}\rapp x,\\
& & \lamb{x}{exp}\lamb{y}{exp}  F_{2}  \rapp y\} 
\eneq 

\smallskip
Let $\xn,\ol{y_{m}}$ be two sets of variables
such that  $\ym\subseteq\xn$.  Let $\zp= \xn-\ym$.
 We first treat the intuitionistic application  case. The complement of 
$\l \xn.\, E \ \ym$ is the set of terms that \emph{may} depend on $\ym$ 
but \emph{has} to depend on one of the $\zp$'s, that is $p$ terms such
that, for an appropriate context $\GG$:
\beq
\GG\prv\mnot(E\ \ol{y_{m}}) & = &  \bigcup\limits_{j=1}^{p} 
\{E_{j} \ \ym\ z_{1}\dots z_{j-1}\mbox{} \rapp z_{j}\ z_{j+1}\dots 
z_{p}\}
\eneq
The complement of terms with strict application is defined as:
\beq
\GG\prv\mnot(E\rapp y_{1}\rapp y_2\dots\rapp y_m) & = &  \bigcup\limits_{j=1}^{m} 
\{E_{j} \ y_{1}\dots y_{j-1}\ y_{j+1}\dots y_{m}\}
\eneq

\begin{Example}
\beq
 \cdot\prv\mnot(\l xyzw.\,E \ y\ w)& = &\{\l xyzw.\,F_{1}\ y\ w\rapp x\ z, 
\l xyzw.\,F_{2}\ y\ w\ x\rapp z\} \\
\cdot\prv\mnot(\l xy.\,E\rapp x\rapp y) & = & \{\l xy.\, F_{1} \ x,   \l 
xy.\,F_{2} \ y\}
\eneq
\end{Example}


Yet, there is a certain asymmetry between strict and intuitionistic
application: while the former completely determines the occurrence
status of a variable, the latter leaves the status floating
indeterminately between the possibility of occurrence or not. We can
benefit from a notation which captures the `non-occurring' condition
explicitly. One possibility is to decorate bound variables as well as
function types with three \emph{occurrence annotations}\ignore{An
  analogous approach can be used to deal with resource management in
  linear logic \cite{Pfenning98notes}.} $1,0,u$ with the intended
meaning of: 
\beq
x^{1} & : & \mbox{$x$ must occur}\\
x^{0} & : & \mbox{$x$ must \emph{not} occur}\\
x^{u} & : & \mbox{$x$ is undetermined} \eneq

Its intended semantics, as a type theory,  is explored next.



