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

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{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{Hanus96RTA}.  Higher-order patterns
inherit many pleasant properties from the first-order case.  In
particular, most general unifiers~\cite{Miller91jlc} and least general
generalizations~\cite{Pfenning91lics} exist, even for complex type
theories.

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 
\cite{Bar90} extended to 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.

The paper is organized as follows: Section \ref{sec:related} briefly reviews
related work, while Section \ref{sec:facomp} treat the case of fully applied patterns.
In Section \ref{sec:strict} we introduce a Strict $\l$-calculus and establish some
basic properties as normalization. Section \ref{sec:strictcomp} introduces a restriction
of the language for which complementation is possible (Section 
\ref{sec:compl}). 
In Section \ref{sec:sunif} we give an unification algorithm for this fragment. Section
\ref{sec:algebra} shows how the former operations induce a boolean algebra
of sets of terms and Section applies the result to 
 the transformational approach to negation in higher-order logic programs. 
We conclude in \ref{sec:concl} with some speculation on future research.

\section{Related Wok}
\label{sec:related}
\subsection{Complement Problems}

Complement problems have some  relevant applications in theoretic computer 
science (see \cite{Comon91} for a list of references); for example in functional programming to 
produce non-ambiguous function definitions by patterns and to 
improve its compilation, in rewriting systems, to check whether an 
algebraic specification is sufficiently completeness,or to analyze 
communicating processes expressed by infinite transition systems, as well as 
in machine learning and inductive theorem proving. In \lp Kunen 
\cite{Kunen87} used them to represent infinite set of answer to 
negative queries. An other approach is discussed in \ref{sec:algebra}.

Lassez et Marriot \cite{Lassez87} proposed the seminal 
{\em uncover} algorithm  for computing relative 
complements and introduced the now familiar restriction to linear terms.
We here quote the definition of the $\mnot$ algorithm for the 
(singleton) complement problem given in \cite{Bar90} as an gentler
 introduction 
to our Definition \ref{def:compl}.
Consider a finite language $L$ and a linear term $t$.  
\[ \begin{array} {lll}
\mnot_L(x  ) & = \emptyset  \\
\mnot_L(f(\tn)  ) & =  \\
 & \{g(\vx)   \mid  \mbox{for all $g \in \Sigma$ distinct from } 
f\} \cup \mbox{} 
\\
& \{f(z_1 \mdots z_{i-1},s,z_{i+1}, \dots,z_n) \mid 
s\in\mnot_L(t_{i}), i \in [1,n] \}
\end{array} \]

An alternative solution to the relative complement problem is
\emph{disunification} (see \cite{Comon91} for a survey and \cite{Lug95} for
an extension to the simply-typed $\l$-calculus): here operations on sets of
terms are translated into conjunctions or disjunctions of equations and
disequation under explicit quantifiers.  Non-deterministic application of a
few dozen rules eventually turns a 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, control is a major problem.
We argue that using disunification for this purpose is unnecessarily
general.  Moreover the \ho case results in additional complications, such as
restrictions on the occurrences of bound variables, which fall outside an
otherwise clean framework.  As we show in this paper, this must not
necessarily be the case.  We believe that our techniques can also be applied
to analyze disunification, although we have not investigated this
possibility at present.



\subsection{Strictness}
\label{sec:strictrel}
%%\subsection{Strictness}

Church original definition of (untyped) $\l$-terms \cite{Church41} has
this clause for abstraction:
\begin{center}
If $M\in\Lambda_{I}$ and $x\in FV(M)$, then $\lx M\in\Lambda_{I}$.
\end{center}
\ie in this language there cannot be vacuous abstractions.  The only
difference between $\Lambda_{I}$ and $\Lambda$ is the lack of
$\mathbf{K}$.  Indeed every term in $\Lambda$ can be defined from
$\Lambda_{I}$ and $\mathbf{K}$.  The $\l\ I$-calculus is the theory of
conversion restricted to those terms.  This fragment was favored by
Church over the usual calculus, because, among other issues, it is
strong enough to represent every partial recursive functions, albeit
not in the most efficient way: see \cite{Barendregt80} Chapter
$2.2.2-2.2.5$ and more extensively in Chapter $9$.  See
\cite{Gabbay92}for an historical account.  Its combinator counterpart
obviously excludes $\mathbf{K}$ and consists of $\mathbf{I,S,B, C}$,
see \cite{Curry58} and \cite{Barendregt80}, Appendix B.

This would correspond in a simply-typed setting to admitting
\emph{only} strict types: more formally if we denote with
$\Lambda^{\GImp{k}}$ the terms typable in a Curry- system based on the
$\GImp{k}$ function space, then $\Lambda^{\GImp{1}}=
\Lambda^{\GImp{u}}\cap \Lambda_{I}$, as noted for example in
\cite{BakerFinch94}.

On an other front, the relevance logic project emerged in the early
sixties out of Anderson and Belnap's dissatisfaction with the
so-called `paradoxes of implication', let it be material,
intuitionistic or strict, was built on the work of Moh, Church, Parry
in the fifties\footnote{Some early work in the twenties in the Soviet
Union was, at the time, not accessible.} and climaxed with the
publication of the first volume of \emph{Entailment}
\cite{Anderson75}.  Following Girard's and Belnap's \cite{SH?}
suggestion we will \emph{not} refer to this calculus as
\emph{relevant}, but as \emph{strict} logic, as the former may also
satisfy other principles such as distributivity of arrow over
conjunction.

On a unrelated front, starting with Mycroft's seminal paper
\cite{Mycroft80}, compile-time analysis of functional programs
approached strictness (and sharing analysis), first in terms of
abstract interpretation, later by using non-standard types to
represent those `intensional' information about functions
(see\cite{Jensen91} for a comparison).  However, earlier works, as
\cite{Kuo89} used non-standard primitive type to distinguish strict or
non-strict terms, closed only under intuitionistic implication.  Not
forgetting Wadler's early paper \cite{Wadler90} on using linear logic
for sharing analysis, Wright \cite{Wright91,Wright92} (see also
\cite{BakerFinch94}) seems the first one to have extended the
Curry-Howard isomorphism to (the implicational fragment of) relevant
logic and connected the two areas.

\begin{metanote} Insert a comparison of those systems to ours.
\end{metanote}


\section{Preliminaries}
\label{sec:facomp}

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 for distinct variables. We promote ``,'' to 
denote disjoint set union.  As usual we identify
terms which differ only in the names of their bound variables.  We
restrict attention to well-typed terms, omitting the standard typing
rules.

In applications such a logic programming or logical frameworks,
$\lambda$-abstraction is used to represent binding operators in some
object language.  In such a situation the most 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}
% 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{Hanus96RTA} because any
fully applied existential variable $\Gamma \vd E\ x_1\ldots x_n$
denotes all canonical terms with free variables from $\Gamma$.
It is this property which makes complementation particularly simple

\begin{example}
\label{ex:lam}
Consider the untyped $\l$-calculus.
\beq
e & \bnfas & x \mid \lx e \mid e_1\, e_2
\eneq
We encode these expressions using the usual techniques of higher-order abstract
syntax (see, for example, \cite{Michaylov91}) as canonical forms
over the following signature.
\beq
\Sigma  & = & exp\hastype \mbox{\textrm{type}}, lam\hastype (exp\Imp 
exp)\Imp exp, app \hastype exp \Imp exp\Imp exp
\eneq
The representation function is given by.
\beq
\rep{x} & = & x\\
\rep{\lx e} & = & lam\ (\lamb{x}{exp} \rep{e})\\
\rep{e_1\ e_2} & = & app\ \rep{e_1}\ \rep{e_2}
\eneq
The representation of an object-language $\beta$-redex then has
the form
\beq
\rep{ (\lx e)\ f} & = & app\ (lam\  (\lamb{x}{exp} \rep{e}))\ \rep{f}
\eneq
 where $\rep{e}$ my have free occurrences of $x$.  When written as a pattern
with variables $E_{exp \arrow exp}$ and $F_{exp}$ ranging over \emph{closed}
terms, this is expressed as $app\ (lam\ (\lamb{x}{exp} (E\ x))\ F)$.  The
complement of the right-hand side considered as a pattern with respect to
the empty context contains every top-level $\lambda$-abstraction plus every
application where the first argument is not an abstraction:
\[
\mmnot(app\ (lam\ (\lamb{x}{exp} (E\ x))\ F)= 
\{ lam\ (\lamb{x}{exp} H\ x), app\ (app\ H_{1}\ H_{2})\ H_{3}\}
 \]
\end{example}

% \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 \hastype 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.}  
% Suppose  we wish to encode a $\beta$-redex (in the object language):
% \beq
% \rep{ (\lx E)\ F} & = & app\ (lam\  (\lamb{x}{exp} (E\ x))\ F
% \eneq
% Its complement denoted, say $\mmnot$, in the given signature, contains every top-level lambda abstraction plus every 
% applications where the first argument is not a lambda: 
% \[
% \mmnot(app\ (lam\ (\lamb{x}{exp} (E\ x))\ F)= 
% \{ lam\ (\lamb{x}{exp} H\ x), app\ (app\ H_{1}\ H_{2})\ H_{3}\}
%  \]
% \end{example}


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

% begin{example}
% \label{ex:etardx}
% Suppose we wish to encode a $\eta$-redex:
% \beq
% \rep{ \lx E\ x} & = & lam(\lamb{x}{exp} app\ E\ x)
% \eneq
% The side condition that $x\not\in FV(E)$ is expressed by the fact that 
% $E$ {\em does not} depend on $x$.  Hence, intuitively its complement 
% should contain only those those applications where $E$ {\em does} 
% depend on $x$.
% \end{example}

%  \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}
 
Note that there is no finite set of patterns which has as its ground
instances exactly those terms $M$ which depend on a given variable $x$.
Following standard terminology, we call such terms \emph{strict in $x$} and
the corresponding function $\lamb{x}{A} M$ a \emph{strict function}.  As the
example above shows, the complement of patterns which are not fully applied
can therefore not be represented as a finite set of patterns.  This failure
of closure under complementation cannot be avoided similarly to the way in
which left-linearization bypasses the limitation to linear patterns and it
needs to be addressed directly.

One approach is taken by Lugiez \cite{Lug95}: he modifies the language of
terms to permit occurrence constraints.  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.

Since our underlying $\lambda$-calculus is typed, we use typing to express
that a function \emph{must} or \emph{must not} depend on its argument.  In
the next section we develop such a $\lambda$-calculus and generalize the
complement algorithm to work on such terms.

%  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 directly 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 make straightforwardly 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.

% Since we live in a typed world, we are going to use typing to  
% express that a function \emph{must} or \emph{must not} depend on its 
% argument(s).  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$. A similar calculus has been investigated 
in \cite{Wright91,BakerFinch94}.

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


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.

Let us go through the typing rules in detail.  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 undetermined variables in $\Gamma$
or irrelevant variables in $\Omega$ can be ignored.  Note that there is no
rule for irrelevant variables, which expresses that they cannot be used.

The introduction rules for undetermined, invariant, and strict functions
simply add a variable to the appropriate context and check the body
of the function.

The difficult rules are the three elimination rules.  First, the
undetermined context $\Gamma$ is always propagated to both premises.
This reflects that we place no restriction on the use of these variables.

Next we consider the strict context $\Delta$.  Recall that this contains
the variables which should occur strictly in a term.  An
undetermined function $M\hastype A \GImp{u} B$ may or may not use
its argument.  An occurrence of a variable in the argument to such
a function can therefore not be guaranteed to be used.  Hence we
must require in the rule $\GImp{u}E$ for an application
$M\ N^u$ that all variables in $\Delta$ occur strictly in $M$.  This
ensures at least one strict occurrence in $M$ and no further
restrictions on occurrences of strict variables in the argument
are necessary.  This is reflected in the rule by adding $\Delta$ to
the undetermined context while checking the argument $N$.  The
treatment of the strict variables in the vacuous application $M\ N^0$
is similar.

In the case of a strict application $M\ N^1$ each strict variable should
occur strictly in either $M$ or $N$.  We therefore split the context into
$\Delta_M$ and $\Delta_N$ guaranteeing that each variable has at least one
strict occurrence in $M$ or $N$, respectively.  However, strict variables
can occur more than once, so variables from $\Delta_N$ can be used freely
in $M$, and variables from $\Delta_M$ can occur freely in $N$.  As before,
we reflect this by adding these variables to the undetermined context.

Finally we consider the irrelevant context $\Omega$.  Variables
declared in $\Omega$ cannot be used \emph{except} in the argument
to an irrelevant function (which is guaranteed to ignore its argument).
We therefore add the irrelevant context $\Omega$ to the undetermined
context when checking the argument of a vacuous application $M\ N^0$.

% Let us go through the typing rules in details.  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.
% Note that there is no rule for variables $x^0$, which expresses that
% they cannot be used.

% 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$ and $\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 why $\D_{N}$ is moved in the 
% undetermined context in the sub-derivation 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, although 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.  
% Namely, 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 (see 
% Theorem \ref{thm:erase}.  Irrelevant variables $x^0$ may still occur, 
% but only in ignored arguments to invariant functions.

% 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 following:

\begin{Remark}[Inversion]
\label{rmk:invert}
All rules in $\lc$ are invertible.
\end{Remark}
As it can be inspected. We will often use inversion principles tacitly 
in proofs by structural induction on the typing derivation.

\begin{metanote} Worth mentioning?\\
Note that, although typing 
is unique, the typing derivation may 
 not.  
\begin{Theorem}[Uniqueness of Typing]
\label{thm:uniqueT}
If $\god\vd M\hastype A$ and  $\GG';\O;\D'\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}
\end{metanote}

We start addressing the structural properties of the context(s).  
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}[Weakening] \mbox{}
 \label{thm:weak}
 \begin{enumerate}
  \item (Weakening$^{u}$) If $\Gamma; \Omega; \Delta\vd M \hastype A$ then $(\Gamma, 
  x\oftp C); \Omega; \Delta\vd M \hastype A$. 
  \item (Weakening$^{0}$) 
  If $\Gamma; \Omega; \Delta\vd M \hastype A$ then $\Gamma
  ; (\Omega, x\oftp C); \Delta\vd M \hastype A$. 
  \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,x\oftp C);\Delta}
\newcommand{\gfod}{(\GG,x\oftp C);\Omega;\Delta}
\newcommand{\bv}{\` By inversion\\}
\newcommand{\bi}{\` By HI }
\newcommand{\bh}{\` By hypothesis\\}
\newcommand{\ba}{\` By assumption\\}
\newcommand{\br}{\` By rule}
\newcommand{\xoc}{x\oftp C}

\begin{Theorem}
\label{thm:0loosex}
If $\gofd\vd M \hastype A$ then $\gfod\vd M \hastype A$. 
\end{Theorem}

\begin{proof}
By  induction on the structure of  $\cD ::\gofd\vd M\hastype  A$ .
\bit

\itc  $$\cD = \ianc{c\oftp A\in\Sigma}{\Gamma; (\Omega,x\oftp C);\cdot \prv  c\hastype  A}{Idc}$$
Then
$$\cE= \ianc{c\oftp A\in\Sigma}{(\GG,\xoc);\Omega;\cdot \prv  c\hastype  A}{Idc}$$
%\item

\itc  $$\cD = \ianc{}{(\Gamma,y\oftp A); (\Omega,\xoc);\cdot\vd y\hastype A}{Id^{u}}$$
Then 
$$\cE = \ianc{}{(\Gamma,y\oftp A,\xoc);\Omega;\cdot\vd y\hastype    
A}{Id^{u}}$$

\itc  $$\cD = \ianc{}{\Gamma;(\Omega,\xoc);y\oftp A\prv  y\hastype  A}{Id^{1}}$$
Then
$$\cE=\ianc{}{(\Gamma,\xoc);\Omega;y\oftp A\prv  y\hastype  A}{Id^{1}}$$

\itc  $$\cD = \ianc{\GG;(\Omega,\xoc,y\oftp A);\Delta\prv M\hastype B}
{\gofd\prv(\lamb{y^0}{A} M) \hastype A\ZImp B} {\ZImp I}$$
\btab
 $\GG;(\Omega,\xoc,y\oftp A);\Delta\prv M\hastype B$
\`  By inversion\\
 $(\GG,\xoc);(\Omega,y\oftp A);\Delta\prv M\hastype B$ 
\` By IH\\
$\gfod\prv(\lamb{y^0}{A} M) \hastype A\ZImp B$\` By rule
\etab

\itc $\cD$ ends in $\TImp I$ or $\RImp I$: the thesis follows from an 
immediate appeal to the inductive hypothesis.

\itc  $$\cD = \ibnc{\gofd \vd M \hastype  A \TImp B}
{(\GG,\Delta);(\Omega,\xoc);\cdot \vd N \hastype A}{\gofd \vd
M\ N^u \hastype  B}{\TImp E}$$
\btab
$\cD_1::\gofd \vd M \hastype  A \TImp $\bv
$\gfod\vd M \hastype A \TImp B$ \bi on $\cD_1$\\
$\cD_2:: (\GG,\Delta);(\Omega,\xoc);\cdot \vd N \hastype A$\bv
$(\GG,\D,\xoc);\Omega;\cdot\vd N \hastype A$\bi on $\cD_2$\\
$\gfod\vd M \ N^{u}\hastype B$\br
\etab

\itc  $$\cD = \ibnc{\gofd \vd M \hastype  A \ZImp B}
{(\GG,\Omega,\Delta,\xoc);\cdot;\cdot \vd N \hastype A}{\gofd \vd
M\ N^0\hastype  B}{\ZImp E}$$
\btab
$\cD_1::\gofd \vd M \hastype  A \TImp $\bv
$\gfod\vd M \hastype A \TImp B$ \bi on $\cD_1$\\
 $(\GG,\Omega,\D,\xoc);\cdot;\cdot\vd N 
\hastype A$\bv
$\gfod\vd M \ N^{0}\hastype B$\br
\etab

\itc $\cD =$ 
$$ \ibnc{(\GG,\Delta_{N});(\Omega,\xoc);\Delta_{M} 
\vd M \hastype A \RImp B}{(\GG,\Delta_M);(\Omega,\xoc);\Delta_{N}\vd N 
\hastype A}{\GG;(\Omega,\xoc);(\Delta_{N},\Delta_{M}) \vd
M\ N^1 \hastype  B}{\RImp E}$$
\btab
$\cD_1::(\GG,\Delta_{N});(\Omega,\xoc);\Delta_{M} 
\vd M \hastype A \RImp B$\bv
$(\GG,\xoc,\Delta_{N});\Omega;\Delta_{M} \vd M 
\hastype A \RImp B$\bi on $\cD_1$\\
$\cD_2::(\GG,\Delta_M);(\Omega,\xoc);\Delta_{N}\vd N 
\hastype A$\bv
$(\GG,\xoc,\Delta_M);\Omega;\Delta_{N}\vd N 
\hastype A$\bi on $\cD_2$\\ 
$(\GG,\xoc);\Omega;(\Delta_{N},\Delta_{M})\vd M \ 
N^{1}\hastype B$\br
\etab
\enit\end{proof}

\begin{Corollary}[Loosening$^{0}$]
\label{thm:0loose}
If $\Gamma; (\Omega,\Phi); \Delta\vd M \hastype A$ then $(\Gamma, 
\Phi); \Omega; \Delta\vd M \hastype A$. 
\end{Corollary}
\begin{proof}
By repeated application of Theorem \ref{thm:0loosex}.
\end{proof}

\newcommand{\godx}{\Gamma; \Omega; (\Delta,x\oftp C)}
\newcommand{\gdo}{(\GG,x\oftp C);\Omega;\Delta}

\begin{Theorem}
\label{thm:1loosex}

If $\Gamma; \Omega; (\Delta,x\oftp C)\vd M \hastype A$, then $\gdo\vd 
M \hastype A$.
\end{Theorem}

\begin{proof}
By  induction on the structure of $\cD ::\godx\vd M\hastype  A$.
\bit
\itc $\cD$ ends in  $Con,Id^{u}$: vacuously true.
\itc  $$\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}}$$

\itc $$\cD = \ianc{\GG;\Omega;(\Delta,x\oftp C,y\oftp A)\prv M\hastype B} 
{\godx\prv(\lamb{y^1}{A} M) \hastype A\RImp B} {\RImp I}$$
\btab
$\GG;\Omega;(\Delta,x\oftp C,y\oftp A)\prv M\hastype B$ \` By inversion  \\
 $(\GG,x\oftp C,);\Omega;(\D,y\oftp A) \prv M\hastype B$ \` By IH\\
$\gdo\prv(\lamb{y^1}{A} M) \hastype A\RImp B$ \` By rule
\etab

\itc $\cD$ ends in $\TImp I$ or $\ZImp I$: the thesis follow from an immediate appeal to the 
inductive hypothesis.

\itc $$\cD = \ibnc{\godx \vd M \hastype A \TImp 
B}{(\GG,\Delta,x\oftp C);\Omega;\cdot \vd N \hastype A}{\godx \vd
M\ N^u\hastype  B}{\TImp E}$$
\btab
$\godx \vd M \hastype A \TImp B$ \` By inversion \\
$\gdo\vd M \hastype A \TImp B$ \` By IH\\
$(\GG,\Delta,x\oftp C),\Omega;\cdot\vd N \hastype A$ \` By inversion \\
$\gdo\vd M \ N^{u}\hastype B$ \` By rule
\etab

\itc $$\cD = \ibnc{\godx \vd M \hastype A \ZImp 
B}{(\GG,\Omega,\Delta,x\oftp C);\cdot;\cdot \vd N \hastype A}{\godx \vd
M\ N^0\hastype  B}{\ZImp E}$$
\btab
$\godx \vd M \hastype A \ZImp 
B$ \` By inversion \\
$\gdo\vd M \hastype A \ZImp B$ \` By IH  \\
$(\GG,\Omega,\Delta,x\oftp C);\cdot;\cdot \vd N \hastype A$ \` By 
inversion\\
$\gdo\vd M \ N^{0}\hastype B$ \` By rule
\etab
\itc $\cD$ ends in $\RImp$. There are two subcases:
\bit
\item[ $x\in\D_{M}$]
$\cD$ =
$$ \ibnc{(\GG,\Delta_{N});\Omega;(\D'_M,x\oftp C) \vd M \hastype A \RImp B}
{(\GG,\D'_M,x\oftp C);\Omega;\Delta_{N} \vd N \hastype A}
{\GG;\Omega;(\D'_M,x\oftp C,\Delta_{N})\vd M\ N^1 \hastype  B}{\RImp E}$$
\btab
$(\GG,\Delta_{N});\Omega;(\D'_M,x\oftp C) \vd M \hastype A \RImp B$ 
\` By inversion\\
$(\GG,\Delta_{N},x\oftp C);\Omega;\D'_M \vd M \hastype A \RImp 
B$ \` By IH\\
$(\GG,\D'_M,x\oftp C);\Omega;\Delta_{N} \vd N \hastype A$ \`
By inversion \\
$(\GG,x\oftp C);\Omega;(\Delta_{N},\D'_M)\vd M \ 
N^{1}\hastype B$\br
\etab
\item[ $x\in\D_N$] Symmetrical to the above.
\enit\enit
\end{proof}

\begin{Corollary}[Loosening$^{1}$]
\label{thm:1loose}
If $\Gamma; \Omega; \Delta\vd M \hastype A$ then $(\GG,\D);\O;\cdot\vd M \hastype A$. 
\end{Corollary}
\begin{proof}
By repeated application of Theorem \ref{thm:1loosex}.
\end{proof}


\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,\D); \Omega;\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, \Delta,\Omega) ;\cdot;\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 mutual induction on the height of the 
derivation of $M\hastype C$.  We show the crucial steps.
\ben
\item
\mbox{}
\bit
\itc
$$\cD = \ianc{c\oftp C\in\Sigma}{ (\Gamma, x\oftp A);\Omega;\cdot\vd c \hastype C}{Con}$$
As $[N/x] c= c$, then 
$$\cF = \ianc{c\oftp C\in\Sigma}{\GG;\Omega;\cdot\vd c \hastype C}{Con}$$
\itc
$$\cD = \ianc{}{ (\Gamma, x\oftp A,y\oftp C);\Omega;\cdot\vd y \hastype C}
{Id^u}$$
As $[N/x] y= y$, then 
$$\cF = \ianc{}{(\GG,y\oftp C);\Omega;\cdot\vd y \hastype C}{Id^u}$$
\itc
$$\cD =  \ianc{}{(\Gamma, x\oftp A);\Omega;\cdot\vd x \hastype C}{Id^u}$$
As $[N/x] x= N$ and $C\equiv A$, then $\cF\equiv\cE::\GG;\Omega;\cdot\vd N \hastype C$
% $$\cF = \ianc{}{\GG;\Omega;\cdot\vd N \hastype C}{Id^u}$$
\itc
$$\cD = \ianc{}{ (\Gamma, x\oftp A);\Omega;y\oftp C\vd y \hastype C}{Id^1}$$
As $[N/x] y= y$, then 
$$\cF = \ianc{}{\GG;\Omega;y\oftp C\vd y \hastype C}{Id^1}$$
\itc
$\cD$ ends with an introduction rule: it follows by an immediate 
appeal to the IH.
\itc
$$
 \cD= \ibnc{\arv{\cD_1}{ (\GG, x\oftp A); \Omega; \Delta \vd P \hastype 
 B \UImp C}}
 {\arv{\cD_{2}}{ (\Gamma, \Delta, x\oftp A);
\Omega; \cdot \vd Q \hastype B}}{(\GG, x\oftp A); \Omega; \Delta
\vd P\ Q^u \hastype C}{\GImp{u}E}$$
\btab
$ (\GG, x\oftp A); \Omega; \Delta \vd P \hastype B \UImp C$ \` By inversion\\
$\cE :: (\GG,\D);\O;\cdot\vd N\hastype A$ \` By hypothesis\\
$\god\vd[N/x]P\hastype  B \UImp C$ \` By IH on $\cD_{1}$ and $\cE$\\
$ (\GG, x\oftp A,\Delta); \Omega;\cdot \vd Q\hastype B$ \` By inversion\\
%$(\GG,\D);\O;\cdot\vd N\hastype A$ \` By hypothesis\\
$(\GG,\D);\O;\cdot\vd[N/x]Q\hastype  B$ \` By IH on $\cD_2$ and $\cE$\\
$\GG; \Omega; \Delta\vd [N/x] (P\ Q^u) \hastype C$ \` By rule
\etab

\itc
$$\cD= \ibnc{\arv {\cD_1}{ (\GG, x\oftp A); \Omega; \Delta \vd P \hastype 
 B \ZImp C}}
 {\arv{\cD_2}{ (\Gamma, \Delta, \Omega,x\oftp A);
\cdot; \cdot \vd Q \hastype B}}{(\GG, x\oftp A); \Omega; \Delta
\vd P\ Q^0 \hastype C}{\GImp{0}E}$$
\btab
$ (\GG, x\oftp A); \Omega; \Delta \vd P \hastype B \ZImp C$ \` By inversion\\
$\cE :: (\GG,\D);\O;\cdot\vd N\hastype A$ \` By hypothesis\\
$\god\vd[N/x]P\hastype  B \ZImp C$ \` By IH on $\cD_{1}$ and $\cE$\\
$ (\GG, x\oftp A,\O,\Delta); \cdot;\cdot \vd Q \hastype B$ \` By inversion\\
%$(\GG,\D);\O;\cdot\vd N\hastype A$ \` By hypothesis\\
$\cE'::(\GG,\D,\O);\cdot;\cdot\vd N\hastype A$ \` By Loosening$^{0}\, \cE$ \\
$(\GG,\D,\O);\cdot;\cdot\vd[N/x]Q\hastype  B$ \` By IH on $\cD_2$ and $\cE'$\\
$\GG; \Omega; \Delta\vd [N/x] (P\ Q)^0 \hastype C$ \` By rule
\etab

\itc
$\cD= $
$$ \ibnc{\arv {\cD_1}{ (\GG, x\oftp A,\D_{Q}); \Omega; 
\Delta_{P} \vd M_1 \hastype B \RImp C}} {\arv{\cD_2}{ 
(\Gamma,x\oftp A,\D_{P});\Omega;\D_{Q} \vd M_2 \hastype B}} 
{(\GG, x\oftp A); \Omega; (\Delta_{P},\D_{Q})
\vd (M_1\ M_2)^1 \hastype C}{\GImp{1}E}$$
\btab
$(\GG, x\oftp A,\D_{Q}); \Omega; \Delta_{P} \vd M_1 \hastype 
B \RImp C$ \` By inversion\\
$\cE :: (\GG,\D_{P},\D_{Q});\O;\cdot\vd N\hastype A$
 \` By hypothesis\\
$(\GG,\D_{Q});\O;\D_{P}\vd[N/x]M_1\hastype  B \RImp C$
 \` By IH on $\cD_{1}$ and $\cE$\\
$  (\GG, x\oftp A,\D_{P}); \Omega; 
\Delta_{Q} \vd M_2 \hastype B $ \` By inversion\\
% $\cE' :: (\GG,\D_{P},\D_{Q});\O;\cdot\vd N\hastype A$
% \` By hypothesis\\
$(\GG,\D_{P};\O;\D_{Q}\vd[N/x]M_2\hastype  B$
 \` By IH on $\cD_{2}$ and $\cE$\\
$\GG; \Omega; (\Delta_{P},\D_{Q})\vd [N/x] (M_1\ M_2)^1 \hastype C$
 \` By rule
\etab
\enit
\item Similar to $1.$
\item
\mbox{}
\bit
\itc $\cD$ ends in   $Con,Id^{u}$: vacuously true.
\itc  
$$\cD = \ianc{}{(\GG,\D_N);\O;x\oftp A\vd x\hastype A}{Id^{1}}$$
and $[N/x]x  = N$;  then $\cF\equiv\cE::\GG;\O;\D_{N}\vd  N$.
% $${\cal F} = \ianc{}{\GG;\O;\D_{N}\vd  N}{Id^{1}}$$
\itc
 $$\cD= \ianc{(\GG,\D_N);(\O,y\oftp B);(\D_{M},x\oftp 
A)\vd Q\hastype C}{(\GG,\D_N);\O;(\D_{M},x\oftp A)\vd \lamb 
{x^{0}} {B} Q\hastype B\ZImp C}{\ZImp I}$$
\btab
$\cD_1::(\GG,\D_N);(\O,y\oftp B);(\D,x\oftp 
A)\vd Q\hastype C$\` By inversion\\
 $\cE::(\GG,\D);\O;(\D_{N},)\vd N\hastype A$ 
\` By hypothesis\\
$\cE'::(\GG,\D);(\O,y\oftp B);(\D_{N})\vd N\hastype A$
\`  by Weakening$^{0}$ on $\cE$\\
$\GG;(\O,y\oftp B);\dmn\vd [N/x] N\hastype C$
\` By IH on $\cD_1$ and $\cE'$\\
 $\GG;\O;\dmn\vd [N/x] (\lamb{y^{0}}{B} N)\hastype B\ZImp C$
\` By rule
\etab
\itc $\cD$ ends with $\TImp I$.  Proceed similarly  using 
Weakening$^{u}$.  
\itc $\cD$ ends with $\RImp I$. It  follows by an immediate appeal to the IH.
\itc
$$\cD=\ibnc{(\GG,\D_N);\O;(\D_M,x\oftp A)\vd P\hastype 
B\TImp C}
{(\GG,\D_M,x\oftp A,\D_N);\O;\cdot\vd Q\hastype B}
{\GG;(\O);(\D_M,x\oftp A,\D_N)\vd P\ Q^{u}}{\TImp E}$$
\btab
$ \cD_1::(\GG,\D_N);\O;(\D_M,x\oftp A)\vd P \hastype B \UImp C$ \` By inversion\\
$\cE :: (\GG,\D);\O;\D_N\vd N\hastype A$ \` By hypothesis\\
$\GG;\O;(\D_M,x\oftp A,,\D_{N})\vd[N/x]P\hastype  B \UImp C$ \` By IH on $\cD_{1}$ and $\cE$\\
$\cD_2::(\GG,\D_M,x\oftp A,\D_N);\O;\cdot\vd Q\hastype  B$ \` By inversion\\
%$(\GG,\D);\O;\cdot\vd N\hastype A$ \` By hypothesis\\
$(\GG,\D_M,\D_{N});\O;\cdot\vd[N/x]Q\hastype  B$ \` By IH on $\cD_2$ and $\cE$\\
$\GG; \Omega; (\Delta,\D_{N})\vd [N/x] (P\ Q)^u \hastype C$ \` By rule
\etab
\itc
$\cD$ ends in $\ZImp E$: similar.
\itc $\cD$ ends in $\RImp E$: there are two subcases:
\bit
\item[\textbf{$x\in \D_{M_1}$}]\mbox{}
$\cD=$
$$
 \ibnc{\arv {\cD_1}{ (\GG,\D_{N},\D_{Q}); \Omega; 
(\Delta'_{P}, x\oftp A) \vd M_1 \hastype B \RImp C}} {\arv{\cD_2}{ 
(\Gamma,\D_{N},x\oftp A,\D'_{P});\Omega;\D_{Q} \vd M_2 \hastype B} }
{\GG; \Omega; (\Delta'_{P}, x\oftp A,\D_{Q})\vd M_1\ M_2^1 \hastype C}{\GImp{1}E}$$
\btab
$(\GG,\D_{N},\D_{Q}); \Omega; 
(\Delta'_{P}, x\oftp A) \vd M_1 \hastype B \RImp C$ \` By 
inversion\\
$\cE::(\GG,\D_{Q});\O;(\Delta'_{P},\D_{N})\vd N\hastype A$ \` By 
hypothesis\\
$(\GG,\D_{N},\D_{Q}); \Omega; 
(\Delta'_{P}, x\oftp A) \vd [N/x] M_1 \hastype B \RImp C$ \` By 
HI on $\cD_{1}, \cE$\\
$(\Gamma,\D_{N},x\oftp A,\D'_{P});\Omega;\D_{Q} \vd M_2 \hastype B$ \` By 
inversion\\
% $(\Gamma,\D_{N},x\oftp A,\D'_{P},\D_{Q});\Omega;\cdot \vd M_2 \hastype B$ \` By 
% Loosening$^{1}$\\
% $\cE'::(\GG,\D_{Q});\O;(\Delta'_{P},\D_{N})\vd N\hastype A$ \` By 
% hypothesis\\
$(\GG,\D_{N},\Delta'_{P}); \Omega; 
(\Delta'_{Q}, x\oftp A) \vd [N/x] M_2 \hastype B$ \` By 
HI on $\cD_{1}, \cE$\\
$\GG;\O;(\Delta'_{P},\D_{Q},\D_{N})\vd[N/x] (P\ Q)^{1}\hastype 
C$
\` By rule.
\etab

\item[\textbf{$x\in \D_{M_2}$}] Symmetrical to the above.
\enit
\enit
\enen   % 123sub
\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/y][z/x]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/y][z/x]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/y][z/x]M \hastype C$.
\end{enumerate}
\end{Theorem}
\begin{proof}
\ben\mbox{}
\item
\btab
$(\Gamma, x\oftp A, y\oftp A);\Omega;\Delta \vd M\hastype C$
\` By assumption\\
$(\Gamma, x\oftp A,\D, z\oftp A);\Omega;\cdot \vd z\hastype A$
\` By rule\\
$(\Gamma, x\oftp A, z\oftp A);\Omega;\Delta \vd [z/x]M\hastype C$
\` By Substitution$^u$\\
$(\Gamma, \D, z\oftp A);\Omega;\cdot\vd z\hastype A$
\` By rule\\
$(\Gamma,  z\oftp A);\Omega;\Delta \vd[z/y] [z/x]M\hastype C$
\` By Substitution$^u$
\etab
\item
Similarly, using Substitution$^0$.
\item
Similarly, using Substitution$^1$.
\enen
\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} \]
 g
Indeed one of the main features of   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}$ 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}$  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}$  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}$  $(\Gamma,x\oftp A);\Omega; \Delta \vd M \hastype 
A\TImp B$.  Take the following instance of $Id^{u}$: $(\Gamma,x\oftp 
A,\Delta);\Omega;\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}$  $\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;\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$^{u}$ 
$(\Gamma,x\oftp A);\Omega; \Delta_{M})\vd M 
\hastype A\RImp B$.  Take the following instance of $Id^{1}$: 
$(\Gamma,\D_{M});\O;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}

The following lemma establish a sort of consistency property of the 
type system, in so far as a term can be typed only by exclusive 
contexts.  That will be central in the proof of disjointness of 
complementation (Theorem \ref{thm:part2}):

\begin{Lemma}[Exclusivity]
\label{le:disj}
It is not the case that both $\GG;\O;(\D,x\oftp C)\vd M\hastype 
A$ and $\GG;(\O,x\oftp C);\D\vd M\hastype A$.
\end{Lemma}
\begin{proof}
By  induction on the structure of $\cD::\GG;\O;(\D,x\oftp C)\vd M\hastype 
A$ and $\cD'::\GG;(\O,x\oftp C);\D\vd M\hastype A$.
\bit
\itc 
$$\cD'=\ianc{c\oftp C\in\Sigma}{\GG;(\O,x\oftp C);\cdot\vd c\hastype 
A}{Con}$$
but there can be no proof of $c\hastype A$ from $\GG;\O;x\oftp C$.
\itc 
$$\cD'=\ianc{}{(\GG,y\oftp A);(\O,x\oftp C);\cdot\vd y\hastype 
A}{Id^{u}}$$
but there can be no proof of $y\hastype A$ from $(\GG,y\oftp A);\O;x\oftp C$.
\itc 
$$\cD'=\ianc{}{\GG;(\O,x\oftp C);y\oftp C\vd y\hastype 
A}{Id^{1}}$$
but there can be no proof of $y\hastype C$ from $\GG;\O;(x\oftp C,y\oftp A)$.
\itc 
$$\cD=\ianc{}{\GG;\O;x\oftp A\vd x\hastype 
A}{Id^{1}}$$
but there can be no proof of $x\hastype A$ from $\GG;(\O,x\oftp 
A);\cdot$.
\itc
$$\cD= \ianc{\GG;\O;(\D,x\oftp C,y\oftp B)\vd M\hastype  A}
{\GG;\O;(\D,x\oftp C)\vd\lamb{y^{1}}{B} M\hastype B\RImp A}{\RImp I}$$
and
$$\cD'= \ianc{\GG;(\O,x\oftp C);(\D,y\oftp B)\vd M\hastype  A}
{\GG;(\O,x\oftp C);\D\vd\lamb{y^{1}}{B} M\hastype B\RImp A}{\RImp I}$$
\btab
$\GG;\O;(\D,x\oftp C,y\oftp B)\vd M\hastype  A$
\` By inversion on $\cD$\\
$\GG;(\O,x\oftp C);(\D,y\oftp B)\vd M\hastype  A$
\` By inversion  on $\cD'$\\
$\perp$ \` By IH\\
$\perp$ \` By rule
\etab
\itc
$\cD$ ends in $\TImp I,\ZImp I$. The result follows by IH.
\itc
$\cD$ ends in $\TImp E,\ZImp E$. The result follows by IH on the leftmost 
derivations.
\itc
$\cD$ ends in $\RImp E$: there are two subcases:
\bit
\item[\textbf{$x\in\D_{M}$}]\mbox{}
$\cD=$
$$ 
\ibnc{(\Gamma, \Delta_N); \Omega; (\Delta'_M,x\oftp C) \vd M \hastype A \RImp 
B}{(\Gamma, \Delta'_M,x\oftp C); \Omega; \Delta_N \vd N \hastype A}{\Gamma; 
\Omega; (\Delta'_M,x\oftp C, \Delta_N) \vd M\ N^1 \hastype B}{\GImp{1}E}
$$ 
and \\
$\cD'=$
$$ 
\ibnc{(\Gamma, \Delta_N); (\Omega,x\oftp C); \Delta'_M \vd M \hastype A \RImp 
B}{(\Gamma, \Delta'_M);( \Omega,x\oftp C); \Delta_N \vd N \hastype A}{\Gamma; 
(\Omega,x\oftp C); (\Delta'_M, \Delta_N) \vd M\ N^1 \hastype B}{\GImp{1}E}
$$
\btab
$(\Gamma, \Delta_N); \Omega; (\Delta'_M,x\oftp C) \vd M \hastype A \RImp 
B$
 \` By inversion on $\cD$\\
$(\Gamma, \Delta_N); (\Omega,x\oftp C); \Delta'_M \vd M \hastype A \RImp 
B$
\` By inversion  on $\cD'$\\
$\perp$ \` By IH\\
$\perp$ \` By rule
\etab
\item[\textbf{$x\in\D_{N}$}] Symmetrically.
\enit %subcase
\enit
\end{proof}

\begin{Corollary}
\label{co:disj}
\mbox{}\ben
\item
It is not the case that both $\GG;\O;(\D,x\oftp C)\vd M\hastype A$ and 
$(\GG,\O,\D);x\oftp C;\cdot\vd M\hastype A$.
\item
It is not the case that both $\GG;(\O,x\oftp C);\D\vd M\hastype A$ and 
$(\GG,\O,\D);\cdot;x\oftp C\vd M\hastype A$.
\enen
\end{Corollary}
\begin{proof}
By Loosening$^{1}$ and Loosening$^{0}$ on Lemma \ref{le:disj}.
\end{proof}

\newcommand{\er}[1]{\mid #1\mid_{\mbox{\textrm{er}}}}

We end this section by checking that our strict calculus is a 
conservative extension of the simply typed $\l$-calculus.  We 
therefore define a forgetful functor from $\lc$ to $\l^{\Imp}$:
\beq
\er{A\LImp B} & = & \er{A}\  \TImp\ \er{B}\\
\er{P} & = & P
\vsk
\er{x} & = & x\\
\er{c} & = & c\\
\er{\lamb{x^{k}}{A} M} & = & \lamb{x}{\er{A}} \er{M}\\
\er{M\ N^{k}} & = & \er{M}\ \er{N}
\vsk
\er{\cdot} & = & \cdot\\
\er{\GG,x\oftp A} & = & \er{\GG}, x\oftp \er{A}\\
\er{\Sigma,P\oftp type} & = & \er{\Sigma}, P\oftp type\\
\er{\Sigma,c\oftp A} & = & \er{\Sigma}, c\oftp \er{A}
\eneq

\begin{Theorem}[Conservativity]
\label{thm:conserv}
If $\god\vd_{\lc}M\hastype A$, then\\ 
$\er{\GG},\er{\O},\er{\D}\vd_{\l^{\Imp}} \er{M}\ \hastype\ \er{A}$.
\end{Theorem}
\begin{proof}
By induction on the structure of the given derivation.
\end{proof}

\subsection{Canonical forms for $\lc$}


We present the inductive definition of \emph(canonical) forms in 
$\lc$, \ie terms in $\be$-long normal form.  This is a generalization 
of canonicity for the simply-typed $\l$-calculus, as  described in 
\cite{Pfenning94un}.  It 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{c\oftp A\in\Sigma}{\GG; \Omega;\cdot  \prv  c\da A}{cIdc}\vsk
\ianc{}{(\GG,x\oftp A);\Omega; \cdot  \prv  x\da A}{cId^{u}}
\qquad \mbox{\textrm{no rule for }}cId^{0}
\qquad
\ianc{}{\GG;\Omega; x\oftp A \prv  x\da A} {cId^{1}}
\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}
\vsk
\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 existential
variables.
We write $ \Phi^{k}$ for $ x_{1}^{k}\dots 
x_{n}^{k}$, where $x_{1}\dots x_{n}\in dom(\Phi)$.  The notation 
$\pi(\Phi)$ stands for a permutation of $dom(\Phi)$.
\beq
%\ianc{\cdot;\cdot;\cdot\vd E_{A}\hastype A}
%{\god\vd E_{A}\ \pi(\GG^u);\pi(\O^0);\pi(\D^1) \hastype P}{Pat}
\ianc{\xnl= \GG^u,\O^0,\D^1}{\god\vd E_{A}\ \xnl) \hastype P}{Pat}
\qquad
\ianc{\god\vd E_{A}\ \xnl \hastype P}{\god \vd E_{A}\ \xnl \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{Towards Complementation}
\label{sec:strictcomp}


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

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


Unfortunately, while the first property follows quite easily from 
Corollary \ref{co:disj}, it turns out that the exhaustivity does not hold in 
general as we allow logic variables in partially applied terms. 
 However, our algorithm is sound and
complete for the fragment which results from the natural embedding of the
original simply-typed $\lambda$-calculus which is sufficient for all
applications we have presently considered (see Section
\ref{sec:concl}).

%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 can be established.
\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  the 
% following to hold:
% \[ \GG\vd M \in \|E\ z^{1}\|  \mbox{\textrm{ or }}  \GG\vd M \in \|\mmnot (E\ 
% z^{1})\|\]
% \ie
% \[ \GG\vd M \in \|E\ z^{1}\|  \mbox{\textrm{ or }}  \GG\vd M \in \|F\ 
% z^{0}\|\]

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


\begin{example}
\label{ex:excont}
 Continuing Example \ref{ex:lam}, we see
\[
\begin{array}{rcl}
\rep{\lambda x.\, \lambda y.\, x} = lam\ (\lamb{x}{exp} lam\ (\lamb{y}{exp} x))
\end{array}
\]
 so the argument to the first occurrence of\ $lam$ is a strict function,
while the argument to the second occurrence is an invariant function.
If we can give only one type to $lam$ is must therefore be
$(exp \GImp{u} exp) \GImp{1} exp$.
\end{example}

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

% But consider the following:
% \begin{example}
% \[
% \begin{array}{l}
% y\oftp ((a\Imp a)\Imp a)\Imp a, x\oftp a\vd y(\lamb{f}{a\Imp a} f\ 
% x) \\
% y\oftp ((a\Imp a)\Imp a)\Imp a, x\oftp a\vd y(\lamb{f}{a\Imp a} x)
% \end{array}
% \]
% Note that $y$ is well-typed but the above term does not satisfy exhaustivity. 
% \end{example}

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

% \smallskip
% We now formalize this an  embedding of the simply-typed $\l$-terms 
% into a fragment of strict terms. This is accomplished 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\\
% c^{+} & = & c\\
% (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\emp\vd y(\lamb{f^{u}}{a\RImp a} f\ 
% x^{1})^{1}\\
% \lefteqn{(y\oftp (a\Imp a)\Imp a, x\oftp a)^{+}\vd (y(\lamb{f}{a\Imp a} x))^{+}  = }\\
% & & y\oftp ((a\RImp a)\TImp a)\RImp a, x\oftp a\emp\vd y(\lamb{f^{u}}{a\RImp a} x)^{1}
% \eneq
% % \end{example}
\begin{example} Continuing Example
 \ref{ex:excont}
\beq
 (lam\ (\lamb{x}{exp} lam\ (\lamb{y}{exp} x)))^+& = & 
 lam\ (\lamb{x^u}{exp} lam\ (\lamb{y^u}{exp} x)^1)^1
\eneq
\end{example}

The image of the embedding of the canonical forms of the simply-typed 
$\lambda$-calculus gives rise to the following fragment, 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^{-}}\ x^u_{1}\dots x^u_{n}
\end{array} \]
We sometimes abridge $(\dots (h\ M_1)^{1} \dots M_n)^{1}$ in $h\ 
\Mns$. Note that by the restriction to long normal
forms such terms and applications of pattern variables must be of base type.
 Moreover, for every judgment $\cal J$ on simple terms,
 we will shorten  $\GG\emp\vd \cal J$ into $\GG\vd \cal J$.
\smallskip

To prove the correctness of the embedding, we will need the following:

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

\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 requires the usual inductive 
definition of canonical terms in the simply-typed $\l$-calculus,
which can be obtained via Theorem \ref{thm:conserv}.

\begin{Theorem}[Correctness of $()^{\pm}$]
\label{thm:embed}
\mbox{}
\ben
\item
If $\GG\vd M\bua A$ then $\ctx\vd M^{-}\bua A^{-}$. 
\item
If $\GG\vd M\da A$ then $\ctx\vd M^{+}\da A^{+}$. 
\enen
\end{Theorem}
\begin{proof}
By mutual induction on the proofs of $\cD::\GG\vd M\bua A$ and 
$\cD'::\GG\vd M\da A$.
\bit
\itc 
\[\cD'= \ianc{c\oftp A\in\Sigma}{\GG\vd c\da A}{atm\_var}\]
Since $c^{+}= c$ and $\Sigma^{+}(c) = A^{+}$ we conclude
$$\ianc{}{\ctx\vd c^{+}\da A^{+}}{cIdc}$$
\itc 
\[\cD'= \ianc{}{(\GG,x\oftp A)\vd x\da A}{atm\_var}\]
Since $x^{+}= x$ and $\GG^{+}(x) = A^{+}$ we conclude
$$\ianc{}{(\GG^{+},x\oftp A^{+})\emp\vd x^{+}\da A^{+}}{cId^{u}}$$
\itc
\[\cD'=\ibnc{\GG\vd M\da B\Imp A}{\GG\vd N\bua B}{\GG\vd M\ N \da 
A}{atm\_app}\]
\btab
$\GG\vd M\da B\Imp A$\bv
$\ctx\vd M^{+}\da (B\Imp A) ^{+}$\bi\\
$\ctx\vd M^{+}\da B^{-}\RImp A ^{+}$\` By the embedding\\
$\GG\vd N\bua B$\bv
 $\ctx\vd N^{-}\bua B^{-}$\bi\\
$\ctx\vd (M^{+}N^{-})^{1}\da A^{+}$\br\\
$\ctx\vd ((M\ N)^{+} )^{1}\da A^{+}$ \` By the embedding
\etab
\itc
\[\cD'=
\ianc{\GG\vd E_{A}\ \xn\hastype P}{\GG\vd E_{A}\ \xn\da 
P}{can\_Pat}\]
\btab
$\GG\vd E_{A}\ \xn\hastype P$\bv
$\ctx\vd F_{A^{-}}\ \ol{x^u_n}\hastype P$
\`   By Lemma \ref{le:aminus} \\
$\ctx\vd F_{A^{-}}\ \ol{x^u_n}\da P$ \br\\
$\ctx\vd (E_{A}\ \xn)^{+}\hastype P^{+}$\`  By the embedding
\etab
\itc
\[\cD=\ianc{\GG\vd M\da P}{\GG\vd M\bua P}{can\_atm}\] 
\btab
$\GG\vd M\da P$\bv
$\ctx\vd M^{+}\da P^{+}$\bi\\
$\ctx\vd M^{+}\bua P^{+}$\br\\
 $\ctx\vd M^{-}\bua P^{-}$\`   By the embedding
\etab
 \itc
\[\cD= \ianc{\GG,x\oftp A\vd M\bua B}{\GG\vd\lxa M\bua A\Imp 
B}{can\_lam}\] 
\btab
$\GG,x\oftp A\vd M\bua B$\bv
$(\GG^{+},x\oftp A^{+})\emp\vd M^{-}\bua B^{-}$\bi\\
$\ctx\vd\lamb{x^{u}}{A^+} M \bua A^{+}\TImp B^{-}$ \br\\
$\ctx\vd (\lxa M)^{-}\bua (A \Imp B)^{-}$\` By the embedding
\etab
\enit\end{proof}

From now on we drop the $()^{\pm}$ embedding annotations from terms, 
types and contexts. We may also hide the $()^1$ decoration
from strict application of constants in examples.

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

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

\begin{Lemma}[Tightening]
\label{le:exh} 
Let $M$ be a simple pattern  without existential variables such that $\cu\vd M\buda A$. Then:
\ben
\item
 $\cxtr\vd M\da A$ or $\cxto\vd M\da A$.
\item
 $\cxtr\vd M\bua A$ or $\cxto\vd M\bua A$.
\enen
\end{Lemma}
\begin{proof}
By mutual induction on $\cD_{1}::\cu\vd M\da A$ and 
$\cD_{2}::\cu\vd M\bua A$.
\bit
\itc 
$$\cD = \ianc{c\oftp A\in\Sigma}{(\GG,x\oftp C);\O;\cdot \prv  c\da A}{cIdc}$$
Then
$$\cE= \ianc{c\oftp A\in\Sigma}{\GG;(\O,x\oftp C);\cdot \prv  c\da A}{cIdc}$$
and by weakening the thesis.
\itc
$$\cD = \ianc{}{(\GG,x\oftp C,y\oftp A);\O; \cdot  \prv  y\da 
A}{cId^{u}}$$
Then 
$$\cE = \ianc{}{(\GG,y\oftp A);(\O,x\oftp C); \cdot  \prv  y\da 
A}{cId^{u}}$$
and by weakening the thesis.
\itc
$$\cD = \ianc{}{(\GG,x\oftp C);\O;\cdot \prv  x\da C}{cId^{u}}$$
Then
$$\cE= \ianc{}{\GG;\O;x\oftp C \prv  x\da C}{cId^{1}}$$
and by weakening the thesis.
\itc 
$$\cD= \ianc{}{(\GG,x\oftp C);\O;y\oftp A\vd y\da A}{Id^{1}}$$
Then $$\cE= \ianc{}{\GG;(\O,x\oftp C);y\oftp A\vd y\da A}{Id^{1}}$$
and by weakening the thesis.
% \itc
% $$\cD=
% \ianc{\cu\vd E_{A}\ \xnl \hastype P}{\cu \vd E_{A}\ \xnl \da  
% P}{cPat}$$
% \btab
% $\cu\vd E_{A}\ \xnl \hastype P$\bv
% $\cdot;\cdot;\cdot\vd E_{A}\hastype A$\bv
% $\cxto\vd E_{A}\ \xnl \hastype P$\br\\
% $\cxto\vd E_{A}\ \xnl \da P$\br\\
% hence by weakening the thesis.
% \etab
 
\itc
$$\cD = \ianc{\cu\prv  M\da P}{\cu \prv  M\bua P} {cAt}$$
\btab
$\cu\prv  M\da P$ \` By inversion\\ 
$\cxtr \prv  M\da P$  \` By the left horn of the IH\\
$\cxtr \prv  M\bua P$ \` By rule $cAt$\\
$\cxtr \prv  M\bua P$ or $\cxto \prv  M\bua P$ \` By weakening\\
$\cxto \prv  M\da P$ \`  By the right horn of the IH \\
$\cxto \prv  M\bua P$ \` By rule $cAt$\\
$\cxtr \prv  M\bua P$ or $\cxto \prv  M\bua P$ \` By weakening
\etab
\itc
$$\cD = \ianc{(\GG,x\oftp C,y\oftp A);\Omega;\Delta \prv M\bua B}{\cu\prv(\lamb{y^u}{A} M) \bua 
A\TImp B} {c\TImp I}$$
\btab
$(\GG,x\oftp C,y\oftp A);\Omega;\Delta \prv M\bua B$ \` By inversion\\
$(\GG,y\oftp A);\Omega;(\Delta,x\oftp C)\vd M\bua $ \` By the left horn of the IH\\
$\cxtr\prv(\lamb{y^u}{A} M) \bua A\TImp B$ \` By rule $c\TImp I$\\
$\cxtr\prv(\lamb{y^u}{A} M) \bua A\TImp B$ or $\cxto\prv(\lamb{y^u}{A} M) 
\bua A\TImp B$\\
 \` By weakening\\
$(\GG,y\oftp A);(\O,x\oftp C);\Delta\vd M\bua $ \` By the right horn of the IH\\
$\cxtr\prv(\lamb{y^u}{A} M) \bua A\TImp B$ or $\cxto\prv(\lamb{y^u}{A} M) 
\bua A\TImp B$\\
 \` Similarly
\etab

\itc
 $$\cD = \ibnc{(\GG,x\oftp C,\D_N);\O;\D_M \vd M \da A \RImp 
B}{(\GG,x\oftp C,\D_M);\O;\D_N \vd N \bua A}{(\GG,x\oftp C);\O;\dmn 
\vd M\ N^1 \da B}{c\RImp E}$$
There are four  sub-cases, stemming from the IH:
\ben
\item
\btab
$(\GG,\D_N);\O;(\D_M,x\oftp C)\vd M\da A\RImp B$
\` By  IH\\
$(\GG\D_{M});\O;(x\oftp C,\D_N)\vd N\bua A$
\` By  IH\\
$(\GG,\D_M,x\oftp C);\O;\D_N\vd N\bua A$ 
\` By Loosening$^{1}$\\
$\GG;\O;(\D_M,x\oftp C,\D_N)\vd M\ N^{1}\da B$
\` By rule\\
 hence  by weakening the thesis.
 \etab

\item 
\btab
$(\GG,\D_N);(\O,x\oftp C);\D_M\vd M\da A\RImp B$ \` By  IH\\
$(\GG,\D_M);(\O,x\oftp C);\D_N\vd N\bua A$ \` By IH\\
$\GG;(\O,x\oftp C);\dmn\vd M\ N^{1}\da B$ \` By rule\\
 hence  by weakening the thesis.
\etab
\item
\btab
$(\GG,\D_N);\O;(\D_M,x\oftp C)\vd M\da A\RImp B$
\` By IH\\
$(\GG,\D_M);(\O,x\oftp C);\D_N\vd N\bua A$ 
\` By IH\\
$(\GG,x\oftp C);\O;(\D_M\vd N\bua A$ 
\` By Loosening$^{0}$\\
$\GG;\O;(\D_M,x\oftp C,\D_N)\vd M\ N^{1}\da B$
\` By rule\\
hence  by weakening the thesis.
\etab
\item Symmetrical to $3.$
%
\enen
\enit
\end{proof}

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


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

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

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


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


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

We have now arrived to the following language, where the labeling 
on flexible 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;(\O,\xoc);\D}
\newcommand{\cgmom}{ \GG;\Omega;\D}

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

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

\itc $$\cD = \ianc{}{\GG ;(\O,\xoc); y\oftp A  \prv  y \da 
A}{cId^{1}}$$

Then
$$\cE = \ianc{}{\GG; \O;y\oftp A  \prv  y\da A}{cId^{1}}$$

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


\subsubsection{Ground Instances}

We recall that we assume every type to be inhabited, so that every 
term can be seen as the intensional representation of the set of its 
ground instances.  The judgment in Fig.\  \ref{fig:grinst} $\GG 
\prv M\in\| N\|\hastype A $ formalizes conditions for  a simple term $M$ to be a 
ground instance of $N$ at type $A$.  
\begin{Remark}
\label{rmrk:gr}
 $\GG \prv M \in\| 
E_A\ \xnl\|\hastype P$ iff $M\equiv t \ \xnl$ and $\cdot\prv t 
\hastype A$, that is $t\equiv \l \xnl\,.\,S$ and if $\xnl = 
(\GG^{u},\O^{0},\D^{1})$ then $\god\vd S \hastype P$.  
\end{Remark}
This fact will be 
heavily used in the following. Moreover we write $\GG\prv M \not\in \| N \|\hastype A$,
 when it is not the case that $\GG\prv M \in \| N \|\hastype A$.

\begin{figure}
\label{fig:grinst}
\[
\begin{array}{c}
\ianc{M\equiv t \ \xnl  \quad \cdot\prv  t \hastype A}
{\GG \prv   M  \in\| E_A\ \xnl\|\hastype P}{grFlx} 
\vsk
\ianc{(\GG,x\oftp A);\Omega;\Delta\prv   M  \in\| N\|\hastype B}
{\GG \prv  \lxua M  \in\|\lxua N \|:A\TImp B}{grLam}
\vsk
% \ianc{\GG \prv h \oftp  A_1\RImp\mdots\RImp A_n \RImp P\quad \GG \prv  \ M_1 \in\| 
% N_{1}\|\hastype A_1\cdots \GG \prv  M_n \in\| N_n\|\hastype A_n }
%  {\GG \prv  h\ \Mns \in\|h\ \Nns
% \|\hastype P} {grApp}
\ianc{\GG \prv h \oftp  A_1\RImp\mdots\RImp A_n \RImp P\quad \GG \prv  \ M_i \in\| 
N_{i}\|\hastype A_i\quad 1\leq i\leq n}
 {\GG \prv  h\ \Mns \in\|h\ \Nns
\|\hastype P} {grApp}
\vsk
\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}} 
\end{array}
\]
\caption{$M$ is a ground instance of $N$ at type $A$}
\end{figure}


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

We implicitly use the above lemma to  weaken different 
contexts with common basis to an unique one.

\smallskip Now we can prove the set-theoretic adequacy of the full 
application translation.

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


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

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

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

% 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 three-valued logic, in the 
sense of the following table: 
\beq 
\mnot(1)& = &0\\
\mnot(0)& = &1\\
\mnot(u) & = & u
\eneq
Note that these labels form a three-valued semi-lattice with 
the (reverse) partial 
information ordering $1\leq u,0 \leq u$. 

% Finally we present the system for pattern complement.  Since we 
% restrict to  simple terms, we need only one context, the 
% undetermined one.  Hence we abridge $\GG\vd\mnot(M)=N$ in 
% $\GG\vd\mnot(M)=N$. However, keep in mind that every token is in the 
% image of the $\_^{\pm}$ translation.


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

Fix a signature $\Sigma$.  For a linear simple term  
$M$ such that $\GG \prv  M \hastype  A$ define $\GG\prv  \mnot(M) \blip  N\hastype A$
by the following rules.  Note that a given $M$ may be related to several
terms $N$ all of which belong to the complement of $M$.

\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}}) \blip  Z\ x_{1}^{u}\dots 
x_{i-1}^{u}\ x_{i}^{\mnot(k)}\ x_{i+1}^{u}\dots x_n^{u}\hastype P} {\mnot\_Flx}
\vsk
\mbox{\textrm{no rule for } $k=u$}
\vsk
\ianc{\GG,x\oftp A\prv  \mnot( M)  \blip   N\hastype B}
{\GG\prv  \mnot(\lxua M)  \blip  \lxua N\hastype A\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) \blip  
(\dots (g\ (Z_{1} \GG^{u}))^{1}\dots (Z_{m}\GG^{u}))^{1}\hastype P} {\mnot\_App^{1}}
\vsk
\ianc{  \GG\prv \mnot( M_i) \blip  N\hastype A_i\qquad 1\leq i\leq n } 
{\GG\prv  \mnot (h\ \Mn^1) \blip  
(\dots (h\ (Z_{1}\GG^{u} ))^{1}\dots (Z_{i-1}\GG^{u} )^{1} \ N^{1}\ 
(Z_{i+1}\GG^{u} )^{1}\dots (Z_{n}\GG^{u}))^{1}\hastype P} {\mnot\_App^{2}}
\end{array}
\]
\end{small}

\noindent where the $Z$'s are fresh logic variables and 
$h\in\Sigma\cup\GG$ and $\GG\prv h\hastype A_{1}\RImp\dots\RImp 
A_{n}\RImp P$. Finally we define $\GG\vd\mmnot(M)= \cN\hastype A$ if 
$\cN=\{N\mid\GG\prv \mnot(M)\blip N\hastype A\}$.
\end{Definition}

 We may drop the type
 %and signature 
information from the above judgment in examples and proofs.

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


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

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


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

\begin{example} Take the signature of numerals:
\beq
\lefteqn{\mmnot(\l x^{u}\l y^{u}.\, s(M\ x^{1} y^{0})^{1}   =}\\
& \{ \l x^u\l y^u .\, x, \l x^u\l y^u .\, y, \l x^u\l y^u .\, 0, \l 
x^u\l y^u .\, s(N\ x^{0} y^{u})^{1}, \l x^u\l y^u .\, s(N'\ x^{u} 
y^{1})^{1} \} 
\eneq
\end{example}

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

% We can now revisit Example \ref{ex:etardx}:
% \beq
% \lefteqn{\mmnot(lam(\lamb{x^{u}}{exp} app\ (M\ x^{0}) x^{1} ))\blip }\\
% & & \{ lam(\lamb{x^u}{exp} app\ (H\ x^1)\ H,
% \{ lam(\lamb{x^u}{exp} app\ (H\ x^u)\ (app\ H_4\ H_5)), \\
% lam(\lamb{x^u}{exp} app\ (H\ x^u)\ ( lam(\lamb{y^u}{exp} H_6\ x^u\ y^u)),
% & & app\ H_1\ H_2,\\
%  & &lam(\lamb{x^u}{exp} lam(\lamb{y^u}{exp} H_3\ x^u\ y^u) )\}
% \eneq
\smallskip

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

\begin{Theorem}
If $M$ is a simple term and $\GG\vd\mnot(M)\blip  N\hastype A$, then  $N$ is simple.
\end{Theorem}
\begin{proof}
By induction on the structure of $\cD::\GG\vd\mnot(M)\blip  N\hastype A$.
\bit
\itc
 $\cD$ ends in $\mnot\_Flx$: immediate.
% $M\equiv E\ \ol{x_{n}^{l}}$. Then for $1\leq i\leq n$ and for 
% $k\in\{1,0\}$ 
% $\GG\prv \mnot(E \ x_{1}^{l_{1}}\dots x_{i-1}^{l_{i-1}} \ 
% x_{i}^{k}\ x_{i+1}^{l_{i+1}}\dots x_n^{l_{n}}) \blip  Z\ x_{1}^{u}\dots 
% x_{i-1}^{u}\ x_{i}^{\mnot(k)}\ x_{i+1}^{u}\dots x_n^{u}\hastype P$ by rule , where the latter is simple.
\itc
$$\cD=\ianc{\GG,x\oftp A\prv  \mnot( M)  \blip   N\hastype B}
{\GG\prv  \mnot(\lxua M)  \blip  \lxua N\hastype A\Imp B}{\mnot\_Lam}$$
By inversion $\GG,x\oftp A\prv  \mnot( M)  \blip   N\hastype B$, hence by IH $N$ 
is simple and so is $\lxua N$.
\itc
$$\cD=\ianc{g\in\Sigma\cup\GG, g \hastype A_{1}\RImp\dots\RImp A_{m}\RImp 
P\quad m\geq 0,h \not\equiv g   } 
{\GG\prv  \mnot (h\ \Mn^1) \blip  
(\dots (g\ (Z_{1} \GG^{u}))^{1}\dots (Z_{m}\GG^{u}))^{1}\hastype 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}$.
\itc
$\cD=$
 \begin{small}
$$\ianc{ 
% h\in\Sigma\cup\GG,\GG\prv h\hastype A_{1}\RImp\dots\RImp 
% A_{n}\RImp P\qquad \mbox{\textrm{for some} $i$} \quad 
\GG\prv \mnot( M_i) \blip  N\hastype A_i \qquad 1\leq i\leq n} 
{\GG\prv  \mnot (h\ \Mn^1) \blip  
(\dots (h\ (Z_{1}\GG^{u} ))^{1}\dots (Z_{i-1}\GG^{u} )^{1} \ N^{1}\ 
(Z_{i+1}\GG^{u} )^{1}\dots (Z_{n}\GG^{u}))^{1}\hastype 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_{n}\GG^{u}))^{1}$ is simple.
\enit\end{proof}

\begin{Corollary}
If $M$ is a simple term, so is $N$, for all $N\in\GG\vd\mmnot(M)\hastype A$.
\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 the algorithm
is syntax-directed and only finitely branching.   
We abridge $\mnot(l)$ in $-l$. We start with soundness:

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

\begin{proof}
By induction on the structure of $\cD::\GG\vd \mnot(N)\blip Q$.
\bit
\itc $\cD$ ends in $\mnot\_Flx$.
First observe that $E\ \ol{x_{n}^{l}}$ can be seen as $E\ 
\Phi^{u}\Omega^{0}\Delta^{1}\ x^{d}$, where $x$ is determined; 
indeed if $x$ is undetermined, the result holds trivially.  Assume 
$\GG\vd M\in \|E\ \Phi^{u}\Omega ^{0}\Delta ^{1}\ x^{d}\|$ and 
$\GG \vd M\in\|F\ \Phi^{u}\Omega ^{u}\Delta ^{u}\ x^{-d}\|$ for 
some $d\in\{1,0\}$.  Then it holds that both $\Phi;\O;(\D,x\oftp 
A)\vd M\hastype C$ and $(\Phi,\O,\D);x\oftp A;\cdot\vd M\hastype 
C$ or $\GG;(\O,x\oftp A);\D\vd M\hastype C$ and 
$(\GG,\O,\D);\cdot;x\oftp A\vd M\hastype C$, depending on the 
polarity of $d$.  Both cases are impossible by Corollary 
\ref{co:disj}.
 
\itc  $\cD$ ends in $\mnot\_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$.  

\itc $\cD$ ends in $\mnot\_App^{2}$.
\btab
$\GG\prv  \mnot (h\ \Mn^1) \blip  
(\dots (h\ (Z_{1}\GG^{u} ))^{1}\dots (Z_{i-1}\GG^{u} )^{1} \ N^{1}\ 
(Z_{i+1}\GG^{u} )^{1}\dots (Z_{n}\GG^{u}))^{1}$\\ \bh
$\GG\vd\mnot(N_i)\blip  Q$,  for $1\leq i\leq n$ \`    By inversion  \\
$\GG\vd h\ \ol{M_n^{1}}\in \|h\ \ol{N_n^{1}}\|$  \` By assumption\\
$\GG \prv h\ \ol{M_n^{1}}\in \| h\ (Z_{1}\GG^{u} )^{1}\dots 
(Z_{i-1}\GG^{u} )^{1}\ Q^{1}\ (Z_{i+1}\GG^{u} )^{1}\dots (Z_{n}\GG^{u} 
)^{1} \|$\\ \` By assumption\\
$\GG \prv M_{i}\in\|N_{i} \|$\`    By inversion \\
$\GG \prv M_{i}\in\|Q \|$\bv
$\perp$\` By IH\\
$\perp$\` By rule
\etab
\itc $\cD$ ends in $\mnot\_Lam$:
\btab
$\GG\vd \mnot( \lxua N) \blip  \lxua Q$\bh
 $\GG,x\oftp A\vd \mnot( N) \blip  Q$\bv
$\GG \prv \lxua M\in \| \lxua N\|$ 
\` By hypothesis\\
 $\GG \prv \lxua M\in \| \lxua Q\|$
\` By assumption\\
$\GG,x\oftp A \vd M\in \| N\|$\`  By inversion \\
$\GG,x\oftp A \prv M\in \| Q\|$,\`  By inversion \\
$\perp$\` By IH\\
$\perp$\` By rule
\etab
\end{itemize}
\end{proof}

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

We are now ready to prove exhaustivity of complementation.

\begin{Theorem}
\label{thm:part2}
Assume $\GG\vd N\hastype A$ is  simple linear pattern and there is a $Q$ 
such that $\GG\vd \mnot(N)\blip Q\hastype A$: then,  either $\GG \prv M\in 
\| N \| \hastype A$ or  $ \GG \prv M\in \| Q\| \hastype A$.
\end{Theorem}
\begin{proof}
By induction on the structure of $\cD::\GG\vd \mnot(N)\blip Q\hastype A$ 
\bit

\itc 

$\cD$ ends in $\mnot\_Flx$.  Again observe that $E\ \ol{x_{n}^{l}}$ can 
be seen as $E\ \Phi^{u}\Omega^{0}\Delta^{1}\ x^{d}$, where 
$x$ is determined; indeed if $x$ is undetermined, the result holds 
trivially; by Corollary \ref{co:exh} either $GG;(\O,x\oftp C);\D\vd M\hastype A$ 
or $(\GG,\O,\D);\cdot;x\oftp C;\vd M\hastype A$ and either 
$\GG;\O;(\D,x\oftp C\vd M\hastype A$ 
or $(\GG,\O,\D);\cdot;x\oftp C \vd M\hastype A$, depending on the 
polarity of $d$.  Thus 
$\GG\vd M\in \|E\ \Phi^{u}\Omega ^{0}\Delta ^{1}\ x^{d}\|$ or $\GG 
\vd M\in\|F\ \Phi^{u}\Omega ^{u}\Delta ^{u}\ x^{-d}\|$ for some 
$d\in\{1,0\}$.
\itc $\cD$ ends in $\mnot\_App^{1}$.
let $M$ be a ground term $g\ \Mm$ where 
$g\in\Sigma\cup\GG, g\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}\| $,
 hence the thesis by weakening.
\itc$\cD$ ends in $\mnot\_App^{2}$.
\btab
$\GG\vd\mnot(N_{i}) \blip  Q$ for $1\leq i\leq n$ \bv
$\GG\vd h\ \ol{N_n^{1}}\hastype P$ \` By assumption\\
$\GG\vd N_{i}\hastype A_{i}$\`  By inversion \\
$\GG \prv M_{i}\in \| N_{i} \| \hastype A_{i}$\`  By the left horn of IH \\
$\GG \prv h\ \ol{M_n^1}\in \| h\ 
\ol{N_n^1} \| \hastype P$\`  by rule $grApp$ \\
%$\GG \prv h\ \ol{M_n^1}\in \| h\ \ol{N_n^1} \| \hastype P$ or \\
% $\GG \prv h\ \ol{M_n^1}\in \| h\ 
% (Z_{1}\GG^{u} )^{1}\dots (Z_{i-1}\GG^{u} )^{1}\ Q^{1}\ 
% (Z_{i+1}\GG^{u} )^{1}\dots (Z_{n}\GG^{u} )^{1} \| \hastype P$\\
% \`  by 
hence the thesis by weakening \\ $ \GG \prv M_{i}\in \| Q\| \hastype
 A$ \` By the right horn of IH\\ $\GG\vd M_{j}\in\|(Z_{j}\GG^{u}
 )^{1}\|$ for $j\neq i, 1\leq j\leq n$\` By rule $grFlx$\\ $\GG \prv
 h\ \ol{M_n^1}\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$\\ \` by rule $grApp$ \\ hence, by weakening the result.
 \etab

\itc $\cD$ ends in $\mnot\_Lam$.  \btab
% $\GG\vd\lxua N\hastype A\TImp B$\` By assumption\\
%  $\GG, x\oftp A\prv N\hastype B$\`  by inversion\\
$\GG,x\oftp A\vd\mnot(N)\blip Q$\bv $\GG,x\oftp A \prv M\in \| N \|
\hastype B$\` By the left horn of IH\\ $\GG \prv \lxua M\in \|\lxua N
\| \hastype A\TImp B$ \` by rule $grLam$ \\
%  $\GG \prv \lxua M\in \|\lxua N \| \hastype 
% A\TImp B$ or there is a $\lxua Q$ such that $\GG\vd\mnot(\lxua N) \blip  
% \lxua Q$ and $ \GG \prv \lxua M\in \|\lxua Q\| \hastype A\TImp B$\` 
hence the thesis by weakening\\ $ \GG \prv M\in \| Q\| \hastype B$\`
By right horn of IH\\ $ \GG \prv \lxua M\in \| \lxua Q\| \hastype
A\TImp B$\` by rule\\
%  $\GG \prv \lxua M\in \|\lxua N 
% \| \hastype A\TImp B$ or there is a $\lxua Q$ such that 
% $\GG\vd\mnot(\lxua N) \blip  \lxua Q$ and $ \GG \prv \lxua M\in \|\lxua 
% Q\| \hastype A\TImp B$\` 
hence the thesis by weakening.  \etab \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 (Disjointness) It is not the case that $\GG\prv M\in \| N
\|\hastype A$ and $\GG\prv M\in \| \mmnot(N) \|\hastype A$.
\item (Exhaustivity) $\GG\prv M\in \| N \| \hastype A$ or $\GG\prv
M\in \| \mmnot(N) \|\hastype A$.  \enen
\end{Corollary}
\begin{proof}
Disjointness is entailed by Theorem \ref{thm:part1},
% and the canonical form Theorem (Theorem \ref{thm:canonical}),
exhaustivity by Theorem \ref{thm:part2}.
\end{proof}


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

We now address the issue of unification, \ie intersection of simple
linear \ho patterns.  We start by determining when two labeling are
compatible: \beq 1 \cap 1 = u \cap 1 = 1\cap u = 1\\ 0 \cap 0 = u \cap
0 = 0\cap u = 0\\ u\cap u = u \eneq
%  we define an intersection operator on occurrence labels as 
% the symmetric and idempotent extension of the following partial 
% operation: 

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

We use $\Phi$ for (contexts) of labeled bound variables, \ie what we
call $\xnl$ and if $x^k\in\Phi$, we say that $\Phi(x)= k$.  We then
extend the intersection operations to these contexts; remember that
full application entails that we only intersect context that are the
same modulo different labeling: \beq \cdot\mcap \cdot & = & \cdot\\
(x^k\ \Phi)\mcap (x^{k'}\ \Phi') & = & x^{k\mcap k'}\ (\Phi\mcap
\Phi') \quad\mbox{\textrm{if $k\mcap k'$ is defined.}}  \eneq

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

Thus if $\Phi_{1}\cap\Phi_{2}$ is defined and $\Phi_{1} = \godf$ and
$\Phi_{2} = \gods$, we call the latter type assignments
\emph{compatible}.

\begin{Remark}
\label{rmrk:compa}
 $\Psi\vd M\in \|E_{A}\ \Phi_{1}\cap\Phi_{2}\|$ iff $M\equiv \l
\Phi_{1}\cap\Phi_{2}\,.\,S$ such that $\god\vd S\hastype A$, where
\beq \GG & = & (\GG_{1}\cap\GG_{2})\\ \O &= &(\O_{1},\O_{2})\\ \D & =
& (\D_{1},\D_{2}) \eneq Indeed, $x\in\GG$ iff $x\in\GG_{1}$ and $x\in
\GG_2$; moreover $x\in\O$ iff either $x\in\O_1\cup\GG_{2}$ or
$x\in\O_2\cup\GG_{1}$.  Analogously for $x\in\D$.
\end{Remark}

\begin{Lemma}
\label{le:compat}
Let $\GG_1\cup\D_1=\GG_2\cup\D_2$. Then
$(\GG_1\cup\D_1)\cap(\GG_2\cup\D_2)= (\GG_1\cap\GG_2)\cup\D_1\cup\D_2 $.
\end{Lemma}
\begin{proof}
\begin{metanote} A miracle \end{metanote}
\end{proof}

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


\begin{Definition}[Higher-Order Pattern Intersection]
Fix a signature $\Sigma$. For simple linear terms $M$ and $N$ without
 shared variables such that $\GG \prv M \hastype A$ and $\GG \prv N
 \hastype A$, define $\GG\prv M \mcap N \blip Q \hastype A$ by the
 following rules:


\begin{small}
\[
\begin{array}{c}
\ianc{
% \Phi_1\mcap \Phi_2 = \Phi%\quad \Phi\not = nil
 }
{\GG\prv  E \ \Phi_1\mcap   F\ \Phi_2\blip  H\ (\Phi_{1}\mcap \Phi_{2}) \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}\blip N_{1}\hastype A_{1}\cdots \GG\prv  H_n \ \Phi_{n}\mcap 
M_{n}\blip N_{n}\hastype A_{n}  } 
{ \GG\prv  E \ \Phi \mcap c\ \Mns\blip  c\ \Nns\hastype  P} {\mcap\_FlxRgd^c }
\vsk
\ianc{y\in\GG\quad  \quad \GG\prv  H_1 \ \Phi_{1}\mcap 
M_{1}\blip N_{1}\hastype A_{1}\cdots \GG\prv  H_n \ \Phi_{n}\mcap 
M_{n}\blip N_{n}\hastype A_{n} } 
{\GG\prv E\ \Phi \mcap y\ \Mns\blip  y\ \Nns \hastype  P} {\mcap\_FlxRgd^y }
\vsk
\ianc{ h\in\GG\cup\Sigma\quad \GG\prv  M_1 \mcap N_{1} \blip  Q_1\hastype  A_1 \cdots \GG\prv  M_n \mcap 
N_{n}\blip  Q_n \hastype  A_n} 
{\GG\prv   h\ \Mns\mcap h\ \Nns \blip  h\ \ol{Q_{n}^{1}} \hastype  P} {\mcap\_App}
\vsk
\ianc{\GG,x\oftp A\prv   M  \mcap  N \blip  Q\hastype  B}
{\GG\prv   \lxua M  \mcap \lxua N \blip \lxua Q \hastype  A\Imp B}{\mcap\_Lam}
\end{array}
\]
\end{small}
where  the $H$'s are fresh 
variables of correct typing and $n\geq 0$. 
 % The rule 
% $\mcap\_FlxRgd^c $ has the following proviso: for all $x\in \Phi$ and
% $1\leq i\leq n$
% \beq
% \forall x. \Phi(x) = 0 & \Imp & \forall i\,.\, \Phi_{i}(x) = 0\\ 
% \forall x. \Phi(x) = u & \Imp & \forall i\,.\, \Phi_{i}(x) = u\\ 
% \forall x. \Phi(x) = 1 & \Imp & \exists i\,.\, \Phi_{i}(x) = 1
% %\And \forall j, j\not = i. \Phi_{j}(x)\not = u
% \eneq
% The rule 
% $\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 
% \beq
% M\mbigcap N \hastype A & =& \{Q\mid\cdot\prv  M\mcap N = Q \hastype  A\}
% \eneq
The rules
$\mcap\_FlxRgd^c$ and $\mcap\_RgdFlx^c$ have the following proviso: for all
$x\in \Phi$ and $1\leq i\leq n$:
\beq
\forall x. \Phi(x) = 0  \Imp  \forall i\,.\, \Phi_{i}(x) = 0\\ 
\forall x. \Phi(x) = u  \Imp  \forall i\,.\, \Phi_{i}(x) = u\\ 
\forall x. \Phi(x) = 1  \Imp  \exists i\,.\, \Phi_{i}(x) = 1
\And \forall j, j\not = i. \Phi_{j}(x) = u
\eneq
The rules $\mcap\_FlxRgd^y$ and $\mcap\_RgdFlx^y$ are subject to the
proviso
\beq
\forall x. \Phi(x) = 0  \Imp  \forall i\,.\, \Phi_{i}(x) = 0\\ 
\forall x. \Phi(x) = u  \Imp  \forall i\,.\, \Phi_{i}(x) = u\\ 
\forall x. x \not= y \And \Phi(x) = 1  \Imp  \exists i\,.\, \Phi_{i}(x) = 1
\And \forall j, j\not = i. \Phi_{j}(x) = u \\
\Phi(y) = u \Or
(\Phi(y)=1 \And  \forall i. \Phi_{i}(y) = u)
\eneq
Finally define $\GG\vd M\mbigcap N \hastype A = {\cal Q}$ if ${\cal Q}=
 \{Q\mid\GG\prv  M\mcap N \blip  Q \hastype  A\}$.
\end{Definition} 

Some remarks are in order:
\bit
\item
In rule $\mcap\_FlxFlx$ we can assume that the same list 
of variables, though with different labeling, is the argument of $E,F$ 
and $H$, since simple terms are fully-applied and due to linearity we 
can always reorder the context to the same list.  
\item
 Since patterns are linear and $M$ and
$N$ share no pattern variables, the flex-flex case arises only with distinct
variables.  This also means we do not have to apply substitutions or perform
the customary occurs-check.
\item 
In the flex/rigid and rigid/flex rules, the proviso enforces the typing
discipline since each strict variable $x$ must be strict in some premise.
% The modified condition on $y$ takes into account that the head of an
% application constitutes a strict occurrence.
% In  rule $\mcap\_FlxRgd$ the proviso enforces the typing discipline, 
% for which $x$ must be strict in some premise.
% %  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, as there are no more requirements on that variable, therefore
the modified condition on $y$ takes into account that the head of an
application constitutes a strict occurrence.
\item
We also need an  exchange rule:
$$
\ianc{ h\in\GG\cup\Sigma\quad  \GG\prv N\mcap h\ \Mns \blip  Q\hastype  P} 
{\GG\prv   h\ \Mns\mcap N \blip  Q \hastype  P} 
{\mcap\_Excng}$$
As usual,  this kind of rule is problematic \wrt termination. We can
 avoid it if we agree to implicitly add the symmetric rules  $\mcap\_
RgdFlex^c$ and  $\mcap\_RgdFlex^y$.
\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\oftp A\prv E\ x^{1}\mbigcap\ 
c\ (F\ x^{u})^{1} \ (F'\ x^{u})^{1}$.  Since $x$ is strict in 
the LHS, there are two ways in which $\Phi$ can be `split' leading 
to the following sub-problems:
\[
\begin{array}{lrr}
x\oftp A\prv E' \ x^{1}\mcap\  F\  x^{u} \blip  H\  x^{1}
& & x\oftp A\prv E''\ x^{u}\mcap\  F'\  x^{u} \blip  H'\  x^{u}
\\
x\oftp A\prv E' \ x^{u}\mcap\  F\  x^{u} \blip  H\  x^{u}
& & x\oftp A\prv E''\ x^{1}\mcap\  F'\  x^{u} \blip  H'\  x^{1}
\end{array}
\]
Hence the result:
\begin{eqnarray*}
%\label{eq:int}
x\oftp A\prv E\ x^{1}\mbigcap\  c\ (F\  x^{u})^{1} \ (F'\  
x^{u})^{1}& = &  \{c\ (H\  x^{1})^{1} \ (H'\  x^{u})^1,c\ (H\  x^{u})^1 \ (H'\  
x^{1})^1\}
\end{eqnarray*}
\end{example}

Note that, similarly to complementation, intersection return a 
solution with some `overlapping' possible; again it is possible, in a 
post-processing phase to make the result exclusive:
for example the above problem \ignore{(\ref{eq:int})} can be explicited in:
\beq
\lefteqn{x\oftp A\prv E\ x^{1}\mbigcap\  c\ (F\  x^{u})^{1} \ (F'\  
x^{u})^{1} = }\\
& & \{c\ (H\ x^{1})^{1} \ (H'\ x^{0})^1,c\ (H\ x^{0})^1 \ 
(H'\ x^{1})^1,c\ (H\ x^{1})^1 \ (H'\ x^{1})^1\}
 \eneq 

However, it must be noted that the latter is not the most general 
solution \wrt the subsumption ordering on terms based on  the 
(reverse) partial information ordering on labels.  Indeed, say, $c\ 
(H\ x^{1})^{1} \ (H'\ x^{0})^1 \leq E\ x^{1}$ and $c\ (H\ 
x^{})^{1} \ (H'\ x^{0})^1\leq c\ (H\ x^{u})^{1} \ (H'\ 
x^{u})^1$, but $c\ (H\ x^{1})^{1} \ (H'\ x^{0})^1\leq c\ 
(H\ x^{1})^{1} \ (H'\ x^{u})^1$.

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

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

\begin{Lemma}
\label{le:flexunif}
Let $\godf\vd M\hastype A$ and $\godf\vd M\hastype A$ be \emph{compatible} 
type assignments; then $\godf\vd M\hastype A$ and 
$\gods\vd M\hastype A$ iff $\godt \vd M\hastype A$.
\end{Lemma}
\begin{proof}
($\Imp$). By induction on the structure of $\cD_1::\godf\vd M\hastype A$ and 
$\cD_2::\gods\vd M\hastype A$.  
\bit
\itc 
$$\cD_1=\ianc{c\oftp A\in \Sigma}{\GG_{1};\O_{1}\cdot\vd c\hastype 
C}{Con}\qquad
\cD_2=\ianc{c\oftp A\in \Sigma}{\GG_{2};\O_{2}\cdot\vd c\hastype 
A}{Con}$$
Then
$$\cE=\ianc{c\oftp A\in \Sigma}{(\GG_{1}\cap\GG_{2});(\O_{1},\O_{2});\cdot\vd c\hastype 
A}{Con}$$
\itc 
$$\cD_1=\ianc{}{(\GG_{1},x \oftp A);\O_{1}\cdot\vd x\hastype 
A}{Id^u}\qquad
\cD_2=\ianc{}{(\GG_{2},x \oftp A);\O_{2}\cdot\vd x\hastype 
A}{Id^u}$$
Then
$$\cE=\ianc{}{(\GG_{1}\cap\GG_{2},x\oftp A);(\O_{1},\O_{2});\cdot\vd x\hastype 
A}{Id^u}$$
\itc 
$$\cD_1=\ianc{}{\GG_{1};\O_{1};x\oftp A\vd x\hastype 
A}{Id^1}\qquad
\cD_2=\ianc{}{\GG_{2};\O_{2};x\oftp A\vd x\hastype 
A}{Id^1}$$
Then
$$\cE=\ianc{}{(\GG_{1}\cap\GG_{2});(\O_{1},\O_{2});x\oftp A\vd x\hastype 
A}{Id^1}$$
\[
\cD_1 =  \ianc{(\Gamma_1, x\oftp A); \Omega_{1}; \Delta_{1}\vd M \hastype B}{\Gamma_1;
\Omega_1; \Delta \vd \lamb{ x^u }{A} M \hastype A \GImp{u}
B}{\GImp{u}I}
\quad
\cD_2 =  \ianc{(\Gamma_2, x\oftp A); \Omega_2; \Delta_{2}\vd M \hastype B}{\Gamma_1;
\Omega_2; \Delta_{2} \vd \lamb{ x^u }{A} M \hastype A \GImp{u}
B}{\GImp{u}I}
\]
\btab
$(\Gamma_1, x\oftp A); \Omega_{1}; \Delta_{1}\vd M \hastype B$\bv
$(\Gamma_2, x\oftp A); \Omega_2; \Delta_{2}\vd M \hastype 
B$\bv
$(\Gamma_1, x\oftp A)\cap (\Gamma_2, x\oftp A); (\Omega_{1},\O_{2}); 
(\Delta_{1},\D_{2})\vd M \hastype B$\bi\\
$(\Gamma_1\cap \GG_{2}, x\oftp A); (\Omega_{1},\O_{2}); 
(\Delta_{1},\D_{2)}\vd M \hastype B$\` By De Morgan\\
$\godt \vd \lamb{ x^u }{A} M \hastype A \GImp{u}
B$\br
\etab
\itc
$$\cD_{1}= \ibnc{(\Gamma_{1}, \Delta_N^{1}); \Omega_{1}; \Delta_M^{1} \vd M \hastype A \RImp 
B}{(\Gamma_{1}, \Delta_M^{1}); \Omega_{1}; \Delta_N^{1} \vd N \hastype 
A}{\Gamma_{1}; 
\Omega_{1}; (\Delta_M^{1}, \Delta_N^{1}) \vd M\ N^1 \hastype B}{\GImp{1}E}
$$
and
$$\cD_{2}= \ibnc{(\Gamma_{2}, \Delta_N^{2}); \Omega_{2}; \Delta_M^{2} \vd M \hastype A \RImp 
B}{(\Gamma_{2}, \Delta_M^{2}); \Omega_{2}; \Delta_N^{2} \vd N \hastype 
A}{\Gamma_{2}; 
\Omega_{2}; (\Delta_M^{2}, \Delta_N^{2}) \vd M\ N^1 \hastype B}{\GImp{1}E}
$$
\btab
$(\Gamma_{1}, \Delta_N^{1}); \Omega_{1}; \Delta_M^{1} \vd M \hastype A \RImp 
B$\bv
$(\Gamma_{2}, \Delta_N^{2}); \Omega_{2}; \Delta_M^{2} \vd M \hastype A \RImp 
B$\bv
$(\Gamma_{1}, \Delta_N^{1})\cap(\Gamma_{2}, \Delta_N^{2}); 
( \Omega_{1},\Omega_{2});(\D_{M}^{1}, \Delta_M^{2}) \vd M \hastype A \RImp 
B$\bi\\
$(\Gamma_{1}, \Delta_M^{1})\cap(\Gamma_{2}, \Delta_M^{2}); 
( \Omega_{1},\Omega_{2});(\D_{N}^{1}, \Delta_N^{2} )\vd N \hastype A$\bi\\
$(\Gamma_{1}\cap \Gamma_{2},  \Delta_N^{1}, \Delta_N^{2}); 
( \Omega_{1},\Omega_{2});(\D_{M}^{1}, \Delta_M^{2}) \vd M \hastype A \RImp 
B$\` By Lemma \ref{le:compat}\\
$(\Gamma_{1}\cap \Gamma_{2}); ( \Omega_{1},\Omega_{2});( \Delta_M^{1},\Delta_M^{2},\D_{N}^{1}, 
\Delta_N^{2}) \vd N \hastype A$
\` By rule
\etab
\enit
($\If$). Similarly by induction on the structure of the derivation of\\
$\godt \vd M\hastype A$.
\end{proof}

%\include{deriv}
{\newcommand{\gm}{(\Gamma,\Delta_i^u);\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,\D^{u}_{i});\O;\D_i^{1} \vd M_{i}\hastype A_{i}\quad 
1\leq i\leq n}{\Gamma;\Omega; \D\vd c\ M_{1}^{1}\dots M_{n}^{1}\hastype 
B}{\RImp E_{n}^{c}} 
\eneq 
where $\GG;\O;\cdot\vd c\ \hastype A_{1}\RImp\dots\RImp A_{n}\RImp B$ and 

\ben
\item 
$\forall x\in\D\,.\,\exists i
:1\leq i\leq n
\,.\,x\in\D_{i}^{1}$.
\item
$\forall i:1\leq i\leq n
\,.\,\D_{i}^{u}\cup\D_{i}^{1}=\D$.
\enen


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

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

\begin{Lemma}
\label{le:derivec}
Let $(\GG,\D^u);\O;\cdot\vd c \hastype A_{1}\RImp\dots\RImp 
A_{n}\RImp B$: if $\gm\D_i^1 \vd M_{i}\hastype A_{i}$ for $1\leq 
i\leq j$, then $(\GG,\D^u);\O;\D^1\vd c\ M^{1}_{1}\dots 
M_{j}^{1}\hastype A_{j+1}\RImp\dots\RImp A_{n}\RImp B$, where
\bit
\item[1.] 
$\forall x\in\D^{1}.\exists i:1\leq i\leq j\,.\,x\in\D_{i}^{1}$.
\item[1'.]
$\forall x\in\D^{1}.\neg\exists i:1\leq i\leq j\,.\,x\in\D_{i}^{u}$.
\item[2.]
$\forall i:1\leq i\leq j\,.\,\D_{i}^{u}\cup\D_{i}^{1}=\D^u\cup\D^1$.
\enit
\end{Lemma}
\begin{proof}
By induction on $j$.
\bit
\item[$\mathbf{ j=0}$]
\btab
$(\GG,\D^u);\O;\cdot\vd c \hastype A_{1}\RImp\dots\RImp 
A_{n}\RImp B$ \` By hypothesis
\etab
\item[$\mathbf{j+1}$]
\btab
$\gm\D_i^1\vd M_i\hastype A_i, 1\leq i\leq j$\` By assumption\\
 $(\GG,\D^u);\O;\D^1\vd c\ M^{1}_{1}\dots 
M_{j}^{1}\hastype A_{j+1}\RImp\dots\RImp A_{n}\RImp B$\bi\\     
$(\GG,\D^u_{j+1});\O;\D^1_{j+1}\vd M_{j+1}\hastype A_{j+1}$\bh
%$(\GG,\D^u_{j+1});\O;\D^1_{j+1}\vd M_i\hastype A_i$\` By assumption\\
 $(\GG,\D^u_+);\O;\D^1_+\vd c\ M^{1}_{1}\dots 
M_{j+1}^{1}\hastype A_{j+2}\RImp\dots\RImp A_{n}\RImp B$ and \\
$x\in\D^1_+ \Bimp x\in \D^1_{j+1}\cup\D^1\And
x\in\D^u_+\Bimp x\in\D^u\cap\D^u_{j+1}$ \br \ $\RImp E$
\etab
We now show that the last step satisfy the condition on  rule $\RImp E$:
\bit
\item[1.]
\btab
$x\in\D^1_+$\ba
$ x\in \D^1_{j+1}\cup\D^1$\` As $x\in\D^1_+ \Bimp x\in \D^1_{j+1}\cup\D^1$\\
$ x\in \D^1_{j+1}$\` Case\\
$x\in\D^1_+ \Imp \exists i\oftp 1\leq i\leq j+1\,.\, x\in\D^1_i$\\
$x\in\D^1       $\` Case\\
$x\in\D^1_i$, for some $1\leq i\leq j$\bi\\
$x\in\D^1_+ \Imp \exists i\oftp 1\leq i\leq j\,.\, x\in\D^1_i$
\etab
\item[1'.]
\btab
$x\in\D^u_+$\ba
$x\in\D^u$\` As $x\in\D^u_+\Bimp x\in\D^u\cap\D^u_{j+1}$\\
$x\in\D^u_+\Imp \neg \exists i\oftp 1\leq i\leq j\,.\, x\in\D^1_i$\bi
\etab
\item[2.]
\btab
$\D^1_+\cup\D^u_+= \D^1\cup\D^u$ \br \\
$\forall i\oftp 1\leq i\leq j\,.\, \D^1_i\cup\D^u_i= \D^1\cup\D^u$\bi\\
$\forall i\oftp 1\leq i\leq j\,.\, \D^1_i\cup\D^u_i= \D^1_+\cup\D^u_+$
\` By replacement
\etab
\enit
\enit
\end{proof}

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

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

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

\label{le:invertey}
Let $(\GG,\D^u)';\O;\D'\vd y\hastype A_{1}\RImp\dots\RImp A_{n}\RImp
B$,
where $\D'=\{y\}$ or $\D'=\cdot \And y\in(\GG,\D^u)'$ and
$(GG,\D^u)'\cup D'=\GG\cup\D^u\cup \D^1 $. If $(\GG,\D^u);\O;\D^1\vd y\ M^{1}_{1}\dots 
M_{j}^{1}\hastype A_{j+1}\RImp\dots\RImp A_{n}\RImp B$, then 
 $\gm\D_i^1 \vd M_{i}\hastype A_{i}$ for $1\leq 
i\leq j$  and 
\bit
\item[1.] 
$\forall x\in\D^{1}.\exists i:1\leq i\leq j\,.\,x\in\D_{i}^{1}$.
\item[1'.]
$\forall x\in\D^{1}.\neg\exists i:1\leq i\leq j\,.\,x\in\D_{i}^{u}$.
\item[2.]
$\forall i:1\leq i\leq j\,.\,\D_{i}^{u}\cup\D_{i}^{1}=\D^u\cup\D^1$.
\enit
\end{Lemma}
\begin{proof}
By induction on $j$ similarly to Lemma \ref{le:invertec}.
\end{proof}

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


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

\begin{Theorem}
\label{thm:unif1}
Let $\GG\vd N_{1}\mcap N_{2}\blip  N\hastype A$.  If $\GG\prv M\in\|N_{1}\|:A$ and 
$\GG\prv M\in\|N_{2}\|:A$, then $\GG\prv M\in\|N\|:A$.
\end{Theorem}
\begin{proof}
% By simultaneous induction on $\cD_{1}::\GG\prv M\in\|N_{1}\|:A$ and 
% $\cD_{2}::\GG\prv M\in\|N_{2}\|:A$.
By induction on the structure of $\cD::\GG\prv N_{1}\mcap N_{2}\blip  N\hastype A$.
\bit
\itc $\cD$ ends in  $\mcap\_FlxFlx$; by Remark \ref{rmrk:compa} and 
the left-to-right direction of Lemma \ref{le:flexunif}.
\itc $\cD$ ends in  $\mcap\_FlxRgd^{c}$:
\btab
$\cD::\GG\vd E\ \Phi\mcap c\ \ol{Q_{n}^{1}} \blip  c\ \Nns$\bh
$\cD_i::\GG\vd E_{i}\ \Phi_i\mcap Q_i \blip  N_i$ for $1\leq i\leq n$
with proviso \bv
$\GG\vd M \in\|c\ \ol{Q_{n}^{1}}\|$\bh
$M\equiv c\ \Mns$ and  $\cD^2_i::\GG\vd M_{i}\in\|Q_{i}\|$ for $1\leq i\leq n$ 
\bv
$\GG\vd c\ \Mns\in\|E\ \Phi\|$\bh
$c\ \Mns\equiv t\ \Phi$, where $t\hastype A$ and $t\equiv \l\Phi\,.\,c\ \tn$ 
for  $\Phi\vd c\ \tn^{1}\hastype P$\bv
$\Phi_{i}\vd t_{i}\hastype A_{i}$\` By inversion on rule $\RImp 
E^{n}_{c}$ (Lemma \ref{le:invertec})\\
$\cD^1_i::\GG\vd M_{i}\in\|E_{i}\ \Phi_{i}\|$ \br\, $grFlx$\\
$\GG\vd M_{i}\in\|N_{i}\|$\bi on $\cD_1,\cD_i^1,\cD_i^2$\\
$\GG\vd c\ \Mns\in\|c\ \Nns\|$\br
\etab
\itc $\cD$ ends in  $\mcap\_FlxRgd^y$. Proceed as above, but using 
Lemma \ref{le:derivey}.

\itc $\cD$ ends in  $\mcap\_Lam$:
\btab
$\GG\vd \lxua N_1\mcap \lxua N_2 \blip  \lxua N$\bh
$\cD::\GG,x\oftp A\prv N_{1}\mcap N_{2}\blip N$\bv
$\GG\prv \lxua M\in\|\lxua N_{1}\|$ \bh
$\cD_1:: \GG,x\oftp A\vd M\in\| N_{1}\|$\bv
$\GG\prv \lxua M\in\|\lxua N_{2}\|$\bh
$\cD_2::\GG,x\oftp A\prv M\in\| N_{2}\|$\bv
$\GG,x\oftp A\prv M\in\| N\|$\bi on $\cD,\cD_1,\cD_2$\\
$\GG\prv \lxua M\in\|\lxua N\|$\br
\etab
\itc $\cD$ ends in  $\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}\blip  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 the structure of $\cD::\GG\vd N_{1}\mcap N_{2}\blip  N$.
\bit
\itc $\cD$ ends in $\mcap\_FlxFlx$; by Remark \ref{rmrk:compa} and the 
right-to-left direction of Lemma \ref{le:flexunif}.

\itc $\cD$ ends in  $\mcap\_FlxRgd $.
\btab
$\cD::\GG\vd E\ \Phi\mcap c\ \ol{Q_{n}^{1}} \blip  c\ \Nns$\bh
$\cD_i::\GG\vd E\ \Phi_i\mcap Q_i \blip N_i, 1\leq i\leq n$\bv
$\GG\vd c\ \Mns\in\|c\ \Nns\|$\bh
$\GG\vd M_{i}\in\|Q_{i}\|$ and $\GG\vd M_{i}\in\|E_{i}\ \Phi_{i}\|$
\bi on $\cD_i$\\
$M_{i}\equiv t\ \Phi$, where $t\hastype A$ and $t\equiv \l\Phi\,.\,t_{i}$ 
for  $\Phi_{i}\vd t_{i}\hastype A_{i}$\br $grFlx$\\
$\Phi\vd c\ \ol{t^{1}_{n}}\hastype P$\` By  rule $\RImp 
E^{n}_{c}$ (Lemma \ref{le:derivec})\\
$\GG\vd c\ \Mns\in\|E\ \Phi\|$\br\\
$\GG\vd c\ \Mns\in\|c\ \ol{Q^{1}_{n}}\|$\br
\etab
\itc $\cD$ ends in  $\mcap\_FlxRgd^y$. Proceed as above, but using 
Lemma \ref{le:derivey}.
\itc $\cD$ ends in  $\mcap\_Lam$; by IH as in Theorem \ref{thm:unif1}
\itc $\cD$ ends in  $\mcap\_App$; ditto.
\enit
\end{proof}

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

\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]\hastype A M\in M_{i}, 
% N\in N_{j}, P \in M\mbigcap N\hastype A\}
% \eneq

\section{The Algebra of Strict Terms}
\label{sec:algebra}
We now extend the intersection and complement operations to \emph{sets} 
of terms, as required by their  finitary nature. 

\begin{Definition}
\label{def:setop} If 
$\cM$ and $\cN$ are sets of \emph{simple} terms of type $A$, define:
\beq      
\cM \mbc \cN & \eqdef & \{Q\mid Q\in
M\mbigcap N\hastype A, M\in \cM, N\in \cN\} 
\vsk
\mna \cM & \eqdef & \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.


\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}\mbox{}
\ben
\item 
By the Partition Lemma,  $\GG\prv  M\in \| \cN \| \hastype A$ 
or $\GG\prv  M\in \| \mmnot(\cN) \|\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}



%That will allows use to solve `multiple' complement problems, as the 
%ones typically required by clause complementation, see Section \ref{}, 
%\ie:
%$$\|Z\|-\|M_{1}\mdots M_{n}\|$$
%as
%$$ \mna \{M_{1}\mdots M_{n}\}$$
%
%\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

\begin{metanote} An involution example ? \end{metanote}

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}_{\Sigma}$ in a boolean algebra $\la \mathbf{\cal 
T}_{\Sigma},\emptyset,\cup,\mbc,\mna\ra$ under set union, patterns 
intersection and complementation.

\begin{Theorem}
\label{thm:algebra}
Consider the algebra  $\la \mathbf{\cal 
T}_{\Sigma},\emptyset,\cup,\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
\btab
 $\cM\mbc(\cN\mbc \{M\}\cup\cP)=$\` LHS\\
$\cM\mbc((\cN\mbc\{M\})\cup(\cN\mbc\cP)) =$ \` By $\ref{it:DM}.$\\
$(\cM\mbc(\cN\mbc\{M\}))\cup\cM\mbc(\cN\mbc\cP))=$ \` By $\ref{it:DM}.$\\
$((\cM\mbc\cN)\mbc\{M\})\cup (\cM\mbc\cN)\mbc\cP))=$\bi\\ 
$(\cM\mbc\cN)\mbc ( \{M\}\cup\cP)$  \` By $\ref{it:DM}.$
\etab
\item
$\GG\vd M\in \|\mna\mna \cM\|$ iff by Corollary \ref{co:setpart} 
$\GG\vd M\not\in\|\mna \cM\|$ iff, again by Corollary \ref{co:setpart} 
$\GG\vd M\in \|\cM\|$.
\item
Immediate from Corollary \ref{co:setpart}.
\item
Immediate from Corollary \ref{co:setpart}.
\enen
\end{proof}


\begin{Corollary}
\label{co:boolean}
The algebra $\la \mathbf{\cal T}_{\Sigma},\emptyset,\cup,\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} guarantees that any other boolean operation 
is definable: indeed complementation and intersection alone allows to 
define the \emph{relative} complement operation:

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

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

\begin{Corollary}
$\GG\vd M\in\|\cM\| - |\cN\|$ iff $\GG\vd M\in\|\cM-\cN\|$ .
\end{Corollary}
\begin{proof}
$\GG\vd M\in\|\cM\| - |\cN\|$ iff $\GG\vd M\in \|\cM\|$ and $\GG\vd 
M\not\in\|N\|$ for every $N\in\cN$ iff (Corollary \ref{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 former.  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{Applications}
%\label{sec:appl}
\begin{example}
\label{ex:combi}
We can therefore combine Example \ref{ex:lam} and \ref{ex:etardx}:
\[
\begin{array}{lll}
\mmnot\{(app\ (lam\ (\lamb{x^u}{exp} E\ x^u))\ 
F),lam(\lamb{x^u}{exp} app\ (E\ x^o) \ x\}
=\\
\quad \mmnot(app\ (lam\ (\lamb{x^u}{exp} E\ x^u))\ 
F)\mbc \mbox{}\\
\quad \mmnot(lam(\lamb{x^{u}}{exp} app\ (E\ x^{0})\ x ))=\\

\qquad \{ lam\ (\lamb{x^u}{exp} (H\ x^u)),\\
 app\ (app\ H_{1}\ H_{2})\ H_{3}\} \mbc \mbox{}\\

\qquad\{ lam(\lamb{x^u}{exp} app\ (H\ x^1)\ (H'\ x^u)),\\
\qquad lam(\lamb{x^u}{exp} app\ (H\ x^u)\ (app\ (H'\ x^u) \ (H'' x^u)), \\
\qquad lam(\lamb{x^u}{exp} app\ (H\ x^u)\ ( lam(\lamb{y^u}{exp} H'\ x^u\ y^u)),\\
\qquad lam(\lamb{x^u}{exp} lam(\lamb{y^u}{exp} H\ x^u\ y^u) ),\\
\qquad lam(\lamb{x^u}{exp}x),\\
\qquad app\ H\ H'\}=\\

% \qquad \{ lam(\lamb{x^u}{exp} app\ (H\ x^1)\ (H\ x^u),\\
% \quad\qquad\lam(\lamb{x^u}{exp} app\ (H\ x^u)\ (app\ (H_4 x^u) \ (H_5 x^u))), \\
% \quad\qquad lam(\lamb{x^u}{exp} app\ (H\ x^u)\ ( lam(\lamb{y^u}{exp} H_6\ x^u\ y^u)),\\
% \quad\qquad app\ H_1\ H_2,\\
%  \quad\qquad lam(\lamb{x^u}{exp} lam(\lamb{y^u}{exp} H_3\ x^u\ y^u) )\}=\\

\qquad\qquad \{ lam(\lamb{x^u}{exp} app\ (H\ x^1)\ H'\ x^{u}), \\ 
\qquad\qquad  lam(\lamb{x^u}{exp} app\ (H\ x^u)\ (app\ H'\ x^{u} H''\ x^{u})),\\
\qquad\qquad lam(\lamb{x^u}{exp} app\ (H\ x^u)\ ( lam(\lamb{y^u}{exp} H'\ x^u\ y^u))\\
\qquad\qquad  lam(\lamb{x^u}{exp} lam(\lamb{y^u}{exp} H'\ x^u\ y^u)),\\
\qquad \qquad lam(\lamb{x^u}{exp}x),\\
\qquad\qquad app\ ( app\ H\ H') H''\}
\end{array}
\]
\end{example}

\smallskip
Solving relative complement problems is not only a question of
intellectual
curiosity, but it is crucial for our intended application, 
the transformational approach to negation in \lp . This idea aims to by-pass most 
of the problems intrinsic to the negation-as-failure rule by replacing 
negative occurrence of predicates in goals
 by equivalent positive predicated whose definition 
has been mechanically synthesized. This entails
two major steps
\ben
\item
Compute complement of heads of clauses in the predicate definition.
\item 
Bring definition in negation normal form the respecting operational 
semantics.
\enen

While this approach has been investigated for \fo Horn clauses 
\cite{Sato84,Bar90} and CLP programs \cite{Bruscoli94}, the field has
not been explored, at the best of our knowledge, 
\wrt \ho logics and logical frameworks.  For the latter 
this notion of intensional negation is the most adequate, see 
\cite{Momigliano99phd} for a discussion.  

We cannot discuss item $2.$ here. We can suggest its usage via this
 example; consider the 
following facts:
\[
\begin{array}{lll}
betarx & : & isredx(app\ (lam\ (\lamb{x^u}{exp} E\ x^u))\ F )\\
etarx & : & isredx(lam(\lamb{x^u}{exp} app\ (E\ x^0) \ x)
\end{array}\]

Computing the relative complement as in Example \ref{ex:combi} yields
 the
complementary  facts: 
\[
\begin{array}{lll}
nb1 & : & non\_isredx(lam(\lamb{x^u}{exp} app\ (H\ x^1)\ H'\ x^{u}))\\
nb2 & : & non\_isredx( lam(\lamb{x^u}{exp} app\ (H\ x^u)\
 (app\ H_4\ x^{u} H_5\ x^{u})))\\
nb3 & : & non\_isredx(lam(\lamb{x^u}{exp} app\ (H\ x^u)\ ( lam(\lamb{y^u}{exp} H_6\ x^u\ y^u))))\\
nb4 & : & non\_isredx(lam(\lamb{x^u}{exp} lam(\lamb{y^u}{exp} H_3\ x^u\ 
y^u) ))\\
nbr & : & non\_isredx(lam(\lamb{x^u}{exp}x))\\ 
nb6 & : & non\_isredx( app\ (app\ H_{1}\ H_{2})\ H_{3}\ )
\end{array}\]


\section{Conclusion}
\label{sec:concl}
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}.
