\documentclass{llncs}
\usepackage{latexsym}
% \usepackage{amssymb}
\usepackage{cdsty}
%\usepackage{prooftree}
\def\zzctdrawdotedge{\drawdotedge{4pt}0}
\def\ctabutborderlr{1em}
\def\ctabutbordertb{1ex}
\usepackage{llncs-com}


\newcommand{\UImp}{\GImp{u}}
\newcommand{\god}{\Gamma; \Omega;\Delta}
\newcommand{\betared}{\stackrel{\beta}{\longrightarrow}}
\newcommand{\etaexp}{\stackrel{\bar\eta}{\longrightarrow}}
\newcommand{\lxua}{\lambda x^{u}\!:\!  A.\, }
\newcommand{\D}{\Delta}
\renewcommand{\O}{\Omega}
\newcommand{\dmn}{(\D_{M},\D_{N})}
\newcommand{\Mns}{\overline{M_n^1}}
\newcommand{\Nns}{\overline{N_n^1}}
\newcommand{\emp}{;\cdot;\cdot}


\title{Higher-Order Pattern Complement\\ and Strict
Lambda-Calculus\thanks{This work has been partially supported by NSF
Grant CCR-9619584.}}

\author{Alberto Momigliano\inst{1} and Frank Pfenning\inst{2}}

\institute{Department of Philosophy \and
	   Department of Computer Science \\
           Carnegie Mellon University\\
	   Pittsburgh, PA 15213, U.S.A.\\[1ex]
  \texttt{mobile@cs.cmu.edu} \hspace{2em} \texttt{fp@cs.cmu.edu}}
\date{UNFINISHED DRAFT OF \today}

\bibliographystyle{alpha}

\begin{document}

\pagestyle{plain}

\maketitle

\begin{abstract}
We address the problem of \ho patterns complementation.  Differently 
from the \fo case, the complement of a non-fully applied pattern 
cannot be described by a pattern, or even by a finite set of 
patterns.  This is due to the issue of \emph{dependency constraints}.  
We therefore introduce 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.  We show that finite sets of linear 
patterns in this calculus are closed under complement and 
unification.  Our principal application is the transformational 
approach to negation in higher-order logic programs \cite{Bar90}.
\end{abstract}

\section{Introduction}
\label{sec:intro}

%\newcommand{\lamb}[2]{\lambda {#1}\!:\!{#2}.\,}
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 or complement also arise
frequently.  In this paper 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{Klop??,Miller91jlc,Nipkow91lics}.  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{Hanus96}.  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.

Unfortunately, the complement operation does not generalize as smoothly.
Lugiez~\cite{Lug95} has studied the more general problem of
higher-order disunification and had to go outside the language of
patterns and terms to describe complex constraints on sets of solutions.
We can isolate one basic difficulty: a pattern such as $\lambda x\ldot
E\, x$ for an existential variable $E$ matches any term of appropriate
type, while $\lambda x\ldot E$ matches precisely those terms $\lambda
x\ldot M$ where $M$ does not depend on $x$.  The complement then
consists of all terms $\lambda x\ldot M$ such that $M$ \emph{does}
depend on $x$.  However, this set cannot be described by a pattern, or
even a finite set of patterns.

This formulation of the problem immediately 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
also add the dual concept of \emph{invariance} expressing that a given
term does not depend on a given variable.  As in the first-order case,
it is useful to single out the case of \emph{linear patterns}, namely
those where no existential variable occurs more than once.  We show that
patterns in our calculus 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 sets of ground
terms (the union of all ground instances), then they form a boolean
algebra under simple union, intersection (implemented via unification)
and the complement operation

Our principal application is the transformational approach to negation
in higher-order logic programs, but we believe that our results could
also be applied in the implementation and analysis of functional logic
languages or logical frameworks.

\section{Complementing Fully Applied Patterns}
\newcommand{\mmnot}{\neg}

In this section we treat the important special case \emph{fully applied
patterns} in the setting of the simply-typed $\lambda$-calculus.  For
this case, the main difference to the first-order case is that we need
to carefully keep track of bound variables.

We use $P$ to for atomic types, $c$ for term-level constants, and
$x$ for term-level variables.

\[ \begin{array}{rrcl}
 \mbox{\textit{Simple Types}} & A & \bnfas & P \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, P
\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. We promote ``,'' to 
denote 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 useful notion of normal
form 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 Sect.~\ref{sec:strict}.  See this
section 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.  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).

Semantically, an existential variable $E_A$ stands for all canonical
terms $M$ of type $A$ in the \textbf{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 Fig.~
\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.

\begin{example}
\label{ex:lam}
Suppose we want to encode predicates on the signature of the (untyped) 
$\l$-calculus.  To distinguish between the former and the 
meta-language we introduce the following signature, which 
declares constants of well-known meaning and type (see 
\cite{Pfenning94un}).
\beq
\Sigma  & \bnfas & exp\hastype \mbox{\textrm{type}}, lam\hastype (exp\Imp 
exp)\Imp exp, app \oftp exp \Imp exp\Imp exp\\
E & \bnfas & x \mid lam\ (\lx E) \mid app \ 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 \emph{Mini-ML} in 
\cite{Pfenning94un}) bijectively relates $\alpha$-equivalence classes 
of object-level terms with $\beta\eta$-equivalence classes at the 
meta-level.}  
The term $\lamb{x} {exp} app \ (E_{1}\ x) (E_{2}\ x)$ represents the set
of all unary functions which return an application (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 abstraction. In symbols:

\[
\mmnot(\lamb{x} {exp} app \ (E_{1}\ x) (E_{2}\ x))= 
\{ \lamb{x}{exp} x, \lamb{x}{exp}lam \ (\lamb {y}{exp}  (E\  x)\ y)\}
 \]
\end{example}

% \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}

While, as  we will see, the class of patterns is \emph{not} closed
under complement, 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$.  Fully applied patterns play an important role in
functional logic programming and rewriting~\cite{Hanus96} 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

\smallskip
For patterns which are not fully applied, the complement cannot
be expressed as a finite set of patterns, as the following example
illustrates.

 \begin{example}
Consider the set of terms representing a
unary function which does not depend on its argument:
\beq
% \begin{equation}
\label{eq:vac}
\lx E
% \end{equation}
\eneq
Intuitively its complement should be the set of terms encoding the 
functions which  do use, somehow, its arguments. 
 \end{example}
 
 While it is easy to write
a logic program which verifies the former,
\ignore{\[
\begin{array}{lll}
strict(\lx x).\\
strict(\lx app (E_{1} x) (E_{2} x)) 
   &\If & strict(\lx E_{1} x) .\\
strict(\lx app (E_{1} x) (E_{2} x)) 
   &\If &  strict(\lx E_{2} x).\\
strict(\lx all (\l y. (E x y))) &\If & \PI {z} { exp}  strict(\lx (E x z)).
\end{array}
\]
Hence the complement of a fact would lead to possibly hypothetical 
and parametrical clauses.  More in general, we would have to decorate 
programs with predicates} we are unable to  represent the complement of non-fully 
applied patterns.  In other words, the simply typed 
$\l$ calculus, or, for that matter, every other intuitionistic type 
theory 
\begin{metanote}
are we implying that strictness, encoded as an 
arithmetic property is not a relation expressible in say CC? It may 
not be extended polynomial, though
\end{metanote}
is not strong enough to directly make available a notion of 
\emph{strictness} which is required to represent the complement of non-fully 
applied patterns and, we conjecture, any other non-fully applied 
expressions built out of a meta-linguistic binding operator.  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.


As can be seen from the example, we must be able to express that a 
function \emph{must} depend on its argument.  In the next section we 
develop such a $\lambda$-calculus and generalize the complement 
algorithm to work on such terms.

\section{A Strict $\lambda$-Calculus}
\label{sec:strict}

As we have seen in the preceding section, the complement of some
partially applied patterns in the simply-typed $\lambda$-calculus cannot
be expressed in a finitary manner within the same calculus.  We thus
generalize our language to include \emph{strict functions} of type $A
\RImp B$ (which are guaranteed to depend on their argument) and
\emph{invariant functions} of type $A \ZImp B$ (which are guaranteed
\textbf{not} to depend on their argument).  Of course, any concretely
given function either will or will not depend on its argument, but in
the presence of existential variables we still need the ability to
remain uncommitted.  Therefore our calculus also contains the full
function space $A \UImp B$.

\[ \begin{array}{rrcl}
 \mbox{\textit{Labels}} & k & \bnfas & 1 \bnfalt 0 \bnfalt u \\
 \mbox{\textit{Types}} & A & \bnfas & P \bnfalt A_1 \GImp{k} A_2 \\
 \mbox{\textit{Terms}} & M & \bnfas & c \bnfalt x \bnfalt \lam x^k\oftp
A\ldot M \bnfalt M_1 \, M_2^k \\
 \mbox{\textit{Contexts}} & \Gamma & \bnfas & \cdot \bnfalt \Gamma, x\oftp A
 \end{array} \]

Note that there are three different forms of abstractions and 
applications, where the latter are distinguished by different labels 
on the argument.  It is not really necessary to distinguish three 
forms of application syntactically, since the type of function 
determines the status of the application, but it is convenient for our 
purposes.  If a label is $u$ it is called \emph{undetermined}, 
otherwise it is \emph{determined} and denoted with the metavariable 
$d$.  Sometimes we omit the undetermined label.

 We use a formulation of the typing judgment with three 
zones, containing the unrestricted, irrelevant and strict hypotheses, 
denoted by $\Gamma$, $\Omega$, and $\Delta$, respectively.  \[ \Gamma; 
\Omega; \Delta \vd M \hastype A \] We implicitly assume a fixed 
signature $\Sigma$ which would otherwise clutter the presentation.  
Recall that $\Gamma_1,\Gamma_2$ is a union of two contexts which do 
not declare any common variables.  Recall also that we consider 
contexts as sets, that is, exchange is left implicit.

\begin{figure}
\begin{small}
\[ \begin{array}{c}
 \ianc{c\oftp A \in \Sigma}{\Gamma; \Omega; \cdot \vd c \hastype A}{Con} \\[1em]

 \ianc{}{(\Gamma, x\oftp A); \Omega; \cdot \vd x \hastype A}{Id^u}
 \hspace{2em}
 \mbox{\textit{no $Id^0$ rule}}
 \hspace{2em}
 \ianc{}{\Gamma; \Omega; x\oftp A \vd x \hastype A}{Id^1} \\[1em]

 \ianc{(\Gamma, x\oftp A); \Omega; \Delta \vd M \hastype B}{\Gamma;
\Omega; \Delta \vd \lam x^u \oftp A\ldot M \hastype A \GImp{u}
B}{\GImp{u}I} \\[1em]

 \ianc{\Gamma; (\Omega, x\oftp A); \Delta \vd M \hastype B}{\Gamma;
\Omega; \Delta \vd \lam x^0 \oftp A\ldot M \hastype A \GImp{0}
B}{\GImp{0}I} \\[1em]

 \ianc{\Gamma; \Omega; (\Delta, x\oftp A)\vd M \hastype B}{\Gamma;
\Omega; \Delta \vd \lam x^1 \oftp A\ldot M \hastype A \GImp{1}
B}{\GImp{1}I} \\[1em]

 \ibnc{\Gamma; \Omega; \Delta \vd M \hastype A \UImp B}{(\Gamma, \Delta);
\Omega; \cdot \vd N \hastype A}{\Gamma; \Omega; \Delta
\vd M\, N^u \hastype B}{\GImp{u}E} \\[1em]

 \ibnc{\Gamma; \Omega; \Delta \vd M \hastype A \ZImp B}{(\Gamma, 
\Omega,\Delta); \cdot; \cdot \vd N \hastype A}{\Gamma; \Omega;
\Delta \vd M\, N^0 \hastype B}{\GImp{0}E} \\[1em]

\ibnc{(\Gamma, \Delta_N); \Omega; \Delta_M \vd M \hastype A \RImp 
B}{(\Gamma, \Delta_M); \Omega; \Delta_N \vd N \hastype A}{\Gamma; 
\Omega; (\Delta_M, \Delta_N) \vd M\, N^1 \hastype B}{\GImp{1}E}

 \end{array} \]
\end{small}
\caption{Typing rules for $\lc$}

\end{figure}
Note that there is no rule for variables $x^0$, which expresses that
they cannot be used.  The requirement for the strict context $\Delta$ to
be empty in the $Id^u$ and $Id^1$ rules expresses that strict variables
must be used, while unrestricted or irrelevant variables can be ignored.

Our system is biased towards a bottom-up reading of the rules in that 
variables never disappear, \ie they are always propagated from the 
conclusion to the premises, although their status might be changed.

The $\GImp{u}E$ has the following rationale: the status of every 
variable in $M$ is preserved and passed on.  As usual in 
resources-sensitive $\l$-calculi, a strict function cannot be used in 
the argument to an undetermined argument: thus $\D$ is moved into the 
undetermined context so that the strict one is vacated.  Similarly in 
$\GImp{0}E$ both strict and irrelevant variables are moved in the 
undetermined context and may be used in an unrestricted way, 
eventually ending up in a leaf as a $Id^{u}$ instance, as they appear 
as an argument which is thrown away. 
%  On the other hand strict 
% variables are moved in the irrelevant context, as the former must not 
% be used, although they may occur.

The most complicated rule is $\GImp{1}E$, where the strict variables 
$\Delta$ are divided into two disjoint parts: $\Delta_M$ which 
declares those variables occurring only in $M$, $\Delta_N$ for those 
variables occurring only in $N$.  If a variable occurs 
\footnote{Recall that ``occurring'' here has to be interpreted 
loosely, since occurrences in arguments to invariant functions do not 
count} only in say $M$, it must be strict in the latter, but it must 
be unrestricted in $N$.  This is way $\D_{N}$ is moved in the 
undetermined context in the subderivation typing $M$.  Symmetrically 
for $N$.  Finally if a variable occurs strictly both in $M$ and $N$, 
it is made available in the undetermined context.  Thus, whole typing 
is unique (see Theorem~\ref{thm:uniqueR}), the typing derivation may 
not.  

In the typing judgment for our calculus there are a few choices.  For 
example, we could decide that that argument $N$ in an application $M\, 
N^0$ does not need to be well-typed, since it will never be used.  
Instead, we choose to verify it, so that we can always obtain a valid 
term in the simply-typed $\lambda$-calculus by erasing all labels.  
Irrelevant variables $x^0$ may still occur, but only in ignored 
arguments to invariant functions. 
%  Moreover in $\TImp E$ strict 
% variables could as well be moved in the undetermined context, where it 
% does not matter whether they are used or not.  The admissibility of 
% this  variant is a special case of Theorem \ref{thm:0loose}.

As a side remark, note that a \emph{linear} function space could easily
be accommodated in this style by introducing another zone.  It would
differ from other linear $\lambda$-calculi in that linear variable
\emph{can} occur non-linearly in the arguments of invariant functions.
For example $\lamb{x^{u}}{a\TImp a} x\ ((\lamb{y^{0}}{a\ZImp a} c) 
x^{0})^{1}$ would be deemed linear, notwithstanding the spurious (\ie 
irrelevant) occurrence of $x$ in the argument of an invariant function.

Our strict $\lambda$-calculus satisfies the expected properties,
culminating in the existence of canonical forms which is critical for
the intended applications.  We begin with the structural properties of
the context.  Exchange is directly built into the formulation and will
not be repeated.  We use $[N/x]M$ for the result of the
capture-avoiding substitution of $N$ for $x$ in $M$.

\begin{theorem}[Uniqueness of Typing]
\label{thm:uniqueT}
If $\god\vd M\hastype A$ and  $\god\vd M\hastype A'$, then $A\equiv A'$.
\end{theorem}
\begin{proof}
By induction on the structure of the given derivations, exploiting 
`functionality' of signatures and contexts.
\end{proof}

\begin{theorem}[Inversion]
\label{thm:invert}
All rules in $\lc$ are invertible.
\end{theorem}
\begin{proof}
By inspection.
\end{proof}

We will often use inversion principles tacitly.
% 
% \begin{theorem}[Renaming]
% \label{thm:rnm}
% Let $z$ be a fresh variable of type $A$: 
% \ben
% \item If $(\GG,x\oftp A);\O;\D\vd M\hastype C$, then 
% $(\GG,z\oftp A);\O;\D\vd [z/x]M\hastype C$.
% \item If $\GG;(\O,x\oftp A);\D\vd M\hastype C$, then 
% $\GG;(\O,z\oftp A);\D\vd [z/x]M\hastype C$.
% \item If $\GG;\O;(\D,x\oftp A)\vd M\hastype C$, then 
% $\GG;\O;(\D,z\oftp A)\vd [z/x]M\hastype C$.
% \enen
% \end{theorem}
% \begin{proof}
% By induction on the typing derivation.
% \end{proof}


 \begin{theorem}[Weakening] \mbox{}
 \label{thm:weak}
 \begin{enumerate}
  \item (Weakening$^{u}$) If $\Gamma; \Omega; \Delta\vd M \hastype C$ then $(\Gamma, 
  x\oftp A); \Omega; \Delta\vd M \hastype C$. 
  \item (Weakening$^{0}$) 
  If $\Gamma; \Omega; \Delta\vd M \hastype C$ then $\Gamma
  ; (\Omega, x\oftp A); \Delta\vd M \hastype C$. 
  \end{enumerate}
  \end{theorem}
 
\begin{proof}
  By induction on the structure of the given derivation. 
 \end{proof}
 
% \begin{theorem}[Strengthening] \mbox{}
% \label{thm:str}
% \begin{enumerate}
%   \item (Strengthening$^{u}$) If $(\Gamma, x\oftp A); \Omega; 
%   \Delta\vd M \hastype C$ and $x\not\in FV(M)$, then $\GG; \Omega; 
%   \Delta\vd M \hastype C$.  
%   \item (Strengthening$^{0}$) If $\Gamma; 
%   (\Omega, x\oftp A); \Delta\vd M \hastype C$ and $x\not\in FV(M)$, 
%   then $\Gamma ; \O; \Delta\vd M \hastype C$.
% \end{enumerate}
% \end{theorem}
%  
% \begin{proof}
% By induction on the structure of the given derivation.
% \end{proof}
% 

 
The following properties allow us to lose track of dependencies, if 
we are so inclined 
\newcommand{\gofd}{\GG;(\Omega,\Phi);\Delta}
\newcommand{\gfod}{(\GG,\Phi);\Omega;\Delta}
 
\begin{Theorem}[Loosening$^{0}$]
\label{thm:0loose}
If $\Gamma; (\Omega,\Phi); \Delta\vd M \hastype A$ then $(\Gamma, 
\Phi); \Omega; \Delta\vd M \hastype A$. 
\end{Theorem}

\begin{proof}
By  induction on the structure of  $\cD ::\gofd\vd M\hastype  A$ .
% 
% \item 
\noindent If  $$\cD = \ianc{c\oftp A\in\Sigma}{\Gamma; (\Omega,\Phi);\cdot \prv  c\hastype  A}{Idc}$$
Then
$$\cE= \ianc{c\oftp A\in\Sigma}{(\GG,\Phi);\Omega;\cdot \prv  c\hastype  A}{Idc}$$
%\item

\noindent If  $$\cD = \ianc{}{(\Gamma,x\oftp A); (\Omega,\Phi);\cdot\vd x\hastype  
A}{Id^{u}}$$
Then 
$$\cE = \ianc{}{(\Gamma,x\oftp A,\Phi);\Omega;\cdot\vd x\hastype    
A}{Id^{u}}$$

\noindent If  $$\cD = \ianc{}{\Gamma;(\Omega,\Phi);x\oftp A\prv  x\hastype  A}{Id^{1}}$$
Then
$$\cE=\ianc{}{(\Gamma,\Phi);\Omega;x\oftp A\prv  x\hastype  A}{Id^{1}}$$
Cases  $\TImp I$ and $\RImp I$ follows from an immediate appeal to the 
inductive hypothesis.

\noindent If  $$\cD = \ianc{\GG;(\Omega,\Phi,y\oftp A);\Delta\prv M\hastype B}
{\gofd\prv(\lamb{y^0}{A} M) \hastype A\ZImp B} {\ZImp I}$$
\ignore{By inversion $\GG;(\Omega,\Phi,y\oftp A);\Delta\prv M\hastype B$ which 
entails b} By inversion and IH $(\GG,\Phi);(\Omega,y\oftp A);\Delta\prv M\hastype B$ 
and thus $\gfod\prv(\lamb{y^0}{A} M) \hastype A\ZImp B$. 

\noindent If  $$\cD = \ibnc{\gofd \vd M \hastype  A \TImp B}
{(\GG,\Delta);(\Omega,\Phi);\cdot \vd N \hastype A}{\gofd \vd
M\, N^u \hastype  B}{\TImp E}$$
By inversion and IH on the leftmost derivation $\gfod\vd M \hastype A 
\TImp B$ and by inversion and  IH on the rightmost derivation 
$(\GG,\D,\Phi);\Omega;\cdot\vd N \hastype A$; thus conclude $\gfod\vd 
M \ N^{u}\hastype B$.

\noindent If  $$\cD = \ibnc{\gofd \vd M \hastype  A \ZImp B}
{(\GG,\Omega,\Delta,\Phi);\cdot;\cdot \vd N \hastype A}{\gofd \vd
M\, N^0\hastype  B}{\ZImp E}$$
By IH on the leftmost derivation $\gfod\vd M \hastype A \ZImp B$
and by inversion on the rightmost $(\GG,\Omega,\D,\Phi);\cdot;\cdot\vd N 
\hastype A$; thus  infer $\gfod\vd M \ N^{0}\hastype B$.

\noindent If $$\cD = \ibnc{(\GG,\Delta_{N});(\Omega,\Phi);\Delta_{M} 
\vd M \hastype A \RImp B}{(\GG,\Delta_M;(\Omega,\Phi);\Delta_{N}\vd N 
\hastype A}{\GG;(\Omega,\Phi);(\Delta_{N},\Delta_{M}) \vd
M\, N^1 \hastype  B}{\RImp E}$$
By inversion and IH on the leftmost derivation 
$(\GG,\Phi,\Delta_{N});\Omega;(\Delta_{M} \vd M 
\hastype A \RImp B$ and by inversion and IH on the rightmost derivation 
$(\GG,\Phi,\Delta_M);\Omega;\Delta_{N}\vd N 
\hastype A$, thus conclude 
$(\GG,\Phi);\Omega;(\Delta_{N},\Delta_{M})\vd M \ 
N^{1}\hastype B$.
\end{proof}
\newcommand{\su}{[z/x][z/y]}



\newcommand{\gdo}{(\GG,\Delta);\Omega;\cdot}

\begin{Theorem}[Loosening$^{1}$]
\label{thm:1loose}
If $\Gamma; \Omega; \Delta\vd M \hastype A$ then $\gdo\vd M \hastype A$. 
\end{Theorem}

\begin{proof}
By  induction on $\cD ::\god\vd M\hastype  A$ .
% 
% \item 
\noindent If  $$\cD = \ianc{c\oftp A\in\Sigma}{\GG;\Omega;\cdot \prv  c\hastype  A}{Idc}$$
Then
$$\cE= \ianc{c\oftp A\in\Sigma}{ \GG;\Omega;\cdot\prv  c\hastype  A}{Idc}$$
%\item

\noindent If  $$\cD = \ianc{}{(\GG,x\oftp A);\Omega;\cdot\vd x\hastype  A}{Id^{u}}$$
Then 
$$\cE = \ianc{}{(\GG,x\oftp A);\Omega;\cdot\vd x\hastype A}{Id^{u}}$$

\noindent If  $$\cD = \ianc{}{\Gamma;\Omega;x\oftp A\prv  x\hastype  A}{Id^{1}}$$
Then
$$\cE=\ianc{}{(\Gamma,x\oftp A);\Omega;\cdot\prv  x\hastype  A}{Id^{u}}$$
Cases  $\TImp I$ and $\ZImp I$ follows from an immediate appeal to the 
inductive hypothesis.

\noindent If  $$\cD = \ianc{\GG;\Omega;(\Delta,y\oftp A)\prv M\hastype B}
{\god\prv(\lamb{y^1}{A} 
M) \hastype A\RImp B} {\RImp I}$$
By inversion $\GG;\Omega;(\Delta,y\oftp A)\prv M\hastype B$ which 
entails by IH $(\GG,\Delta);\Omega;y\oftp A\prv M\hastype B$ and thus 
$\gdo\prv(\lamb{y^1}{A} M) \hastype A\RImp B$.

\noindent If  $$\cD = \ibnc{\god \vd M \hastype  A \TImp B}{(\GG,\Delta);\Omega;\cdot \vd N \hastype A}{\god \vd
M\, N^u\hastype  B}{\TImp E}$$
By inversion and IH on the leftmost derivation $\gdo\vd M \hastype A \TImp B$ and
 by inversion  on the rightmost derivation 
$(\GG,\Delta),\Omega;\cdot\vd N \hastype A$; thus conclude $\gdo\vd M \ N^{u}\hastype B$.

\noindent If  $$\cD = \ibnc{\god \vd M \hastype  A \ZImp B}{(\GG,\Omega);\Delta;\cdot \vd N \hastype A}{\god \vd
M\, N^0\hastype  B}{\ZImp E}$$
By IH on the leftmost derivation $\gdo\vd M \hastype A \ZImp B$ and 
by by Loosening$^{0}$ (Theorem \ref{thm:0loose}) on the rightmost 
derivation $(\GG,\Delta,\Omega);\cdot;\cdot\vd N \hastype A$; thus 
conclude $\gdo\vd M \ N^{0}\hastype B$.

\noindent If  $$\cD = \ibnc{\GG;(\Omega,\Delta_{N});(\Delta_{M} 
\vd M \hastype A \RImp B}{\GG;(\Omega,\Delta_{M});(\Delta_{N} \vd N 
\hastype A}{\GG;(\Omega);(\Delta_{N},\Delta_{M})\vd
M\, N^1 \hastype  B}{\RImp E}$$
By IH on the leftmost derivation 
$(\GG,\Delta_{M},\Delta_{N},\Delta_{M 
N});\Omega; \cdot\vd M \hastype A \RImp B$
and by IH on the rightmost derivation 
$(\GG,\Delta_{M},\Delta_{N},\Delta_{M
N});\Omega ;\cdot\vd N \hastype A$
; thus conclude 
$(\GG,\Delta_{N},\Delta_{M};\Omega;\cdot\vd M \ 
N^{1}\hastype B$.
\end{proof}

\begin{Corollary}
\label{co:1loose}
If $\Gamma; \Omega; \Delta\vd M \hastype A$ then $\gdo\vd M \hastype A$. 
\end{Corollary}


\newcommand{\cxd}{\Gamma;(\Omega,\Delta_N); (\Delta_M, 
\Delta_{MN}, x\oftp A )} 
\newcommand{\cxe}{\Gamma;(\Omega,\Delta_M);( \Delta_N, \Delta_{MN}) }
\newcommand{\cxf}{\Gamma; \Omega;( \Delta_M, \Delta_N }
\newcommand{\qm}{[N/x]M}
 
\begin{theorem}[Substitution Properties] \mbox{}
\label{thm:substitution}
\begin{enumerate}
\item (Substitution$^u$) If $(\Gamma, x\oftp A);\Omega;\Delta\vd M 
\hastype C$ and $\Gamma; (\Omega,\Delta);\cdot \vd N \hastype A$ then 
$\Gamma;\Omega;\Delta \vd [N/x]M \hastype C$.  \item 
(Substitution$^0$) If $\Gamma;(\Omega,x\oftp A);\Delta \vd M \hastype 
C$ and $(\Gamma, \Omega) ;\Delta;\cdot \vd N \hastype A$ then 
$\Gamma;\Omega;\Delta \vd [N/x]M \hastype C$.  \item 
(Substitution$^1$) If $(\Gamma,\Delta_N);\Omega; (\Delta_M, x\oftp A 
)\vd M \hastype C$ and $(\Gamma,\Delta_M);\Omega;\Delta_N \vd N 
\hastype A$ then $\Gamma; \Omega;( \Delta_M, \Delta_N) \vd [N/x]M 
\hastype C$.
\end{enumerate}
\end{theorem}

\begin{proof}
The proof is by simultaneous induction on the structure of $M$. We go 
through the cases for Substitution$^{1}$:. The $Con,Id^{u}$ are 
vacuously true. Otherwise If
$$\cD = \ianc{}{\GG;(\O,\D_{N});x\oftp A\vd x\hastype A}{Id^{1}}$$
and $\cE::\GG;(\O,x\oftp A);\D_{N}\vd N\hastype A$ then 
$${\cal F} = \ianc{}{\GG;\O;(\D_{N},x\oftp A)\vd  N}{Id^{1}}$$
Assume $$\cD::\ianc{\GG;(\O,\D_{N},y\oftp B);(\D_{M},\D_{MN},x\oftp 
A)\vd M\hastype C}{\GG;(\O,\D_{N});(\D_{M},\D_{MN},x\oftp A)\vd \lamb 
{x^{0}} {B} M\hastype B\ZImp C}{\ZImp I}$$
and $\cE::\GG;(\O,\D_{M});(\D_{N},\D_{MN})\vd N\hastype A$: by 
Weakening$^{0}$ infer $\cE::\GG;(\O,\D_{M},y\oftp 
B);(\D_{N},\D_{MN})\vd N\hastype A$: then by IH $\GG;(\O,y\oftp 
B);\dmn\vd [N/x] N\hastype C$ and finally $\GG;\O;\dmn\vd [N/x] 
\lamb{y^{0}}{B} N\hastype B\ZImp C$.  Similarly for $\TImp I$, using 
Weakening$^{u}$.  The case $\RImp I$  follows by an appeal to the IH.

\noindent
Assume
$$\cD=\ibnc{\GG;(\O,\D_{N});(\D_{M},\D_{MN},x\oftp A)\vd P\hastype 
B\TImp C}
{\GG;(\O,\D_{N},\D_{M},\D_{MN},x\oftp A);\cdot\vd Q\hastype B}
{\GG;(\O,\D_{N});(\D_{M},\D_{MN})\vd P\ Q^{u}}{\TImp E}
$$
and $\cE_{1}::\GG;(\O,\D_{M});(\D_{N},\D_{MN})\vd N\hastype A$.  By 
inversion and IH on $\cD$'s leftmost derivation and $\cE$ infer 
$\cD'_{1}::\GG;\O;(\D_{M},\D_{N},\D_{MN})\vd [N/x]P$; secondly obtain 
by inversion $\GG;(\O,\D_{N},\D_{M},\D_{MN},x\oftp A);\cdot\vd 
Q\hastype B$.  By IH get $\cE_{2}:: 
\GG;(\O,\D_{M},\D_{N},\D_{MN});\cdot\vd N\hastype A$.  By 
Loosening$^{0}$ obtain $(\GG,\O,\D_{M},\D_{N},\D_{MN});\cdot;\cdot\vd 
N\hastype A$.  Apply (by IH) Substitution $^{0}$ to infer 
$\cD'_{2}::\GG;(\O,\D_{N},\D_{M},\D_{MN},x\oftp A);\cdot\vd 
[n/x]Q\hastype B$.  Combine $\cD'_1$ and $\cD'_2$ to conclude by rule 
$\TImp E$ $\GG;\O;(\D_{N},\D_{M},\D_{MN}\vd[N/x] P\

\end{proof}


\begin{theorem}[Contraction] 
Let $z$ be a fresh variable of type $A$:
\label{thm:contr}
   \begin{enumerate}
   \item (Contraction$^{u}$)
  If $(\Gamma, x\oftp A, y\oftp A);\Omega;\Delta \vd M
\hastype C$ then $(\Gamma, z\oftp A) ;\Omega;\Delta\vd [z/x][z/y]M \hastype C$.
 \item  (Contraction$^{0}$)
  If $\Gamma; (\Omega, x\oftp A, y\oftp A);\Delta \vd M
\hastype C$ then $\Gamma;(\Omega, z\oftp A);\Delta \vd [z/x][z/y]M \hastype C$.
 \item  (Contraction$^{1}$)
  If $\Gamma;\Omega;(\Delta, x\oftp A, y\oftp A ) \vd M
\hastype C$ then $\Gamma;\Omega;(\Delta, z\oftp A) \vd [z/x][z/y]M \hastype C$.
 \end{enumerate}
 \end{theorem}
\begin{proof}
Using the opportune Substitution principle.
\end{proof}
 


\smallskip
The notions of reduction and expansion derive directly from the ordinary
$\beta$ and $\eta$ rules.

\[ \begin{array}{rcl}
   (\lam x^k\oftp A\ldot M)\, N^k & \betared & [N/x]M \\
   [1ex]
   M \hastype A \GImp{k} B & \etaexp & \lam x^k\oftp A\ldot M\, x^k \\
 \end{array} \]
 
Indeed one of the main reason to introduce irrelevant variables, as 
ones which \emph{may} occur but \emph{must not} be used, is to 
well-type $\eta$-expansion of invariant functions:
\[ \begin{array}{rcl}
  
   M \hastype A \GImp{0} B & \etaexp & \lam x^0\oftp A\ldot M\, x^0 \\
 \end{array} \]
  
The subject reduction and expansion theorems are an immediate consequence 
of the structural and substitution properties.

\begin{theorem}[Subject Reduction] \mbox{}
\label{thm:subred}
If $\Gamma;\Omega; \Delta \vd M \hastype A$ and $M \betared M'$ then 
$\Gamma;\Omega; \Delta \vd M' \hastype A$.
\end{theorem}
\begin{proof}  By cases on $k$:
\ben
\item
Let $M\equiv (\lamb{x^{u}}{B} P)Q^{u}\hastype A$ and $M'\equiv[Q/x]P$. 
Assume $\god\vd (\lamb{x^{u}}{B} P)Q^{u}\hastype A$. By inversion 
$\god\vd \lamb{x^{u}}{B} P\hastype B\TImp A$ and $\cE::(\GG,\D);\O;\cdot\vd 
Q\hastype B$. Again by inversion on the former derivation $\cD::(\GG,x\oftp 
B);\O;\D\vd P\hastype A$. By substitution$^{u}$ (Theorem 
\ref{thm:substitution}) on $\cD,\cE$ conclude $\god\vd[Q/x]P\hastype A$.
\item
Let $M\equiv (\lamb{x^{0}}{B} P)Q^{0}\hastype A$ and $M'\equiv[Q/x]P$. 
Assume $\god\vd (\lamb{x^{0}}{B} P)Q^{0}\hastype A$. By inversion 
$\god\vd \lamb{x^{0}}{B} P\hastype B\ZImp A$ and $\cE::(\GG,\O,\D);\cdot;\cdot\vd 
Q\hastype B$. Again by inversion on the former derivation $\cD::\GG;(\O,x\oftp 
B);\D\vd P\hastype A$. By substitution$^{0}$ (Theorem 
\ref{thm:substitution}) on $\cD,\cE$ conclude $\god\vd[Q/x]P\hastype A$.
\item
Let $M\equiv (\lamb{x^{1}}{B} P)Q^{1}\hastype A$ and $M'\equiv[Q/x]P$.  
Assume $\GG;\O;(\D_{P},\D_{Q})\vd (\lamb{x^{1}}{B} P)Q^{1}\hastype A$.  
By inversion $(\GG,\D_{Q});\O;\D_{P}\vd \lamb{x^{1}}{B} P\hastype 
B\RImp A$ and $\cE::(\GG,\D_{P});\O;\D_{Q}\vd Q\hastype B$.  Again by 
inversion on the former derivation 
$\cD::(\GG,\D_{Q});\O;(\D_{P},x\oftp B)\vd P\hastype A$.  By 
substitution$^{1}$ (Theorem \ref{thm:substitution}) on $\cD,\cE$ 
conclude $\GG;\O;(\D_{P},\D_{Q})\vd[Q/x]P\hastype A$.
\enen
\end{proof}

\begin{theorem}[Subject Expansion] \mbox{}
\label{thm:subexp}
If $\Gamma;\Omega; \Delta \vd M \hastype A \GImp{k} B$ and $M \etaexp 
M'$ then $\Gamma;\Omega; \Delta \vd M' \hastype A \GImp{k} B$.
\end{theorem}
\begin{proof} By cases on $k$:
\ben
\item
Assume $\god\vd M\hastype A\TImp B$.  By Weakening$^{u}$ (Theorem 
\ref{thm:weak}) $(\Gamma,x\oftp A);\Omega; \Delta \vd M \hastype 
A\TImp B$.  Take the following instance of $Id^{u}$: $(\Gamma,x\oftp 
A);(\Omega, \Delta);\cdot \vd x\hastype A$. By rule $\TImp E$ infer
$(\Gamma,x\oftp A);\Omega; \Delta \vd M\ x^{u} \hastype B$. Finally 
conclude by rule $\TImp I$ $\Gamma;\Omega; \Delta \vd \lxua M\ x^{u} 
\hastype A\TImp  B$.
\item
Assume $\god\vd M\hastype A\ZImp B$.  By Weakening$^{0}$ (Theorem 
\ref{thm:weak}) $\Gamma;(\Omega,x\oftp A); \Delta \vd M \hastype 
A\ZImp B$.  Take the following instance of $Id^{u}$: $(\Gamma,\O,x\oftp 
A); \Delta;\cdot \vd x\hastype A$. By rule $\ZImp E$ infer
$(\Gamma,x\oftp A);\Omega; \Delta \vd M\ x^{0} \hastype B$. Finally 
conclude by rule $\ZImp I$ $\Gamma;\Omega; \Delta \vd \lamb{x^{0}}{A} M\ x^{0} 
\hastype A\ZImp  B$.
\item
Assume $\GG;\O;\D_{M}\vd M\hastype A\RImp B$.  By Weakening$^{0}$ 
(Theorem \ref{thm:weak}) $\Gamma;(\Omega,x\oftp A); \Delta_{M})\vd M 
\hastype A\RImp B$.  Take the following instance of $Id^{1}$: 
$\Gamma;(\O,\D_{M});x\oftp A\vd x\hastype A$.  By rule $\RImp E$ infer 
$\Gamma;\Omega; (\Delta_{M},x\oftp A) \vd M\ x^{1} \hastype B$.  
Finally conclude by rule $\RImp I$ $\Gamma;\Omega; \Delta_{M})\vd 
\lamb{x^{1}}{A} M\ x^{1} \hastype A\RImp B$.
\enen
\end{proof}


% \subsection{Properties of Contexts}
% 
% We establish some  properties of contexts:

\begin{theorem}[Uniqueness of the Strict Context]
\label{thm:uniqueD}
If $\cD::\god\vd M\hastype A$ and $\cD'::\Gamma; \Omega'; \Delta'\vd M\hastype A$ 
then $\Delta = \Delta'$.
\end{theorem}
\begin{proof}
By induction on the structure of $\cD$ and $\cD'$. 
Cases $Con,Id^{u},Id^{1}$ are immediate, in the former $\Delta$ 
being empty, in the latter being a singleton. 
Cases $\TImp I$ and $\ZImp I$ 
follows immediately by induction hypothesis. Otherwise suppose:
\[
\cD =  \ianc{\Gamma; \Omega; (\Delta, x\oftp A)\vd M \hastype B}{\Gamma;
\Omega; \Delta \vd \lam x^1 \oftp A\ldot M \hastype A \GImp{1}
B}{\GImp{1}I}
\] and
\[
\cD' =  \ianc{\Gamma; \Omega'; (\Delta', x\oftp A)\vd M \hastype B}{\Gamma;
\Omega'; \Delta' \vd \lam x^1 \oftp A\ldot M \hastype A \GImp{1}
B}{\GImp{1}I}
\]
By IH $(\Delta, x\oftp A) = (\Delta', x\oftp A)$ and thus 
$\Delta=\Delta'$.  Cases $\TImp E$ and $\ZImp E$ follows immediately 
by an appeal to the induction hypothesis on the leftmost derivation.  
For case $\RImp$, by inductive hypothesis on the leftmost derivation 
$\Delta_M= \Delta_M'$; by inductive hypothesis on the rightmost 
derivations $\Delta_N=\Delta_N'$.  Thus $\Delta_M,\Delta_{N}= 
\Delta_M', \Delta_{N}'$.
\end{proof}

% The following properties will be useful in Sect.~\ref{sec:sunif}:



\subsection{Canonical forms for $\lc$}

\newcommand{\da}{\downarrow}
\newcommand{\bua}{\Uparrow}
\newcommand{\buda}{\Uparrow\!\downarrow}

We present the inductive definition  of  
\emph(canonical) forms in $\lc$, \ie terms in $\be$-long normal form.  This is 
realized by the two mutually recursive judgments depicted in Fig.~ 
\ref{fig:canon}:

\ben 
\item$\GG;\Omega;\Delta\prv M \da A$: $M$ is atomic of type $A$.
\item$\GG;\Omega;\Delta\prv M \bua A$: $M$ is canonical of type $A$.
\enen

\begin{figure}
\label{fig:canon}
\[
\begin{array}{c}
\ianc{}{\GG;\Omega; x\oftp A \prv  x\da A} {cId^{1}}
\qquad
\ianc{}{(\GG,x\oftp A);\Omega; \cdot  \prv  x\da A}{cId^{u}}\vsk
\qquad \mbox{\textrm{no rule for }}cId^{0}
\qquad
\ianc{c\oftp A\in\Sigma}{\GG; \Omega;\cdot  \prv  c\da A}{cIdc}\vsk
%\ianc{}{\GG;\Omega;\Delta\vd E\ \ol{x_{n}^{l}}\da P}{cPat}
%\qquad
\ianc{\GG;\Omega;\Delta \prv  M\da P}{\GG;\Omega;\Delta \prv  M\bua P} 
{cAt}\vsk
\ianc{(\GG,x\oftp A) ; \Omega;\Delta \prv M\bua B}{\GG;\Omega;\Delta\prv(\lamb{x^u}{A} M) \bua 
A\TImp B} {c\TImp I}
\vsk
\ianc{\GG ; \Omega; (\Delta,x\oftp A) \prv M\bua B}{\GG;\Delta\prv(\lamb{x^1}{A} M) \bua 
A\RImp B}{c\RImp I}
\qquad
\ianc{\GG ;(\Omega, x\oftp A) ;\Delta \prv M\bua B}{\GG;\Omega;\Delta\prv(\lamb{x^0}{A} M) \bua 
A\ZImp B}{c\ZImp I}
\vsk
 \ibnc{\Gamma; \Omega; \Delta \vd M \da A \TImp B}{(\Gamma, \Delta);
\O; \cdot \vd N \bua A}{\Gamma; \Omega; \Delta
\vd M\, N^u \da B}{c\GImp{u}E}
\vsk
\ianc{\GG;\Omega;\Delta\prv M \da A \ZImp B \quad (\GG,\Omega,\Delta);\cdot;\cdot \prv N \bua A
}
{\GG;\Omega;\Delta  \prv M  \ N^0 \da B}{c\ZImp E}\vsk

\ibnc{(\Gamma, \Delta_N); \Omega; \Delta_M \vd M \da A \RImp 
B}{(\Gamma, \Delta_M); \Omega; \Delta_N \vd N \bua A}{\Gamma; \Omega; 
(\Delta_M, \Delta_N) \vd M\, N^1 \da B}{c\RImp E}
\end{array}
\]
\caption{Canonical forms for $\lc$}
\end{figure}


We will also need the typing rule and the the canonical form for logic 
variables:

\beq
\ianc{\cdot\vd E_{A}\hastype A}{\god\vd E_{A}\ \xn \hastype P}{Pat}
\qquad
\ianc{\god\vd E_{A}\ \xn \hastype P}{\god \vd E_{A}\ \xn \da  P}{cPat}
\eneq

\begin{Theorem}[Canonical Form Theorem]
\label{thm:canonical}
If $\god\vd M\hastype A$, then there is $N$ such that $\god\vd M\bua 
N\hastype A$.
% \ben 
% \item $\GG;\Omega;\Delta\prv M \da A$.
% \item $\GG;\Omega;\Delta\prv M \bua A$.
% \enen
\end{Theorem}
\begin{proof}
A suitable reformulation of Tait's method along the lines of 
\cite{Cervesato96phd}.
\end{proof}

We sometimes abridge the statement of the canonical form theorem in 
$\GG;\Omega;\Delta\prv M \buda A$.


\section{Complement in Strict $\lambda$-Calculus}

We require that our complement operator, denoted, say, $\mmnot$, satisfies the usual boolean 
rules for negation, that is:
\ben
\item (Exhaustivity) $M$ is a ground instance of $N$ or $M$ is a 
ground instance of $\mmnot(N)$.
\item (Disjointness) It is not the case that $M$ is both a ground 
instance of $N$  and of $\mmnot(N)$.
\enen

Unfortunately, it turns out that the first property does not hold in 
general as we allow logic variables in partially applied terms.  We 
must therefore isolate the right fragment of the strict calculus: 
this entails two separate phases:

\bit
\item restrict to a class of terms (that we call \emph{simple}) for
which exhaustivity holds.
\item
bring to full application those terms.
\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 something as the 
following to hold:
\[ M \in \|E\ z^{1}\|  \mbox{\textrm{ or }}  M \in \|\mmnot (E\ 
z^{1})\|\]
\ie
\[ M \in \|E\ z^{1}\|  \mbox{\textrm{ or }}  M \in \|F\ 
z^{0}\|\]
But consider the following counterexample:
\[
\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 but the above term does not satisfy exhaustivity. 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.

\smallskip
We now formalize an embedding through the two mutually recursive 
functions $\_^{-}$ and $\_^+$:

\beq
(A\Imp B)^{-} & = & A^{+} \TImp B^{-}\\
(A\Imp B)^{+} & = & A^{-} \RImp B^{+}\\
P^{\pm} & = & P
\eneq
We then extend it to terms (including logic variables), 
signatures and contexts as follows:

\beq
(\lxa M)^{-} & = & \lamb{x^{u}}{A^{+}} M^{-}\\
M^{-} & = & M^{+}\\
x^{+} & = & x\\
(E_A\ \xn)^{+} &=& F_{A^{-}} \ \xn^u\\
(M\ N)^{+} & = & (M^{+}\ N^{-})^{1}\\
[1em]
(\cdot)^{+} & = & \cdot\\
(\GG,x\oftp A)^{+} & = & \GG^{+}, x\oftp A^{+}\\
(\Sigma,P\oftp type)^{+} & = & \Sigma^{+}, P\oftp type\\
(\Sigma,c\oftp A)^{+} & = & \Sigma^{+}, c\oftp A^{+}
\eneq

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\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\vd y(\lamb{f^{u}}{a\RImp a} x)^{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, which we 
call:

\[ \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 
E_{A^{-}}\ \xn^u
\end{array} \]
We sometimes abridge $(\dots (h\ M_1)^{1} \dots M_n)^{1}$ in $h\ 
\Mns$.
\smallskip

We prove the correctness of the embedding. We will need the following:

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

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

The following theorem includes the usual inductive 
definition of canonical terms in the simply-typed $\l$-calculus


\begin{theorem}
\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 simultaneous induction on the proofs of $\cD::\GG\vd M\bua A$ and 
$\cD'::\GG\vd M\da A$.
 
\[\cD'= \ianc{\GG(x) = A}{\GG\vd x\da A}{atm\_var}\]
Since $x^{+}= x$ and $\GG^{+}(x) = A^{+}$ we conclude by rule 
$cId^{u}$ $\ctx\vd x^{+}\da A^{+}$.

\[\cD'=\ibnc{\GG\vd M\da B\Imp A}{\GG\vd N\bua B}{\GG\vd M\ N \da 
A}{atm\_app}\]
By IH on the leftmost derivation $\ctx\vd M^{+}\da (B\Imp A) ^{+}$, 
\ie $\ctx\vd M^{+}\da B^{-}\RImp A ^{+}$. By IH on the rightmost 
derivation and $\ctx\vd N^{-}\bua 
B^{-}$.  By rule $c\RImp E$ conclude $\ctx\vd (M^{+}N^{-})^{1}\da 
A^{+}$, that is $\ctx\vd ((M\ N)^{+} )^{1}\da A^{+}$.

\[\cD'=
\ianc{\GG\vd E_{A}\ \xn\hastype P}{\GG\vd E_{A}\ \xn\da 
P}{can\_Pat}\]
By inversion $\GG\vd E_{A}\ \xn\hastype P$.  By Lemma \ref{le:aminus} 
$\ctx\vd F_{A^{-}}\ \ol{x^u_n}\hastype P$.  Thus $\ctx\vd F_{A^{-}}\ 
\ol{x^u_n}\da P$ and finally $\ctx\vd (E_{A}\ \xn)^{+}\hastype P^{+}$.

\[\cD=\ianc{\GG\vd M\da P}{\GG\vd M\bua P}{can\_atm}\] 
By IH, $\ctx\vd M^{+}\da P^{+}$ which by rule $cAt$ yields $\ctx\vd 
M^{+}\bua P^{+}$, \ie by the embedding $\ctx\vd M^{-}\bua P^{-}$.  
\[\cD= \ianc{\GG,x\oftp A\vd M\bua B}{\GG\vd\lxa M\bua A\Imp 
B}{can\_lam}\] 
By IH, $x\oftp A^{+},\ctx\vd M^{-}\bua B^{-}$ and rule 
$c\RImp I$ yields $\ctx\vd\lamb{x^{u}}{A^{+}} \bua A^{+}\TImp B^{-}$ 
and by definition $\ctx\vd (\lxa M)^{-}\bua (A \Imp B)^{-}$.
\end{proof}

From now on we drop the $\pm$ embedding annotations from terms, 
types and contexts.


\subsubsection{Ground Instances}

We recall that we assume every type to be inhabited, so that every 
term can be see as the intensional representation of the set of its 
ground instances.  The judgment in Fig.~ \ref{fig:grinst} $\GG\emp 
\prv M\in\| N\| : A$ formalizes the fact that a simple term $M$ is a 
ground instance of $N$ at type $A$.

\begin{figure}
\label{fig:grinst}
\[
\begin{array}{c}
\ianc{M\equiv t \ \ol{x_n}  \quad \cdot\prv  t \hastype A}
{\GG\emp \prv   M  \in\| F_A\ \xn\| : P}{grFlx} 
\vsk
\ianc{(\GG,x\oftp A);\Omega;\Delta\prv   M  \in\| N\| : B}
{\GG\emp \prv  \lxua M  \in\|\lxua N \|:A\TImp B}{grLam}
\vsk
% \ianc{\GG\emp \prv h \oftp  A_1\RImp\mdots\RImp A_n \RImp P\quad \GG\emp \prv  \ M_1 \in\| 
% N_{1}\| : A_1\cdots \GG\emp \prv  M_n \in\| N_n\| : A_n }
%  {\GG\emp \prv  h\ \Mns \in\|h\ \Nns
% \| : P} {grApp}
\ianc{\GG\emp \prv h \oftp  A_1\RImp\mdots\RImp A_n \RImp P\quad \GG\emp \prv  \ M_i \in\| 
N_{i}\| : A_i\quad 1\leq i\leq n}
 {\GG\emp \prv  h\ \Mns \in\|h\ \Nns
\| : P} {grApp}

\end{array}
\]
\caption{$M$ is a ground instance of $N$ at type $A$}
\end{figure}
% 
% The judgment in Fig.~ \ref{fig:grinst} $\god\prv 
% M\in\| N\| : A$ formalizes the fact that, in a context $\god$, a 
% simple term $M$ is a ground instance of $N$ at type $A$.  This can 
% obviously be generalized to any strict term.
% 
% \begin{figure}
% \label{fig:grinst}
% \[
% \begin{array}{c}
% \ianc{M\equiv t \ \ol{x_n}  \quad \cdot\prv  t \hastype A}
% {\god\prv   M  \in\| F_A\ \xn\| : P}{grFlx} 
% \vsk
% \ianc{(\GG,x\oftp A);\Omega;\Delta\prv   M  \in\| N\| : B}
% {\god\prv  \lxua M  \in\|\lxua N \|:A\TImp B}{grLam}
% \vsk
% % \ianc{\god\prv h \oftp  A_1\RImp\mdots\RImp A_n \RImp P\quad \god\prv  \ M_1 \in\| 
% % N_{1}\| : A_1\cdots \god\prv  M_n \in\| N_n\| : A_n }
% %  {\god\prv  h\ \Mns \in\|h\ \Nns
% % \| : P} {grApp}
% \ianc{\god\prv h \oftp  A_1\RImp\mdots\RImp A_n \RImp P\quad \god\prv  \ M_i \in\| 
% N_{i}\| : A_i\quad 11\leq i\leq n}
%  {\god\prv  h\ \Mns \in\|h\ \Nns
% \| : P} {grApp}
% 
% \end{array}
% \]
% \caption{$M$ is a ground instance of $N$ at type $A$}
% \end{figure}



\begin{Lemma}[Ground Instance Weakening]
\label{le:giweak}\mbox{}
 \begin{enumerate}
  \item If $\Gamma\emp\vd M \in \|N\| :C$ then $(\Gamma, 
  x\oftp A)\emp\vd M \in \|N\| :C$. 
  \item
  If $\Gamma\emp\vd M \in \|N\| :C$ then $\Gamma
  ; (\Omega, x\oftp A); \Delta\vd M \in \|N\| :C$. 
  \end{enumerate}
  \end{Lemma}
\begin{proof}
By induction on the structure of the given derivation
\end{proof}
% 
% \begin{Lemma}[Ground Instance Weakening]
% \label{le:giweak}\mbox{}
%  \begin{enumerate}
%   \item If $\Gamma; \Omega; \Delta\vd M \in \|N\| :C$ then $(\Gamma, 
%   x\oftp A); \Omega; \Delta\vd M \in \|N\| :C$. 
%   \item
%   If $\Gamma; \Omega; \Delta\vd M \in \|N\| :C$ then $\Gamma
%   ; (\Omega, x\oftp A); \Delta\vd M \in \|N\| :C$. 
%   \end{enumerate}
%   \end{Lemma}
% \begin{proof}
% By induction on the structure of the given derivation
% \end{proof}
We implicitly use the above lemma to opportunely weaken different 
contexts with common basis to an unique one.

\subsection{Full Application}

We describe in Fig.~ \ref{fig:trans} how to make every term fully 
applied: while this is achieved via a translation from simple terms, 
it is clear how to generalize this judgment to the canonical forms of the 
simply-typed $\l$-calculus. We write $Z\ \GG^{u}$ for $Z\ 
x_{1}^{u}\dots x_{n}^{u}$, where $x_{1}\dots x_{n}\in dom(\GG)$. The 
notation $\pi(\GG)$ stands for a permutation of  $\GG$.


\newcommand{\LBimp}{\longleftrightarrow}

% same context
\begin{figure}
\label{fig:trans}  
\[
\begin{array}{c}
\ianc{}{(\GG,\Omega)\emp\prv  E\ \pi(\GG^{u}) \LBimp F\ \GG^{u} \
 \Omega^{0}}{\mbox{\rm Trn\_Pat}} 
\vsk
\ianc{ (\GG,x\oftp A)\emp \prv  M \LBimp  N }
{\GG\emp\prv \lxua M \LBimp  \lamb{x^u}{A }N }{\mbox{\rm Trn\_Lam}}\vsk
\ianc{  \GG\emp\prv  M_{1}  \LBimp   N_{1}\cdots \GG\emp\prv  M_{n} \LBimp   N_{n} }
{\GG\emp\prv h\  \Mns \LBimp   h\ \Nns} {\mbox{\rm Trn\_App}}
\end{array}
\]
\caption{Full application Translation}
\end{figure}

We have now arrived to the following language, where the labeling 
on patterns is unrestricted, that we still call:

\[ \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 E\ 
x^{l_{1}}_{1}\dots{x^{l_{n}}_{n}}
\end{array} \]

To prove the adequacy of the translation, we need  the 
following irrelevance Lemma:

% \newcommand{\cx}{x\oftp C;\cdot;\cdot}
% \newcommand{\cxom}{ x\oftp C;\Omega;\cdot}
\newcommand{\cgm}{\GG;\cdot;\cdot}
\newcommand{\cgmom}{ \GG;\Omega;\cdot}

\begin{Lemma}[Irrelevance]
\label{le:fat}
Suppose $M$ is simple: the following holds:
\ben
\item
If  $\cgm\vd M\da A$ then $\cgmom\vd M\da A$.
\item
If $\cgm\vd M\bua A$ then $\cgmom\vd M\bua A$.
\enen
\end{Lemma}

% proof for \newcommand{\cgm}{\GG;\cdot;\cdot}
\begin{proof}
($\Imp$). By simultaneous induction on $\cD_{1}::\cgm\vd M\da A$ and
 $\cD_{2}::\cgm\vd M\bua A$.
% 
% \item 
\noindent If  $$\cD = \ianc{c\oftp A\in\Sigma}{\cgm \prv  c\da A}{cIdc}$$
Then
$$\cE= \ianc{c\oftp A\in\Sigma}{\cgmom \prv  c\da A}{cIdc}$$
% \item
\noindent If  $$\cD = \ianc{}{(\GG, y\oftp A) ;\cdot; \cdot  \prv  y \da 
A}{cId^{u}}$$
Then 
$$\cE = \ianc{}{(\GG, y\oftp A); \O;\cdot  \prv  y\da 
A}{cId^{u}}$$
% \item No case for $\cD = Id^{1}$.
\noindent If  $$\cD = \ianc{\cgm\vd E\ \ol{x_{n}^{l}} \hastype P}{\cgm \vd E\ \ol{x_{n}^{l}} \da  P}{cPat}$$
By inversion $\cgm\vd E\ \ol{x_{n}^{l}} \hastype P$: by Weakening$^0$ (Theorem 
\ref{thm:weak}) $\GG;\Omega;\cdot\vd E\ \ol{x_{n}^{l}} \hastype 
P$; thus conclude $\GG;\Omega;\cdot\vd E\ \ol{x_{n}^{l}} \da P$.
% \item
\noindent If  $$\cD = \ianc{\cgm\prv  M\da P}{\cgm \prv  M\bua P} {cAt}$$
By inversion $\cgm\prv  M\da P$, by IH  $\cgmom \prv  M\da 
P$ and hence   $\cgmom \prv  M\bua P$.
% \item
\noindent If  $$\cD = \ianc{(\GG,y\oftp A)\emp \prv M\bua B}{\cgm\prv(\lamb{y^u}{A} M) \bua 
A\TImp B} {c\TImp I}$$
By inversion $(\GG,y\oftp A)\emp \prv M\bua B$ which entails by IH 
$(\GG,y\oftp A);\O;\cdot \prv M\bua B$ and $\cgmom\prv(\lamb{y^u}{A} 
M) \bua A\TImp B$.  % \item
\noindent If  $$\cD = \ibnc{\cgm \vd M \da A \RImp B}{\cgm \vd N \bua A}{\cgm \vd
M\, N^1 \da B}{c\RImp E}$$
By inversion there are derivations $\cD_{1}:: \cgm \vd M \da A \RImp 
B$ and $\cD_{2}:: \cgm \vd N \bua A$. By IH there are derivations 
$\cE_{1}:: \cgmom \vd M \da A \RImp B$ and $\cE_{2}:: \cgmom \vd N \bua A$; 
by rule $c\RImp E$ we conclude $\cgmom\vd M\ N^{1}\da B$.
%  \enit
\end{proof}

\begin{Corollary}
\label{co:fat}
If $M$ is simple and $\cgmom\vd M\buda A$, then $(\GG,\Omega)\emp\vd 
M\buda A$.
\end{Corollary}
\begin{proof}
It follows from Loosening$^0$ (Theorem \ref{thm:0loose}) and the 
canonical form theorem (Theorem \ref{thm:canonical}).
\end{proof}

\begin{theorem}
\label{thm:fat}
Let $N$ be a simple term (in canonical form) such that $\GG\emp \vd N 
\LBimp Q$; then $\GG\emp\vd M\in\|N\|\hastype A$ iff $\GG\emp \vd 
M\in \|Q\|\hastype A$.
\end{theorem}
\begin{proof}
By induction on $N$.
($\Imp$) Base: $(\GG,\Omega)\emp\vd M \in \|E_{B}\ 
\pi(\GG^{u})\|$ iff $M\equiv t\ \pi(\GG^{u})$ and $\cdot\emp\vd 
t\hastype B$.  Thus $(\GG,\O)\emp \vd M\hastype A$.  By the canonical 
form theorem (Theorem \ref{thm:canonical}) this implies 
$(\GG,\Omega)\emp\vd M\buda A$.  Lemma \ref{le:fat} entails 
$\GG;\Omega;\cdot\vd M\buda A$, which yields 
$\GG;\Omega;\cdot\vd M\hastype A$.  Thus $M\equiv t'\ \GG^{u} 
\Omega^{0}$ for $\cdot\emp\vd t'\hastype B'$, \ie $\GG\emp\vd M\in 
\|F_{B'}\ \GG^{u} \Omega^{0}\|$.  ($\If$).  Conversely, proceed 
similarly to the above, but using Corollary \ref{co:fat} in place of 
Lemma \ref{le:fat}.

\noindent
Step: a straightforward application of the inductive hypothesis.
\end{proof}


\section{The Complement Algorithm}

The idea of complementation of flexible simple patterns is to form 
a set of terms under a  context according to the occurrence status of every 
variable; if the former is determined (must or must not occur) a term 
with the given variable annotated with the complement of the 
annotation is built where the remaining variables are set to 
undetermined, otherwise we do nothing, \ie we do not build a term.  

First, observe that the complement operation on terms behaves on 
labels like negation does on truth-values in Kleene's 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 partial 
(information) ordering $u\leq 1, u\leq 0$. 

Finally we present the system for pattern complement.  Since we are 
dealing only with simple terms, we need only one context, the 
unrestricted one.  Hence we abridge $\GG\emp\vd\mnot(M)=N$ in 
$\GG\vd\mnot(M)=N$.


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

Fix a signature $\Sigma$.  For a linear simple term (in canonical form) 
$M$ such that $\GG \prv  M \hastype  A$ define $\GG\prv  \mnot(M) = N : A$ as:

\begin{small}
\[
\begin{array}{c}
\ianc{1\leq i\leq n\quad k\in\{1,0\}} {\GG\prv \mnot(E \ x_{1}^{l_{1}}\dots x_{i-1}^{l_{i-1}} \ 
x_{i}^{k}\ x_{i+1}^{l_{i+1}}\dots x_n^{l_{n}}) = Z\ x_{1}^{u}\dots 
x_{i-1}^{u}\ x_{i}^{\mnot(k)}\ x_{i+1}^{u}\dots x_n^{u} : P} {\mnot\_Flx}
\vsk
\mbox{\textrm{no rule for } $k=u$}
\vsk
\ianc{\GG,x\oftp A\prv  \mnot( M)  =  N : B}
{\GG\prv  \mnot(\lxua M)  = \lxua N : A\Imp B}{\mnot\_Lam}
\vsk
\ianc{g\in\Sigma\cup\GG, g \hastype A_{1}\RImp\dots\RImp A_{m}\RImp 
P\quad m\geq 0,h \not\equiv g   } 
{\GG\prv  \mnot (h\ \Mn^1) = 
(\dots (g\ (Z_{1} \GG^{u}))^{1}\dots (Z_{m}\GG^{u}))^{1} : P} {\mnot\_App^{1}}
\vsk
\ianc{ h\in\Sigma\cup\GG, \GG\prv h\hastype A_{1}\RImp\dots\RImp A_{n}\RImp P
 \quad \GG\prv \mnot( M_i) = N : A_i\quad 1\leq i\leq n } 
{\GG\prv  \mnot (h\ \Mn^1) = 
(\dots (h\ (Z_{1}\GG^{u} ))^{1}\dots (Z_{i-1}\GG^{u} ) \ N^{1}\ 
(Z_{i+1}\GG^{u} )^{1}\dots (Z_{m}\GG^{u}))^{1} : P} {\mnot\_App^{2}}
\end{array}
\]
\end{small}

\noindent where $m\geq 0$ and $(Z\ \GG^{u})$'s denotes the application 
of a fresh variable of opportune typing to the parameters contained in 
an undetermined context. More formally:
\beq
(\cdot)^{k} & = & \cdot\\
(x\oftp A,\GG)^{k} & = & (x^{k}) \GG^{k}
\eneq
  Finally define $\mmnot(M\hastype A) = 
\{N\mid\cdot\prv \mnot(M)=N:A\}$
\end{Definition} 


It also convenient to have a forgetful function on labeled contexts:
\beq
erase(\cdot) & = & \cdot\\
erase(x^{k}\GG^{k}) & = & (x\ erase(\GG^{k}))
\eneq

Note  that if $E\hastype A$ is a variable, it has the canonical form $\l 
\ol{x_{n}^{u}}\,.\,E\ \ol{x_{n}^{u}}$: hence $\mmnot(E\hastype A) = \eset$ as 
expected.


\begin{example}
\begin{eqnarray}
\mmnot( E\ x^{0} y^{1}) & = & \{  F\  
x^{1} y^{u},   G\  x^{u} y^{0}\} \label{eq:l}\\
\mmnot(  E\ x^{u} y^{1}) & = & \{  F\  x^{u} y^{0}\}\nonumber
\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}) is made explicit into:
\[
\{F_{1} \ x^{1} y^{1},    G_{1} \ x^{1} y^{0},   G_{2} \ x^{0} y^{0}\}
\]
It is clear that in the worst case scenario the number of terms is 
bound by $2^{n}$; hence the usefulness of this further step 
needs to be pragmatically determined.


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

\begin{example}
\beq
\lefteqn{\mmnot(\l x^{u}\l y^{u}.\, s(M\ x^{1} y^{0})^{1} \hastype
  nat\Imp nat\Imp nat)  =}\\
& \{ \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(N\ x^{0} y^{u})^{1}, \l x^u\l y^u .\, s(N'\ x^{u} 
y^{1})^{1} \} 
\eneq
\end{example}

We now show that simple terms are closed under complementation.

\begin{theorem}
If $M$ is a simple term and $\GG\vd\mnot(M)= N$ then  $N$ is simple.
\end{theorem}

\begin{proof}
By induction on $M$.
\begin{sloppy}
$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}^{l_{1}}\dots x_{i-1}^{l_{i-1}} \ 
x_{i}^{k}\ x_{i+1}^{l_{i+1}}\dots x_n^{l_{n}}) = Z\ x_{1}^{u}\dots 
x_{i-1}^{u}\ x_{i}^{\mnot(k)}\ x_{i+1}^{u}\dots x_n^{u} : P$ by rule $
\mnot\_Flx$, where the latter is simple.
\end{sloppy}

$$\ianc{\GG,x\oftp A\prv  \mnot( M)  =  N : B}
{\GG\prv  \mnot(\lxua M)  = \lxua N : A\Imp B}{\mnot\_Lam}$$
By inversion $\GG,x\oftp A\prv  \mnot( M)  =  N : B$, hence by IH $N$ 
is simple and so is $\lxua N$.

$$\ianc{g\in\Sigma\cup\GG, g \hastype A_{1}\RImp\dots\RImp A_{m}\RImp 
P\quad m\geq 0,h \not\equiv g   } 
{\GG\prv  \mnot (h\ \Mn^1) = 
(\dots (g\ (Z_{1} \GG^{u}))^{1}\dots (Z_{m}\GG^{u}))^{1} : P} {\mnot\_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}$.
\begin{small}
$$\ianc{ h\in\Sigma\cup\GG,\GG\prv h\hastype A_{1}\RImp\dots\RImp A_{n}\RImp P\quad \mbox{\textrm{for some} $i$} \quad \GG\prv \mnot( M_i) = N : A_i } 
{\GG\prv  \mnot (h\ \Mn^1) = 
(\dots (h\ (Z_{1}\GG^{u} ))^{1}\dots (Z_{i-1}\GG^{u} ) \ N^{1}\ 
(Z_{i+1}\GG^{u} )^{1}\dots (Z_{m}\GG^{u}))^{1} : P} {\mnot\_App^{2}}
$$
\end{small}
By inversion and 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_{m}\GG^{u}))^{1}$ is simple.
\end{proof}

\begin{Corollary}
If $M$ is a simple term, so is $N$, for all $N\in\mmnot(M)$.
\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. Termination is obvious, as in rules 
$\mnot\_Lam$ and $\mnot\_app^{1}$ the size of the term affected by the 
recursive call is clearly smaller. \ignore{We use the abridged notation 
$\GG\prv M\in\|\mnot(N)\| :A$ for $\GG\prv M\in \|Q\|:A$ where $ 
\GG\prv \mnot(N) = Q : A$.} We may drop the type and signature 
information from the above judgment in proofs.  We abridge $\mnot(l)$ 
in $-l$.  Note that soundness does not require simple terms, nor 
canonical forms.


\smallskip

\begin{Lemma}
\label{le:disjD}
It is not the case that both $\GG;\O;(\D,x\oftp A)\vd M\hastype C$ and 
$(\GG,\O,\D);x\oftp A;\cdot\vd M\hastype C$.
\end{Lemma}
\begin{proof}
By simultaneous induction on the structure of $\cD::\GG;\O;(\D,x\oftp 
A)\vd M\hastype C$ and $\cD'::(\GG,\O,\D);x\oftp A;\cdot\vd M\hastype C$.
\end{proof}

\begin{Lemma}
\label{le:disjO}
It is not the case that both $\GG;(\O,x\oftp A);\D\vd M\hastype C$ and 
$(\GG,\O,\D);\cdot;x\oftp A\vd M\hastype C$.
\end{Lemma}
\begin{proof}
By simultaneous induction on the structure of $\cD::\GG;(\O,x\oftp 
A);\D\vd M\hastype C$ and $\cD'::(\GG,\O,\D);\cdot;x\oftp A\vd 
M\hastype C$.
\end{proof}


% with \god instead of \GG\emp
% \begin{corollary}
% \label{co:part1}
% It is not the case that both $\god\vd M \in \| E\ \ol{x_{n}^{l}}\|$ 
% and there is a $Q$, such that $(\GG;\O;\D)\emp
%  \vd \mnot(E\ \ol{x_{n}^{l}})= Q$ 
% and $\god\vd M \in \| Q\|$.
% \end{corollary}
% 
% \begin{proof}
% First observe that $E\ \ol{x_{n}^{l}}$ can be viewed as $E\ 
% \GG^{u}\Omega^{0}\Delta^{1}$.  Assume $\god\vd M\in \|E\ 
% \GG^{u}\Omega^{0}\Delta^{1} \|$ and $(\GG;\O;\D)\emp \vd \mnot(E\ 
% \ol{x_{n}^{l}})=F\ \GG'^{u}\Omega'^{0}\Delta'^1$, where $\GG'= (\god)- 
% x\oftp C$ and for $x\oftp C\in \D$ either $\D'=x\oftp C, \O'=\cdot$ or 
% for $x\oftp C\in \O$ it holds $\O'=x\oftp C, \D'=\cdot$.  By rule 
% $grFlex$ this is equivalent to both $\Gamma;\Omega;\Delta \vd M 
% \hastype A$ and $\Gamma';\Omega';\Delta' \vd M \hastype A $.  But this 
% impossible by uniqueness of strict contexts (Theorem 
% \ref{thm:uniqueD}).
% \end{proof}



\begin{theorem}
\label{thm:part1}
Let$\GG\vd N\hastype A$ be a linear pattern: it is not the case that 
both $\GG\vd M \in \| N\|\hastype A$ and there is a $Q$ such that 
$\GG\vd \mnot(N)=Q$ and $\GG\vd M \in \| Q\|\hastype A$.
\end{theorem}

\begin{proof}
By induction on $N$.  Basis: first observe that $E\ \ol{x_{n}^{l}}$ 
can be re-written as $E\ \GG^{u}\Omega^{0}\Delta^{1}\ x^{d}$, where 
$x$ is determined; indeed if $x$ is undetermined, the result holds 
trivially.  Assume $\Xi\vd M\in \|E\ \GG^{u}\Omega ^{0}\Delta ^{1}\ 
x^{d}\|$ and $\Xi \vd M\in\|F\ \GG^{u}\Omega ^{u}\Delta ^{u}\ 
x^{-d}\|$ for some $d\in\{1,0\}$. Then it holds that both 
$\Gamma;\Omega;(\Delta, x\oftp A) \vd M \hastype C$ or 
$\Gamma;(\Omega, x\oftp A);\Delta \vd M \hastype C$ and 
$\Gamma;(\Omega, x\oftp A);\Delta\vd M\hastype C$ or $\Gamma 
;\Omega;(\Delta, x\oftp A)\vd M\hastype C$.  Both cases are 
impossible by Lemma \ref{le:disjO} and \ref{le:disjO}.
\\ \noindent 
Step: 
\bit 
\item Case: $N$ is an application $(h\ \ol{N_n^{1}})$ for $ n\geq 0$.  
Sub-case $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 
$grApp$ as the root of $M$ should be both $h$ and $g$.  Sub-case 
$app^2$: suppose both $\GG\vd h\ \ol{M_n^{1}}\in \|h\ \ol{N_n^{1}}\|$ 
and $\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} \|$.  By inversion $\GG \prv M_{i}\in\|N_{i} \|$ and $\GG \prv 
M\in\|Q \|$, for $1\leq i\leq n$, which by the inductive hypothesis  
is impossible.  This yields the thesis.
\item 
Case: $N$ is an abstraction $\lxua N$.  Assume $\GG \prv \lxua M\in \| 
\lxua N\|$ and $\GG \prv \lxua M\in \| \lxua Q\|$, where $\GG\vd 
\mnot( \lxua N) = \lxua Q$.  By inversion $\GG \prv,x\oftp A M\in \| 
N\|$ and $\GG,x\oftp A \prv M\in \| Q\|$, where $\GG,x\oftp A\vd \mnot( 
N) = Q$.  The latter is impossible by IH and this yields the thesis.
\end{itemize}
\end{proof}

\smallskip
We now prove the crucial tightening lemma.


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


\begin{lemma}
\label{le:embex} Let $M$ be a simple patterns:
\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 simultaneous induction on $\cD_{1}::\cu\vd M\da A$ and $\cD_{2}::\cu\vd M\bua A$.
% \bit
% \item 
$$\cD = \ianc{c\oftp A\in\Sigma}{\cu \prv  c\da A}{cIdc}$$
Then
$$\cE= \ianc{c\oftp A\in\Sigma}{\cxto \prv  c\da A}{cIdc}$$
%\item
$$\cD = \ianc{}{(\GG,\Omega,\Delta,x\oftp C,y\oftp A);\cdot; \cdot  \prv  y\da 
A}{cId^{u}}$$
Then 
$$\cE = \ianc{}{(\GG,\Omega,\Delta,y\oftp A);x\oftp C; \cdot  \prv  y\da 
A}{cId^{u}}$$
$$\cD = \ianc{}{\cu \prv  x\da C}{cId^{u}}$$
Then
$$\cE= \ianc{}{\cxtr \prv  x\da C}{cId^{1}}$$

%\item No case for $\cD = Id^{1}$.
%\item
$$\cD = \ianc{\cu\prv  M\da P}{\cu \prv  M\bua P} {cAt}$$
By inversion $\cu\prv  M\da P$, by IH $\cxtr \prv  M\da P$ or $\cxto \prv  M\da 
P$ and hence $\cxtr \prv  M\bua P$ or $\cxto \prv  M\bua P$.
%\item
$$\cD = \ianc{y\oftp A,\cu \prv M\bua B}{\cu\prv(\lamb{y^u}{A} M) \bua 
A\TImp B} {c\TImp I}$$
By inversion $y\oftp A,\cu \prv M\bua B$ which entails by IH $y\oftp 
A,\cxtr \prv M\bua B$ or $y\oftp A,\cxto \prv M\bua B$ and finally 
$\cxtr\prv(\lamb{y^u}{A} M) \bua A\TImp B$ or $\cxto\prv(\lamb{y^u}{A} M) 
\bua A\TImp B$.
%\item
$$\cD = \ibnc{\cu \vd M \da A \RImp B}{\cu \vd N \bua A}{\cu \vd
M\, N^1 \da B}{c\RImp E}$$
By inversion there are derivations $\cD_{1}:: \cu \vd M \da A \RImp 
B$ and $\cD_{2}:: \cu \vd N \bua A$.
There are four disjoint sub-cases, stemming from the IH  :
\ben
\item $\cxtr\vd M\da A\RImp B$ and $\cxtr\vd N\bua A$. Thus $\cxtr\vd M\ 
N^{1}\da B$, hence  by weakening the thesis.
\item $\cxto\vd M\da A\RImp B$ and $\cxto\vd N\bua A$. Thus $\cxto\vd M\ 
N^{1}\da B$, hence  by weakening the thesis.
\item $\cxtr\vd M\da A\RImp B$ and $\cxto\vd N\bua A$. Thus  $\cxtr\vd M\da A\RImp B$
or  $\cxto\vd M\da A\RImp B$ and $\cxtr\vd N\bua A$ or $\cxto\vd N\bua 
A$. Hence the thesis.
\item Symmetrical to the last one.
%
\enen
\end{proof}




\begin{Corollary}
\label{co:part2}
If $(\GG, \O,\D)\emp\vd M\buda P$ then $\godemp\vd M\in \|E\ 
\ol{x^l_n}\| \hastype P$ or there is a $F\ \ol{x^{l'}_n}$, such that 
$\godemp\vd\mnot(E\ \ol{x^l_n})= F\ \ol{x^{l'}_n} \hastype P$ and $\godemp\vd 
M\in \|F\ \ol{x^{l'}_n}\| \hastype P$.
\end{Corollary}
\begin{proof} By Lemma \ref{le:tight1} $\god\vd M\buda A$ or $\godap\vd 
M\buda A$, where $\GG'= (\god)- x\oftp C$ and for $x\oftp C\in \D$ 
either $\D'=x\oftp C, \O'=\cdot$ or for $x\oftp C\in \O$ it holds 
$\O'=x\oftp C, \D'=\cdot$.  If we write $E\ \ol{x^l_n}$ as $E\ \GG^{u} 
\ \O^0 \ \D^{1}$, the condition implies that $\godemp\vd\mnot(E\ 
\GG^{u} \ \O^0 \ \D^{1})=F\ \GG'^{u} \ \O'^0 \ \D'^{1}$.  Thus by rule 
$grFlex$, $\godemp\vd M\in \|E\ \GG^{u} \ \O^0 \ \D^{1} \|$ or 
$\godemp\vd M\in \|F\ \GG'^{u} \ \O'^0 \ \D'^{1} \|$.
\end{proof}




\begin{theorem}
\label{thm:part2}
Given a linear simple term $\GG\vd N\hastype A$, either $\GG \prv M\in 
\| N \| \hastype A$ or there is a $Q$ such that $\GG\vd\mnot(N) = Q$ 
and $ \GG \prv M\in \| Q\| \hastype A$.
\end{theorem}
\begin{proof}
By  induction on $N$.
Basis:by Corollary \ref{co:part2}.
\\ \noindent 
Step: 
\bit 
\item Case: $N$ is an application $(h\ \ol{N_n^{1}})$ for $ n\geq 0$.  
Sub-case $app^1$: let $M$ be a ground term $g\ \Mm$ where 
$q\not\equiv h$.  Then clearly $\GG\vd g\ \Mm\in \|g\ (Z_{1} 
\GG^{u})^{1}\dots (Z_{m}\GG^{u})^{1}\\| $, where $\GG \prv \mnot(h\ 
\ol{N_n^{1}}) = g\ (Z_{1} \GG^{u})^{1}\dots (Z_{m}\GG^{u})^{1}\| $, 
by rule $\mnot\_App^{2}$ $\GG \prv g\ \ol{M_m}\in \| h\ \ol{N_n} \| 
\hastype P$ or $Q$ such that $\GG\vd\mnot( h\ \ol{N_n} ) = Q$ and $ 
\GG \prv g\ \ol{M_m} \in \| Q\| \hastype P$.
 
 
Sub-case $app^2$: $\GG\vd h\ \ol{N_n^{1}}\hastype P$.  By inversion 
$\GG\vd N_{i}\hastype A_{i}$ for $1\leq i\leq n$.  By IH either $\GG 
\prv M_{i}\in \| N_{i} \| \hastype A_{i}$ or there is a $Q$ such that 
$\GG\vd\mnot(N_{i}) = Q$ and $ \GG \prv M_{i}\in \| Q\| \hastype A$.  
Assume $\GG \prv M_{i}\in \| N_{i} \| \hastype A_{i}$ for $1\leq 
i\leq n$.  Then by rule $grApp$ $\GG \prv h\ \ol{M_n}\in \| h\ 
\ol{N_n} \| \hastype P$ and by weakening $\GG \prv h\ \ol{M_n}\in \| 
h\ \ol{N_n} \| \hastype P$ or $\GG \prv h\ \ol{M_n}\in \| h\ 
(Z_{1}\GG^{u} )^{1}\dots (Z_{i-1}\GG^{u} )^{1}\ N^{1}\ 
(Z_{i+1}\GG^{u} )^{1}\dots (Z_{m}\GG^{u} )^{1} \| \hastype P$, \ie by 
rule $\mnot\_App^{2}$ $\GG \prv h\ \ol{M_n}\in \| h\ \ol{N_n} \| 
\hastype P$ or $Q$ such that $\GG\vd\mnot( h\ \ol{N_n} ) = Q$ and $ 
\GG \prv h\ \ol{M_n} \in \| Q\| \hastype P$.  Otherwise assume there 
is a $Q$ and $i\hastype 1\leq i\leq n$ such that $\GG\vd\mnot(N_{i}) = 
Q$ and $ \GG \prv M_{i}\in \| Q\| \hastype A$.  Clearly $\GG\vd 
M_{j}\in\|(Z_{j}\GG^{u} )^{1}\|$ for $j\neq i, 1\leq j\leq n$.  Thus 
by rule $grApp$ $\GG \prv h\ \ol{M_n}\in \| h\ (Z_{1}\GG^{u} 
)^{1}\dots (Z_{i-1}\GG^{u} )^{1}\ N^{1}\ (Z_{i+1}\GG^{u} )^{1}\dots 
(Z_{m}\GG^{u} )^{1} \| \hastype P$, \ie by rule $\mnot\_App^{2}$ $\GG 
\prv h\ \ol{M_n}\in \| h\ \ol{N_n} \| \hastype P$ or $Q$ such that 
$\GG\vd\mnot( h\ \ol{N_n} ) = Q$ and $ \GG \prv h\ \ol{M_n} \in \| 
Q\| \hastype P$.

\item
Case: $N$ is an abstraction $\lxua N$.  Assume $\GG\vd\lxua N\hastype 
A\TImp B$; by inversion $\GG, x\oftp A\prv N\hastype B$.  By IH 
either $\GG,x\oftp A \prv M\in \| N \| \hastype B$ or there is a $Q$ 
such that $\GG,x\oftp A\vd\mnot(N) = Q$ and $ \GG \prv M\in \| Q\| 
\hastype B$.  Assume $\GG,x\oftp A \prv M\in \| N \| \hastype B$; 
then by rule $grLam$ $\GG \prv \lxua M\in \|\lxua N \| \hastype 
A\TImp B$ and finally $\GG \prv \lxua M\in \|\lxua N \| \hastype 
A\TImp B$ or there is a $\lxua Q$ such that $\GG\vd\mnot(\lxua N) = 
\lxua Q$ and $ \GG \prv \lxua M\in \|\lxua Q\| \hastype A\TImp B$.  
Otherwise, assume for a generic $Q$ $\GG, x\oftp A\vd\mnot(N) = Q$ and 
$ \GG \prv M\in \| Q\| \hastype B$.  Then $ \GG \prv \lxua M\in \| 
\lxua Q\| \hastype A\TImp B$.  Finally $\GG \prv \lxua M\in \|\lxua N 
\| \hastype A\TImp B$ or there is a $\lxua Q$ such that 
$\GG\vd\mnot(\lxua N) = \lxua Q$ and $ \GG \prv \lxua M\in \|\lxua 
Q\| \hastype A\TImp B$.
\enit
\end{proof}

\begin{Corollary}[Partition Lemma] For a fixed signature $\Sigma$ let 
$\GG\vd N \hastype A$ be a linear simple term:
\label{lemma:part}
\ben
\item (Exhaustivity) $\GG\prv  M\in \| N \| \hastype A$ or $\GG\prv  M\in \| 
\mmnot(N) \|\hastype A$.
\item (Disjointness) It is not the case that $\GG\prv  M\in \| N \|\hastype A$ and 
$\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}
\end{document}

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

We now address the issue of unification, \ie intersection of simple 
linear \ho patterns.  We start by determining when two labeling are 
compatible: 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
  We then 
extend it again to lists (contexts) of labeled variables; remember 
that full application entails that we only intersect context that are 
the same modulo different labeling: 
\beq 
\cdot\mcap \cdot & = & 
\cdot\\
(x^k\ xs)\mcap (x^{k'}\ ys) & = &  (x^{k\mcap k'}\ (xs\mcap ys))
\quad\mbox{\textrm{if $k\mcap k'$ is defined.}}
\eneq


\begin{Definition}[Higher-Order Pattern Intersection]
Fix a signature $\Sigma$.  For  linear simple terms in canonical 
form $M,N$ such that $\GG \prv  M \buda A$ and $\GG \prv  N 
\buda A$ define $\GG\prv  M \mcap N = Q \hastype  A$ as:


\begin{small}
\[
\begin{array}{c}
\ianc{\Phi_1\mcap \Phi_2 = \Phi%\quad \Phi\not = nil
 }
{\GG\prv  E \ \Phi_1\mcap   F\ \Phi_2= H\ \Phi \hastype  P} 
{\mcap\_FlxFlx}
\vsk
\mbox{\textrm{no rule for flex-flex same}}
\vsk
\ianc{c\in\Sigma\quad \GG\prv  H_1 \ \Phi_{1}\mcap 
M_{1}=N_{1}\hastype A_{1}\cdots \GG\prv  H_n \ \Phi_{n}\mcap 
M_{n}=N_{n}\hastype A_{n}  } 
{ \GG\prv  E \ \Phi \mcap c\ \Mns= c\ \Nns\hastype  P} {\mcap\_FlxRgd^c }
\vsk
\ianc{y\in\GG\quad  \quad \GG\prv  H_1 \ \Phi_{1}\mcap 
M_{1}=N_{1}\hastype A_{1}\cdots \GG\prv  H_n \ \Phi_{n}\mcap 
M_{n}=N_{n}\hastype A_{n} } 
{\GG\prv E\ \Phi \mcap y\ \Mns= y\ \Nns \hastype  P} {\mcap\_FlxRgd^y }
\vsk
\ianc{ h\in\GG\cup\Sigma\quad \GG\prv  M_1 \mcap N_{1} = Q_1\hastype  A_1 \cdots \GG\prv  M_n \mcap 
N_{n}= Q_n \hastype  A_n} 
{\GG\prv   h\ \Mm^{1}\mcap h\ \Nns = h\ \ol{Q_{n}^{1}} \hastype  P} {\mcap\_App}
\vsk
\ianc{ h\in\GG\cup\Sigma\quad  \GG\prv N\mcap h\ \Mm^{1} = Q\hastype  P} 
{\GG\prv   h\ \Mm^{1}\mcap N = Q \hastype  P} 
{\mcap\_Excng}
\vsk
\ianc{\GG,x\oftp A\prv   M  \mcap  N = Q\hastype  B}
{\GG\prv   \lxua M  \mcap \lxua N =\lxua Q \hastype  A\Imp B}{\mcap\_Lam}
\end{array}
\]
\end{small}
where the $\Phi$'s are fully-applied contexts and the $H$'s are fresh 
variables of opportune typing and $m\geq 0$.  The rule 
$\mcap\_FlxRgd^c $ has the following proviso: 
\beq
\forall x. \Phi(x) = 0 & \Imp & \forall i:1\leq i\leq n. \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 
$\mcap\_FlxRgd^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 
$M\mbigcap N \hastype A  = \{Q\mid\cdot\prv  M\mcap N = Q \hastype  A\}$
\end{Definition} 

Some remarks are in order:
\bit
\item
In rule $\mcap\_FlxFlx$ we can assume that the same list 
of variables, though with different labeling, is the argument of $E,F$ 
and $G$, since simple terms are fully-applied and due to linearity we 
can always reorder the context to the same list.  
\item
Thanks to linearity 
again the flex-flex same variable case does not occur. 
\item 
In  rule $\mcap\_FlxRgd$ the proviso is compelled by the typing 
rules not to leave the status of $x$ undetermined in the antecedent, 
when $c$ is a constant.  
\item
If instead $y$ is the projected variable, it 
\textbf{does} occur in the RHS: hence it \emph{ought to} occur in the 
LHS: moreover, since it did occur, it is set to $u$ in the rest of the 
computation.
\item
The exchange rule can be avoided if we agree to see the LHS of the 
judgment $\GG\vd M\mcap N=Q\hastype A$ as a multiset.
\enit

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

\begin{example}
Consider the unification problem $x^{u}\oftp A\prv E\ x^{1}\mbigcap\ 
c\ (F_{1}\ x^{u})^{1} \ (F_{2}\ x^{u})^{1}$.  Since $x$ is strict in 
the LHS, there are three ways in which $\Phi$ can be `split' leading 
to the following sub-problems:
\[
\begin{array}{ll}
x\oftp A\emp\prv E_{1}\ x^{1}\mcap\  (F_{1}\  x^{u})^{1} = (H_{1}\  
x^{1})^{1}
&x\oftp A\emp\prv E_{2}\ x^{1}\mcap\  (F_{2}\  x^{u})^{1} = (H_{2}\  
x^{1})^{1}\\
x\oftp A\emp\prv E_{1}\ x^{1}\mcap\  (F_{1}\  x^{u})^{1} = (H_{1}\  
x^{1})^{1}
&x\oftp A\emp\prv E_{2}\ x^{0}\mcap\  (F_{2}\  x^{u})^{1} = (H_{2}\  
x^{0})^{1}\\
x\oftp A\emp\prv E_{1}\ x^{0}\mcap\  (F_{1}\  x^{u})^{1} = (H_{1}\  
x^{0})^{1}
&x\oftp A\emp\prv E_{2}\ x^{1}\mcap\  (F_{2}\  x^{u})^{1} = (H_{2}\  
x^{1})^{1}
\end{array}
\]
Hence the result:
\beq
\lefteqn{x\oftp A\emp\prv E\ x^{1}\mbigcap\  c\ (F_{1}\  x^{u})^{1} \ (F_{2}\  
x^{u})^{1} = }\\
& \{c\ (H_{1}\  x^{1})^{1} \ (H_{2}\  x^{0})^1,c\ (H_{1}\  x^{0})^1 \ (H_{2}\  
x^{1})^1,c\ (H_{1}\  x^{1})^1 \ (H_{2}\  x^{1})^1\}
\eneq
\end{example}

The following example illustrates the additional proviso on 
$\mcap\_FlxRgd_{y}$:
\begin{example}
The unification problem $y\oftp A\vd E\ y^{0} \mcap y\ (F_{1}\  y^{u})^{1} \ (F_{2}\  
y^{u})^{1}$ has no solution, whereas 
$y\oftp A\vd E\ y^{1} \mcap y\ (F_{1}\  y^{1})^{1} \ (F_{2}\  
y^{u})^{1}=y \ (H_{1}\  y^{1})^1 \ (H_{2}\  y^{u})^1\ $
\end{example}

{\newcommand{\gm}{\Gamma;(\Omega, }

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}.

\beq 
\ianc{\GG;(\O,\D^{0}_{i});\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\,.\,\in\D_{i}^{0}\cup\D_{i}^{1}=\D$.
\enen


%proj rule
\beq 
\ianc{\GG;(\O,\D^{0}_{i});\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 $\god\vd y\ \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}^{0}\cup\D_{i}^{1}=\D$.
\item 
$y\in\GG\cup\D$.
\item 
$y\in \D\Imp \forall i:1\leq i\leq n\,.\, y\in \GG$.
\enen

% \beq
% \ibnc{\gm \D_{M_{2}}\dots\D_{M_{n}});(\D_{M_{1}},\D_{\ol{M_{n}}})\vd 
% M_{1}\bua A_{1}}{\gm \D_{M_{1}}\dots\D_{M_{n-1}});(\D_{M_{n}},\D_{\ol{M_{n}}})\vd 
% M_{n}\bua A_{n}}{\Gamma;\Omega; 
% (\D_{M_{1}}\dots\D_{M_{n}},\D_{\ol{M_{n}}})\vd c\ M_{1}\dots 
% M_{n}\da P}{c\RImp E }
% \eneq
% where $\emp\vd c\da A_{1}\RImp\dots\RImp A_{n}\RImp B$.

We then show that both are invertible and derivable rules. 
We drop the $\_^{1}$ annotations in the following lemmata:

\begin{Lemma}
\label{le:soundec}
If $\gm \D_i^{0});\D_i \vd ^{1}\vd M_{j}\hastype A_{j}$ for $1\leq 
i\leq j$ and where $\GG;\O;\cdot\vd c\ \hastype A_{1}\RImp\dots\RImp 
A_{n}\RImp B$, then $\gm D^{0});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^{1}.\neg\exists i:1\leq i\leq j\,.\,x\in\D_{i}^{0}$.
\item[2.]
$\forall i:1\leq i\leq j\,.\,\in\D_{i}^{0}\cup\D_{i}^{1}=\D$.
\enit
\end{Lemma}
\begin{proof}
By induction on $j$.
\end{proof}

\begin{theorem}
\label{thm:soundec}
If $\GG;(\O,\D^{0}_{i});\D_i^{1} \vd M_{i}\hastype A_{i}\quad 
1\leq i\leq n$ then $\Gamma;\Omega; \D\vd c\ M_{1}^{1}\dots M_{n}^{1}\hastype 
B$, 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\,.\,\in\D_{i}^{0}\cup\D_{i}^{1}=\D$.
\enen
\end{theorem}
\begin{proof}
Use Lemma \ref{le:soundec} with $j=n$. Indeed, 
$\D^{0}=\cdot,\D^{1}=\D$, conditions $1.$ and $2.$ are immediately 
satisfied and condition $1'.$ is trivially true.
\end{proof}




% sound of proj

\begin{theorem}
\label{thm:soundey}
If $\GG;(\O,\D^{0}_{i});\D_i^{1} \vd M_{i}\hastype A_{i}\quad 
1\leq i\leq n$ then $\Gamma;\Omega; \D\vd c\ M_{1}^{1}\dots M_{n}^{1}\hastype 
B$, where $\god\vd y\ \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}^{0}\cup\D_{i}^{1}=\D$.
\item 
$y\in\GG\cup\D$.
\item 
$y\in \D\Imp \forall i:1\leq i\leq n\,.\, y\in \GG$.
\enen
\end{theorem}
\begin{proof}
Use Lemma \ref{le:soundec} with $j=n$. Indeed, 
$\D^{0}=\cdot,\D^{1}=\D$, conditions $1.$ and $2.$ are immediately 
satisfied and condition $1'.$ is trivially true.
\end{proof}


% \begin{Lemma}
% \label{le:sounder1}
% If $\gm \D_{M_{j}});(\D_{M_{1}}\dots\D_{M_{i-1}},\D_{\ol{M_{i-1}} M_j})\vd 
% c\ M_{1}\dots M_{i-1}\hastype A_{i}\RImp\dots\RImp A_{n}\RImp B$ and 
% $\gm \D_{M_{1}}\dots\D_{M_{i-1}});(\D_{M_{j}},\D_{\ol{M_{i-1}} M_j})\vd 
% M_{j}\hastype A_{j} $ for $i-1\leq j\leq n$ then 
% $\Gamma;\Omega;(\D_{M_{1}}\dots\D_{M_{n}},\D_{\ol{M_{n}}}
% )\vd c\ M_{1}\dots M_{n}\hastype B$.
% \end{Lemma}
% 
% \begin{proof}
% By induction on $j$.
% 
% \item Base: $j=n$.  $\gm 
% \D_{M_{n}});(\D_{M_{1}}\dots\D_{M_{n-1}},\D_{\ol{M_{n}}})\vd c\ 
% M_{1}\dots M_{n-1}\hastype  A_{n}\RImp B$ and $\gm 
% \D_{M_{1}}\dots\D_{M_{n-1}});(\D_{M_{n}},\D_{\ol{M_{n}}})\vd 
% M_{n}\hastype A_{n} $; then by one application of $\RImp E$ infer 
% $\Gamma;\Omega; (\D_{M_{1}}\dots\D_{M_{n}},\D_{\ol{M_{n}}} )\vd c\ 
% M_{1}\dots M_{n}\hastype B$.
% 
% \item Step: $j=i-1$.  $\gm \D_{M_{i-1}});(\D_{M_{1}}\dots\D_{M_{i-2}}, 
% \D_{\ol{M_{i-1}} M_j})\vd c\ M_{1}\dots M_{i-2}\hastype A_{i-1}\RImp A_{i} 
% \dots \RImp A_{n}\RImp B$ and $\gm 
% \D_{M_{1}}\dots\D_{M_{i-2}});(\D_{M_{i-1}},\D_{\ol{M_{i-1}} M_j})\vd 
% M_{i-1}\hastype A_{i-1} $; then by one application of $\RImp E$ \ infer 
% $\Gamma;\Omega; (\D_{M_{1}}\dots\D_{M_{i-1}},\D_{\ol{M_{i-1}} M_j})\vd c\ 
% M_{1}\dots M_{i-1}\hastype B$.  By IH we conclude $\Gamma;\Omega; 
% (\D_{M_{1}}\dots\D_{M_{n}},\D_{\ol{M_{n}}})\vd c\ M_{1}\dots 
% M_{n}\hastype B$.  
% \enit
% \end{proof}
% 
% Note how the side conditions in the $n$-ary rules entail the provisos 
% on the intersection rules.  Firstly note that if $\Phi(x) = 0$ then 
% $x\in\O$ which is unchanged in the premisses; 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 entails $\exists i:1\leq i\leq n.  
% \Phi_{i}(x) = 1$, while the second that there are no undetermined 
% labels, \ie $\forall j:1\leq i\leq n, j\neq i.  \Phi_{i}(x) \neq u$.
% As far as the $FlxRgd^{y}$ rule is concerned condition $3$ and $4$ 
% entails the additional proviso.

\begin{Lemma}
\label{le:flexunif}
$\GG\prv M\in\|E\ \Phi_{1}\|:P$ and $\GG\prv M\in\|F\ \Phi_{2}\|:P$ iff $\GG\prv 
M\in\|H\ \Phi_{1}\mcap \Phi_{2}\|:P$.
\end{Lemma}
\begin{proof}
By induction on $\Phi_{1}$.
Base: if $\Phi_{1}=\Phi_{2}=\cdot$, the result is immediate.
\newline\noindent
Step: otherwise $\Phi_{i}$, for $i \in\{1,2\}$, can be written as 
$\GG^{u}_{i},\Omega^{0}_{i},\Delta^{1}_{i}, x^{k_{i}}$. We proceed by 
cases on $x^{k_{i}}$:
\bit
\item $k_{1}=1,k_{2}=u$, $ (\Imp)$. Then immediately $\GG\vd M\in \|H\ 
(\GG^{u}_{1}\mcap \GG^{u}_{2})\ (\Omega^{0}_{1}\mcap \Omega^{0}_{2}) \ 
(\Delta^{1}_{1}\mcap \Delta^{1}_{2}) \ x^{1}\|$. $(\If)$.
Assume $\GG\vd M\in \|H\ (\GG^{u}_{1}\mcap \GG^{u}_{2})\ 
(\Omega^{0}_{1}\mcap \Omega^{0}_{2}) \ (\Delta_{1}\mcap 
\Delta_{2}) \ x^{1}\|$; then by rule $grFlx$ $ (\GG_{1}, 
\GG_{2}); (\Omega_{1}, \Omega_{2}) ; (\Delta_{1}, \Delta_{2}, x\oftp 
B)\vd M\hastype A$.  By Loosening$^{1}$ (Theorem \ref{thm:1loose}) 
this implies $ (\GG_{1}, \GG_{2}, x\oftp B); (\Omega_{1}, \Omega_{2}) 
; (\Delta_{1}, \Delta_{2})\vd M\hastype A$.  Thus conclude 
$\GG\vd M\in \|F\ (\GG_{1}^u, \GG_{2}^u)\ (\Omega_{1}^0, \Omega_{2}^0) \ 
(\Delta_{1}^1, \Delta_{2}^1) \ x^{u}\|$.

\item $k_{1}=0,k_{2}=u$, $ (\Imp)$.  Then $\GG\vd M\in \|H\ 
(\GG^{u}_{1}\mcap \GG^{u}_{2})\ (\Omega^{0}_{1}\mcap \Omega^{0}_{2}) \ 
(\Delta^{1}_{1}\mcap \Delta^{1}_{2}) \ x^{0}\|$.  $(\If)$.  Assume 
$\GG\vd M\in \|H\ (\GG^{u}_{1}\mcap \GG^{u}_{2})\ (\Omega^{0}_{1}\mcap 
\Omega^{0}_{2}) \ (\Delta^{1}_{1}\mcap \Delta^{1}_{2}) \ x^{0}\|$; 
then by rule $grFlx$ $ (\GG_{1}, \GG_{2}); (\Omega_{1}, \Omega_{2}, 
x\oftp B) ; (\Delta_{1}, \Delta_{2})\vd M\hastype A$.  By 
Loosening$^{0}$ (Theorem \ref{thm:0loose}) this implies $ (\GG_{1}, 
\GG_{2}, x\oftp B); (\Omega_{1}, \Omega_{2}) ; (\Delta_{1},
\Delta_{2})\vd M\hastype A$.  Thus conclude $\GG\vd M\in \|F\ 
(\GG_{1}^u, \GG_{2}^u)\ (\Omega_{1}^0, \Omega_{2}^0) \ (\Delta_{1}^1, 
\Delta_{2}^1) \ x^{u}\|$.

\item The symmetrical cases are identical. The idempotent 
ones are immediate.
\enit
\end{proof}

\begin{theorem}
\label{thm:unif1}
If $\GG\prv M\in\|N_{1}\|:A$ and $\GG\prv M\in\|N_{2}\|:A$ for $\GG\vd 
N_{1}\mcap N_{2}= N$, then $\GG\prv M\in\|N\|:A$.
\end{theorem}
\begin{proof}
By induction on $N$.
\bit
\item Case: $\mcap\_FlxFlx$; apply left-to-right direction of Lemma \ref{le:flexunif}.
\item Case: $\mcap\_FlxRgd _{1}$; assume $\GG\vd M\in\|E\ 
\Phi\|$ and $\GG\vd M \in\|c\ \ol{Q_{n}^{1}}\|$, where $\GG\vd E\ 
\Phi\mcap c\ \ol{Q_{n}^{1}} = c\ \Nns$. By definition 
$\GG\vd c\ \Mns\in\|E\ 
\Phi\|$ and $\GG\vd c\ \Mns \in\|c\ \ol{Q_{n}^{1}}\|$ if by 
inversion $\GG\vd M_{i}\in\|N_{i}\|$ for $1\leq i\leq n$ and $c\ 
\Mn\equiv t\ \Phi$, where $t\hastype A$ and $t\equiv \l\Phi\,.\,c\ \tn$ 
for  $\Phi\vd c\ \tn^{1}\hastype P$. By inversion on rule $\RImp 
E^{n}_{c}$ (Lemma \ref{le:}) this entails the 
existence of a context $\Phi_{i}$ which satisfies the  proviso 
such that $\Phi_{i}\vd t_{i}\hastype A_{i}$. Thus $\GG\vd 
M_{i}\in\|E_{i}\ \Phi_{i}\|$ for a new existential variable, where 
$\GG\vd E_{i}\ \Phi_{i}\mcap Q_{i}=N_{i}$. By IH $\GG\vd 
M_{i}\in\|N_{i}\|$ and finally $\GG\vd c\ \Mns\in\|c\ \Nns\|$.
% \item Case: $\mcap\_FlxRgd_{2}$. Proceed as above, but using 
% Lemma \ref{le:}.

\item Case: $\mcap\_Lam$; assume $\GG\prv \lxua M\in\|\lxua N_{1}\|$ 
and $\GG\prv \lxua M\in\|\lxua N_{2}\|$ by inversion $ \GG,x\oftp 
A\vd M\in\| N_{1}\|$ and $\GG,x\oftp A\prv M\in\| N_{2}\|$.  By 
inductive hypothesis for $\GG\vd 
N_{1}\mcap N_{2}= N$ and $\GG,x\oftp A\prv M\in\| N\|$, 
thus $ \GG\vd \GG\prv \lxua M\in\|\lxua N\|$.
\item Case: $\mcap\_App$; by a straightforward appeal to the inductive hypothesis 
as in the above case.
\enit
\end{proof}

% start other direction
 
\begin{theorem}
\label{thm:unif2}
If $\GG\vd N_{1}\mcap N_{2}= N$ and $\GG\prv M\in\|N\|:A$, then $ \GG\prv 
M\in\|N_{1}\|:A$ and $\GG\prv M\in\|N_{2}\|:A$ .
\end{theorem}
\begin{proof}
By induction on $N$.
\bit

\item Case: $\mcap\_FlxFlx$; apply right-to-left direction of Lemma
 \ref{le:flexunif}.

\item Case: $\mcap\_FlxRgd $; assume $\GG\vd M\in\|c\ \Nns|$ 
, where $\GG\vd E\ \Phi\mcap c\ \ol{Q_{n}^{1}} = c\ \Nns$.  By 
definition $\GG\vd c\ \Mns \in\|c\ \ol{N_{n}^{1}}\|$ if by 
inversion $\GG\vd M_{i}\in\|N_{i}\|$ and $\GG\vd E\ \Phi_{i}\mcap 
Q_{i}=N_{i}$ for $1\leq i\leq n$.  By induction hypothesis $\GG\vd 
M_{i}\in\|E\ \Phi_{i}|$ and $\GG\vd M_{i}\in\|Q_{i}|$ and $M_{i}\equiv 
t\ \Phi_{i}$, where $t\hastype A$ and $t\equiv \l\Phi_{i}\,.\,c\ \tn$ 
for $\Phi_{i}\vd c\ \tn^{1}\hastype P$.  By rule $\RImp E^{n}_{c}$ 
(Lemma \ref{le:}) this entails the existence of a context $\Phi$ which 
satisfies the first proviso such that $\Phi\vd c\ \tn\hastype B$.  
Thus $\GG\vd M_{i}\in\|E\ \Phi\|$.  Thus finally $\GG\vd c\ 
\Mns\in\|E\ \Phi\|$ and $\GG\vd c\ \Mns\in\|c\ \ol{Q_n^{1}}\|$.

%  \item Case: $\mcap\_FlxRgd_{2}$.  Proceed as 
% above, but using Lemma \ref{le:}.

\item Case: $\mcap\_Lam$; assume $\GG\prv \lxua M\in\|\lxua N\|$, where 
$\GG\vd \lxua N_{1}\mcap \lxua N_2 = \lxua N$.  By inversion $ 
\GG,x\oftp A\vd M\in\| N_\|$ where $\GG,x\oftp A\vd N_{1}\mcap N_2 = 
N$.  By inductive hypothesis $ \GG, x\oftp A\prv M\in\|N_{1}\|$ and 
$\GG,x\oftp A\prv M\in\|N_{2}\|$, hence $ \GG\prv \lxua M\in\|\lxua 
N_{1}\|$ and $\GG\prv \lxua M\in\|\lxua N_{2}\|$.

\item Case: $\mcap\_App$; by a straightforward appeal to the inductive 
hypothesis as in the above case.

\enit
\end{proof}

\begin{Corollary}[Soundness and Completeness of Pattern intersection]
\label{co:unif}
If $\GG\vd N_{1}\mcap N_{2}= N\hastype A$,then $\GG\prv 
M\in\|N_{1}\|\hastype A$ and $\GG\prv M\in\|N_{2}\|\hastype A$, iff $\GG\prv 
M\in\|N\|\hastype A$.
\end{Corollary}

\smallskip
We now list some basic properties of intersection, which follows from 
Corollary \ref{co:unif} and will be useful in the next Section.

\begin{Corollary}
\label{co:unifpr}
Let $M,N$ be simple linear terms of type $A$:
\bit
\item
$ M\mbigcap M = \{M\} $.
\item
$ M\mbigcap N = N\mbigcap M$.
\enit
\end{Corollary}
% 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] : M\in M_{i}, 
% N\in N_{j}, P \in M\mbigcap N : A\}
% \eneq

\section{The Algebra of Strict Terms}

\newcommand{\cM}{{\cal M}}
\newcommand{\mbc}{\bigcap} %overloaded notation: may be changed
\newcommand{\mna}{\mmnot} %overloaded notation: may be changed

We now extend the intersection and complement operations to \emph{sets} 
of terms: this is required by the finitary nature of the former. 

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

Those operations on set of terms satisfy the same properties that 
`singleton' intersection and complementation do. We need to extend the 
judgment in Fig.~ \ref{fig:grinst} to \emph{sets} of terms:
\[
\ianc{\god\prv  M \in \|N_{i}\|:A\quad 1\leq i\leq n}
{\god\prv  M \in \|N_{1}\cdots N_{n}\|:A}{gr_{i}} 
\]
Moreover we write $\GG\prv M \not\in \| N \| :A$, when it is not the 
case that $\GG\prv M \in \| N \| :A$.


\begin{Corollary} [Adequacy of Set Pattern Intersection]
\label{co:setunif}
If $\cN_{1},\cN_{2}$ are sets of 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 linear simple term of type $A$:
\label{co:setpart}
\ben
\item (Exhaustivity) $\GG\prv  M\in \| \cN \| \hastype A$ or $\GG\prv  M\in \| 
\mna(\cN) \|\hastype A$.
\item (Disjointness) It is not the case that $\GG\prv  M\in \| N \|\hastype A$ and 
$\GG\prv  M\in \| \mna(N) \|\hastype A$.
\enen
\end{Corollary}
\begin{proof}
\ben
\item 
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}


\smallskip 

That will allows use to solve `multiple' complement problems, as the 
ones typically required by clause complementation, see Sect.~\ref{}, 
\ie:
$$\|Z\|-\|M_{1}\mdots M_{n}\|$$
as
$$ \mna \{M_{1}\mdots M_{n}\}$$
We can therefore re-visit Example \ref{ex:lam}:
\beq
\mna\{ \lamb{x}{exp} x, \lamb{x}{exp}lam \ (\lamb 
{y}{exp} (E\ x)\ y)\} = \\ 
 \mna(\lamb{x}{exp} 
x)\mbc\mna(\lamb{x}{exp}lam \ (\lamb {y}{exp} (E\ x)\ y)=\\ 
\{\lamb{x}{exp}lam \ (\lamb {y}{exp} (E\ x)\ y),\lamb{x} {exp} app \ 
(E_{1}\ x) (E_{2}\ x))\} \mbc\mbox{}\\
\{\lamb{x}{exp} x,\lamb{x} {exp} app \ 
(E_{1}\ x) (E_{2}\ x))\}=\\ 
 \{\lamb{x} {exp} app \ (E_{1}\ x) (E_{2}\ 
x))\}
\eneq

This suggests that complementation is involutive.  This should come as 
no surprise, as the Partition Lemma tell us that complementation is 
essentially boolean.  It is in fact possible to organize the set of 
finite sets of simple terms over a given signature say $\mathbf{\cal 
T}_{\S}$ in a boolean algebra $\la \mathbf{\cal 
T}_{\S},\emptyset,\bigcup,\mbc,\mna\ra$ under set union, patterns 
intersection and complementation.

\begin{theorem}
\label{thm:algebra}
Consider the algebra  $\la \mathbf{\cal 
T}_{\Sigma},\emptyset,\bigcup,\mbc,\mna\ra$ under set union, patterns 
intersection and complementation. Then the following holds:
\ben
\item
$\cM\mbc\cM = \cM$.
\item
$\cM\mbc\cN = \cM\mbc\cN$.
\item\label{it:DM}
$\cM\mbc(\cN\cup\cP)= (\cM\mbc\cN)\cup(\cM\mbc\cP)$.
\item
$\cM\mbc(\cN\mbc\cP) = (\cM\mbc\cN)\mbc\cP$.
\item
$\mna\mna \cM=\cM$.
\item
$\mna \mathbf{\cal 
T}_{\Sigma}= \emptyset$.
\item
$\mna \emptyset=\mathbf{\cal 
T}_{\Sigma}$.
\enen
\end{theorem}
\begin{proof}\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 $\cM\mbc(\cN\mbc 
\{M\}\cup\cP)=\cM\mbc((\cN\mbc\{M\})\cup(\cN\mbc\cP)) = 
(\cM\mbc(\cN\mbc\{M\}))\cup)\cM\mbc(\cN\mbc\cP))$ by two application 
of (\ref{it:DM}).  Then, by IH, 
$(\cM\mbc\cN)\mbc\{M\}))\cup)(\cM\mbc\cN)\mbc\cP))$ and by 
(\ref{it:DM}) again conclude $(\cM\mbc\cN)\mbc \{M\}\cup\cP)$.  
\item
$\GG\vd M\in \|\mna\mna \cM\|$ iff by Corollary \ref{co:setpart} 
$\GG\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}_{\Sigma},\emptyset,\bigcup,\mbc,\mna\ra$ 
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} suggests 
that any other boolean operation in definable: indeed complementation 
and intersection alone allows to define the \emph{relative} complement 
operation:

\begin{Definition}
\label{def:relcompl}
Given $\cM$ and $\cN$ sets of terms of type $A$:
\beq
\cM - \cN & =_{\textrm{def}} & \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{lemma:part}) 
$\GG\vd M\in \|\cM\|$ and $\GG\vd M\in\|\mmnot(N)\|$ for every 
$N\in\cN$ iff (Corollary \ref{co:unif}) iff $\GG\vd M\in \| \cM\mbc 
(\mna \cN)\|$ iff by definition $\GG\vd M\in\|\cM-\cN\|$.
\end{proof}

Compare with the way in which 
\emph{disunification} approaches the relative complement problems: 
here algebraic operations on sets of terms are translated into 
conjunctions or disjunctions of (dis)equations whose quantification 
status is also kept explicit.  Non-deterministic application of a few 
dozens rules, some addressing identity on finite trees, other 
(dis)equality in general, eventually turns the given problem into a 
solved form.  Though a reduction to a significant subset of the 
disunification rules is likely to be attainable for complement 
problems, it maybe argued that disunification is not necessarily the 
master road to the latter.  Moreover the \ho case brings in 
additional complications, as dependencies which are orthogonal to the 
hyper-logical structuring that disunification requires.

\begin{metanote} 
Insert a remark (and counter-example) on why $\cup$ must be 
set-theoretic union rather than anti-unification?
\end{metanote}

\section{Conclusion}
We have shown that the complement of linear pattern is a finite set 
of simple terms in the strict $\lambda$-calculus.  Moreover, 
unification of simple terms is decidable and leads to a finite set of 
most general unifiers.  We will consider two orthogonal follow-up to 
this work.  First, an extension to the dependent types case, so as to 
endow languages as Twelf \cite{Schurmann98cade} of a logically founded notion of 
negation in the sense of \cite{Bar90}.  Second we will address the 
general case of complementation and unification in the strict 
$\lambda$-calculus; this is likely to be useful in linear logical 
frameworks as \em{LLF} \cite{Cervesato96lics}.

\bibliography{complement,not,lfs,strictness}
 
 \end{document}

