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

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

Perhaps the most fundamental problems are matching and unification, but
other questions such as generalization or complement also arise
frequently.  In this paper we are concerned with the problem of pattern
complement in a setting were patterns may contain binding operators,
so-called \emph{higher-order
patterns}~\cite{Miller91jlc,Nipkow91lics}.  Higher-order patterns
have found applications in logic
programming~\cite{Miller91jlc,Pfenning91lf,Michaylov93}, logical
frameworks~\cite{Despeyroux97}, term rewriting~\cite{Nipkow93tlca}, and
functional logic programming~\cite{Hanus96RTA}.  Higher-order patterns
inherit many pleasant properties from the first-order case.  In
particular, most general unifiers~\cite{Miller91jlc} and least general
generalizations~\cite{Pfenning91lics} exist, even for complex type
theories.

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

This formulation of the problem immediately suggests that we should
consider a $\lambda$-calculus with an internal notion of
\emph{strictness} so that we can directly express that a term must
depend on a given variable.  For reasons of symmetry and elegance we
also add the dual concept of \emph{invariance} expressing that a given
term does not depend on a given variable.  As in the first-order case,
it is useful to single out the case of \emph{linear patterns}, namely
those where no existential variable occurs more than once.  We show that
patterns in our calculus have the following properties:
 \begin{enumerate}
  \item The complement of a linear pattern is a finite set of
linear patterns.
  \item Unification of two patterns is decidable and leads
to a finite set of most general unifiers.
 \end{enumerate}
 Consequently, finite sets of linear patterns in the strict
$\lambda$-calculus are closed under complement and unification.  If we
think of finite sets of linear patterns as representing sets of ground
terms (the union of all ground instances), then they form a boolean
algebra under simple union, intersection (implemented via unification)
and the complement operation

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

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

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

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

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

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



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

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

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

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

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

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


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

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

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

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

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

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

We denote existential variables of type $A$ (also called logical
variables, meta-variables, or pattern variables) by $E_A$, although we
mostly omit the type $A$ when it is clear from the context.  We think of
existential variables as syntactically distinct from bound variables or
free variables declared in a context.  A term possibly containing some
existential variables is called a \emph{pattern} if each occurrence of
an existential variable has the form $E\ x_1\ldots x_n$, where the
arguments $x_i$ are distinct occurrences of free or bound variables (but
not existential variables).

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

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

While, as  we will see, the class of patterns is \emph{not} closed
under complement, a special subclass is.  We call a canonical
pattern $\Gamma \vd M \hastype A$ \emph{fully applied} if each
occurrence of an existential variable $E$ under binders $y_1,\ldots,y_m$
is applied to some permutation of the variables in $\Gamma$ and
$y_1,\ldots,y_m$.  Fully applied patterns play an important role in
functional logic programming and rewriting~\cite{Hanus96RTA} because any
fully applied existential variable $\Gamma \vd E\ x_1\ldots x_n$
denotes all canonical terms with free variables from $\Gamma$.
It is this property which makes complementation particularly simple

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

% \begin{example}
% \label{ex:lam}
% Suppose we want to encode predicates on the signature of the (untyped) 
% $\l$-calculus.  To distinguish between the former and the 
% meta-language we introduce the following signature, which 
% declares constants of well-known meaning and type (see 
% \cite{Pfenning94un}).
% \beq
% \Sigma  & \bnfas & exp\hastype \mbox{\textrm{type}}, lam\hastype (exp\Imp 
% exp)\Imp exp, app \hastype exp \Imp exp\Imp exp\\
% E & \bnfas & x \mid lam\ (\lx E) \mid app \ E_{1} E_{2}
% \eneq
% As usual with \ho abstract syntax \cite{Pfenning88pldi}, we identify the name of 
% (bound) variables in both languages.  \ignore{It is maybe worthwhile 
% to stress that we have three layers: the object language, the 
% (untyped) $\l$-calculus, the meta-language, our \ho logic or type 
% theory (whose variables are called \emph{logical} variables) and the 
% meta-meta language, the informal mathematical one used to describe the 
% former.   The adequacy of the encoding (proved for \emph{Mini-ML} in 
% \cite{Pfenning94un}) bijectively relates $\alpha$-equivalence classes 
% of object-level terms with $\beta\eta$-equivalence classes at the 
% meta-level.}  
% Suppose  we wish to encode a $\beta$-redex (in the object language):
% \beq
% \rep{ (\lx E)\ F} & = & app\ (lam\  (\lamb{x}{exp} (E\ x))\ F
% \eneq
% Its complement denoted, say $\mmnot$, in the given signature, contains every top-level lambda abstraction plus every 
% applications where the first argument is not a lambda: 
% \[
% \mmnot(app\ (lam\ (\lamb{x}{exp} (E\ x))\ F)= 
% \{ lam\ (\lamb{x}{exp} H\ x), app\ (app\ H_{1}\ H_{2})\ H_{3}\}
%  \]
% \end{example}


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

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

%  \begin{example}
% Consider the set of terms representing a
% unary function which does not depend on its argument:
% \beq
% % \begin{equation}
% \label{eq:vac}
% \lx E
% % \end{equation}
% \eneq
% Intuitively its complement should be the set of terms encoding the 
% functions which  do use, somehow, its arguments. 
%  \end{example}
 
Note that there is no finite set of patterns which has as its ground
instances exactly those terms $M$ which depend on a given variable $x$.
Following standard terminology, we call such terms \emph{strict in $x$} and
the corresponding function $\lamb{x}{A} M$ a \emph{strict function}.  As the
example above shows, the complement of patterns which are not fully applied
can therefore not be represented as a finite set of patterns.  This failure
of closure under complementation cannot be avoided similarly to the way in
which left-linearization bypasses the limitation to linear patterns and it
needs to be addressed directly.

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

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

%  While it is easy to write
% a logic program which verifies the former,
% \ignore{\[
% \begin{array}{lll}
% strict(\lx x).\\
% strict(\lx app (E_{1} x) (E_{2} x)) 
%    &\If & strict(\lx E_{1} x) .\\
% strict(\lx app (E_{1} x) (E_{2} x)) 
%    &\If &  strict(\lx E_{2} x).\\
% strict(\lx all (\l y. (E x y))) &\If & \PI {z} { exp}  strict(\lx (E x z)).
% \end{array}
% \]
% Hence the complement of a fact would lead to possibly hypothetical 
% and parametrical clauses.  More in general, we would have to decorate 
% programs with predicates} we are unable to directly represent the complement of non-fully 
% applied patterns.  In other words, the simply typed 
% $\l$ calculus, or, for that matter, every other intuitionistic type 
% theory 
% % \begin{metanote}
% % are we implying that strictness, encoded as an 
% % arithmetic property is not a relation expressible in say CC? It may 
% % not be extended polynomial, though
% % \end{metanote}
% is not strong enough to make straightforwardly available a notion of 
% \emph{strictness} which is required to represent the complement of non-fully 
% applied patterns and, we conjecture, any other non-fully applied 
% expressions built out of a meta-linguistic binding operator.  This 
% failure of closure under complementation cannot be avoided similarly 
% to the way in which left-linearization bypasses the limitation to 
% linear terms and it needs to be addressed directly.

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

% Since we live in a typed world, we are going to use typing to  
% express that a function \emph{must} or \emph{must not} depend on its 
% argument(s).  In the 
% next section we develop such a $\lambda$-calculus and generalize the 
% complement algorithm to work on such terms.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\end{figure}


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

Let us go through the typing rules in detail.  The requirement for the
strict context $\Delta$ to be empty in the $Id^u$ and $Id^1$ rules expresses
that strict variables must be used, while undetermined variables in $\Gamma$
or irrelevant variables in $\Omega$ can be ignored.  Note that there is no
rule for irrelevant variables, which expresses that they cannot be used.

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

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

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

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

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

% Let us go through the typing rules in details.  The requirement for the strict context $\Delta$ to
% be empty in the $Id^u$ and $Id^1$ rules expresses that strict variables
% must be used, while unrestricted or irrelevant variables can be ignored.
% Note that there is no rule for variables $x^0$, which expresses that
% they cannot be used.

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

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

% In the typing judgment for our calculus there are a few choices.  
% Namely, we could decide that that argument $N$ in an application $M\ 
% N^0$ does not need to be well-typed, since it will never be used.  
% Instead, we choose to verify it, so that we can always obtain a valid 
% term in the simply-typed $\lambda$-calculus by erasing all labels (see 
% Theorem \ref{thm:erase}.  Irrelevant variables $x^0$ may still occur, 
% but only in ignored arguments to invariant functions.

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


Our strict $\lambda$-calculus satisfies the expected properties,
culminating in the existence of canonical forms which is critical for
the intended applications.  We begin with the following:

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

\begin{metanote} Worth mentioning?\\
Note that, although typing 
is unique, the typing derivation may 
 not.  
\begin{Theorem}[Uniqueness of Typing]
\label{thm:uniqueT}
If $\god\vd M\hastype A$ and  $\GG';\O;\D'\vd M\hastype A'$, then $A\equiv A'$.
\end{Theorem}
\begin{proof}
By induction on the structure of the given derivations, exploiting 
`functionality' of signatures and contexts.
\end{proof}
\end{metanote}

We start addressing the structural properties of the context(s).  
Exchange is directly built into the formulation and will not be 
repeated.  We use $[N/x]M$ for the result of the capture-avoiding 
substitution of $N$ for $x$ in $M$.


 \begin{Theorem}[Weakening] \mbox{}
 \label{thm:weak}
 \begin{enumerate}
  \item (Weakening$^{u}$) If $\Gamma; \Omega; \Delta\vd M \hastype A$ then $(\Gamma, 
  x\oftp C); \Omega; \Delta\vd M \hastype A$. 
  \item (Weakening$^{0}$) 
  If $\Gamma; \Omega; \Delta\vd M \hastype A$ then $\Gamma
  ; (\Omega, x\oftp C); \Delta\vd M \hastype A$. 
  \end{enumerate}
  \end{Theorem}
 
\begin{proof}
By induction on the structure of the given derivation. 
\end{proof}
 
 
The following properties allow us to lose track of dependencies, if 
we are so inclined.

\newcommand{\gofd}{\GG;(\Omega,x\oftp C);\Delta}
\newcommand{\gfod}{(\GG,x\oftp C);\Omega;\Delta}
\newcommand{\bv}{\` By inversion\\}
\newcommand{\bi}{\` By HI }
\newcommand{\bh}{\` By hypothesis\\}
\newcommand{\ba}{\` By assumption\\}
\newcommand{\br}{\` By rule}
\newcommand{\xoc}{x\oftp C}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

\begin{proof}
By  induction on the structure of $\cD ::\godx\vd M\hastype  A$.
\bit
\itc $\cD$ ends in  $Con,Id^{u}$: vacuously true.
\itc  $$\cD = \ianc{}{\Gamma;\Omega;x\oftp A\prv  x\hastype  A}{Id^{1}}$$
Then
$$\cE=\ianc{}{(\Gamma,x\oftp A);\Omega;\cdot\prv  x\hastype  A}{Id^{u}}$$

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

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

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

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

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


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

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

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

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

\item[\textbf{$x\in \D_{M_2}$}] Symmetrical to the above.
\enit
\enit
\enen   % 123sub
\end{proof}


\begin{Theorem}[Contraction] 
Let $z$ be a fresh variable of type $A$:
\label{thm:contr}
\begin{enumerate}
\item (Contraction$^{u}$)
If $(\Gamma, x\oftp A, y\oftp A);\Omega;\Delta \vd M
\hastype C$, then\\  $(\Gamma, z\oftp A) ;\Omega;\Delta\vd [z/y][z/x]M \hastype C$.
\item  (Contraction$^{0}$)
If $\Gamma; (\Omega, x\oftp A, y\oftp A);\Delta \vd M
\hastype C$ then\\  $\Gamma;(\Omega, z\oftp A);\Delta \vd [z/y][z/x]M \hastype C$.
\item  (Contraction$^{1}$)
If $\Gamma;\Omega;(\Delta, x\oftp A, y\oftp A ) \vd M
\hastype C$ then\\  $\Gamma;\Omega;(\Delta, z\oftp A) \vd [z/y][z/x]M \hastype C$.
\end{enumerate}
\end{Theorem}
\begin{proof}
\ben\mbox{}
\item
\btab
$(\Gamma, x\oftp A, y\oftp A);\Omega;\Delta \vd M\hastype C$
\` By assumption\\
$(\Gamma, x\oftp A,\D, z\oftp A);\Omega;\cdot \vd z\hastype A$
\` By rule\\
$(\Gamma, x\oftp A, z\oftp A);\Omega;\Delta \vd [z/x]M\hastype C$
\` By Substitution$^u$\\
$(\Gamma, \D, z\oftp A);\Omega;\cdot\vd z\hastype A$
\` By rule\\
$(\Gamma,  z\oftp A);\Omega;\Delta \vd[z/y] [z/x]M\hastype C$
\` By Substitution$^u$
\etab
\item
Similarly, using Substitution$^0$.
\item
Similarly, using Substitution$^1$.
\enen
\end{proof}
 

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

\[ \begin{array}{rcl}
   (\lam x^k\oftp A\ldot M)\, N^k & \betared & [N/x]M \\
   [1ex]
   M \hastype A \GImp{k} B & \etaexp & \lam x^k\oftp A\ldot M\  x^k \\
\end{array} \]
 g
Indeed one of the main features of   irrelevant variables, as 
ones which \emph{may} occur but \emph{must not} be used, is to 
well-type $\eta$-expansion of invariant functions:

\[ \begin{array}{rcl}
M \hastype A \GImp{0} B & \etaexp & \lam x^0\oftp A\ldot M\ x^0 \\
\end{array} \]
  
The subject reduction and expansion theorems are an immediate consequence 
of the structural and substitution properties.

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

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


% \subsection{Properties of Contexts}

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

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

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

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

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

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