\documentclass[10pt]{article}
% \usepackage{latexsym}
 \usepackage{amsfonts}
\usepackage{cdsty}
\usepackage{mit-com}
%\usepackage{prooftree}
\def\zzctdrawdotedge{\drawdotedge{4pt}0}
\def\ctabutborderlr{1em}
\def\ctabutbordertb{1ex}
\textwidth 12.7cm
\textheight 21.5cm
\pagestyle{plain} %change to empty
\bibliographystyle{alpha}
% \bibliographystyle{plain}  %Change to this

\newcommand{\eqdef}{\stackrel{\mbox{\tiny  def}}{=}}
\newcommand{\mmnot}{\neg}
\newcommand{\rep}[1]{\ulcorner #1\urcorner}  % amsfonts.sty
\newcommand{\arv}[2]{\begin{array}{c} #1\\#2\end{array}}
\newcommand{\UImp}{\GImp{u}}
\newcommand{\god}{\Gamma; \Omega;\Delta}
\newcommand{\godemp}{(\GG,\O,D)\emp}
\newcommand{\betared}{\stackrel{\beta}{\longrightarrow}}
\newcommand{\etaexp}{\stackrel{\bar\eta}{\longrightarrow}}
\newcommand{\lxua}{\lambda x^{u}\!:\!  A.\, }
\newcommand{\D}{\Delta}
\renewcommand{\O}{\Omega}
\newcommand{\dmn}{(\D_{M},\D_{N})}
\newcommand{\Mns}{\overline{M_n^1}}
\newcommand{\Nns}{\overline{N_n^1}}
\newcommand{\emp}{;\cdot;\cdot}
\newcommand{\itc}{\item[\textbf{case}]}
\newcommand{\btab}{\begin{tabbing}}
\newcommand{\etab}{\end{tabbing}}
\newcommand{\cF}{{\cal F}}
\newcommand{\xnl}{\overline{x_{n}^{l}}}
\newcommand{\cM}{{\cal M}}
\newcommand{\mbc}{\bigcap} %overloaded notation: may be changed
\newcommand{\mna}{\mmnot} %overloaded notation: may be changed
\newcommand{\mcap}{\cap}
\newcommand{\mbigcap}{\hat\cap}
\newcommand{\da}{\downarrow}
\newcommand{\bua}{\Uparrow}
\newcommand{\buda}{\Uparrow\!\downarrow}


\begin{document}
\huge
\noindent
{\bf
 The Relative Complement Problem for Higher-Order Patterns}
\normalsize
\\
\\
\large
\noindent {\bf Alberto Momigliano}\\
Department of Philosophy\\
           Carnegie Mellon University\\
	   Pittsburgh, PA 15213, U.S.A\\
 \texttt{mobile@cs.cmu.edu}\\
\\
{\bf  Frank Pfenning}\\
 Department of Computer Science \\
           Carnegie Mellon University\\
	   Pittsburgh, PA 15213, U.S.A.\\
 \texttt{fp@cs.cmu.edu}
\\
\\

\Large
\noindent
{\bf Abstract}
\normalsize
\\
\noindent We address the problem of complementing \ho unrestricted patterns, 
\ie without repetitions of free variables.  Differently from the \fo 
case, the complement of a pattern cannot, in general, be described by 
a pattern, or even by a finite set of patterns.  We therefore 
generalize the simply-typed $\lambda$-calculus to include an internal 
notion of \emph{strict function} so that we can directly express that 
a term must depend on a given variable.  We show that, in this more 
expressive calculus, finite sets of unrestricted patterns are closed under 
complement and unification.  Our principal application is the 
transformational approach to negation in higher-order logic programs.

%We address the problem of higher-order patterns complementation.  Differently 
%from the first-order case, the complement of a linear non-fully applied 
%pattern cannot be described by  a finite set of 
%patterns.  This is due to the issue of \emph{dependency constraints},
%that is when a $\lambda$ term depends on its arguments.  
%We therefore introduce a $\lambda$-calculus with an internal notion 
%of \emph{strictness} so that we can directly express that a term must 
%depend on a given variable.  We show that finite sets of linear 
%patterns in this calculus are closed under complement and 
%unification.  Our principal application is the transformational 
%approach to negation in higher-order logic programs.


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

%\newcommand{\lamb}[2]{\lambda {#1}\!:\!{#2}.\,}
In most functional and logic programming languages the notion of a
pattern, together with the requisite algorithms for matching or
unification, play an important role in the operational semantics.  \ignore{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{unrestricted 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 unrestricted pattern is a finite set of
unrestricted patterns.
  \item Unification of two patterns is decidable and leads
to a finite set of most general unifiers.
 \end{enumerate}
 Consequently, finite sets of unrestricted patterns in the strict
$\lambda$-calculus are closed under complement and unification.  If we
think of finite sets of unrestricted 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, 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 \ref{sec:appl} 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.  For reasons 
of space, proof are omitted here and can be found in the full version 
of the paper \cite{Momigliano99www}.


\section{Related Wok}
\label{sec:related}

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 application is discussed in Section \ref{sec:appl}.

Lassez and Marriot \cite{Lassez87} proposed the seminal 
{\em uncover} algorithm  for computing relative 
complements and introduced the now familiar restriction to unrestricted terms.
We here quote the definition of the $\mmnot$ 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 unrestricted term $t$.  
\[ \begin{array} {lll}
\mmnot_L(x  ) & = \emptyset  \\
\mmnot_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\mmnot_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 
(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, controls is a major problem.  We 
argue that using disunification for this purpose remains over-killing.  
Moreover the \ho case brings in additional complications, as 
dependencies, which are orthogonal to
 %the hyper-logical structuring that
 disunification.
% requires.


\section{Complementing Fully Applied Patterns}
\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$ 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 district 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 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.  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}
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}
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}
 
 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 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 
unrestricted 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 independently 
investigated in \cite{Wright92,Baker-Finch94}.

\[ \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 undetermined, 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 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 undetermined 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 variable cannot be used in 
the argument to an undetermined function: 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 undetermined 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 undetermined 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. A full account can be found in \ref{Momigliano99www}.
% 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{Theorem}[Uniqueness of Typing]
% \label{thm:uniqueT}
% If $\god\vd M\hastype A$ and  $\god\vd M\hastype A'$, then $A\equiv A'$.
% \end{Theorem}
% \begin{proof}
% By induction on the structure of the given derivations, exploiting 
% `functionality' of signatures and contexts.
% \end{proof}

With respect to the structural properties of the context(s).  
Exchange is directly built into the formulation and will not be 
repeated. \ignore{ We use $[N/x]M$ for the result of the capture-avoiding 
substitution of $N$ for $x$ in $M$. } Weakening is allowed in the undetermined 
and in the irrelevant contexts. Contraction holds anywhere.
% \begin{Theorem}[Weakening] \mbox{}
% \label{thm:weak}
% \begin{enumerate}
%  \item (Weakening$^{u}$) If $\Gamma; \Omega; \Delta\vd M \hastype C$ then $(\Gamma, 
%  x\oftp A); \Omega; \Delta\vd M \hastype C$. 
%  \item (Weakening$^{0}$) 
%  If $\Gamma; \Omega; \Delta\vd M \hastype C$ then $\Gamma
%  ; (\Omega, x\oftp A); \Delta\vd M \hastype C$. 
%  \end{enumerate}
%  \end{Theorem}
We also have the possibility   to lose track of dependencies, if 
we are so inclined.

\newcommand{\gofd}{\GG;(\Omega,\Phi);\Delta}
\newcommand{\gfod}{(\GG,\Phi);\Omega;\Delta}
\newcommand{\bv}{\` By inversion\\}
\newcommand{\bi}{\` By HI }
\newcommand{\bh}{\` By hypothesis\\}
\newcommand{\br}{\` By rule}

%\begin{Theorem}[Loosening$^{0}$]
%\label{thm:0loose}
\ben
\item
If $\Gamma; (\Omega,\Phi); \Delta\vd M \hastype A$ then $(\Gamma, 
\Phi); \Omega; \Delta\vd M \hastype A$. 
%\end{Theorem}
\newcommand{\godx}{\Gamma; \Omega; (\Delta,x\oftp C)}
\newcommand{\gdo}{(\GG,x\oftp C);\Omega;\Delta}

%\begin{Theorem}[Loosening$^{1}$]
%\label{thm:1loose}
\item
If $\Gamma; \Omega; \Delta\vd M \hastype A$, then $(\GG,\D);\O;\cdot\vd 
M \hastype A$.
%\end{Theorem}
\enen

%\begin{Corollary}
%\label{co:1loose}
%If $\Gamma; \Omega; \Delta\vd M \hastype A$ then $(\GG,\D);\O;\cdot\vd M \hastype A$. 
%\end{Corollary}

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

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

\[ \begin{array}{rcl}
   (\lam x^k\oftp A\ldot M)\, N^k & \betared & [N/x]M \\
   [1ex]
   M \hastype A \GImp{k} B & \etaexp & \lam x^k\oftp A\ldot M\  x^k \\
\end{array} \]
 
%Indeed one of the main 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 generalized to this three-zoned calculus.

\begin{Theorem}
[Subject Reduction and Expansion]
 \mbox{}
\label{thm:subred}

\ben
\item 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}
\item
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$.
\enen
\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 is central in the proof of disjointness of 
% complementation (Theorem \ref{lemma:part}):

\begin{Lemma}[Exclusivity]
\label{le:disj}
It is not the case that both $\GG;\O;(\D,x\oftp A)\vd M\hastype 
C$ and $\GG;(\O,x\oftp A);\D\vd M\hastype C$.
\end{Lemma}
% \begin{proof}
% By  induction on the structure of $\cD::\GG;\O;(\D,x\oftp A)\vd M\hastype 
% C$ and $\cD'::\GG;(\O,x\oftp 
% A);\D\vd M\hastype C$.
% \bit
% \itc 
% $$\cD'=\ianc{c\oftp C\in\Sigma}{\GG;(\O,x\oftp A);\cdot\vd c\hastype 
% C}{Con}$$
% but there can be no proof of $c\hastype C$ from $\GG;\O;x\oftp A$.
% \itc 
% $$\cD'=\ianc{}{(\GG,y\oftp C);(\O,x\oftp A);\cdot\vd y\hastype 
% C}{Id^{u}}$$
% but there can be no proof of $y\hastype C$ from $(\GG,y\oftp C);\O;x\oftp A$.
% \itc 
% $$\cD'=\ianc{}{\GG;(\O,x\oftp A);y\oftp C\vd y\hastype 
% C}{Id^{1}}$$
% but there can be no proof of $y\hastype C$ from $\GG;\O;(x\oftp A,y\oftp C)$.
% \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 A,y\oftp B)\vd M\hastype  C}
% {\GG;\O;(\D,x\oftp A)\vd\lamb{y^{1}}{B} M\hastype B\RImp C}{\RImp I}$$
% and
% $$\cD'= \ianc{\GG;(\O,x\oftp A);(\D,y\oftp B)\vd M\hastype  C}
% {\GG;(\O,x\oftp A);\D\vd\lamb{y^{1}}{B} M\hastype B\RImp C}{\RImp I}$$
% \btab
% $\GG;\O;(\D,x\oftp A,y\oftp B)\vd M\hastype  C$
% \` By inversion on $\cD$\\
% $\GG;(\O,x\oftp A);(\D,y\oftp B)\vd M\hastype  C$
% \` 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 A) \vd M \hastype A \RImp 
% B}{(\Gamma, \Delta'_M,x\oftp A); \Omega; \Delta_N \vd N \hastype A}{\Gamma; 
% \Omega; (\Delta'_M,x\oftp A, \Delta_N) \vd M\ N^1 \hastype B}{\GImp{1}E}
% $$ 
% and \\
% $\cD'=$
% $$ 
% \ibnc{(\Gamma, \Delta_N); (\Omega,x\oftp A); \Delta'_M \vd M \hastype A \RImp 
% B}{(\Gamma, \Delta'_M);( \Omega,x\oftp A); \Delta_N \vd N \hastype A}{\Gamma; 
% (\Omega,x\oftp A); (\Delta'_M, \Delta_N) \vd M\ N^1 \hastype B}{\GImp{1}E}
% $$
% \btab
% $(\Gamma, \Delta_N); \Omega; (\Delta'_M,x\oftp A) \vd M \hastype A \RImp 
% B$
%  \` By inversion on $\cD$\\
% $(\Gamma, \Delta_N); (\Omega,x\oftp A); \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 A)\vd M\hastype C$ and 
%$(\GG,\O,\D);x\oftp A;\cdot\vd M\hastype C$.
%\item
%It is not the case that both $\GG;(\O,x\oftp A);\D\vd M\hastype C$ and 
%$(\GG,\O,\D);\cdot;x\oftp A\vd M\hastype C$.
%\enen
%\end{Corollary}
% \begin{proof}
% By Lemma \ref{le:disj} and opportune Loosening$^{1}$ and 
% Loosening$^{0}$.
% \end{proof}

\newcommand{\er}[1]{\mid #1\mid_{\mbox{\tiny \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} & = & \lx\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]
%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$}

%Thus we assume we have canonical forms expressed

%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 logic 
%variables:

%\beq
%\ianc{\cdot;\cdot;\cdot\vd E_{A}\hastype A}{\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

The above results culminate in the Canonical Form Theorem: for every
term $M$ such that  $\god\vd M\hastype A$, there exists an $N$ in canonical
 form, denoted$\god\vd M\buda 
N\hastype A$, such that $M$ reduces to $N$.
%then there is $N$ such that $\god\vd M\buda 
%N\hastype A$.
% \ben 
% \item $\GG;\Omega;\Delta\prv M \da A$.
% \item $\GG;\Omega;\Delta\prv M \bua A$.
% \enen
%\end{Theorem}
% \begin{proof}
% A suitable reformulation of Tait's method along the lines of 
% \cite{Cervesato96phd}.
% \end{proof}

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


\section{Complement in Strict $\lambda$-Calculus}
\label{sec:strictcomp}
We require that our complement operator, denoted, say, $\mmnot$, satisfies the usual boolean 
rules for negation, that is:
\ben
\item (Exclusivity) 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 
Lemma \ref{le:disj}, it turns out that the exhaustivity does not hold in 
general as we allow undetermined function and logic variables in partially applied terms.  We 
must therefore isolate the right fragment of the strict calculus: 
this entails two separate phases:

\bit
\item restrict to a class of terms (that we call \emph{simple}) for
which exhaustivity holds.
\item
bring to full application those terms.
\enit

Note that the first item is not required for disjointness.


\subsection{Simple Terms}

We now address the issue of exhaustivity: once we have allowed 
existential variables,  we would like 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}\|\]

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}

The image of the embedding of the canonical forms of the simply-typed 
$\lambda$-calculus gives rise to the following fragment, which we 
call

\[ \begin{array}{rrcl}
\mbox{\textit{Simple Terms}} & M & \bnfas &  \lam x^{u}\oftp
A^{+}\ldot M \bnfalt (\dots (h\ M_1)^{1} \dots M_n)^{1} \bnfalt 
E_{A^{-}}\ \xn^u
\end{array} \]
We sometimes abbreviate $(\dots (h\ M_1)^{1} \dots M_n)^{1}$ as $h\ 
\Mns$.
\smallskip

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

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

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

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


\begin{Theorem}
\label{thm:embed}
If $\GG\vd M\buda A$ then $\ctx\vd M^{-}\buda A^{-}$. 
\end{Theorem}
% \begin{proof}
% By simultaneous 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.

Simple terms enjoy the required tightening property.

\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 such that $\cu\vd M\buda A$. Then 
 $\cxtr\vd M\buda A$ or $\cxto\vd M\buda A$.
\end{Lemma}
% \begin{proof}
% By simultaneous 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
% \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} and opportune 
% Loosening$^{0}$ and Loosening$^{1}$.
% \end{proof}


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

We describe in Fig.\ \ref{fig:trans} the judgment $\GG\emp\vd M\LBimp 
N$ which turns a term $M$ into an equivalent, yet 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.  We write $(Z\ \GG^{u})$ for $Z\ x_{1}^{u}\dots 
x_{n}^{u}$, where $x_{1}\dots x_{n}\in dom(\GG)$.  The notation 
$\pi(\GG)$ stands for a permutation of $dom(\GG)$.


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

We have now arrived to the following language, where the labeling 
on 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;\cdot;\cdot}
%\newcommand{\cgmom}{ \GG;\Omega;\cdot}

%\begin{Lemma}[Irrelevance]
%\label{le:fat}
%Suppose $M$ is simple:
%\ben
%\item
%If  $\cgm\vd M\da A$ then $\cgmom\vd M\da A$.
%\item
%If $\cgm\vd M\bua A$ then $\cgmom\vd M\bua A$.
%\enen
%\end{Lemma}
% 
% % proof for \newcommand{\cgm}{\GG;\cdot;\cdot}
% \begin{proof}
%  By simultaneous 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}{\cgm \prv  c\da A}{cIdc}$$
% Then
% $$\cE= \ianc{c\oftp A\in\Sigma}{\cgmom \prv  c\da A}{cIdc}$$
%  
% \itc  $$\cD = \ianc{}{(\GG, y\oftp A) ;\cdot; \cdot  \prv  y \da 
% A}{cId^{u}}$$
% Then, by Weakening$^{0}$ 
% $$\cE = \ianc{}{(\GG, y\oftp A); \O;\cdot  \prv  y\da 
% A}{cId^{u}}$$
% \itc $\cD$ ends in $Id^{1}$: vacuously true.
% 
% \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)\emp \prv M\bua B}{\cgm\prv(\lamb{y^u}{A} M) \bua 
% A\TImp B} {c\TImp I}$$
% \btab
% $(\GG,y\oftp A)\emp \prv M\bua B$\bv
% $(\GG,y\oftp A);\O;\cdot \prv M\bua B$ \bi\\
%  $\cgmom\prv(\lamb{y^u}{A} M) \bua A\TImp B$\br
%  \etab
%  
% \itc  $$\cD = \ibnc{\cgm \vd M \da A \RImp B}{\cgm \vd N \bua A}{\cgm \vd
% M\ N^1 \da B}{c\RImp E}$$
% \btab
% $\cD_{1}:: \cgm \vd M \da A \RImp B$\bv
% $\cD_{2}:: \cgm \vd N \bua A$\bv
% $\cE_{1}:: \cgmom \vd M \da A \RImp B$ \bi\\
%  $\cE_{2}:: \cgmom \vd N \bua A$\bi\\
% $\cgmom\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  $\GG\emp 
\prv M\in\| N\| : A$ formalizes conditions for  a simple term $M$ to be a 
ground instance of $N$ at type $A$.
\ignore{Note that $\GG\emp \prv M \in\| 
E_A\ \xnl\| : P$ if $M\equiv t \ \xnl$ and $\cdot\emp\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$.  This fact will be 
heavily used in the following. Moreover we write $\GG\prv M \not\in \| N \| :A$, when it is not the 
case that $\GG\prv M \in \| N \| :A$.

\begin{figure}
\label{fig:grinst}
\[
\begin{array}{c}
\ianc{M\equiv t \ \xnl  \quad \cdot\emp\prv  t \hastype A}
{\GG\emp \prv   M  \in\| E_A\ \xnl\| : P}{grFlx} 
\vsk
\ianc{(\GG,x\oftp A);\Omega;\Delta\prv   M  \in\| N\| : B}
{\GG\emp \prv  \lxua M  \in\|\lxua N \|:A\TImp B}{grLam}
\vsk
% \ianc{\GG\emp \prv h \oftp  A_1\RImp\mdots\RImp A_n \RImp P\quad \GG\emp \prv  \ M_1 \in\| 
% N_{1}\| : A_1\cdots \GG\emp \prv  M_n \in\| N_n\| : A_n }
%  {\GG\emp \prv  h\ \Mns \in\|h\ \Nns
% \| : P} {grApp}
\ianc{\GG\emp \prv h \oftp  A_1\RImp\mdots\RImp A_n \RImp P\quad \GG\emp \prv  \ M_i \in\| 
N_{i}\| : A_i\quad 1\leq i\leq n}
 {\GG\emp \prv  h\ \Mns \in\|h\ \Nns
\| : P} {grApp}
\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\emp\vd M \in \|N\| :C$ then $(\Gamma, x\oftp A)\emp\vd M 
% \in \|N\| :C$.
% \end{Lemma}
% \begin{proof}
% By induction on the structure of the given derivation.
% \end{proof}
% 
% We implicitly use the above lemma to opportunely weaken different 
% contexts with common basis to an unique one.
% 
 \smallskip Now we can prove the set-theoretic adequacy of the full 
application translation.

\begin{Theorem}
\label{thm:fat}
Let $N$ be a simple term (in canonical form) such that $\GG\emp \vd N 
\LBimp Q$; then $\GG\emp\vd M\in\|N\|\hastype A$ iff $\GG\emp \vd 
M\in \|Q\|\hastype A$.
\end{Theorem}
% \begin{proof}
% By induction on the structure of $\cD::\GG\emp\vd M\LBimp 
% N$.
% \bit
% \itc
% $\cD$ ends in $Trn\_Pat$:
% \item[$\Imp$]
%  $(\GG,\Omega)\emp\vd M \in \|E_{B}\ 
% \pi(\GG^{u})\|$ iff $M\equiv t\ \pi(\GG^{u})$ and $\cdot\emp\vd 
% t\hastype B$.  Thus $(\GG,\O)\emp \vd S\hastype A$.  By the canonical 
% form theorem (Theorem \ref{thm:canonical}) this implies 
% $(\GG,\Omega)\emp\vd S\buda A$.  Lemma \ref{le:fat} entails 
% $\GG;\Omega;\cdot\vd S\buda A$, which yields 
% $\GG;\Omega;\cdot\vd S\hastype A$.  Thus
% \ignore{ $M\equiv t'\ \GG^{u} 
% \Omega^{0}$ for $\cdot\emp\vd t'\hastype B'$, \ie}
%  $\GG\emp\vd M\in \|F_{B'}\ \GG^{u} \Omega^{0}\|$.
% \item[$\If$]
% Conversely, proceed similarly to the above, but using Loosening$^0$ 
% (Theorem \ref{thm:0loose}) and the canonical form theorem (Theorem 
% \ref{thm:canonical}) in place of Lemma \ref{le:fat}.
% \itc
% $\cD$ ends in $Trn\_Lam$ or $Trn\_Lam$:
% the result follows from a straightforward application of the inductive hypothesis.
% \enit\end{proof}
% 

\section{The Complement Algorithm}
\label{sec:compl}
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\quad
\mnot(0)  =  1\quad
\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\emp\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 unrestricted simple term (in canonical form) 
$M$ such that $\GG \prv  M \hastype  A$ define $\GG\prv  \mnot(M) = N : A$ as:

\begin{small}
\[
\begin{array}{c}
\ianc{1\leq i\leq n\quad k\in\{1,0\}} {\GG\prv \mnot(E \ x_{1}^{l_{1}}\dots x_{i-1}^{l_{i-1}} \ 
x_{i}^{k}\ x_{i+1}^{l_{i+1}}\dots x_n^{l_{n}}) = Z\ x_{1}^{u}\dots 
x_{i-1}^{u}\ x_{i}^{\mnot(k)}\ x_{i+1}^{u}\dots x_n^{u} : P} {\mnot\_Flx}
\vsk
\mbox{\textrm{no rule for } $k=u$}
\vsk
\ianc{\GG,x\oftp A\prv  \mnot( M)  =  N : B}
{\GG\prv  \mnot(\lxua M)  = \lxua N : A\Imp B}{\mnot\_Lam}
\vsk
\ianc{g\in\Sigma\cup\GG, g \hastype A_{1}\RImp\dots\RImp A_{m}\RImp 
P\quad m\geq 0,h \not\equiv g   } 
{\GG\prv  \mnot (h\ \Mn^1) = 
(\dots (g\ (Z_{1} \GG^{u}))^{1}\dots (Z_{m}\GG^{u}))^{1} : P} {\mnot\_App^{1}}
\vsk
\ianc{  \GG\prv \mnot( M_i) = N : A_i\qquad 1\leq i\leq n } 
{\GG\prv  \mnot (h\ \Mn^1) = 
(\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} : 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 define:
\beq 
\mmnot(M\hastype A) & =&  \{N\mid\cdot\prv \mnot(M)=N:A\}
\eneq
\end{Definition} 


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


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

%We can now revisit Example \ref{ex:etardx}:
\beq
\lefteqn{\mmnot(lam(\lamb{x^{u}}{exp} app\ (M\ x^{0}) x^{1} ))=}\\
& & \{ 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)= N\hastype A$, then  $N$ is simple.
% \end{Theorem}
% 
% \begin{proof}
% By induction on the structure of $\cD::\GG\vd\mnot(M)= N\hastype A$.
% % \begin{sloppy}
% \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}}) = Z\ x_{1}^{u}\dots 
% % x_{i-1}^{u}\ x_{i}^{\mnot(k)}\ x_{i+1}^{u}\dots x_n^{u} : P$ by rule , where the latter is simple.
% % \end{sloppy}
% \itc
% $$\cD=\ianc{\GG,x\oftp A\prv  \mnot( M)  =  N : B}
% {\GG\prv  \mnot(\lxua M)  = \lxua N : A\Imp B}{\mnot\_Lam}$$
% By inversion $\GG,x\oftp A\prv  \mnot( M)  =  N : B$, hence by IH $N$ 
% is simple and so is $\lxua N$.
% \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) = 
% (\dots (g\ (Z_{1} \GG^{u}))^{1}\dots (Z_{m}\GG^{u}))^{1} : P} {\mnot\_App^{1}}
% $$ 
% Since every $(Z_{i}\GG^{u)}$ is simple, so is $(\dots (g\ (Z_{1} 
% \GG^{u}))^{1}\dots (Z_{m}\GG^{u}))^{1}$.
% \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) = N : A_i \qquad 1\leq i\leq n} 
% {\GG\prv  \mnot (h\ \Mn^1) = 
% (\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} : 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{Theorem}
If $M$ is a simple term, so is $N$, for all $N\in\mmnot(M\hastype A)$.
\end{Theorem}

\medskip We address the soundness and completeness of the complement 
algorithm \wrt the set-theoretic semantics: the proof obligation 
consists in proving that the former does behave as a complement 
operation on sets of patterns. Termination is obvious, as in rules 
$\mnot\_Lam$ and $\mnot\_app^{2}$ The size of the term affected by the 
recursive call is clearly smaller. \ignore{We use the abridged notation 
$\GG\prv M\in\|\mnot(N)\| :A$ for $\GG\prv M\in \|Q\|:A$ where $ 
\GG\prv \mnot(N) = Q : A$. We may drop the type and signature 
information from the above judgment in proofs.  We abridge $\mnot(l)$ 
in $-l$. We start with soundness:}

%\begin{Theorem}
%\label{thm:part1}
%Assume there is a $Q$ such that $\GG\vd \mnot(N)=Q\hastype A$ for 
%$\GG\vd N\hastype A$ a simple unrestricted pattern: 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)=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\vd\mnot(N_i)= Q$ \`    By inversion  \\
% $\GG\vd h\ \ol{M_n^{1}}\in \|h\ \ol{N_n^{1}}\|$  \` By hypothesis\\
% $\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 hypothesis\\
% $\GG \prv M_{i}\in\|N_{i} \|$,  for $1\leq i\leq n$ \`    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) = \lxua Q$\bh
%  $\GG,x\oftp A\vd \mnot( N) = Q$\bv
% $\GG \prv \lxua M\in \| \lxua N\|$ 
% \` By hypothesis\\
%  $\GG \prv \lxua M\in \| \lxua Q\|$
% \` By hypothesis\\
% $\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}



%We are now ready to prove exhaustivity of complementation.

%\begin{Theorem}
%\label{thm:part2}
%Assume there is a $Q$ such that $\GG\vd \mnot(N)=Q\hastype A$ for 
%$\GG\vd N\hastype A$ a simple unrestricted pattern:  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 N\hastype A$ 
% %and $\cD'::\GG\vd M \in \| Q\|\hastype A$, where $\GG\vd \mnot(N)=Q$.
% \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^{1}$.
% \btab
% $\GG\vd\mnot(N_{i}) = Q$ \bv
% $\GG\vd h\ \ol{N_n^{1}}\hastype P$ \` By hypothesis\\
% $\GG\vd N_{i}\hastype A_{i}$ for $1\leq i\leq n$\`  By inversion \\
% $\GG \prv M_{i}\in \| N_{i} \| \hastype A_{i}$ for $1\leq 
% i\leq n$\`  By the left horn of IH \\
% $\GG \prv h\ \ol{M_n}\in \| h\ 
% \ol{N_n} \| \hastype P$\`  by rule $grApp$ \\
% $\GG \prv h\ \ol{M_n}\in \| 
% h\ \ol{N_n} \| \hastype P$ or \\
% % $\GG \prv h\ \ol{M_n}\in \| h\ 
% % (Z_{1}\GG^{u} )^{1}\dots (Z_{i-1}\GG^{u} )^{1}\ 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}\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\_App^{1}$.
% \btab
% % $\GG\vd\lxua N\hastype A\TImp B$\` By hypothesis\\
% %  $\GG, x\oftp A\prv N\hastype B$\`  by inversion\\
% $\GG,x\oftp A\vd\mnot(N)=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) = 
% % \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) = \lxua Q$ and $ \GG \prv \lxua M\in \|\lxua 
% % Q\| \hastype A\TImp B$\` 
% hence the thesis by weakening.
% \etab
% \enit
% \end{proof}

\begin{Theorem}[Partition] For a fixed signature $\Sigma$ let 
$\GG\vd N \hastype A$ be a unrestricted simple term:
\label{lemma:part}
\ben
\item (Exclusivity) 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{Theorem}
% \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}
Note that soundness is based on Corollary \ref{le:disj}, which holds 
for \emph{any} strict term: thus disjointness does not require simple 
terms, nor canonical forms. Exhaustivity requires instead Tightening,
\ref{le:exh} which holds only for simple terms.

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

We now address the issue of unification, \ie intersection of simple 
unrestricted \ho patterns.  We start by determining when two labeling are 
compatible: we define an intersection operator on occurrence labels as 
the symmetric and idempotent extension of the following partial 
operation: 
\beq
1\cap u = 1\quad 0\cap u = 0\quad 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:\ignore{ 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


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


\begin{small}
\[
\begin{array}{c}
\ianc{
% \Phi_1\mcap \Phi_2 = \Phi%\quad \Phi\not = nil
 }
{\GG\prv  E \ \Phi_1\mcap   F\ \Phi_2= H\ (\Phi_{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}=N_{1}\hastype A_{1}\cdots \GG\prv  H_n \ \Phi_{n}\mcap 
M_{n}=N_{n}\hastype A_{n}  } 
{ \GG\prv  E \ \Phi \mcap c\ \Mns= c\ \Nns\hastype  P} {\mcap\_FlxRgd^c }
\vsk
\ianc{y\in\GG\quad  \quad \GG\prv  H_1 \ \Phi_{1}\mcap 
M_{1}=N_{1}\hastype A_{1}\cdots \GG\prv  H_n \ \Phi_{n}\mcap 
M_{n}=N_{n}\hastype A_{n} } 
{\GG\prv E\ \Phi \mcap y\ \Mns= y\ \Nns \hastype  P} {\mcap\_FlxRgd^y }
\vsk
\ianc{ h\in\GG\cup\Sigma\quad \GG\prv  M_1 \mcap N_{1} = Q_1\hastype  A_1 \cdots \GG\prv  M_n \mcap 
N_{n}= Q_n \hastype  A_n} 
{\GG\prv   h\ \Mns\mcap h\ \Nns = h\ \ol{Q_{n}^{1}} \hastype  P} {\mcap\_App}
\vsk
\ianc{\GG,x\oftp A\prv   M  \mcap  N = Q\hastype  B}
{\GG\prv   \lxua M  \mcap \lxua N =\lxua Q \hastype  A\Imp B}{\mcap\_Lam}
\end{array}
\]
\end{small}
where  the $H$'s are fresh 
variables of correct  typing and $m\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
\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 unrestrictness we 
can always reorder the context to the same list.  
\item
Thanks to unrestrictness
again the flex-flex same variable case does not occur. 
\item 
In  rule $\mcap\_FlxRgd$ the proviso enforces the typing discipline, 
for which $x$ must be strict somewhere.
%  is compelled by the typing 
% rules not to leave the status of $x$ undetermined in the antecedent, 
% when $c$ is a constant.  
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.
\item
Rather than adding an  exchange rule.
%$$
%\ianc{ h\in\GG\cup\Sigma\quad  \GG\prv N\mcap h\ \Mns = Q\hastype  P} 
%{\GG\prv   h\ \Mns\mcap N = Q \hastype  P} 
%{\mcap\_Excng}$$
 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} = H\  x^{1}
& & x\oftp A\prv E''\ x^{u}\mcap\  F'\  x^{u} = H'\  x^{u}
\\
x\oftp A\prv E' \ x^{u}\mcap\  F\  x^{u} = H\  x^{u}
& & x\oftp A\prv E''\ x^{1}\mcap\  F'\  x^{u} = H'\  x^{1}
\end{array}
\]
Hence the result:
\beq
%\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\}
\eneq
\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} \mcap y\ (F\ y^{u})^{1} 
\ (F'\ y^{u})^{1}$ has no solution, whereas $y\oftp A\vd E\ y^{1} 
\mcap y\ (F\ y^{1})^{1} \ (F'\ y^{0})^{1}=y \ (H\ y^{1})^1 \ 
(H'\ y^{0})^1\ $.
\end{Example}

%{\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 $\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 $\god\vd y\ \hastype A_{1}\RImp\dots\RImp A_{n}\RImp B$ and 

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

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

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

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

%\begin{Corollary}
%\label{thm:soundec}
%If $\GG;(\O,\D^{u}_{i});\D_i^{1} \vd M_{i}\hastype A_{i}\quad 
%1\leq i\leq n$ then $\Gamma;\Omega; \D\vd c\ M_{1}^{1}\dots M_{n}^{1}\hastype 
%B$, where $\GG;\O;\cdot\vd c\ \hastype A_{1}\RImp\dots\RImp A_{n}\RImp B$ and 
%\ben
%\item 
%$\forall x\in\D.\exists i:1\leq i\leq n\,.\,x\in\D_{i}^{1}$.
%\item
%$\forall i:1\leq i\leq n\,.\,\in\D_{i}^{u}\cup\D_{i}^{1}=\D$.
%\enen
%\end{Corollary}
%\begin{proof}
%Use Lemma \ref{le:soundec} with $j=n$. Indeed, 
%$\D^{u}=\cdot,\D^{1}=\D$, conditions $1.$ and $2.$ are immediately 
%satisfied and condition $1'.$ is trivially true.
%\end{proof}




%% sound of proj

%\begin{Corollary}
%\label{thm:soundey}
%If $\GG;(\O,\D^{u}_{i});\D_i^{1} \vd M_{i}\hastype A_{i}\quad 
%1\leq i\leq n$ then $\Gamma;\Omega; \D\vd y\ M_{1}^{1}\dots M_{n}^{1}\hastype 
%B$, where $\god\vd y\ \hastype A_{1}\RImp\dots\RImp A_{n}\RImp B$ and 
%\ben
%\item 
%$\forall x\in\D.\exists i:1\leq i\leq n\,.\,x\in\D_{i}^{1}$.
%\item
%$\forall i:1\leq i\leq n\,.\,\D_{i}^{u}\cup\D_{i}^{1}=\D$.
%\item 
%$y\in\GG\cup\D$.
%\item 
%$y\in \D\Imp \forall i:1\leq i\leq n\,.\, y\in \GG$.
%\enen
%\end{Corollary}
%\begin{proof}
%Use Lemma \ref{le:soundey} with $j=n$. Indeed, 
%$\D^{u}=\cdot,\D^{1}=\D$, conditions $1.$ and $2.$ are immediately 
%satisfied and condition $1'.$ is trivially true.
%\end{proof}


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

%\begin{Lemma}
%\label{le:flexunif}
%$\GG\prv M\in\|E\ \Phi_{1}\|:P$ and $\GG\prv M\in\|F\ \Phi_{2}\|:P$ iff $\GG\prv 
%M\in\|H\ (\Phi_{1}\mcap \Phi_{2})\|:P$.
%\end{Lemma}
%\begin{proof}
%By simultaneous induction on $\Phi_{i}$, for $i \in\{1,2\}$.
%\bit
%\itc
%If $\Phi_{1}=\Phi_{2}=\cdot$, the result is immediate.
%\itc
%$\Phi_{i}$, can be written as 
%$\GG^{u}_{i},\Omega^{0}_{i},\Delta^{1}_{i}, x^{k_{i}}$. We proceed by 
%cases on $x^{k_{i}}$:
%\bit
%\item[$k_{1}=1,k_{2}=u$] $ (\Imp)$. Then $x^{1}\mcap x^{u}=x^{1}$ and 
%thus $\GG\vd M\in \|H\ 
%(\GG^{u}_{1}\mcap \GG^{u}_{2})\ (\Omega^{0}_{1}\mcap \Omega^{0}_{2}) \ 
%(\Delta^{1}_{1}\mcap \Delta^{1}_{2}) \ x^{1}\|$.

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

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

%\begin{theorem}
%\label{thm:unif1}
%Let $\GG\vd N_{1}\mcap N_{2}= 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}= N\hastype A$.
%\bit
%\itc $\cD$ ends in  $\mcap\_FlxFlx$; apply 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}} = c\ \Nns$\bh
%$\cD_i::\GG\vd E_{i}\ \Phi_i\mcap Q_i = N_i$ for $1\leq i\leq n$ \bv
%$\GG\vd M \in\|c\ \ol{Q_{n}^{1}}\|$\bh
%$M\equiv c\ \Mns$ and  $\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:invec})\\
%$\GG\vd M_{i}\in\|E_{i}\ \Phi_{i}\|$ \br\, $grFlx$\\
%$\GG\vd M_{i}\in\|N_{i}\|$\bi\\
%$\GG\vd c\ \Mns\in\|c\ \Nns\|$\br
%\etab
%\itc $\cD$ ends in  $\mcap\_FlxRgd^y$. Proceed as above, but using 
%Lemma \ref{le:}.

%\itc $\cD$ ends in  $\mcap\_Lam$:
%\btab
%$\GG\vd \lxua N_1\mcap \lxua N_2 = \lxua N$\bh
%$\GG,x\oftp A\prv N_{1}\mcap N_{2}=N$\bv
%$\GG\prv \lxua M\in\|\lxua N_{1}\|$ \bh
%$ \GG,x\oftp A\vd M\in\| N_{1}\|$\bv
%$\GG\prv \lxua M\in\|\lxua N_{2}\|$\bh
%$\GG,x\oftp A\prv M\in\| N_{2}\|$\bv

%$\GG,x\oftp A\prv M\in\| N\|$\bi\\
%$\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}= 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}= N$.
%\bit

%\itc $\cD$ ends in  $\mcap\_FlxFlx$; apply 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}} = c\ \Nns$\bh
%$\GG\vd c\ \Mns\in\|c\ \Nns\|$\bh
%$\GG\vd M \in\|c\ \ol{Q_{n}^{1}}\|$\bh
%$\GG\vd M_{i}\in\|N_{i}\|$,  for $1\leq i\leq n$ \bv
%$\GG\vd M_{i}\in\|E_{i}\ \Phi_{i}\|$ \bi
%$\GG\vd M_{i}\in\|Q_{i}\|$\bi\\
%$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 B$\` By  on rule $\RImp 
%E^{n}_{c}$ (Lemma \ref{le:soundec})\\
%$\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:}.
%\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{Theorem}[Adequacy of Pattern intersection]
\label{co:unif}
$\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{Theorem}

%\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 unrestricted terms of type $A$:
%\bit
%\item
%$ M\mbigcap M = \{M\} $.
%\item
%$ M\mbigcap N = N\mbigcap M$.
%\enit
%\end{Corollary}
% We will overload our notation in the definition of families, indexed 
% by types of complementation and intersection operations between 
% \emph{sets} of terms:
% 
% \beq
% \mmnot_{A}\{M_{1}\mdots M_{m}\} & = & \{N\mid\forall i\in[1,m]  N\in 
% \mnot(M_{i}:A)\}\\
% \{M_{1}\mdots M_{m}\} \mbigcap_{A} \{N_{1}\mdots N_{n}\} & = & 
% \{P\mid \forall  i\in[1,m], \forall  j\in[1,n] : M\in M_{i}, 
% N\in N_{j}, P \in M\mbigcap N : A\}
% \eneq

\section{The Algebra of Strict Terms}
\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}

It can be shown that 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 unrestricted simple term of type $A$:
%\label{co:setpart}
%\ben
%\item (Disjointness) It is not the case that $\GG\prv  M\in \| N \|\hastype A$ and 
%$\GG\prv  M\in \| \mna(N) \|\hastype A$.
%\item (Exhaustivity) $\GG\prv  M\in \| \cN \| \hastype A$ or $\GG\prv  M\in \| 
%\mna(\cN) \|\hastype A$.

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



%\begin{metanote} An involution example from etaredex\end{metanote}



%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}\}$$
%We can therefore combine Example \ref{ex:lam} and \ref{ex:etared}:
%\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

\ignore{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,\bigcup,\mbc,\mna\ra$ under set union, patterns 
intersection and complementation.

%\begin{theorem}
%\label{thm:algebra}
%Consider the algebra  $\la \mathbf{\cal 
%T}_{\Sigma},\emptyset,\bigcup,\mbc,\mna\ra$ under set union, patterns 
%intersection and complementation. Then the following holds:
%\ben
%\item
%$\cM\mbc\cM = \cM$.
%\item
%$\cM\mbc\cN = \cM\mbc\cN$.
%\item\label{it:DM}
%$\cM\mbc(\cN\cup\cP)= (\cM\mbc\cN)\cup(\cM\mbc\cP)$.
%\item
%$\cM\mbc(\cN\mbc\cP) = (\cM\mbc\cN)\mbc\cP$.
%\item
%$\mna\mna \cM=\cM$.
%\item
%$\mna \mathbf{\cal 
%T}_{\Sigma}= \emptyset$.
%\item
%$\mna \emptyset=\mathbf{\cal 
%T}_{\Sigma}$.
%\enen
%\end{theorem}
%\begin{proof}\mbox{}
%\ben
%\item
%From idempotency of $\mcap$, Corollary \ref{co:unifpr}.
%\item
%From commutativity of $\mcap$, Corollary \ref{co:unifpr}.  
%\item 
%Immediate from Corollary \ref{co:setunif} and properties of 
%set-theoretic union.
%\item 
%By induction on $\cP$.  If the latter is empty, the result is 
%immediate.  Otherwise $\cM\mbc(\cN\mbc 
%\{M\}\cup\cP)=\cM\mbc((\cN\mbc\{M\})\cup(\cN\mbc\cP)) = 
%(\cM\mbc(\cN\mbc\{M\}))\cup)\cM\mbc(\cN\mbc\cP))$ by two application 
%of (\ref{it:DM}).  Then, by IH, 
%$(\cM\mbc\cN)\mbc\{M\}))\cup)(\cM\mbc\cN)\mbc\cP))$ and by 
%(\ref{it:DM}) again conclude $(\cM\mbc\cN)\mbc \{M\}\cup\cP)$.  
%\item
%$\GG\vd M\in \|\mna\mna \cM\|$ iff by Corollary \ref{co:setpart} 
%$\GG\not\in\|\mna \cM\|$ iff, again by Corollary \ref{co:setpart} 
%$\GG\vd M\in \|\cM\|$.
%\item
%Immediate from Corollary \ref{co:setpart}.
%\item
%Immediate from Corollary \ref{co:setpart}.
%\enen
%\end{proof}


\begin{Corollary}
\label{co:boolean}
The algebra $\la \mathbf{\cal T}_{\Sigma},\emptyset,\bigcup,\mbc,\mna\ra$ 
of simple unrestricted 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}



%%%%%%%%%%%%%%
\section{Applications}
\label{sec:appl}
The transformational approach to negation in \lp 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
\bit
\item
Compute complement of heads of clauses in the predicate definition
\item 
Bring definition in negation normal form respecting the operational 
semantics 
\enit

While this approach has been investigated for \fo Horn clauses 
\cite{Sato84,Bar90} and CLP programs \cite{Bruscoli94}, the field is 
almost virgin \wrt \ho logics and logical frameworks.  For the latter 
this notion of intensional negation is the most adequate, see 
\cite{Momigliano99www} for a discussion.  For example, consider the 
following program:
\[
\begin{array}{lll}
betarx & : & isredx(app\ (lam\ (\lamb{x^u}{exp} E\ x^u))\ F )\\
etarx & : & isredx(lam(\lamb{x^u}{exp} app\ M\ x^u))
\end{array}\]

We can compute
\[
\begin{array}{lll}
\mmnot\{(app\ (lam\ (\lamb{x^u}{exp} E\ x^u))\ 
F),lam(\lamb{x^u}{exp} app\ M\ x^u)\}
=\\
\quad \mmnot(app\ (lam\ (\lamb{x^u}{exp} E\ x^u))\ 
F)\mbc \mbox{}\\
\quad \mmnot(lam(\lamb{x^{u}}{exp} app\ (M\ x^{0}) x^{1} ))=\\

\qquad \{ lam\ (\lamb{x}{exp} H\ x), app\ (app\ H_{1}\ H_{2})\ H_{3}\}
\mbc \mbox{}\\
\qquad \{ lam(\lamb{x^u}{exp} app\ (H\ x^1)\ H,\\
\quad\qquad lam(\lamb{x^u}{exp} app\ (H\ x^u)\ (app\ H_4\ H_5)), \\
\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_4\ x^{u} H_5\ x^{u})),\\
\qquad\qquad lam(\lamb{x^u}{exp} app\ (H\ x^u)\ ( lam(\lamb{y^u}{exp} H_6\ x^u\ y^u))\\
\qquad\qquad  lam(\lamb{x^u}{exp} lam(\lamb{y^u}{exp} H_3\ x^u\ y^u) ),\\
\qquad\qquad app\ ( app\ H_1\ H_2) H_{3}\}
\end{array}
\]
Yielding the program: 

\[
\begin{array}{lll}
nb1 & : & non\_isredx(lam(\lamb{x^u}{exp} app\ (H\ x^1)\ H'\ x^{u}))\\
nb2 & : & non\_isredx( lam(\lamb{x^u}{exp} app\ (H\ x^u)\
 (app\ H_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) ))\\
nb5 & : & non\_isredx( app\ (app\ H_{1}\ H_{2})\ H_{3}\ )
\end{array}\]



\section{Conclusion}
\label{sec:concl}
We have shown that the complement of unrestricted 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}.

\noindent
{\bf Acknowledgments} We are grateful to Iliano Cervesato, Carsten Sch\''{u}rmann
and Roberto Virga for useful comments to previous version of this paper.
This work has been partially supported by NSF
Grant CCR-9619584.

\bibliography{iclp,not,framework,strictness,strict}
 
 \end{document}
