\chapter{The  Relative Complement Problem for Higher-Order Patterns}
\label{ch:relcomp}

We introduce in the next Section~\ref{sec:strictcomp} a restriction of
the language for which complementation is possible (Section
\ref{sec:compl}).  Moreover, in Section \ref{sec:sunif} we will give
an unification algorithm for this fragment. Section \ref{sec:algebra}
shows how the former operations induce a boolean algebra over finite
sets of terms.

\section{Towards Term Complementation}
\label{sec:strictcomp}


%\input{quest}

Now that we have developed a calculus which is potentially strong
enough to represent the complement of linear patterns, we need to answer
two questions: how do we embed the original $\lambda$-calculus, and is
the calculus now closed under complement?

We reiterate that we require that our complement operator ought to satisfy
the usual boolean rules for negation: 
\ben
\item (Disjointness) It is not the case that some $M$ is both a ground 
instance of $N$  and of $\mnot(N)$.
\item (Exhaustivity) Every $M$ is a ground instance of $N$ or  of $\mnot(N)$.
\enen

Unfortunately, while the first property follows quite easily from
Corollary \ref{co:disj}, it turns out that exhaustivity does not hold
in general in the presence of intuitionistic application.  In fact,
consider the application $y\ x^u$; while it is clear that $\GG\vd y\ 
x^u\in \|E\ x^u\ y^u\|$, it is  \emph{not} the case that $\GG\vd y\ 
x^u\in \|E\ x^1\ y^u\|$ or $\GG\vd y\ 
x^u\in \|E\ x^0\ y^u\|$. 

However, the main result of this Chapter is that the complement
algorithm presented in Definition \ref{def:compl} is sound and
complete for the fragment which results from the natural embedding of
the original simply-typed $\lambda$-calculus; this is sufficient for
our overall goal, that is to use term complementation as a subroutine
of clause complementation (see Section \ref{sec:cc}).
%must therefore isolate the right fragment of the strict calculus: 
We will proceed in  two separate phases:
\bit
\item Restrict to a class of terms (that we call \emph{simple}) for
  which the crucial property of \emph{tightening} (Lemma \ref{le:exh}) can be
  established, yielding exhaustivity as a  corollary.
\item Bring  simple terms to `full application'.  
\enit

%Note that the first item is not required for disjointness.


\subsection{Simple Terms}

% We now address the issue of exhaustivity: once we have allowed 
% existential variables,  we would like  the 
% following to hold:

Recall that we have introduced strictness to capture occurrence conditions
on variables in canonical forms.  This means that \fo constants (and
by extension bound variables) should be considered \emph{strict}
functions of their argument, since these arguments will indeed occur
in the canonical form.  On the other hand, if we have a second order
constant, we cannot restrict the argument function to be either strict
or vacuous, since this would render our representations inadequate.


\begin{Example}
\label{ex:excont}
Continuing Example \ref{ex:lam}, consider the representation of the
\textbf{K} combinator:
% \[
% \begin{array}{rcl}
% \rep{\lambda x.\, \lambda y.\, x} = lam\ (\lamb{x}{exp} lam\ (\lamb{y}{exp} x))
% \end{array}
% \]
\beq
\rep{\lambda x.\, \lambda y.\, x}& = & lam\ (\lamb{x}{exp} lam\ (\lamb{y}{exp} x))
\eneq
Notice that the argument to the first occurrence of `$lam$' is a
strict function, while the argument to the second occurrence is an
invariant function.  If we can give only one type to `$lam$' it must
therefore be $(exp \GImp{u} exp) \GImp{1} exp$.
\end{Example}

Generalizing this observation means that positive occurrence of
function types are translated to strict functions, while negative
occurrences to undetermined functions.  We can formalize this as an
embedding of the simply-typed $\l$-calculus into a fragment of the
strict calculus via two (overloaded) mutually recursive functions
$()^{-}$ and $()^{+}$.  First, the definition on types.
\beq
(A\Imp B)^{+} & = & A^{-} \RImp B^{+}\\
(A\Imp B)^{-} & = & A^{+} \TImp B^{-}\\
a^{-} = a^{+} & = & a 
\eneq 
We extend it to canonical terms (including
existential variables), signatures, and contexts; we remark that 
embedding only canonical forms rules out the case of `$+$-ing' a
lambda expression.
\beq
(\lxa M)^{-} & = & \lamb{x^{u}}{A^{+}} M^{-}\\
M^{-} & = & M^{+} \qquad\qquad \mbox{for $M$ of base type}\\
x^{+} & = & x\\
c^{+} & = & c\\
(E_A\ x_1\dots x_n)^{+} &=& F_{A^{-}} \ x_1^u\dots x^u_n \\
(M\ N)^{+} & = & M^{+}\ (N^{-})^{1}\\
[1em]
(\cdot)^{+} & = & \cdot\\
(\GG,x\oftp A)^{+} & = & \GG^{+}, x\oftp A^{+}\\
(\Sigma,a\oftp type)^{+} & = & \Sigma^{+}, a\oftp type\\
(\Sigma,c\oftp A)^{+} & = & \Sigma^{+}, c\oftp A^{+} \eneq

% But consider the following:
% \begin{Example}
% \[
% \begin{array}{l}
% y\oftp ((a\Imp a)\Imp a)\Imp a, x\oftp a\vd y(\lamb{f}{a\Imp a} f\ 
% x) \\
% y\oftp ((a\Imp a)\Imp a)\Imp a, x\oftp a\vd y(\lamb{f}{a\Imp a} x)
% \end{array}
% \]
% Note that $y$ is well-typed 
% \end{Example}

% The idea is then to make the status of terms as determined as 
% possible, while preserving the possibility of well-typing sub-terms 
% as $y$ above.  The trick is to keep undetermined every negative 
% occurrence of the arrow, while making determined the positive ones.



% The example before is translated as follows:
% %  \begin{Example}
% \beq
% \lefteqn{(y\oftp ((a\Imp a)\Imp a)\Imp a, x\oftp a)^{+}\vd (y(\lamb{f}{a\Imp a} f\ 
% x))^{+}  = }\\
% & & y\oftp ((a\RImp a)\TImp a)\RImp a, x\oftp a\emp\vd y(\lamb{f^{u}}{a\RImp a} f\ 
% x^{1})^{1}\\
% \lefteqn{(y\oftp (a\Imp a)\Imp a, x\oftp a)^{+}\vd (y(\lamb{f}{a\Imp a} x))^{+}  = }\\
% & & y\oftp ((a\RImp a)\TImp a)\RImp a, x\oftp a\emp\vd y(\lamb{f^{u}}{a\RImp a} x)^{1}
% \eneq
% % \end{Example}
\begin{Example} Coming back to  Example \ref{ex:excont}:
\beq
 (lam\ (\lamb{x}{exp} lam\ (\lamb{y}{exp} x)))^+& = & 
 lam\ (\lamb{x^u}{exp} lam\ (\lamb{y^u}{exp} x)^1)^1
\eneq
\end{Example}

The image of the embedding of the canonical forms of the simply-typed
$\lambda$-calculus gives rise to the following fragment:
\[ \begin{array}{rrcl}
\mbox{\textit{Simple Terms}} & M & \bnfas &  \lam x^{u}\oftp
A^{+}\ldot M \bnfalt (\dots (h\ M_1)^{1} \dots M_n)^{1} \bnfalt 
%&&&
 (\dots (E_{A^{-}}\ x_{1})^u\dots x_{n})^u
\end{array} \]
We often abbreviate $(\dots (h\ M_1)^{1} \dots M_n)^{1}$ as $h\ \Mns$;
similarly we shall use $ F_{A^{-}}\ \ol{x^u_n}$. Note that, by the
restriction to $\eta$-long $\beta$-normal forms, such terms, as well as
pattern variables, must be of base type.

\smallskip
To prove the correctness of the embedding (Theorem \ref{thm:embed}),
we will need the following:

\newcommand{\ctx}{\GG^{+};\cdot;\cdot}

\begin{Lemma}
\label{le:aminus}
If $\GG\vd E_{A}\ \xn \hastype a$, then $\ctx\vd F_{A^{-}}\ 
\ol{x^u_n}\hastype a$.
\end{Lemma}
\begin{proof}
A straightforward induction on $A$.
\end{proof}

The next theorem requires the usual inductive definition of canonical
terms in the simply-typed $\l$-calculus, which can be obtained by
dropping labels (Theorem \ref{thm:conserv}) from the definition of
canonical form in Figure~\ref{fig:canon}.

\begin{Theorem}[Correctness of $()^{\pm}$]
\label{thm:embed}
\mbox{}
\ben
\item
If $\GG\vd M\bua A$, then $\ctx\vd M^{-}\bua A^{-}$. 
\item
If $\GG\vd M\da A$, then $\ctx\vd M^{+}\da A^{+}$. 
\enen
\end{Theorem}
\begin{proof}
By mutual induction on the proofs of $\cD_1::\GG\vd M\bua A$ and 
$\cD_2::\GG\vd M\da A$.
\bit
\itc 
\[\cD_2= \ianc{c\oftp A\in\Sigma}{\GG\vd c\da A}{\tt atmCnst}\]
Since $c^{+}= c$ and $\Sigma^{+}(c) = A^{+}$ we conclude
$$\cE-\ianc{}{\ctx\vd c^{+}\da A^{+}}{cIdc}$$
\itc 
\[\cD_2= \ianc{}{(\GG,x\oftp A)\vd x\da A}{\tt atmVar}\]
Since $x^{+}= x$ and $\GG^{+}(x) = A^{+}$ we conclude
$$\cE=\ianc{}{(\GG^{+},x\oftp A^{+})\vd x^{+}\da A^{+}}{cId^{u}}$$
\itc
\[\cD_2=\ibnc{\GG\vd M\da B\Imp A}{\GG\vd N\bua B}{\GG\vd M\ N \da 
A}{\tt atmApp}\]
\btab
$\GG\vd M\da B\Imp A$\bs
$\ctx\vd M^{+}\da (B\Imp A) ^{+}$\bi $2$\\
$\ctx\vd M^{+}\da B^{-}\RImp A ^{+}$\` By the embedding\\
$\GG\vd N\bua B$\bs
 $\ctx\vd N^{-}\bua B^{-}$\bi $1$\\
$\ctx\vd M^{+} ( N^{-})^{1}\da A^{+}$\br $c\RImp E$\\
$\ctx\vd (M\ N)^{+} \da A^{+}$ \` By the embedding
\etab
\itc
\[\cD_2=
\ianc{\GG\vd E_{A}\ \xn\hastype a}{\GG\vd E_{A}\ \xn\da 
a}{\tt canPat}\]
\btab
$\GG\vd E_{A}\ \xn\hastype a$\bs
$\ctx\vd F_{A^{-}}\ \ol{x^u_n}\hastype a$
\`   By Lemma \ref{le:aminus} \\
$\ctx\vd F_{A^{-}}\ \ol{x^u_n}\da a$ \br $cPat$\\
$\ctx\vd (E_{A}\ \xn)^{+}\hastype a^{+}$\`  By the embedding
\etab
\itc
\[\cD_1=\ianc{\GG\vd M\da a}{\GG\vd M\bua a}{\tt canAtm}\] 
\btab
$\GG\vd M\da a$\bs
$\ctx\vd M^{+}\da a^{+}$\bi $2$\\
$\ctx\vd M^{+}\bua a^{+}$\br $cAt$\\
 $\ctx\vd M^{-}\bua a^{-}$\`   By the embedding
\etab
 \itc
\[\cD_1= \ianc{\GG,x\oftp A\vd M\bua B}{\GG\vd\lxa M\bua A\Imp 
B}{\tt canLam}\] 
\btab
$\GG,x\oftp A\vd M\bua B$\bs
$(\GG^{+},x\oftp A^{+})\vd M^{-}\bua B^{-}$\bi $1$\\
$\ctx\vd\lamb{x^{u}}{A^+} M \bua A^{+}\TImp B^{-}$ \br $c\TImp I$\\
$\ctx\vd (\lxa M)^{-}\bua (A \Imp B)^{-}$\` By the embedding
\etab
\enit\end{proof}

From now on we may hide the $()^1$ decoration from strict application
of constants in examples. Moreover, for every judgment $\cal J$ on
simple terms, we will shorten $\GG;\cdot;\cdot\vd \cal J$ into $\GG\vd
\cal J$.

\smallskip We can now prove the crucial tightening lemma.  It
expresses the property that every \emph{closed simple term} is either strict or
vacuous in a given undetermined variable.

\newcommand{\cu}{(\GG, x\oftp C);\Omega;\Delta}
\newcommand{\cxtr}{\GG;\O; (\D, x\oftp C)}
\newcommand{\cxto}{\GG; (\O,x\oftp C);\D}

\begin{Lemma}[Tightening]
\label{le:exh} 
Let $M$ be a simple pattern without existential variables:
\ben
\item
If $\cu\vd M\da A$, then  $\cxtr\vd M\da A$ or $\cxto\vd M\da A$.
\item
If $\cu\vd M\bua A$, then  $\cxtr\vd M\bua A$ or $\cxto\vd M\bua A$.
\enen
\end{Lemma}
\begin{proof}
By mutual induction on $\cD_{1}::\cu\vd M\da A$ and 
$\cD_{2}::\cu\vd M\bua A$.
\bit
\itc 
$$\cD_1 = \ianc{c\oftp A\in\Sigma}{(\GG,x\oftp C);\O;\cdot \prv  c\da A}{cIdc}$$
Then
$$\cE= \ianc{c\oftp A\in\Sigma}{\GG;(\O,x\oftp C);\cdot \prv  c\da A}{cIdc}$$
and by weakening the claim.
\itc
$$\cD_1 = \ianc{}{(\GG,x\oftp C,y\oftp A);\O; \cdot  \prv  y\da 
A}{cId^{u}}$$
Then 
$$\cE = \ianc{}{(\GG,y\oftp A);(\O,x\oftp C); \cdot  \prv  y\da 
A}{cId^{u}}$$
and by weakening the claim.
\itc
$$\cD_1 = \ianc{}{(\GG,x\oftp C);\O;\cdot \prv  x\da C}{cId^{u}}$$
Then
$$\cE= \ianc{}{\GG;\O;x\oftp C \prv  x\da C}{cId^{1}}$$
and by weakening the claim.
\itc 
$$\cD_1= \ianc{}{(\GG,x\oftp C);\O;y\oftp A\vd y\da A}{Id^{1}}$$
Then $$\cE= \ianc{}{\GG;(\O,x\oftp C);y\oftp A\vd y\da A}{Id^{1}}$$
and by weakening the claim.
% \itc
% $$\cD=
% \ianc{\cu\vd E_{A}\ \xnl \hastype a}{\cu \vd E_{A}\ \xnl \da  
% P}{cPat}$$
% \btab
% $\cu\vd E_{A}\ \xnl \hastype a$\bs
% $\cdot;\cdot;\cdot\vd E_{A}\hastype A$\bs
% $\cxto\vd E_{A}\ \xnl \hastype a$\br\\
% $\cxto\vd E_{A}\ \xnl \da a$\br\\
% hence by weakening the claim.
% \etab
 \itc
$$\cD_2 = \ianc{\cu\prv  M\da a}{\cu \prv  M\bua a} {cAt}$$
\btab
$\cu\prv  M\da a$ \` By sub-derivation\\ 
$\cxtr \prv  M\da a$ or $\cxto \prv  M\da a$ \bi $1$
\etab
\bit
\item[\subcase]
\btab
$\cxtr \prv  M\da a$  \ba
$\cxtr \prv  M\bua a$ \` By rule $cAt$\\
\hence
\etab
\item[\subcase]
\btab
$\cxto \prv  M\da a$ \ba
$\cxto \prv  M\bua a$ \` By rule $cAt$\\
\hence
\etab
\enit
\itc
$$\cD = \ianc{(\GG,x\oftp C,y\oftp A);\Omega;\Delta \prv M\bua B}{\cu\prv(\lamb{y^u}{A} M) \bua 
A\TImp B} {c\TImp I}$$
\btab
$(\GG,x\oftp C,y\oftp A);\Omega;\Delta \prv M\bua B$ \` By sub-derivation\\
$(\GG,y\oftp A);\Omega;(\Delta,x\oftp C)\vd M\bua B$ 
or $(\GG,y\oftp A);(\O,x\oftp C);\Delta\vd M\bua $ \bi $2$
\etab
\bit
\item[\subcase]
\btab
$(\GG,y\oftp A);\Omega;(\Delta,x\oftp C)\vd M\bua B$ \ba
$\cxtr\prv(\lamb{y^u}{A} M) \bua A\TImp B$ \` By rule $c\TImp I$\\
\hence
\etab
\item[\subcase]
$(\GG,y\oftp A);(\O,x\oftp C);\Delta\vd M\bua $: symmetrical 
\enit
\itc
 $$\cD = \ibnc{(\GG,x\oftp C,\D_N);\O;\D_M \vd M \da A \RImp 
B}{(\GG,x\oftp C,\D_M);\O;\D_N \vd N \bua A}{(\GG,x\oftp C);\O;\dmn 
\vd M\ N^1 \da B}{c\RImp E}$$
There are four  sub-cases, stemming from  IH $1$ and $2$:
\ben
\item
\btab
%$(\GG,x\oftp C,\D_N);\O;\D_M \vd M \da A \RImp B\ba
$(\GG,\D_N);\O;(\D_M,x\oftp C)\vd M\da A\RImp B$\ba
%$(\GG,x\oftp C,\D_M);\O;\D_N \vd N \bua A$\ba
$(\GG\D_{M});\O;(x\oftp C,\D_N)\vd N\bua A$
\ba
$(\GG,\D_M,x\oftp C);\O;\D_N\vd N\bua A$ 
\` By Loosening$^{1}$ $x$\\
$\GG;\O;(\D_M,x\oftp C,\D_N)\vd M\ N^{1}\da B$
\` By rule\\
 hence  by weakening the claim.
 \etab
\item 
\btab
$(\GG,\D_N);(\O,x\oftp C);\D_M\vd M\da A\RImp B$ \ba
$(\GG,\D_M);(\O,x\oftp C);\D_N\vd N\bua A$ \ba
$\GG;(\O,x\oftp C);\dmn\vd M\ N^{1}\da B$ \` By rule\\
 hence  by weakening the claim.
\etab
\item
\btab
$(\GG,\D_N);\O;(\D_M,x\oftp C)\vd M\da A\RImp B$
\ba
$(\GG,\D_M);(\O,x\oftp C);\D_N\vd N\bua A$ 
\ba
$(\GG,x\oftp C,\D_N);\O;\D_M\vd N\bua A$ 
\` By Loosening$^{0}$ $x$\\
$\GG;\O;(\D_M,x\oftp C,\D_N)\vd M\ N^{1}\da B$
\` By rule\\
hence  by weakening the claim.
\etab
\item Symmetrical to $3.$
%
\enen
\enit
\end{proof}

We remark that  tightening fails to hold once we allow non-simple
terms, namely intuitionistic application. For example $y\oftp A\TImp
B,\xoa\emp\vd y\ x^u\hastype B$ but both $y\oftp A\TImp
B;\cdot;\xoa\nvd y\ x^u\hastype B$ and $y\oftp A\TImp B;\xoa;\cdot\nvd
y\ x^u\hastype B$. This suggest that simple terms are not only a
useful technical device to achieve term complement in the simply-typed
case, but possibly for other more general calculi such as the linear
$\l$-calculus.
%namely in the sub-case where the leftmost derivation is
%vacuous in $x$ and the rightmost is strict in $x$.

% WITHOUT CANONICAL FORMS
% \begin{Corollary}
% \label{co:exh} 
% Let $(\GG,\O,\D,x\oftp C)\emp\vd M\hastype A$; then
% \ben
% \item
% either $\GG;(\O,x\oftp C);\D\vd M\hastype A$ or 
% $(\GG,\O,\D);\cdot;x\oftp C;\vd M\hastype A$.
% \item 
% either $\GG;\O;(\D,x\oftp C)\vd M\hastype A$ or $(\GG,\O,\D);\cdot;x\oftp C 
% \vd M\hastype A$.
% \enen\end{Corollary}
% \begin{proof}
% \ben
% \item 
% \btab
% By repeated application of Lemma \ref{le:exh},
% Loosening$^{0}$ and Loosening$^{1}$.
% \end{proof}

% \begin{Corollary}
% \label{co:exh} 
% Let $M$ be a simple closed pattern such that $(\GG,\O,\D,x\oftp
% C)\emp\vd M\buda A$; then
% \ben
% \item either $\GG;\O;(\D,x\oftp C)\vd M\buda A$ or
%   $(\GG,\O,\D);\cdot;x\oftp C \vd M\buda A$.
% \item either $\GG;(\O,x\oftp C);\D\vd M\buda A$ or
%   $(\GG,\O,\D);\cdot;x\oftp C;\vd M\buda A$.  
% \enen
% \end{Corollary}
% \begin{proof}
% \mbox{}
% \ben
% \item 
% \btab
% $(\GG,\O,\D,x\oftp C)\emp\vd M\buda A$\bh
% $\GG;\cdot;(\O,\D,x\oftp C)\vd M\buda A$ or $\GG;(\O,\D,x\oftp
% C);\cdot\vd M\buda A$ \`By repeated application of Lemma \ref{le:exh}\\
% $\GG;\O;(\D,x\oftp C)\vd M\buda A$ or $\GG;(\O,\D,x\oftp
% C);\cdot\vd M\buda A$ \` By Loosening$^{1}$  $\O$\\
% $\GG;\O;(\D,x\oftp C)\vd M\buda A$ or $(\GG,\O,\D);x\oftp C;\cdot\vd
% M\buda A$ \` By Loosening$^{0}$  $\O,\D$
% \etab
% \item 
% Similarly to above.
% \enen
% \end{proof}

\begin{Corollary}
\label{co:exh} 
Let $M$ be a simple closed pattern such that $\GG\emp\vd M\buda A$;
then there are $\Delta,\O$ such that $\GG=\D,\O$ and $\cdot;\O;\D\vd
M\buda A$.
\end{Corollary}
\begin{proof}
  By induction on $\GG$, using Lemma \ref{le:exh}.
\end{proof}


\subsection{Full Application}
\newcommand{\LBimp}{\longleftrightarrow}

We can simplify the presentation of the algorithms for complement and
later unification if we extend every term to be applied to all bound
variables in their declaration order.  This is possible for simple
\emph{linear} patterns without changing the set of its ground instances.  We
just insert vacuous applications, which guarantees that the extra
variables are not used.
%We furthermore permute the arguments to the
%standard order, which also does not affect the set of ground instances of linear patterns.
In slight abuse of notation we call the resulting terms \emph{fully
  applied}.

We describe\fixed in Figure~\ref{fig:trans} the judgment $\GG\vd
M\LBimp N$ which turns a term $M$ into an equivalent fully applied
term $N$: while we need this translation specialized to simple terms,
it is clear how to generalize this judgment to the canonical forms of
any strict term.
%The notation $\pi(\GG)$ stands for a permutation of $\dom(\GG)$.


% same context
\begin{figure}
\label{fig:trans}  
\[
\begin{array}{c}
\ianc{\O=\dom(\GG)\setminus\mid\Phi\mid}{\GG\prv  E\ \Phi^u \LBimp Z\ \Phi^{u} \
\Omega^{0}}{\mbox{\tt TrnPat}} 
\vsk
\ianc{ \GG,x\oftp A \prv  M \LBimp  N }
{\GG\prv \lxua M \LBimp  \lamb{x^u}{A }N }{\mbox{\tt TrnLam}}\vsk
\ianc{  \GG\prv  M_{1}  \LBimp   N_{1}\cdots \GG\prv  M_{n} \LBimp   N_{n} }
{\GG\prv h\  \Mns \LBimp   h\ \Nns} {\mbox{\tt TrnApp}}
\end{array}
\]
\caption{Full application translation: $\GG\vd M\LBimp N$}
\end{figure}


\begin{Example}
Recall the simple term from Example \ref{ex:etardx}:
$$lam\ (\lamb{x^u}{exp} app\ E\ x)$$ has fully applied form
$$lam\ (\lamb{x^u}{exp} app\ (Z\ x^0)\ x)$$
for a fresh existential
variable $Z$ of type $exp \GImp{0} exp$.
\end{Example}

We may check the the output of the translation is indeed fully
applied \wrt its definition in Figure \ref{fig:fa}:

\begin{Lemma}
If $M$ is a simple term and $\GG\vd M\LBimp N$, then $\GG\vd N\fa$.
\end{Lemma}
\begin{proof}
  A straightforward induction on the structure of the given
  derivation.
\end{proof}

We have now arrived to the following language, where the labeling on
flexible patterns is unrestricted, still called ``simple terms'':
\[ \begin{array}{rrcl}
\mbox{\textit{Simple Terms}} & M & \bnfas &  \lam x^{u}\oftp
A^{+}\ldot M \bnfalt (\dots (h\ M_1)^{1} \dots M_n)^{1}\bnfalt (\dots (E\ 
x^{l_{1}}_{1})\dots{x^{l_{n}}_{n}})
\end{array} \]


To prove the set-theoretic adequacy of the translation, we will need
the following irrelevance Lemma.

% \newcommand{\cx}{x\oftp C;\cdot;\cdot}
% \newcommand{\cxom}{ x\oftp C;\Omega;\cdot}
\newcommand{\cgm}{\GG;(\O,\xoc);\D}
\newcommand{\cgmom}{ \GG;\Omega;\D}

\begin{Lemma}[Irrelevance]
\label{le:fat}
If $M$ is a closed simple term, then:
\begin{enumerate}
\item 
If $\cgm\vd M\bua A$, then $\cgmom\vd M\bua A$.
\item
If $\cgm\vd M\da A$, then $\cgmom\vd M\da A$.
\end{enumerate}
\end{Lemma}

\begin{proof}
By mutual induction on $\cD_{1}::\cgm\vd M\da A$ and
$\cD_{2}::\cgm\vd M\bua A$.
\bit
\itc  $$\cD_1 = \ianc{c\oftp A\in\Sigma}{\GG;(\O,\xoc);\cdot \prv  c\da A}{cIdc}$$
Then
$$\cE= \ianc{c\oftp A\in\Sigma}{\GG;\O;\cdot\prv  c\da A}{cIdc}$$
\itc  $$\cD_1 = \ianc{}{(\GG, y\oftp A) ;(\O,\xoc); \cdot  \prv  y \da 
A}{cId^{u}}$$
Then
$$\cE = \ianc{}{(\GG, y\oftp A); \O;\cdot  \prv  y\da A}{cId^{u}}$$
\itc $$\cD_1 = \ianc{}{\GG ;(\O,\xoc); y\oftp A  \prv  y \da 
A}{cId^{1}}$$
Then
$$\cE = \ianc{}{\GG; \O;y\oftp A  \prv  y\da A}{cId^{1}}$$

% \itc  $$\cD = \ianc{\cgm\vd E\ \ol{x_{n}^{l}} \hastype a}{\cgm \vd E\ \ol{x_{n}^{l}} \da  P}{cPat}$$
% \btab
% $\cgm\vd E\ \ol{x_{n}^{l}} \hastype a$\bs
%  $\GG;\Omega;\cdot\vd E\ \ol{x_{n}^{l}} \hastype a$\` By 
%  Weakening$^0$\\
%   $\GG;\Omega;\cdot\vd E\ \ol{x_{n}^{l}} \da a$\br
%   \etab
 \itc  $\cD_2$ ends in $cAt$: by IH $2$.
% \itc  $$\cD = \ianc{\cgm\prv  M\da a}{\cgm \prv  M\bua a} {cAt}$$
% By sub-derivation $\cgm\prv  M\da a$, by IH  $\cgmom \prv  M\da 
% P$ and hence   $\cgmom \prv  M\bua a$.
  \itc  $$\cD_2= \ianc{(\GG,y\oftp A);(\O,\xoc);\D \prv M\bua B}{\cgm\prv(\lamb{y^u}{A} M) \bua 
A\TImp B} {c\TImp I}$$
\btab
$(\GG,y\oftp A);(\O,\xoc);\D \prv M\bua B$\bs
$(\GG,y\oftp A);\O;\D\prv M\bua B$ \bi $2$\\
 $\cgmom\prv(\lamb{y^u}{A} M) \bua A\TImp B$\br
 \etab
\itc  $\cD_2 =$ $$ \ibnc{(\GG,\D_N);(\O,\xoc);\D_M \vd M \da A \RImp
  B}{(\GG,\D_M);(\O,\xoc);\D_N\vd N \bua A}{\GG;(\O,\xoc);\dmn\vd M\ N^1 \da B}{c\RImp E}$$
\btab
$(\GG,\D_N);(\O,\xoc);\D_M \vd M \da A \RImp B$\bs
$ (\GG,\D_N);\O;\D_M \vd M \da A \RImp B$ \bi $2$\\
$ (\GG,\D_M);(\O,\xoc);\D_N \vd N \bua A$\bs
$ (\GG,\D_M);\O;\D_N \vd N \bua A$\bi $1$\\
$\GG;\O;\dmn\vd M\ N^{1}\da B$\br
\etab
\enit
\end{proof}

Note that this holds for any strict canonical terms, but it is false
for terms containing redeces. For example $\cdot;\xoa;\cdot\vd
(\lamb{y^0}{A} c) \ x^0\hastype B$, as $x$ becomes unbound in the
rightmost premise, but $\cdot;\cdot;\cdot\nvd (\lamb{y^0}{A} c) \ 
x^0\hastype B$.

\subsubsection{Ground Instances}

We recall that we assume every type to be inhabited, so that every
term can be seen as the intensional representation of the set of its
ground instances.  The judgment in Figure \ref{fig:grinst} $\GG \prv
M\in\| N\|\hastype A $ formalizes conditions for $M$ to be a ground
instance of a simple \emph{linear} term $N$ at type $A$.  We then
extend the judgment to \emph{sets} of terms of the same type as
follows: 
\beq \ianc{\exists i\oftp 1\leq i\leq n\quad\GG\prv M \in
  \|N_{i}\|\hastype A} {\GG\prv M \in \|N_{1}\cdots N_{n}\|\hastype
  A}{\mbox{\tt gr}_i}
 \eneq

\begin{Remark}
\label{rmrk:gr}
$\GG \prv M \in\| E_A\ \Phi\|\hastype a$ iff $M\da  t \ \Phi$ and
$\cdot\prv t \hastype A$ iff $t\equiv \l \Phi\,.\,S$ and if $\god\vd\Phi\ ok$
, then $\god\vd S \hastype A$.
\end{Remark}
This fact will be heavily used in the following. 

\begin{figure}
\[
\begin{array}{c}
\ianc{M\da  t \ \Phi  \quad \cdot\prv  t \hastype A}
{\GG \prv   M  \in\| E_A\ \Phi\|\hastype a}{\mbox{\tt grFlx}} 
\vsk
\ianc{(\GG,x\oftp A);\Omega;\Delta\prv   M  \in\| N\|\hastype B}
{\GG \prv  \lxua M  \in\|\lxua N \|:A\TImp B}{\mbox{\tt grLam}}
\vsk
\ibnc{\GG \prv h \hastype  \ol{A_n}\RImp a}{ \GG \prv   M_1 \in\| 
N_{1}\|\hastype A_1\cdots \GG\vd M_n\in\|A_n\| \hastype A_n} {\GG \prv  h\ \Mns \in\|h\ \Nns
\|\hastype a} {\mbox{\tt grApp}}
\end{array}
\]
\caption{Ground instance: $\GG\vd M\in  \|N\| \hastype A$}
\label{fig:grinst}
\end{figure}


\begin{Lemma}[Ground Instance Weakening]
\label{le:giweak}
If $\Gamma\vd M \in \|N\|\hastype A$ then $(\Gamma, x\oftp A)\vd M \in
\|N\|\hastype A$.
\end{Lemma}
\begin{proof}
  By induction on the structure of the given derivation.
\end{proof}

We implicitly use the above lemma to  weaken different 
contexts with common basis to an unique one.
%\bmeta Really??\emeta

\smallskip Now we can prove that the the full application translation
preserves the set of ground instances.

\begin{Theorem}[Adequacy of Full Application Translation]
\label{thm:fat}
Let $N$ be a simple term of type $A$, such that $\GG \vd N \LBimp Q$;
then $\GG\vd M\in\|N\|\hastype A$ iff $\GG \vd M\in \|Q\|\hastype A$.
\end{Theorem}
\begin{proof}
By induction on the structure of $\cD::\GG\vd M\LBimp 
N$.
\bit
\itc
$\cD$ ends in \texttt{TrnPat}:
\item[$(\Imp)$]
\btab
$\GG\vd M \in \|E_{B}\ \Phi^{u})\|$ and
$\O=\dom(\GG)\setminus\mid \Phi\mid$\ba
$M\da  t\ \Phi^{u}$ and $\cdot\vd t\hastype B$ for $\GG\emp\vd\Phi\ ok$ \bv
$\GG\emp \vd S\hastype A$\` By Remark \ref{rmrk:gr}\\
 $\GG\emp\vd S\buda A$\` By  the canonical form Theorem  \\
$\GG;\Omega;\cdot\vd S\buda A$\` By Weakening$^0$\\
$\GG;\Omega;\cdot\vd S\hastype A$\` By soundness of canonicity\\
%$\GG;\Omega;\cdot\vd S\hastype A$.  Thus
 $M\da  t'\ \Phi^{u} 
\Omega^{0}$ for $\cdot\vd t'\hastype B'$ and $\GG;\O;\cdot\vd (\Phi^u,\O^0) \ ok$ \`   By Remark \ref{rmrk:gr}\\
 $\GG\emp\vd M\in \|F_{B'}\ \Phi^{u} \Omega^{0}\|$\br 
\etab
\item[$(\If)$]
\btab
$\GG\emp\vd M\in \|F_{B'}\ \Phi^{u} \Omega^{0}\|$ 
  and $\O=\dom(\GG)\setminus\mid\Phi\mid$\ba
$M\da  t'\ \Phi^{u} \Omega^{0}$ for $\cdot\vd t'\hastype B'$ and
$\GG;\O;\cdot\vd (\Phi^u,\O^0) \ ok$\bv 
$\GG;\O;\cdot \vd S\hastype A$\` By Remark \ref{rmrk:gr}\\
$\GG;\O;\cdot \vd S\buda A$\` By  the canonical form Theorem  \\
$\GG;\cdot;\cdot\vd S\buda A$\` By Irrelevance (Lemma \ref{le:fat})\\ 
$\GG;\cdot;\cdot\vd S\hastype A$\` By soundness of canonicity\\
$\GG\emp\vd M \in \|E_{B}\ \Phi^{u}\|$ \br  and  Remark \ref{rmrk:gr}
\etab
\itc
$\cD$ ends in \texttt{TrnLam} or \texttt{TrnApp}:
the result follows from a straightforward application of the inductive hypothesis.
\enit\end{proof}


From now on we tacitly assume that all simple terms are fully applied.
We call a term $E\, x_1^{l_1}\ldots x_n^{l_n}$ a \emph{generalized
  variable}.

\section{The Complement Algorithm}
\label{sec:compl}

The idea of complementation for applications and abstractions is quite
simple and similar to the first-order case.  For generalized variables
we consider each argument in turn.  If an argument variable is
undetermined it does not contribute to the negation.  If an argument
variable is strict then any term where this variable does not occur
contributes to the negation.  We therefore complement the
corresponding label from $0$ to $1$ while all other arguments are
undetermined.  For vacuous argument variables we proceed dually.  If
$\Gamma = x_1\oftp A_1,\ldots, x_n\oftp A_n$, we write $E\ \Gamma^u$
for the application of $E\ {x_1}^u\ldots{x_n}^u$.  Such an application
represents the set of all terms without existential variables and free
variables from $\Gamma$.


In preparation for the rules, we observe that the complement operation
on terms behaves on labels like negation does on truth-values in
Kleene's three-valued logic, in the sense of the following table: 
\beq
\mnot(1)& = &0\\
\mnot(0)& = &1\\
\mnot(u) & = & u \eneq 
Note that these labels form a three-valued semi-lattice with the
(reverse) partial information ordering $1\leq u,0 \leq u$.

\renewcommand{\mmnot}{\mnot}

\begin{Definition}[Higher-Order Pattern Complement]
\label{def:compl}

Fix a signature $\Sigma$.  For a linear simple term $M$ such that $\GG
\prv M \hastype A$ define $\GG\prv \mnot(M) \blip N\hastype A$ by the
following rules:

%\begin{small}
\[
\begin{array}{c}
\ianc{\exists i\oftp 1\leq i\leq n\quad k\in\{1,0\}} {\GG\prv \mnot(E \ x_{1}^{k_{1}}\dots x_{i-1}^{k_{i-1}} \ 
x_{i}^{k}\ x_{i+1}^{k_{i+1}}\dots x_n^{k_{n}}) \blip  Z\ x_{1}^{u}\dots 
x_{i-1}^{u}\ x_{i}^{\mnot(k)}\ x_{i+1}^{u}\dots x_n^{u}\hastype a} {\mnot\mbox{\tt Flx}}
\vsk
\mbox{\textrm{no rule for } $k=u$}
\vsk
\ianc{\GG,x\oftp A\prv  \mnot( M)  \blip   N\hastype B}
{\GG\prv  \mnot(\lxua M)  \blip  \lxua N\hastype A\TImp B}{\mnot\mbox{\tt Lam}}
\vsk
\ianc{g\in\Sigma\cup\GG, g \hastype A_{1}\RImp\dots\RImp A_{m}\RImp 
a\quad m\geq 0,h \not\equiv g   } 
{\GG\prv  \mnot (h\ \ol{M_n^1}) \blip  
(\dots (g\ (Z_{1} \ \GG^{u}))^{1}\dots (Z_{m}\ \GG^{u}))^{1}\hastype a} {\mnot\mbox{\tt App}^{1}}
\vsk
\ibnc{\exists i\oftp1\leq i\leq n } {  \GG\prv \mnot( M_i) \blip  N\hastype A_i}
{\GG\prv  \mnot (h\ \ol{M_n^1}) \blip  
(\dots (h\ (Z_{1}\ \GG^{u} ))^{1}\dots (Z_{i-1}\ \GG^{u} )^{1} \ N^{1}\ 
(Z_{i+1}\ \GG^{u} )^{1}\dots (Z_{n}\ \GG^{u}))^{1}\hastype a} {\mnot\mbox{\tt App}^{2}}
\end{array}
\]
%\end{small}
where the $Z$'s are fresh logic variables of appropriate typing,
$h\in\Sigma\cup\GG$ and $\GG\prv h\hastype A_{1}\RImp\dots\RImp
A_{n}\RImp a$.  Note that a given $M$ may be related to several terms
$N$ all of which belong to the complement of $M$.  Finally we define
$\GG\vd\mmnot(M)= \cN\hastype A$ if $\cN=\{N\mid\GG\prv \mnot(M)\blip
N\hastype A\}$.
\end{Definition}

We may drop the type information from the above judgment in examples
and proofs; we will write $\GG\prv M \in \| \mnot(N) \|\hastype A$, when
$\GG\vd\mmnot(N)=\cN$ and $\GG\prv M \in \| \cN \|\hastype A$. 
%This in turn holds by inversion if there is a $Q$ such that
%$\GG\vd\mnot(N)\blip Q$.

Note that if $E_A$ is a generalized variable considered in the empty context,
 it has the canonical form $\l \ol{x_{n}^{u}}\,.\,E\ \ol{x_{n}^{u}}$. Hence
$\cdot\vd\mmnot(E_{A}) = \eset$ as expected.


\begin{Example} Let $\GG=x\oftp B,y\oftp C$:
\begin{eqnarray}
\GG\vd\mmnot( E\ x^{u} y^{1}) & = & \{ F\ x^{u} y^{0}\}\nonumber \\
\GG\vd\mmnot( E\ x^{0} y^{1}) & = & \{ F\ x^{1} y^{u}, G\ x^{u} y^{0}\} 
\label{eq:l}
\end{eqnarray}
\end{Example}

It is worthwhile to observe that the members of a complement set are
not mutually disjoint, due to the indeterminacy of $u$. We can achieve
an exclusive `or' if we resolve this indeterminacy, that is by
considering for every $x^{u}$ the two possibilities $x^{1},x^{0}$.
Thus, for example, equation (\ref{eq:l}) may be made explicit into:
\[
\{F \ x^{1} y^{1},    G \ x^{1} y^{0},  H \ x^{0} y^{0}\}
\]
It is clear that in the worst case scenario the number of terms in a 
complement set is bound by $2^{n}$; hence the usefulness of this 
further step needs to be pragmatically determined.


% \renewcommand{\ng}{\GG\prv\mnot}

\begin{Example} In the signature of numerals:
\beq
\lefteqn{\mmnot(\l x^{u}\l y^{u}.\, s(E\ x^{1} y^{0})^{1}   =}\\
& \{ \l x^u\l y^u .\, x, \l x^u\l y^u .\, y, \l x^u\l y^u .\, 0, \l 
x^u\l y^u .\, s(Z\ x^{0} y^{u})^{1}, \l x^u\l y^u .\, s(Z'\ x^{u} 
y^{1})^{1} \} 
\eneq
\end{Example}

We can now revisit\footnote{To avoid too many indices on existential
  variables, we adopt a convention that the scope of existential
  variables is limited to each member of a complement set.} Example
\ref{ex:etardx}:
\beq
\lefteqn{\mmnot(lam(\lamb{x^{u}}{exp} app\ (E\ x^{0})\ x ))=}\\
& & \{ lam(\lamb{x^u}{exp} app\ (Z\ x^1)\ (Z'\ x^u)),\\
& & lam(\lamb{x^u}{exp} app\ (Z\ x^u)\ (app\ (Z'\ x^u) \ (Z'' x^u)), \\
& &lam(\lamb{x^u}{exp} app\ (Z\ x^u)\ ( lam(\lamb{y^u}{exp} Z'\ x^u\ y^u)),\\
& & lam(\lamb{x^u}{exp} lam(\lamb{y^u}{exp} Z\ x^u\ y^u) ),\\
& & lam(\lamb{x^u}{exp}x),\\
& & app\ Z\ Z'\}
\eneq


\smallskip

It is easy to show that simple terms are closed under complementation.

\begin{Theorem}
  If $M$ is a simple term and $\GG\vd\mnot(M)\blip N\hastype A$, then
  $N$ is simple.
\end{Theorem}
\begin{proof}
  By induction on the structure of $\cD::\GG\vd\mnot(M)\blip N\hastype
  A$.
\bit
\itc
 $\cD$ ends in $\mnot\mbox{\tt Flx}$: immediate.
% $M\equiv E\ \ol{x_{n}^{l}}$. Then for $1\leq i\leq n$ and for 
% $k\in\{1,0\}$ 
% $\GG\prv \mnot(E \ x_{1}^{k_{1}}\dots x_{i-1}^{k_{i-1}} \ 
% x_{i}^{k}\ x_{i+1}^{k_{i+1}}\dots x_n^{k_{n}}) \blip  Z\ x_{1}^{u}\dots 
% x_{i-1}^{u}\ x_{i}^{\mnot(k)}\ x_{i+1}^{u}\dots x_n^{u}\hastype a$ by rule , where the latter is simple.
\itc
$$\cD=\ianc{\GG,x\oftp A\prv  \mnot( M)  \blip   N\hastype B}
{\GG\prv  \mnot(\lxua M)  \blip  \lxua N\hastype A\TImp B}{\mnot\mbox{\tt Lam}}$$
By sub-derivation $\GG,x\oftp A\prv  \mnot( M)  \blip   N\hastype B$, hence by IH $N$ 
is simple and so is $\lxua N$.
\itc
$$\cD=\ianc{g\in\Sigma\cup\GG, g \hastype A_{1}\RImp\dots\RImp A_{m}\RImp 
a\quad m\geq 0,h \not\equiv g   } 
{\GG\prv  \mnot (h\ \ol{M_n^1}) \blip  
(\dots (g\ (Z_{1} \ \GG^{u}))^{1}\dots (Z_{m}\ \GG^{u}))^{1}\hastype a} {\mnot\mbox{\tt App}^{1}}
$$ 
Since every $(Z_{i}\ \GG^{u})$ is simple, so is $(\dots (g\ (Z_{1} 
\ \GG^{u}))^{1}\dots (Z_{m}\ \GG^{u}))^{1}$.
\itc
$\cD=$
% \begin{small}
$$\ianc{ 
% h\in\Sigma\cup\GG,\GG\prv h\hastype A_{1}\RImp\dots\RImp 
% A_{n}\RImp P\qquad \mbox{\textrm{for some} $i$} \quad 
\GG\prv \mnot( M_i) \blip  N\hastype A_i \qquad 1\leq i\leq n} 
{\GG\prv  \mnot (h\ \ol{M_n^1}) \blip  
(\dots (h\ (Z_{1}\ \GG^{u} ))^{1}\dots (Z_{i-1}\ \GG^{u} )^{1} \ N^{1}\ 
(Z_{i+1}\ \GG^{u} )^{1}\dots (Z_{n}\ \GG^{u}))^{1}\hastype a} {\mnot\mbox{\tt App}^{2}}
$$
% \end{small}
%\begin{sloppypar}
  By IH $N$ is simple and as above so is every $(Z_{i}\ \GG^{u})$.  Thus\\
  $(\dots (h\ (Z_{1}\ \GG^{u} ))^{1}\dots (Z_{i-1}\ \GG^{u} ) \ N^{1}\ 
  (Z_{i+1}\ \GG^{u} )^{1}\dots (Z_{n}\ \GG^{u}))^{1}$ is simple.
%\end{sloppypar}
\enit
\end{proof}

\begin{Corollary}
  If $M$ is a simple term, and $\GG\vd\mmnot(M)=\cN$, then $\cN$ is a
  set of simple terms.
\end{Corollary}

\medskip We address the soundness and completeness of the complement
algorithm \wrt the set-theoretic semantics: the proof obligation
consists in proving that the former does behave as a complement
operation on sets of patterns, \ie it satisfies disjointness and
exhaustivity. Termination is obvious as the algorithm is
syntax-directed and only finitely branching.  
%We abbreviate $\mnot(l)$ as $-l$.
We start with soundness: 
 for $\Phi\equiv x_{1}^{k_{1}}\dots
 x_{i-1}^{k_{i-1}} \ x_{i}^{d}\ x_{i+1}^{k_{i+1}}\dots x_n^{k_{n}}$
 let $\mnot(\Phi)\equiv x_{1}^u\dots x_{i-1}^u \ 
 x_{i}^{\mnot(d)}\ x_{i+1}^u\dots x_n^u$.

\begin{Theorem}
\label{thm:part1}
Let $\GG\vd N\hastype A$ be simple linear pattern: for every $Q$ such
that $\GG\vd \mnot(N)\blip Q\hastype A$, it is not the case that both
$\GG\vd M \in \| N\|\hastype A$ and $\GG\vd M \in \| Q\|\hastype A$.
\end{Theorem}

\begin{proof}
  By induction on the structure of $\cD::\GG\vd \mnot(N)\blip Q$.
  \bit   
    \itc $\cD$ ends in $\mnot\mbox{\tt Flx}$.  For $\xoa\in\GG $ let
  $\Phi(x_i)=1$;
% and  $\mnot(\Phi)\equiv
% x_{1}^{k_{1}}\dots x_{i-1}^{k_{i-1}} \ x_{i}^{0}\ 
%x_{i+1}^{k_{i+1}}\dots x_n^{k_{n}}$; 
  moreover let
  $\Psi;\O;(\D,\xoa)\vd \Phi\ ok$; assume $\GG\vd M\in \|E\ \Phi\|$ and
  $\GG\vd M\in \|\mnot(E\ \Phi)\|$, that is $\GG\vd M\in \|Z\ 
  \mnot(\Phi)\|$. Then both $\Psi;\O;(\D,\xoa)\vd M\hastype A$ and
  $(\Psi,\O,\D);\xoa;\cdot\vd M\hastype A$, impossible by Corollary
  \ref{co:disj}. Analogously for $k_i=0$. The result follows trivially
  for $k_i=u$.
 
\itc  $\cD$ ends in $\mnot\mbox{\tt App}^{1}$.
Suppose both $\GG\vd M\in \|h\ \ol{N_n^{1}}\|$ and 
$\GG \prv M\in \|g\ (Z_{1} \ \GG^{u})^{1}\dots (Z_{m}\ \GG^{u})^{1}\| $ 
for $h\not\equiv g$; but this is immediately impossible by rule 
\texttt{grApp} as the root of $M$ should be both $h$ and $g$.  
\itc $\cD$ ends in $\mnot\mbox{\tt App}^{2}$.
\btab
$\GG\prv  \mnot (h\ \ol{N_n^1}) \blip  
(\dots (h\ (Z_{1}\ \GG^{u} ))^{1}\dots (Z_{i-1}\ \GG^{u} )^{1} \ Q^{1}\ 
(Z_{i+1}\ \GG^{u} )^{1}\dots (Z_{n}\ \GG^{u}))^{1}\hastype a$ \bh
$\GG\vd\mnot(N_i)\blip  Q\hastype A_i$,  for some $1\leq i\leq n$ \`    By
sub-derivation \\ 
$\GG\vd h\ \ol{M_n^{1}}\in \|h\ \ol{N_n^{1}}\|\hastype a$  \` By assumption\\
$\GG \prv h\ \ol{M_n^{1}}\in \| h\ (Z_{1}\ \GG^{u} )^{1}\dots 
(Z_{i-1}\ \GG^{u} )^{1}\ Q^{1}\ (Z_{i+1}\ \GG^{u} )^{1}\dots (Z_{n}\ \GG^{u} 
)^{1} \|\hastype a$ \` By assumption\\
$\GG \prv M_{i}\in\|N_{i} \|\hastype A_i$\`    By inversion \\
$\GG \prv M_{i}\in\|Q \|\hastype A_i$\bv
$\perp$\` By IH
\etab
\itc $\cD$ ends in $\mnot\mbox{\tt Lam}$:
\btab
$\GG\vd \mnot( \lxua N) \blip  \lxua Q\hastype A\TImp B$\bh
 $\GG,x\oftp A\vd \mnot( N) \blip  Q\hastype B$\bs
$\GG \prv \lxua M\in \| \lxua N\|\hastype A\TImp B$ \` By hypothesis\\
 $\GG \prv \lxua M\in \| \lxua Q\|\hastype A\TImp B$\` By assumption\\
$\GG,x\oftp A \vd M\in \| N\|\hastype B$\`  By inversion \\
$\GG,x\oftp A \prv M\in \| Q\|\hastype B$\`  By inversion \\
$\perp$\` By IH
\etab
\end{itemize}
\end{proof}

Note that soundness is based on Corollary \ref{co:disj}, which holds
for \emph{any} strict term: thus disjointness does not require simple
terms.  

\begin{Lemma}
\label{le:exhflex}
Assume $\GG\vd E_A\ \Phi\hastype a$; then, either $\GG \prv M\in \|
E_A\ \Phi \| \hastype a$ or  there exists $1\leq i\leq n$ such that
$\GG\vd \mnot( E_A\ \Phi)\blip Z\ \mnot(\Phi)\hastype a$ and $ \GG
\prv M\in \| Z\ \mnot(\Phi)\| \hastype a$.
\end{Lemma}
\begin{proof}
  Let $\GG\emp\vd M\hastype A$; then by
  Corollary \ref{co:exh} there exists $\O$ and $\D$ such that
  $\GG=\O,\D$ and $\cdot;\O;\D\vd M\buda A$. Fix $x_i^{k_i}$ for
  $1\leq i\leq n$:
\begin{itemize}
\itc For every $x\in\dom(\O)$ such that $x=x_i^{k_i}$ it
  holds $k_i\in\{0,u\}$ and for every $x\in\dom(\D)$, $k_i\in\{1,u\}$.
  Then $\GG\vd M\in\| E\ \Phi\|$.
\itc For some $x\in\dom(\O)$ such that $x=x_i^{k_i}$ it
  holds $k_i=1$. Then $\GG\vd M\in\|Z\ x_{1}^{u}\dots x_{i-1}^{u}\ 
  x_{i}^{1}\ x_{i+1}^{u}\dots x_n^{u} \|$, that is $\GG\vd
  M\in\|Z| \mnot( \Phi)\|$.
\itc For some $x\in\dom(\D)$ such that $x=x_i^{k_i}$ it
  holds $k_i=0$. Then $\GG\vd M\in\|Z\ x_{1}^{u}\dots x_{i-1}^{u}\ 
  x_{i}^{0}\ x_{i+1}^{u}\dots x_n^{u} \|$, that is $\GG\vd
  M\in\|Z\ \mnot( \Phi)\|$.  
\end{itemize}
\end{proof}

For technical reasons, we need the rules complementary to
Figure~\ref{fig:grinst}. Those are depicted in Figure~\ref{fig:ngrinst}:

\begin{figure}
\[
\begin{array}{c}
\ianc{M\da  t \ \Phi  \quad \cdot\nvd t \hastype A}
{\GG \prv   M  \not\in\| E_A\ \Phi\|\hastype a}{\mbox{\tt ngrFlx}} 
\vsk
\ianc{\GG,x\oftp A\prv   M  \not\in\| N\|\hastype B}
{\GG \prv  \lxua M  \not\in\|\lxua N \|:A\TImp B}{\mbox{\tt ngrLam}}
\vsk
\ibnc{\GG \prv h \hastype  \ol{A_n}\RImp a}{ \exists i:1\leq i\leq n.\, 
\GG \prv   M_i \not\in\| N_{i}\|\hastype A_i}{\GG \prv  h\ \Mns
\not\in\|h\ \Nns\|\hastype a} {\mbox{\tt ngrApp}}\vsk
\ianc{g\not\equiv h}
{\GG \prv  g\ \Mm \not\in\|h\ \Nns\|\hastype a} {\mbox{\tt ngrAppCls}}

\end{array}
\]
\caption{Not a ground instance: $\GG\vd M\not\in  \|N\| \hastype A$}
\label{fig:ngrinst}
\end{figure}

\smallskip We are now ready to prove exhaustivity of
complementation.

\begin{Theorem}
\label{thm:part2}
Assume $\GG\vd N\hastype A$ is a simple linear pattern; then if $\GG
\prv M\not\in \| N \| \hastype A$, then there is a $Q$ such that
$\GG\vd \mnot(N)\blip Q\hastype A$ and $ \GG \prv M\in \| Q\| \hastype
A$.
\end{Theorem}
\begin{proof}
  By induction on the structure of $\cD::\GG \prv M\not\in \| N \|
  \hastype A$. 
%and inversion on $\cD'::\GG\vd \mnot(N)\blip Q\hastype  A$.  
\bit 
\itc  $\cD$ ends in \texttt{ngrFlx}: by Lemma \ref{le:exhflex}.
%   Again observe that $E\ 
% \ol{x_{n}^{l}}$ can be seen as $E\ \Phi^{u}\Omega^{0}\Delta^{1}\ 
% x^{d}$, where $x$ is determined; indeed if $x$ is undetermined, the
% result holds trivially; by Corollary \ref{co:exh} either
% $\GG;(\O,x\oftp C);\D\vd M\hastype A$ or $(\GG,\O,\D);\cdot;x\oftp
% C;\vd M\hastype A$ and either $\GG;\O;(\D,x\oftp C)\vd M\hastype A$ or
% $(\GG,\O,\D);\cdot;x\oftp C \vd M\hastype A$, depending on the
% polarity of $d$.  Thus $\GG\vd M\in \|E\ \Phi^{u}\Omega ^{0}\Delta
% ^{1}\ x^{d}\|$ or $\GG \vd M\in\|F\ \Phi^{u}\Omega ^{u}\Delta ^{u}\ 
% x^{-d}\|$ for some $d\in\{1,0\}$.
\itc $\cD$ ends in \texttt{ngrAppCls}.
\btab
$\GG \prv  g\ \Mm \not\in\|h\ \Nns\|\hastype a$\bh
$\GG\prv  \mnot (h\ \ol{N_n^1}) \blip  
(\dots (g\ (Z_{1} \ \GG^{u}))^{1}\dots (Z_{m}\ \GG^{u}))^{1}\hastype a$\`
By rule $\mnot\mbox{\tt App}^1$\\ 
$\GG\vd g\ \Mm\in \|g\ (Z_{1}  \ \GG^{u})^{1}\dots
(Z_{m}\ \GG^{u})^{1}\|\hastype a$\br \texttt{grApp}
\etab
\itc$\cD$ ends in \texttt{ngrApp}:
\btab
$\GG \prv  h\ \Mns\not\in\|h\ \Nns\|\hastype a$\bh
$\GG \prv   M_i \not\in\| N_{i}\|\hastype A_i$  for some $1\leq i\leq n$ \bs
$\GG\vd\mnot(N_{i}) \blip  Q\hastype A_i$ and 
$ \GG \prv M_{i}\in \| Q\| \hastype A_i$  \bi\\
 $\GG\vd M_{j}\in\|(Z_{j}\ \ \GG^{u}
 )^{1}\|$ for all  $j\neq i, 1\leq j\leq n$\` By rule \texttt{grFlx}\\ 
$\GG\prv  \mnot (h\ \ol{M_n^1}) \blip  
(\dots (h\ (Z_{1}\ \GG^{u} ))^{1}\dots (Z_{i-1}\ \GG^{u} )^{1} \ N^{1}\ 
(Z_{i+1}\ \GG^{u} )^{1}\dots (Z_{n}\ \GG^{u}))^{1}\hastype a$\br
$\mnot\mbox{\tt Lam}$\\
$\GG \prv h\ \ol{M_n^1}\in \| h\ (Z_{1}\ \GG^{u} )^{1}\dots (Z_{i-1}\ \GG^{u}
 )^{1}\ Q^{1}\ (Z_{i+1}\ \GG^{u} )^{1}\dots (Z_{m}\ \GG^{u} )^{1} \|
 \hastype a$ \` By rule \texttt{grApp}.
\etab
\itc $\cD$ ends in \texttt{ngrLam}. 
 \btab
$\GG \prv \lxua M\not\in \|\lxua N\| \hastype A\TImp B$ \bh
$ \GG,\xoa \prv M\not\in \| N\| \hastype B$\bs
$\GG,x\oftp A\vd\mnot(N)\blip Q\hastype B$ and $ \GG,\xoa \prv M\in \| Q\|
\hastype B$ for some $Q$ \bi\\
$\GG\vd\mnot(\lxua N)\blip\lxua Q \hastype A\TImp B$\br $\mnot\mbox{\tt Lam}$\\
$\GG\vd\lxua M\in\|\lxua Q\|\hastype A\TImp B$\br \texttt{grLam}
  \etab\enit 
\end{proof}

\begin{Corollary}[Partition Lemma]
\label{le:part}
For a fixed signature $\Sigma$ let $\GG\vd N \hastype A$ be a linear
simple term:
\ben
\item (Disjointness) It is not the case that $\GG\prv M\in \| N
\|\hastype A$ and $\GG\prv M\in \| \mmnot(N) \|\hastype A$.
\item (Exhaustivity) $\GG\prv M\in \| N \| \hastype A$ or $\GG\prv
M\in \| \mmnot(N) \|\hastype A$.  \enen
\end{Corollary}
\begin{proof}
  Disjointness is entailed by Theorem \ref{thm:part1},
% and the canonical form Theorem (Theorem \ref{thm:canonical}),
  exhaustivity by Theorem \ref{thm:part2}.
\end{proof}


\section{Unification of Simple Terms 
% in the Strict $\lambda$-Calculus
}
\label{sec:sunif}

As we observed earlier in Chapter \ref{ch:el-rel}, we can solve a
relative complement problem pairing complementation with intersection.
We thus address now the task of giving an algorithm for unification of
(linear) simple terms.  
We start by determining when two labeling are
compatible:
 \beq 1 
\cap 1 = u \cap 1 = 1\cap u = 1\\ 
0 \cap 0 = u \cap 0 = 0\cap u = 0\\ 
u\cap u = u 
\eneq
%  we define an intersection operator on occurrence labels as 
% the symmetric and idempotent extension of the following partial 
% operation: 

% \beq
% 1\cap u = 1\\ 0\cap u = 0\\ u\cap u = u
% \eneq

Recall that $\Phi$ is a list of labeled bound variables; we can extend
the intersection operations to these contexts.
\beq 
\cdot\mcap \cdot & = & \cdot\\
( \Phi, x^k)\mcap ( \Phi', x^{k'}) & = & (\Phi\mcap \Phi', x^{k\mcap
k'}) \quad\mbox{\textrm{if $k\mcap k'$ is defined.}} 
 \eneq

 \newcommand{\godf}{\GG_{1};\Omega_{1};\Delta_{1}}
\newcommand{\gods}{\GG_{2};\Omega_{2};\Delta_{2}}
\newcommand{\godt}{(\GG_{1}\cap\GG_{2});(\Omega_{1},\Omega_{2});(\Delta_{1},\Delta_{2})}

% If $ \godf\vd\Phi_1\ ok$ and $\gods\vd\Phi_2\ ok$, and 
% $\Phi_{1}\cap\Phi_{2}$ is defined, the we call those contexts
% \emph{compatible}.
% \bmeta Do I still need this?\emeta
\begin{Remark}
\label{rmk:compa}
If $\GG_i;\O_i;\D_i\vd\Phi_i\ ok$, $1\leq i\leq 2$, then
$(\GG_1\cap\GG_2);(\O_1,\O_2);(\D_1,\D_2)\vd (\Phi_1\cap\Phi_2) \ ok$,
where $\GG_1\cap\GG_2$ denotes set-theoretic intersection and
$(\Phi_1\cap\Phi_2)(x)\eqdef \Phi_1(x)\cap\Phi_2(x)$.  Indeed,
$(\Phi_1\cap\Phi_2)(x)=u$ iff $x\in\dom(\GG_{1})$ and $x\in\dom(
\GG_2)$; moreover $(\Phi_1\cap\Phi_2)(x)=0$ iff either
$x\in\dom(\O_1\cup\GG_{2})$ or $x\in\dom(\O_2\cup\GG_{1})$.
Analogously for $(\Phi_1\cap\Phi_2)(x)=1$.  From that, as before, it
follows that $\Psi\vd M\in \|E_{A}\ \Phi_{1}\cap\Phi_{2}\|$ iff
$M\da  \l \Phi_{1}\cap\Phi_{2}\,.\,S$ such that
$(\GG_1\cap\GG_2);(\O_1,\O_2);(\D_1,\D_2)\vd S\hastype A$.
\end{Remark}

\smallskip
Following standard terminology with call atomic terms whose head is a
free or bound variable \emph{rigid}, while terms whose head is an
existential variable is called \emph{flexible}.


\begin{Definition}[Higher-Order Pattern Intersection]
Fix a signature $\Sigma$. For simple linear terms $M$ and $N$ without
shared variables such that $\GG \prv M \hastype A$ and $\GG \prv N
\hastype A$, define $\GG\prv M \mcap N \blip Q \hastype A$ by the
following rules:
%\begin{small}
\[
\begin{array}{c}
\ianc{}
{\GG\prv  (E_1 \ \Phi_1)\mcap   (E_2\ \Phi_2)\blip  H\ (\Phi_{1}\mcap \Phi_{2}) \hastype  a} 
{\mcap FF}
\vsk
\mbox{\textrm{no rule for flex-flex same}}
\vsk
\ianc{c\in\Sigma\quad \GG\prv  (H_1 \ \Phi_{1}) \mcap 
M_{1}\blip N_{1}\hastype A_{1}\cdots \GG\prv  (H_n \ \Phi_{n})\mcap 
M_{n}\blip N_{n}\hastype A_{n}  } 
{ \GG\prv  (E \ \Phi) \mcap (c\ \Mns)\blip  c\ \Nns\hastype  a} {\mcap
  FR^c }
\vsk
\ianc{y\in\GG\quad  \quad \GG\prv  (H_1 \ \Phi_{1})\mcap 
M_{1}\blip N_{1}\hastype A_{1}\cdots \GG\prv  (H_n \ \Phi_{n})\mcap 
M_{n}\blip N_{n}\hastype A_{n} } 
{\GG\prv (E\ \Phi) \mcap (y\ \Mns)\blip  y\ \Nns \hastype  a} {\mcap FR^y }
\vsk
\ianc{ h\in\GG\cup\Sigma\quad \GG\prv  M_1 \mcap N_{1} \blip
  Q_1\hastype  A_1 \cdots \GG\prv  M_n \mcap N_{n}\blip  Q_n \hastype  A_n} 
{\GG\prv   h\ \Mns\mcap h\ \Nns \blip  h\ \ol{Q_{n}^{1}} \hastype  a}
{\mcap RR}
\vsk
\ianc{\GG,x\oftp A\prv   M  \mcap  N \blip  Q\hastype  B}
{\GG\prv   \lxua M  \mcap \lxua N \blip \lxua Q \hastype  A\TImp B}{\mcap L}
\end{array}
\]
%\end{small}
where the $H$'s are fresh variables of appropriate typing and $n\geq
0$. We omit two rules $\mcap RF^c$ and $\mcap RF^y$ which are
symmetric to $\mcap FR^c$ and $\mcap FR^y$.
 % The rule 
% $\mcap FR^c $ has the following proviso: for all $x\in \Phi$ and
% $1\leq i\leq n$
% \beq
% \forall x. \Phi(x) = 0 & \Imp & \forall i\,.\, \Phi_{i}(x) = 0\\ 
% \forall x. \Phi(x) = u & \Imp & \forall i\,.\, \Phi_{i}(x) = u\\ 
% \forall x. \Phi(x) = 1 & \Imp & \exists i\,.\, \Phi_{i}(x) = 1
% %\And \forall j, j\not = i. \Phi_{j}(x)\not = u
% \eneq
% The rule 
% $\mcapFR^y $ has the additional proviso: 
% \beq
% \Phi(y) \not = 0\And ( \Phi(y)=1& \Imp & \forall i. \Phi_{i}(y) = u)\ignore{\\
% \forall x. \Phi(x) = 0 & \Imp & \forall i. \Phi_{i}(x) = 0\\ 
% \forall x. \Phi(x) = u & \Imp & \forall i. \Phi_{i}(x) = u\\ 
% \forall x. \Phi(x) = 1 & \Imp & \exists i. \Phi_{i}(x) = 0
% \And \forall j, j\not = i. \Phi_{j}(x)\not = u
% }\eneq
% Finally define 
% \beq
% M\mbigcap N \hastype A & =& \{Q\mid\cdot\prv  M\mcap N = Q \hastype  A\}
% \eneq
The rules
$\mcap FR^c$ and $\mcap RF^c$ have the following proviso: for all
$x\in \Phi$ and $1\leq i,j\leq n$:
\beq
\forall x. \Phi(x) = 0  \Imp  \forall i\,.\, \Phi_{i}(x) = 0\\ 
\forall x. \Phi(x) = u  \Imp  \forall i\,.\, \Phi_{i}(x) = u\\ 
\forall x. \Phi(x) = 1  \Imp  \exists i\,.\, \Phi_{i}(x) = 1
\And \forall j, j\not = i. \Phi_{j}(x) = u
\eneq
The rules $\mcap FR^y$ and $\mcap RF^y$ are subject to the
proviso:
\beq
\forall x. \Phi(x) = 0  \Imp  \forall i\,.\, \Phi_{i}(x) = 0\\ 
\forall x. \Phi(x) = u  \Imp  \forall i\,.\, \Phi_{i}(x) = u\\ 
\forall x. x \not= y \And \Phi(x) = 1  \Imp  \exists i\,.\, \Phi_{i}(x) = 1
\And \forall j, j\not = i. \Phi_{j}(x) = u \\
\Phi(y) = u \Or
(\Phi(y)=1 \And  \forall i. \Phi_{i}(y) = u)
\eneq
Finally define $\GG\vd M\mbigcap N \hastype A = {\cal Q}$ if ${\cal Q}=
 \{Q\mid\GG\prv  M\mcap N \blip  Q \hastype  A\}$.
\end{Definition} 

Some remarks are in order:
\bit
\item In rule $\mcap FF$ we can assume that the same list of
  variables, though with different labeling, is the argument of $E,F$
  and $H$, since simple terms are fully-applied and due to linearity
  we can always reorder the context to the same list.
\item Since patterns are linear and $M$ and $N$ share no pattern
  variables, the flex-flex case arises only with distinct variables.
  This also means we do not have to apply substitutions or perform the
  customary occurs-check.
\item In the flex/rigid and rigid/flex rules, the proviso enforces the
  typing discipline since each strict variable $x$ must be strict in
  some premise.
% The modified condition on $y$ takes into account that the head of an
% application constitutes a strict occurrence.
% In  rule $\mcap\_FlxRgd$ the proviso enforces the typing discipline, 
% for which $x$ must be strict in some premise.
  If instead $y$ is the projected variable, the modified condition on
  $y$ takes into account that the head of an application constitutes a
  strict occurrence; moreover, since $y$ did occur, it
  is set to $u$ in the rest of the computation, as there are no more
  requirements on that variable.
\item The symmetric rules take the place of an explicit exchange rule
  that is problematic \wrt termination. 
\enit

The following example illustrates how the Flex-Rigid rules, in this 
case $\mcap FR^c$, make unification on simple terms finitary.

\begin{Example}
  Consider the unification problem
  $$x\oftp A\prv E\ x^{1}\mbigcap\ c\ (F\ x^{u})^{1} \ (F'\ 
  x^{u})^{1}$$
  Since $x$ is strict in the LHS, there are two ways in
  which $\Phi$ can be `split' leading to the following sub-problems:
\[
\begin{array}{rlrr}
1. &x\oftp A\prv E' \ x^{1}\mcap\  F\  x^{u} \blip  H\  x^{1}
& & x\oftp A\prv E''\ x^{u}\mcap\  F'\  x^{u} \blip  H'\  x^{u}
\\
2. & x\oftp A\prv E' \ x^{u}\mcap\  F\  x^{u} \blip  H\  x^{u}
& & x\oftp A\prv E''\ x^{1}\mcap\  F'\  x^{u} \blip  H'\  x^{1}
\end{array}
\]
Hence the result:
\begin{eqnarray*}
%\label{eq:int}
x\oftp A\prv E\ x^{1}\mbigcap\  c\ (F\  x^{u})^{1} \ (F'\  
x^{u})^{1}=  \{c\ (H\  x^{1})^{1} \ (H'\  x^{u})^1,c\ (H\  x^{u})^1 \ (H'\  
x^{1})^1\}
\end{eqnarray*}
\end{Example}

Note that, similarly to complementation, intersection return a
solution with some `overlapping' possible; again it is possible, in a
post-processing phase to make the result exclusive: for example the
above problem \ignore{(\ref{eq:int})} can be made explicit in:
\beq
\lefteqn{x\oftp A\prv E\ x^{1}\mbigcap\  c\ (F\  x^{u})^{1} \ (F'\  
x^{u})^{1} = }\\
& & \{c\ (H\ x^{1})^{1} \ (H'\ x^{0})^1,c\ (H\ x^{0})^1 \ 
(H'\ x^{1})^1,c\ (H\ x^{1})^1 \ (H'\ x^{1})^1\}
\eneq 
 
However, differently from complementation, we must remark that the
latter is not the most general solution \wrt the subsumption ordering
on terms based on the (reverse) partial information ordering on
labels.  Indeed, a member of the intersection, e.g.\ $c\ (H\ x^1)^1 \ 
(H'\ x^{0})^1$ is a lower bound of both terms above, \ie
\beq
c\ (H\ x^1)^1 \ (H'\ x^{0})^1 & \leq  & E\ x^1 \\
c\ (H\ x^1)^1 \ (H'\ x^{0})^1 & \leq & c\ (H\ x^{u})^1 \ (H'\ x^{u})^1
\eneq
but it is not the greatest upper bound:
$$c\ (H\ x^1)^1 \ (H'\ x^{0})^1\leq c\ 
(H\ x^1)^1 \ (H'\ x^{u})^1$$

\smallskip The following example illustrates the additional proviso on
$\mcap FR^{y}$:

\begin{Example}
  The unification problem $y\oftp A\vd (E\ y^{0}) \mbigcap (y\ (F\ 
  y^{u})^1 \ (F'\ y^{u})^1)$ has no solution, whereas $y\oftp A\vd (E\ 
  y^1) \mbigcap (y\ (F\ y^1)^1 \ (F'\ y^{0})^1)= \{y \ (H\ y^1)^1 \ 
  (H'\ y^{0})^1\} $.
\end{Example}


\begin{Lemma}
\label{le:flexunif}
Let $M$ be a closed simple term such that $\godf\vd M\hastype A$ and
$\gods\vd M\hastype A$
% be \emph{compatible} type assignments
; then $\godf\vd M\hastype A$ and $\gods\vd M\hastype A$ iff $\godt
\vd M\hastype A$.
\end{Lemma}
\begin{proof}
  ($\Imp$) By induction on the size of $(\GG_1\cup\GG_2)\setminus
  (\GG_1\cap\GG_2)$.
  \begin{itemize}
  \item[\textbf{Base}] Let $\GG_1=\GG_2$, thus $(\GG_1\cup\GG_2)\setminus
    (\GG_1\cap\GG_2)=\eset$. Then by Exclusivity (Lemma \ref{le:disj})
    $\O_1=\O_2$ and $\D_1=\D_2$ and the claim holds.
  \item[\textbf{Step}] Let $\GG_1=(\GG'_1,\xoc)$, where $x\not\in\dom(\GG_2)$.
    By Tightening (Lemma \ref{le:exh}) either
    $\GG'_1;(\O_1,\xoc);\D_1\vd M\hastype A$ or
    $\GG'_1;\O_1;(\D_1,\xoc)\vd M\hastype A$:
    \begin{itemize}
    \item[\subcase] 
      \btab
      $\GG'_1;(\O_1,\xoc);\D_1\vd M\hastype A$\ba
      $(\GG'_1\cap\GG_2);(\O_1,\xoc,\O_2);(\D_1,\D_2)\vd M\hastype
      A$\bi\\
      $(\GG_1\cap\GG_2);(\O_1,\xoc,\O_2);(\D_1,\D_2)\vd M\hastype
      A$\` $x\not\in\dom(\GG_2)$\\
      $(\GG_1\cap\GG_2);(\O_1,\O_2);(\D_1,\D_2)\vd M\hastype
      A$\` $x\in\dom(\O_2)$ by Lemma \ref{le:disj}
      \etab
    \item[\subcase] $\GG'_1;\O_1;(\D_1,\xoc)\vd M\hastype
      A$. Analogously. 
    \end{itemize}
  \end{itemize}
  ($\If$) \btab $\godt \vd M\hastype A$\bh
  $(\GG_1\cap\GG_2,\O_2);\O_1;(\D_1,\D_2)\vd M\hastype A$\` By
  Loosening$^0$ on $\O_2$\\
  $(\GG_1\cap\GG_2,\O_2,\D_2);\O_1;\D_1\vd M\hastype A$\` By
  Loosening$^1$ on $\D_2$\\
  $\godf\vd M\hastype A$\` Since $(\GG_1\cap\GG_2),\O_2,\D_2,\O_1,\D_1=\GG_1,\O_1,\D_1$\\
  $\gods\vd M\hastype A$\` Analogously
  \etab
\end{proof}
%\include{deriv}
\newcommand{\gm}{(\Gamma,\Delta_i^u);\Omega; \D^1_i} 
  
We introduce two $n$-ary strict application rules, one which
correspond to the imitation step and the other to projection, which
will be needed in the proof of Theorem \ref{thm:unif1} and
\ref{thm:unif2}; in the following we shorten $x\in\dom(\GG)$ to $x\in\GG$.

\beq 
\ianc{(\GG,\D^{u}_{i});\O;\D_i^1 \vd M_{i}\hastype A_{i}\quad 
1\leq i\leq n}{\Gamma;\Omega; \D\vd c\ M_1^1\dots M_{n}^1\hastype 
B}{\RImp E_{n}^{c}} 
\eneq 
where $\GG;\O;\cdot\vd c\ \hastype A_1\RImp\dots\RImp A_{n}\RImp B$ and 
\ben
\item 
$\forall x\in\D\,.\,\exists i
:1\leq i\leq n
\,.\,x\in\D_{i}^1$.
\item
$\forall i:1\leq i\leq n
\,.\,\D_{i}^{u}\cup\D_{i}^1=\D$.
\enen


%proj rule
\beq 
\ianc{(\GG,\D^{u}_{i});\O;\D_i^1 \vd M_{i}\hastype A_{i}\quad 
1\leq i\leq n}{\Gamma;\Omega; \D\vd y\ M_1^1\dots M_{n}^1\hastype 
B}{\RImp E_{n}^{y}} 
\eneq 
where $\GG_0;\O;\D_0\vd y \hastype A_1\RImp\dots\RImp A_{n}\RImp B$
%such that $\GG_0\cup\D_0=\GG\cup\D$
 and
\ben
\item 
$\forall x\in\D, x\not= y\,.\,\exists i:1\leq i\leq n
\,.\,x\in\D_{i}^1$.
\item
$\forall i:1\leq i\leq n
\,.\,\D_{i}^{u}\cup\D_{i}^1=\D$. 
\item $\D_0=\{y\}$ and $\forall i:1\leq i\leq n.\, y\in\D_i^u$.
\enen
Note that in the latter rule we consider only the case where $y$
occurs strictly, that is $\D_0=\{y\}$; indeed, if  $y\in\GG_0$, then
the rule is just a renaming of the previous rule $\RImp E_{n}^{c}$.

% Note how the side conditions in the $n$-ary rules mirrors the proviso
% on the intersection rules.  Firstly notice that if $\Phi(x) = 0$ then
% $x\in\O$ which is unchanged in the premises; thus $\forall i:1\leq
% i\leq n.  \Phi_{i}(x) = 0$.  Similarly for $\Phi(x) = u$.  Finally, if
% $\Phi(x) = 1$, the first condition is equal to $\exists i:1\leq i\leq
% n.  \Phi_{i}(x) = 1$, while the requirement $\forall j:1\leq i\leq n,
% j\neq i.  \Phi_{i}(x) = u$ is met by Loosening$^1$.  As far as the
% $\mcap FR^{y}$ rule is concerned the assumption on $\GG',\D'$ is
% equivalent to the additional proviso.

\smallskip
We proceed to show that both are derivable and invertible rules. 

\begin{Lemma}
\label{le:derivec}
Let $\GG;\O;\cdot\vd c \hastype A_1\RImp\dots\RImp 
A_{n}\RImp B$: if $\gm\vd M_{i}\hastype A_{i}$ for $1\leq 
i\leq j$, then $(\GG,\D^u);\O;\D^1\vd c\ M^1_1\dots 
M_{j}^1\hastype A_{j+1}\RImp\dots\RImp A_{n}\RImp B$, where
\bit
\item[1.] 
$\forall x\in\D^1.\exists i:1\leq i\leq j\,.\,x\in\D_{i}^1$.
\item[1'.]
$\forall x\in\D^u.\neg\exists i:1\leq i\leq j\,.\,x\in\D_{i}^{1}$.
\item[2.]
$\forall i:1\leq i\leq j\,.\,\D_{i}^{u}\cup\D_{i}^1=\D^u\cup\D^1$.
\enit
\end{Lemma}
\begin{proof}
By induction on $j$.
\bit
\item[$\mathbf{j=0}$] Set $\D^1=\cdot$; then by hypothesis and
  Weakening$^u$ 
  $(\GG,\D^u);\O;\cdot\vd c \hastype A_1\RImp\dots\RImp A_{n}\RImp B$.
\item[$\mathbf{j+1}$]
\btab
$\gm\vd M_i\hastype A_i, 1\leq i\leq j$\` By assumption\\
 $(\GG,\D^u);\O;\D^1\vd c\ M^1_1\dots 
M_{j}^1\hastype A_{j+1}\RImp\dots\RImp A_{n}\RImp B$\bi\\     
$(\GG,\D^u_{j+1});\O;\D^1_{j+1}\vd M_{j+1}\hastype A_{j+1}$\bh
%$(\GG,\D^u_{j+1});\O;\D^1_{j+1}\vd M_i\hastype A_i$\` By assumption\\
 $(\GG,\D^u_+);\O;\D^1_+\vd c\ M^1_1\dots 
M_{j+1}^1\hastype A_{j+2}\RImp\dots\RImp A_{n}\RImp B$ \br \ $\RImp E$
\etab
such that:
\bit
\item[(a)]
$x\in\D^1_+ \Bimp x\in \D^1_{j+1}$ or $x\in\D^1$.
\item [(b)]
$x\in\D^u_+\Bimp x\in\D^u_{j+1}$ and $x\in\D^u$. 
\enit
We now show that the last step satisfy the conditions in the claim.
\bit
\item[1.]
\btab
$x\in\D^1_+$\ba
$ x\in \D^1_{j+1}\cup\D^1$\` By (a)
\etab
\bit
\item[\subcase]
$ x\in \D^1_{j+1}$\\
$ \exists i\oftp 1\leq i\leq j+1\,.\, x\in\D^1_i$
\item[\subcase] $x\in\D^1       $
\btab
$x\in\D^1_i$, for some $1\leq i\leq j$\bi\\
$ \exists i\oftp 1\leq i\leq j+1\,.\, x\in\D^1_i$\` A fortiori
\etab
\enit
\item[1'.]
\btab
$x\in\D^u_+$\bh
$x\in\D^u$\` By (b)\\
$\neg \exists i\oftp 1\leq i\leq j\,.\, x\in\D^1_i$\bi\\
$x\in\D^u_{j+1}$\` By (b)\\
$x\not\in\D^1_{j+1}$\` By disjointness of  contexts\\
$\neg \exists i\oftp 1\leq i\leq j+1\,.\, x\in\D^1_i$
\etab
\item[2.]
\btab
$\forall i\oftp 1\leq i\leq j\,.\, \D^1_i\cup\D^u_i= \D^1\cup\D^u$\bi\\
$\D^1_{j+1}\cup\D^u_{j+1}= \D^1\cup\D^u$\bh
$\forall i\oftp 1\leq i\leq j+1\,.\, \D^1_i\cup\D^u_i= \D^1_+\cup\D^u_+$
 \` By (a) and (b) and set manipulations
\etab
\enit
\enit
\end{proof}

\begin{Lemma}
\label{le:invertec}
Let $\GG;\O;\cdot\vd c \hastype A_1\RImp\dots\RImp A_{n}\RImp
B$: if $(\GG,\D^u);\O;\D^1\vd c\ M^1_1\dots M_{j}^1\hastype
A_{j+1}\RImp\dots\RImp A_{n}\RImp B$, then for every $1\leq i\leq j$
there are $\D_i^u,\D_i^1$ such that $\gm \vd M_{i}\hastype A_{i}$ and
\bit
\item[1.] 
$\forall x\in\D^1.\exists i:1\leq i\leq j\,.\,x\in\D_{i}^1$.
\item[1'.]
$\forall x\in\D^u.\neg\exists i:1\leq i\leq j\,.\,x\in\D_{i}^{1}$.
\item[2.]
$\forall i:1\leq i\leq j\,.\,\D_{i}^{u}\cup\D_{i}^1=\D^u\cup\D^1$.
\enit
\end{Lemma}
\begin{proof}
By induction on $j$.
\bit
\item[$\mathbf{ j=0}$] Set $\D^1=\cdot$; then by hypothesis and
  Weakening$^u$
  $(\GG,\D^u);\O;\cdot\vd c \hastype A_1\RImp\dots\RImp A_{n}\RImp B$.
\item[$\mathbf{ j+1}$]
\btab
$(\GG,\D^u);\O;\D^1\vd c\ M^1_1\dots 
M_{j+1}^1\hastype A_{j+2}\RImp\dots\RImp A_{n}\RImp B$\ba
$(\GG,\D^u_+);\O;\D^1_+\vd c\ M^1_1\dots M_{j}^1\hastype
A_{j+1}\RImp\dots\RImp A_{n}\RImp B$ and \\ 
$(\GG,\D^u_{j+1});\O;\D^1_{j+1}\vd M_{j+1}\hastype A_{j+1}$\` By
inversion on rule $\RImp E$ and\\
($x\in\D^1_+ \Bimp x\in \D^1_{j+1}\Or x\in\D^1$) and ($x\in\D^u_+\Bimp
x\in\D^u_{j+1}\And x\in\D^u$)\\
$\gm \vd M_{i}\hastype A_{i}$ for $1\leq i\leq j$\bi
\etab
since the conditions on the claim are satisfied as in the above Lemma \ref{le:derivec}.
\enit
\end{proof}

\begin{Corollary}
\label{co:derivec}
Rule $\RImp E_{n}^c$ is derivable and invertible.
\end{Corollary}
\begin{proof}
For derivability, use Lemma \ref{le:derivec} with $j=n$, $\D^{u}=\cdot,\D^1=
\D$; conditions $1.$ and $2.$ are immediately satisfied. Ditto \wrt 
invertibility, using Lemma  \ref{le:invertec}.
\end{proof}

\begin{Lemma}
\label{le:derivey}
Let $\GG_0;\O;y\oftp\dots\vd y\hastype A_1\RImp\dots\RImp A_{n}\RImp
B$.
%where $\D_0=\{y\}$ or $\D'=\cdot \And y\in\GG_0$ and
%$(\GG,\D^u)'\cup \D'=\GG\cup\D^u\cup \D^1 $.
If $\gm \vd M_{i}\hastype A_{i}$ for $1\leq 
i\leq j$, then $(\GG,\D^u);\O;\D^1\vd y\ M^1_1\dots 
M_{j}^1\hastype A_{j+1}\RImp\dots\RImp A_{n}\RImp B$  and 
\bit
\item[1.] 
$\forall x\in\D^1.\exists i:1\leq i\leq j\,.\,x\in\D_{i}^1$.
\item[1'.]
$\forall x\in\D^u.\neg\exists i:1\leq i\leq j\,.\,x\in\D_{i}^{1}$.
\item[2.]
$\forall i:1\leq i\leq j\,.\,\D_{i}^{u}\cup\D_{i}^1=\D^u\cup\D^1$.
\enit
\end{Lemma}
\begin{proof}
By induction on $j$.
\bit
\item[$\mathbf{ j=0}$] Let $\D_1=\{y\}$ and weaken $\GG_0$ to
  $\GG,\D^u$; by hypothesis $(\GG,\D^u);\O;\D^1\vd y
  A_{1}\RImp\dots\RImp A_{n}\RImp B$.
% $(\GG,\D^u)';\O;\D_\vd y \hastype A_1\RImp\dots\RImp 
% A_{n}\RImp B$ \` By hypothesis\\
% $(\GG,\D^u);\O;\D^1\vd y \hastype A_1\RImp\dots\RImp 
% A_{n}\RImp B$ \` By the condition
  
\item[$\mathbf{j+1}$] Completely analogous to the same case in Lemma
  \ref{le:derivec}.
\enit
\end{proof}
\begin{Lemma}

\label{le:invertey}
Let $\GG_0;\O;y\oftp\dots\vd y\hastype A_1\RImp\dots\RImp A_{n}\RImp
B$: if $(\GG,\D^u);\O;\D^1\vd c\ M^1_1\dots M_{j}^1\hastype
A_{j+1}\RImp\dots\RImp A_{n}\RImp B$, then for every $1\leq i\leq j$
there are $\D_i^u,\D_i^1$ such that $\gm \vd M_{i}\hastype A_{i}$ and
\bit
\item[1.] 
$\forall x\in\D^1.\exists i:1\leq i\leq j\,.\,x\in\D_{i}^1$.
\item[1'.]
$\forall x\in\D^1.\neg\exists i:1\leq i\leq j\,.\,x\in\D_{i}^{u}$.
\item[2.]
$\forall i:1\leq i\leq j\,.\,\D_{i}^{u}\cup\D_{i}^1=\D^u\cup\D^1$.
\enit
\end{Lemma}
\begin{proof}
By induction on $j$ similarly to Lemma \ref{le:invertec}.
\end{proof}

\begin{Corollary}
\label{co:derivey}
Rule $\RImp E_{n}^y$ is derivable and invertible.
\end{Corollary}
\begin{proof}
As in Corollary \ref{co:derivec}, using Lemma  \ref{le:derivey} and
\ref{le:invertey}. 
\end{proof}

\bigskip
We are now ready to address soundness and completeness of
intersection:
\renewcommand{\tn}{\ol{t_n^1}}

\begin{Theorem}
\label{thm:unif1}
\renewcommand{\GG}{\Psi} For any simple linear term $N_1$ and $N_2$
without shared variables such that $\GG \prv N_1 \hastype A$ and $\GG
\prv N_2 \hastype A$, if $\GG\prv M\in\|N_1\|\hastype A$ and $\GG\prv
M\in\|N_{2}\|\hastype A$, then there is $N$ such that $\GG\vd N_1\mcap
N_{2}\blip N\hastype A$ and $\GG\prv M\in\|N\|\hastype A$.
\end{Theorem}
\begin{proof}
  \renewcommand{\GG}{\Psi} By simultaneous induction on the structure
  of $\cD_1::\GG \prv M\in\|N_1\| \hastype A$ and $\cD_2::\GG \prv
  M\in\| N_2\| \hastype A$.
%and inversion on $\cD::\GG\prv N_1\mcap N_{2}\blip  N\hastype A$.
\bit
\itc $\cD_1,\cD_2$ end in  \texttt{grFlx}; by Remark \ref{rmk:compa} and 
the left-to-right direction of Lemma \ref{le:flexunif}.
\itc $\cD_1$ ends in  \texttt{grFlx} and $\cD_2$ ends in \texttt{grApp}: there are
  two cases depending whether the head of $N_2$ is a constant or a
  bound variable:
\bit
\item[\emph{Imit}]
\btab
$\GG\vd M \in\|c\ \ol{Q_{n}^1}\|$\bh
$M\equiv c\ \Mns$ and  $\cD^2_i::\GG\vd M_{i}\in\|Q_{i}\|$ for all $1\leq i\leq n$ 
\bs
$\GG\vd c\ \Mns\in\|E\ \Phi\|$\bh
$c\ \Mns\da  t\ \Phi$, where $t\equiv \l\Phi\,.\,c\ \tn$ 
\bs
$\god\vd c\ \tn\hastype B$\` For $\god\vd\Phi\ ok$\\
$(\Gamma,\D^u_i);\O;\D^1_i\vd t_{i}\hastype A_{i}$\` For some
$\D^u_i,\D^u_i$ satisfying $1$ and $2$, by inversion on rule $\RImp
E^{n}_{c}$ \\
\` (Corollary \ref{co:derivec})\\ 
$\cD^1_i::\GG\vd M_{i}\in\|E_{i}\ \Phi_{i}\|$ \br\, \texttt{grFlx}
choosing $\Phi_i$ such that $(\Gamma,\D^u_i);\O;\D^1_i\vd\Phi_i \ ok$\\
$\cD_i::\GG\vd E_{i}\ \Phi_i\mcap Q_i \blip  N_i$ for  $1\leq i\leq n$
and\\
 $\GG\vd M_{i}\in\|N_{i}\|$\bi on $\cD_i^1,\cD_i^2$ since the
proviso is satisfied\\
$\cD::\GG\vd E\ \Phi\mcap c\ \ol{Q_{n}^1} \blip  c\ \Nns$\br
$\mcap FR^c$\\
$\GG\vd c\ \Mns\in\|c\ \Nns\|$\br \texttt{grApp}
\etab
\item[\emph{Proj}]  Proceed as above, but using inversion
on rule $\RImp E^{n}_{y}$, \ie Corollary \ref{co:derivey}.
\enit
\itc $\cD_2$ ends in  \texttt{grFlx} and $\cD_1$ ends in \texttt{grApp}:
symmetrical to the above.
\itc $\cD_1,\cD_2$ end in \texttt{grLam}:
\btab
$\GG\prv \lxua M\in\|\lxua N_1\|$ \bh
$\cD'_1:: \GG,x\oftp A\vd M\in\| N_1\|$\bs
$\GG\prv \lxua M\in\|\lxua N_{2}\|$\bh
$\cD'_2::\GG,x\oftp A\prv M\in\| N_{2}\|$\bs
$\cD'::\GG,x\oftp A\prv N_1\mcap N_{2}\blip N$ and 
$\GG,x\oftp A\prv M\in\| N\|$\bi on $\cD'_1,\cD'_2$\\
$\GG\vd \lxua N_1\mcap \lxua N_2 \blip  \lxua N$\br\\
$\GG\prv \lxua M\in\|\lxua N\|$\br
\etab
\itc $\cD_1,\cD_2$ end in \texttt{grApp}: a straightforward appeal to the
inductive hypothesis as in the above case. 
\enit
\end{proof}

% start other direction

For the other direction, we are going to prove a stronger result:
\begin{Theorem}
\label{thm:unif2}
\renewcommand{\GG}{\Psi} For any simple linear term $N_1$ and $N_2$
without shared variables such that $\GG \prv N_1 \hastype A$ and $\GG
\prv N_2 \hastype A$, for every $N$ such that $\GG\vd N_1\mcap
N_{2}\blip N$ if $\GG\prv M\in\|N\|\hastype A$, then $ \GG\prv
M\in\|N_1\|\hastype A$ and $\GG\prv M\in\|N_{2}\|\hastype A$ .
\end{Theorem}
\begin{proof}
\renewcommand{\GG}{\Psi}
By induction on the structure of $\cD::\GG\vd N_1\mcap N_{2}\blip  N$
and inversion on $\cD'::\GG\prv M\in\|N\|\hastype A$.
\bit
\itc $\cD$ ends in $\mcap FF$; by Remark \ref{rmk:compa} and the 
right-to-left direction of Lemma \ref{le:flexunif}.
\itc $\cD$ ends in  $\mcap FR $.
\btab
$\cD::\GG\vd E\ \Phi\mcap c\ \ol{Q_{n}^1} \blip  c\ \Nns$\bh
$\cD_i::\GG\vd E\ \Phi_i\mcap Q_i \blip N_i, 1\leq i\leq n$\bs
$\GG\vd c\ \Mns\in\|c\ \Nns\|$\bh
$\GG\vd M_i\in\|N_i\|$\bv
$\GG\vd M_{i}\in\|Q_{i}\|$ and $\GG\vd M_{i}\in\|E_{i}\ \Phi_{i}\|$
\bi on $\cD_i$\\
$M_{i}\da t\ \Phi_i$, where  $t\equiv \l\Phi_i\,.\,t_{i}$ 
such that  $(\GG_{i},D^u_i);\O;\D^1_i\vd t_{i}\hastype A_{i}$
\br $grFlx$ for $(\GG_{i},D^u_i);\O;\D^1_i\vd \Phi_i\ ok$  \\
$\god\vd c\ \ol{t^1_{n}}\hastype a$\` By  rule $\RImp 
E^{n}_{c}$ (Lemma \ref{le:derivec}), since the proviso satisfies $1,2$\\
$\GG\vd c\ \Mns\in\|E\ \Phi\|$\br \texttt{grFlx}\\
$\GG\vd c\ \Mns\in\|c\ \ol{Q^1_{n}}\|$\br \texttt{grApp}
\etab
\itc $\cD$ ends in  $\mcap FR^y$. Proceed as above, but using 
Lemma \ref{le:derivey}.
\itc $\cD$ ends in  $\mcap L$; by IH as in Theorem \ref{thm:unif1}
\itc $\cD$ ends in  $\mcap RR$; ditto.
\enit
\end{proof}
 
% \begin{Theorem}
% \label{thm:unif2}
% \renewcommand{\GG}{\Psi} For every simple linear term $N_1$ and $N_2$
% without shared variables such that $\GG \prv N_1 \hastype A$ and $\GG
% \prv N_2 \hastype A$, if there is $N$ such that $\GG\vd N_1\mcap
% N_{2}\blip N$ and for every $M$ it holds $\GG\prv M\in\|N\|\hastype
% A$, then $ \GG\prv M\in\|N_1\|\hastype A$ and $\GG\prv
% M\in\|N_{2}\|\hastype A$ .
% \end{Theorem}
% \begin{proof}
% \renewcommand{\GG}{\Psi}
% By simultaneous induction on the structure of the typing derivations and 
% inversion on $\cD::\GG\vd N_1\mcap N_{2}\blip  N$
% and  on $\cD'::\GG\prv M\in\|N\|\hastype A$.
% \bit
% \itc $\cD$ ends in $\mcap FF$; by Remark \ref{rmk:compa} and the 
% right-to-left direction of Lemma \ref{le:flexunif}.
% \itc $\cD$ ends in  $\mcap FR $.
% \btab
% $\cD::\GG\vd E\ \Phi\mcap c\ \ol{Q_{n}^1} \blip  c\ \Nns$\bh
% $\cD_i::\GG\vd E\ \Phi_i\mcap Q_i \blip N_i, 1\leq i\leq n$\bs
% $\GG\vd c\ \Mns\in\|c\ \Nns\|$\bh
% $\GG\vd M_{i}\in\|Q_{i}\|$ and $\GG\vd M_{i}\in\|E_{i}\ \Phi_{i}\|$
% \bi on $\cD_i$\\
% $M_{i}\da  t\ \Phi$, where  $t\equiv \l\Phi\,.\,t_{i}$ 
% for  $\Phi_{i}\vd t_{i}\hastype A_{i}$\br \texttt{grFlx}\\
% $\Phi\vd c\ \ol{t^1_{n}}\hastype a$\` By  rule $\RImp 
% E^{n}_{c}$ (Corollary \ref{co:derivec})\\
% $\GG\vd c\ \Mns\in\|E\ \Phi\|$\br\\
% $\GG\vd c\ \Mns\in\|c\ \ol{Q^1_{n}}\|$\br
% \etab
% \itc $\cD$ ends in  $\mcap FR^y$. Proceed as above, but using 
% Corollary \ref{co:derivey}.
% \itc 
% \btab
% $\GG\vd \lxua N_1\hastype A\TImp B$\bh
% $\GG\vd \lxua N_2\hastype A\TImp B$\bh
% $\GG,xoa\vd  N_1\hastype B$\bs
% $\GG,xoa\vd  N_2\hastype B$\bs
% $\cD'::\GG,x\oftp A\prv N_1\mcap N_{2}\blip N$ and 
% $\GG,x\oftp A\prv M\in\| N\|$ \bi for some $N$\\
% $\GG\vd \lxua N_1\mcap \lxua N_2 \blip  \lxua N$\br
% $\GG\prv \lxua M\in\|\lxua N_1\|$ \br
% $\cD'_1:: \GG,x\oftp A\vd M\in\| N_1\|$\bs
% $\GG\prv \lxua M\in\|\lxua N_{2}\|$\bh
% $\cD'_2::\GG,x\oftp A\prv M\in\| N_{2}\|$\bs



% $\GG\prv \lxua M\in\|\lxua N\|$\br
% \etab
% \itc $\cD$ ends in  $\mcap RR$; ditto.
% \enit
% \end{proof}

\begin{Corollary}[Adequacy of Pattern Intersection]
\label{co:unif}
Fix a signature $\Sigma$.  For every simple linear term $N_1$ and
$N_2$ without shared variables such that $\GG \prv N_1 \hastype A$ and
$\GG \prv N_2 \hastype A$, for every $M$, $\GG\prv M\in\|N_1\|\hastype
A$ and $\GG\prv M\in\|N_{2}\|\hastype A$ iff $\GG\prv
M\in\|N_1\mbigcap N_2\|\hastype A$.
\end{Corollary}
\begin{proof}
  From Theorem \ref{thm:unif1} and \ref{thm:unif2}.
\end{proof}



% We will overload our notation in the definition of families, indexed 
% by types of complementation and intersection operations between 
% \emph{sets} of terms:
% 
% \beq
% \mmnot_{A}\{M_1\mdots M_{m}\} & = & \{N\mid\forall i\in[1,m]  N\in 
% \mnot(M_{i}:A)\}\\
% \{M_1\mdots M_{m}\} \mbigcap_{A} \{N_1\mdots N_{n}\} & = & 
% \{P\mid \forall  i\in[1,m], \forall  j\in[1,n]\hastype A M\in M_{i}, 
% N\in N_{j}, P \in M\mbigcap N\hastype A\}
% \eneq

\section{The Algebra of Strict Terms}
\label{sec:algebra}

An interesting and natural question is wondering whether
complementation is involutive. The answer is of course positive, since
the latter is a boolean property and the complement operation has been
shown to satisfy ``tertium non datur'' and the principle of
non-contradiction. Rather than proving involution in isolation, we
will show that every other boolean property is satisfied. As the
complement of a term is possibly a finite set of terms we need to
extend the intersection and complement operations to \emph{finite }
sets of terms. For the sake of readability, we shall define this the
empty context.  It is clear, although cumbersome, how to generalize it.
We also drop the type information.

\begin{Definition}
\label{def:setop} If 
$\cM$ and $\cN$ are finite sets of linear simple terms of type $A$, define:
\beq      
\cM \mbc \cN & \eqdef & \{Q\mid Q\in M\mbigcap N, M\in \cM, N\in \cN\} 
\vsk
\mna (\cM) & \eqdef & \bigcap_{M\in\cM} \mmnot(M)
\eneq
\end{Definition}

Those operations on set of terms satisfy the same properties that 
`singleton' intersection and complementation do.

\begin{Corollary} [Adequacy of Set Intersection]
\label{co:setunif}
If $\cN_1,\cN_{2}$ are finite sets of linear simple terms of type $
A$, then $\GG\prv M\in\|\cN_1\|\hastype A$ and $\GG\prv
M\in\|\cN_{2}\|\hastype A$ iff $\GG\prv M\in\|\cN_1\mbc
\cN_{2}\|\hastype A$.
\end{Corollary}
\begin{proof}
  $\GG\prv M\in\|\cN_1\|\hastype A$ and $\GG\prv
  M\in\|\cN_{2}\|\hastype A$ iff there is $N_1\in\cN_1$ and
  $N_{2}\in\cN_{2}$ such that $\GG\prv M\in\|N_1\|\hastype A$ and
  $\GG\prv M\in\|N_{2}\|\hastype A$ iff, by Corollary \ref{co:unif},
  $\GG\prv M\in\|N_1\mbigcap N_{2}\|\hastype A$ iff, by definition,
  $\GG\prv M\in\|\cN_1\mbc \cN_{2}\|\hastype A$.
\end{proof}

\begin{Corollary}[Set Partition Lemma] 
% For a fixed signature $\Sigma$ let 
Let $ \cN $ be a finite set of linear simple terms of type $A$:
\label{co:setpart}
\ben
\item (Disjointness) It is not the case that $\GG\prv M\in \| \cN
  \|\hastype A$ and $\GG\prv M\in \| \mna(\cN) \|\hastype A$.  
\item (Exhaustivity) $\GG\prv M\in \| \cN \| \hastype A$ or $\GG\prv
  M\in \| \mna(\cN) \|\hastype A$.

\enen
\end{Corollary}
\begin{proof}\mbox{}
\ben
\item Assume $\GG\prv M\in \| \cN \|\hastype A$ and $\GG\prv M\in \|
  \mna(\cN) \|\hastype A$. By rule \texttt{gr}$_i$, $\GG\prv M\in \| N \|
  \hastype A$, for some $N\in\cN$. By definition, $\GG\prv M\in \|
  \mbc_{N\in\cN}\mmnot(N) \|\hastype A$; by (repeated application of)
  Corollary \ref{co:unif} $\GG\prv M\in \| \mmnot(N) \|\hastype A$,
  for every $N\in \cN$, impossible by the Partition Lemma.
% By the Partition Lemma, $\GG\prv M\in \| N \| \hastype A$ or
%   $\GG\prv M\in \| \mmnot(N) \|\hastype A$, for every $N\in \cN$.
%   Assume $\GG\prv M\in \| N \| \hastype A$; then $\GG\prv M\in \| \cN
%   \| \hastype A$ and finally $\GG\prv M\in \| \cN \| \hastype A$ or
%   $\GG\prv M\in \| \mna(\cN) \|\hastype A$. Otherwise assume $\GG\prv
%   M\in \| \mmnot(N) \|\hastype A$, for every $N\in \cN$. Then by
%   Corollary \ref{co:unif} $\GG\prv M\in \| \mbc_{N\in\cN}\mmnot(N)
%   \|\hastype A$, so by definition $\GG\prv M\in \| \mna(\cN)
%   \|\hastype A$ and finally $\GG\prv M\in \| \cN \| \hastype A$ or
%   $\GG\prv M\in \| \mna(\cN) \|\hastype A$.
\item Similarly to the above.
\enen
\end{proof}

It is therefore possible\fixed to organize the set
of \emph{finite} sets of simple terms over a given signature, call it
$\mathbf{\cal T}_{F}$ in a boolean algebra
% $\la \mathbf{\cal  T}_{F},\emptyset,\cup,\mbc,\mna\ra$
under set union, patterns intersection and complementation, by taking
 equality as extensional identity (on sets of ground terms), that is, in symbols:
\beq
% \cN_1\simeq \cN_2 & \mbox{iff} & \forall M\,.\, M\in\|\cN_1\| \mbox{
%  iff } M\in\|\cN_2\|
\cN_1\simeq \cN_2 & \mbox{iff} & \|\cN_1\| = \|\cN_2\|
\eneq


\smallskip
We now list some basic properties of intersection, which follows from 
Corollary \ref{co:unif} and will be useful   next.
\begin{Corollary}
\label{co:unifpr}
Let $M,N$ be simple linear terms of type $A$:
\ben
\item $ M\mbigcap M \simeq \{M\} $.
\item $ M\mbigcap N \simeq \GG\vd N\mbigcap M$.  
\enen
\end{Corollary}

\begin{Theorem}
\label{thm:algebra}
Consider the algebra  of finite sets of simple terms $\la \mathbf{\cal 
T}_{F},\emptyset,\cup,\mbc,\mna\ra$ under set union, pattern 
intersection and complementation. Then the following holds:
\ben
\item $\cM\mbc\cM \simeq \cM$.
\item $\cM\mbc\cN \simeq \cN\mbc\cM$.
\item\label{it:DM} $\cM\mbc(\cN\cup\cP)\simeq
  (\cM\mbc\cN)\cup(\cM\mbc\cP)$.
\item $\cM\mbc(\cN\mbc\cP) \simeq (\cM\mbc\cN)\mbc\cP$.
\item $\mna(\mna (\cM))\simeq\cM$.
\item $\mna( \mathbf{\cal T}_{F})\simeq \emptyset$.
\item $\mna (\emptyset)\simeq\mathbf{\cal T}_{F}$.  
\enen
\end{Theorem}
\begin{proof}
From Corollary \ref{co:unifpr}, \ref{co:setunif} and \ref{co:setpart}.
%\ben
% \mbox{}
% \ben
% \item
% From idempotency of $\mcap$, Corollary \ref{co:unifpr}.
% \item
% From commutativity of $\mcap$, Corollary \ref{co:unifpr}.  
% \item 
% Immediate from Corollary \ref{co:setunif} and properties of 
% set-theoretic union.
% \item 
% By induction on $\cP$.  If the latter is empty, the result is 
% immediate.  Otherwise
% \btab
%  $\cM\mbc(\cN\mbc \{M\}\cup\cP)=$\` LHS\\
% $\cM\mbc((\cN\mbc\{M\})\cup(\cN\mbc\cP)) =$ \` By $\ref{it:DM}.$\\
% $(\cM\mbc(\cN\mbc\{M\}))\cup\cM\mbc(\cN\mbc\cP))=$ \` By $\ref{it:DM}.$\\
% $((\cM\mbc\cN)\mbc\{M\})\cup (\cM\mbc\cN)\mbc\cP))=$\bi\\ 
% $(\cM\mbc\cN)\mbc ( \{M\}\cup\cP)$  \` By $\ref{it:DM}.$
% \etab
% \item
% $\GG\vd M\in \|\mna\mna \cM\|$ iff by Corollary \ref{co:setpart} 
% $\GG\vd M\not\in\|\mna \cM\|$ iff, again by Corollary \ref{co:setpart} 
% $\GG\vd M\in \|\cM\|$.
% \item
% Immediate from Corollary \ref{co:setpart}.
% \item
% Immediate from Corollary \ref{co:setpart}.
% \enen
\end{proof}


\begin{Corollary}
\label{co:boolean}
The algebra $\la \mathbf{\cal T}_{F},\emptyset,\cup,\mbc,\mna\ra$ 
of finite sets of simple linear terms is boolean.
\end{Corollary}
\begin{proof}
Theorem \ref{thm:algebra} confirms that the above operators satisfy 
the boolean algebra axioms.
\end{proof}

Corollary \ref{co:boolean} guarantees that any other boolean operation 
is definable: indeed complementation and intersection alone allows to 
define the \emph{relative} complement operation:

\begin{Definition}
\label{def:relcompl}
Given $\cM$ and $\cN$ finite sets of terms of type $A$:
\beq
\cM - \cN & \eqdef & \cM\mbc (\mna (\cN))
\eneq
\end{Definition}

The adequacy of this encoding follows immediately from the Partition 
Lemma and soundness and completeness of intersection.

\begin{Corollary}
$\GG\vd M\in\|\cM\| - \|\cN\|$ iff $\GG\vd M\in\|\cM-\cN\|$ .
\end{Corollary}
\begin{proof}
$\GG\vd M\in\|\cM\| - \|\cN\|$ iff $\GG\vd M\in \|\cM\|$ and $\GG\vd 
M\not\in\|N\|$ for every $N\in\cN$ iff (Corollary \ref{co:setpart}) 
$\GG\vd M\in \|\cM\|$ and $\GG\vd M\in\|\mmnot(N)\|$  iff (Corollary
\ref{co:unif})  $\GG\vd M\in \| \cM\mbc 
(\mna (\cN))\|$ iff by definition $\GG\vd M\in\|\cM-\cN\|$.
\end{proof}

It is notable that the $\cup$ operator must be set-theoretic union
rather than anti-unification or generalization, as traditional in
lattice-theoretic investigations of the algebra of terms \cite{Plotkin71}. The problem
is the intrinsic classical nature of complementation which is not
compatible with the very irregular structure of the lattice of terms
where anti-unification is interpreted as the lowest upper bound.
Indeed, De Morgan's rules would fail, namely, denoting
anti-unification with $`\Or'$:
$$\mnot(s(0)\Or s(s(0))) = \mnot(s(X))=0 \not=
\mnot(s(0))\cap\mnot(s(s(0)))=\{0,s(s(s(X)))\}$$

\medskip We end this chapter with a preview of how term complement
will be used as a building block of the clause complement algorithm.

\begin{Example}
\label{ex:combi}
We can  combine Example \ref{ex:lam} and \ref{ex:etardx}:
\[
\begin{array}{lll}
\mmnot\{(app\ (lam\ (\lamb{x^u}{exp} E\ x^u))\ 
F),lam(\lamb{x^u}{exp} app\ (E\ x^o) \ x)\}
=\\
\quad \mmnot(app\ (lam\ (\lamb{x^u}{exp} E\ x^u))\ 
F)\mbc \mbox{}\\
\quad \mmnot(lam(\lamb{x^{u}}{exp} app\ (E\ x^{0})\ x ))=\\
\\
\qquad \{ lam\ (\lamb{x^u}{exp} (H\ x^u)),\\
\qquad app\ (app\ H\ H') \ H''\}\\
\qquad\mbox{} \mbc \mbox{}\\
\\
\qquad\{ lam(\lamb{x^u}{exp} app\ (H\ x^1)\ (H'\ x^u)),\\
\qquad lam(\lamb{x^u}{exp} app\ (H\ x^u)\ (app\ (H'\ x^u) \ (H'' x^u))), \\
\qquad lam(\lamb{x^u}{exp} app\ (H\ x^u)\ ( lam(\lamb{y^u}{exp} H'\ x^u\ y^u))),\\
\qquad lam(\lamb{x^u}{exp} lam(\lamb{y^u}{exp} H\ x^u\ y^u) ),\\
\qquad lam(\lamb{x^u}{exp}x),\\
\qquad app\ H\ H'\}=\\
\\
\qquad\qquad \{ lam(\lamb{x^u}{exp} app\ (H\ x^1)\ (H'\ x^{u})), \\ 
\qquad\qquad  lam(\lamb{x^u}{exp} app\ (H\ x^u)\ (app\ (H'\ x^{u}) \ ( H''\ x^{u}))),\\
\qquad\qquad lam(\lamb{x^u}{exp} app\ (H\ x^u)\ ( lam(\lamb{y^u}{exp} H'\ x^u\ y^u)))\\
\qquad\qquad  lam(\lamb{x^u}{exp} lam(\lamb{y^u}{exp} H'\ x^u\ y^u)),\\
\qquad \qquad lam(\lamb{x^u}{exp}x),\\
\qquad\qquad app\ ( app\ H\ H')\  H''\}
\end{array}
\]
Thus given the `program':
\[
\begin{array}{lll}
betarx & : & isredx(app\ (lam\ (\lamb{x^u}{exp} E\ x^u))\ F ).\\
etarx & : & isredx(lam(\lamb{x^u}{exp} app\ (E\ x^0) \ x)).
\end{array}\]
Computing the complement of each head as in Example \ref{ex:combi}
yields the complementary program:
\[
\begin{array}{lll}
nb1 & : & non\_isredx(lam(\lamb{x^u}{exp} app\ (H\ x^1)\ (H'\ x^{u}))).\\
nb2 & : & non\_isredx( lam(\lamb{x^u}{exp} app\ (H\ x^u)\
 (app\ (H'\ x^{u}) \ ( H''\ x^{u})))).\\
nb3 & : & non\_isredx(lam(\lamb{x^u}{exp} app\ (H\ x^u)\ 
( lam(\lamb{y^u}{exp} H'\ x^u\ y^u)))).\\
nb4 & : & non\_isredx(lam(\lamb{x^u}{exp} lam(\lamb{y^u}{exp} H\ x^u\ 
y^u) )).\\
nbr & : & non\_isredx(lam(\lamb{x^u}{exp}x)).\\ 
nb6 & : & non\_isredx( app\ (app\ H\ H')\ H''\ ).
\end{array}\]
\end{Example}

\section{Summary}

In this part of the dissertation, we have been concerned with the
relative complement problem in a setting where patterns may contain
binding operators, so-called \emph{higher-order patterns}.
Higher-order patterns inherit many pleasant properties from the
first-order case, even for complex type theories.
Unfortunately, the complement operation does not generalize as
smoothly. The complement of a partially applied \ho pattern cannot be
described by a pattern, or even a by finite set of patterns.  The
formulation of the problem suggests that we should consider a
$\lambda$-calculus with an internal notion of \emph{strictness} so
that we can directly express that a term must depend on a given
variable.  For reasons of symmetry and elegance we have also added the dual
concept of \emph{invariance} expressing that a given term does not
depend on a given variable. We have developed such a calculus, so that
we can show that for a suitable embedding in our calculus simply-typed
patterns have the following properties:
\begin{enumerate}
 \item The complement of a linear pattern is a finite set of linear
patterns.
 \item Unification of two patterns is decidable and leads to a finite set of
most general unifiers.
\end{enumerate}
Consequently, finite sets of linear patterns in the strict
$\lambda$-calculus are closed under complement and unification.  If we think
of finite sets of linear patterns as representing the set of all their
ground instances, then they form a boolean algebra under simple union,
intersection (implemented via unification) and the complement operation.
