\section{Complementing Higher-Order Patterns}

\renewcommand{\S}{\Sigma}

In this section we introduce a generalization to the complement 
algorithm for the \ho case to patterns. 

\begin{Definition}[Pattern]
A term $M$ in canonical form is a \emph{\ho pattern} if every free 
occurrence of a variable $F$ is in a subterm $F(\xn)$ of $M$ such 
that $\xn$ is a list of distinct bound variables.
\end{Definition}

We assume the following:
 \bit
\item
All terms are linear \ie free variables occurs only once.  
\item 
Types do not contain occurrences of the primitive type $o$.  We 
thus complement only terms with no inner logical structure.  The kind 
of programs that we discuss here do not require predicate 
quantification.  Note of course that this is the restriction intrinsic 
in the \emph{LF} type theory and implemented in \emph{Elf}.  
\enit 

As we said, the treatment differentiates depending on whether the term 
to be complemented is \emph{fully applied} or not, which we define in 
Figure \ref{fig:fa}.  In the latter case the complement has to take 
into account whether some of the variables mentioned in a lambda 
binder does appear in the matrix.  For fully applied terms instead, we 
proceed similarly to \fo with an additional case for lambda 
expressions and bound variables: those are collected in a context 
$\GG$, so that the complement of a rigid term is taken \wrt both the 
signature and the current context.  We first analyze this case.

\newcommand{\fa}{ \,\ \mbox{\rm {f.a.}}}
\begin{figure}
\label{fig:fa}  
\[
\begin{array}{c}
\ianc{\ol{x_{\pi(n)}}=\GG}{\GG\prvs  F\ \xn \fa }{\mbox{\rm fa\_Pat}} 
\qquad 
\ianc{ \GG,\of{x}{A}\prvs  M \fa }{\GG\prvs \lxa M \fa }
{\mbox{\rm fa\_Lam}}\vsk
\ianc{ h \in\Gamma\cup\Sigma \qquad \GG\prvs  N_{1} \fa
\cdots \GG\prvs  N_{n} \fa}
{\GG\prvs h\  \Nn \fa } {\mbox{\rm fa\_App}}
% \vsk
% \ianc{x\in\GG}{\GG \prvs  x \fa }{\mbox{\rm fa\_Var}} 
% \qquad 
% \ianc{c\in\Sigma}{\GG \prvs  c \fa }{\mbox{\rm 
% fa\_Const}}
\end{array}
\]
\caption{Judgment 
$\GG\prvs  M \fa$: $M$ is a fully applied pattern}
\end{figure}

Simple types:
\beq
A & \bnfas & P\mid A\Imp B
\eneq

Signatures, as usual, declare constants. 
\beq
\Sigma & \bnfas & \cdot\mid \Sigma, c:A
\eneq
Contexts for parameters are \textbf{sets}; this builds in contraction, but not weakening;
exchange is immaterial, since there is no ordering.
\beq
\GG  & \bnfas &  \cdot\mid \GG , x:A
\eneq
We assume `functionality' of context and signatures, \ie every token 
is declared uniquely (even though possibly several times).  Moreover 
we consider logical variables to be typed `from the outside', \ie 
before parameters are introduced; this is possible as simple types do 
not introduce dependencies and all context have therefore a $\Sigma 2$ 
format.  \ignore{A more rigorous approach might require Miller's \emph{mixed 
prefixes} \cite{Miller92jsc}}. Finally we say $h\in\GG\cup\Sigma$ to abbreviate 
$h\in (dom(\GG)\cup dom(\Sigma))$.

\newcommand{\ng}{\GG\prv\mnot}

\begin{Definition}[Fully applied \ho pattern complement]
\label{def:fa-compl}
Fix a signature $\Sigma$.  For a fully applied \ho linear pattern in canonical 
form $M$,  define $\ng(M: A)$ as:

% \newcommand{\diff}{{\textrm diff}}

\[\begin{array}{lll}
\ng(E\ \xn : P) & = & \eset \\ %& \mbox{\rm if $$ is fully applied} 
\ng (h\ M_{1}\dots M_{m}: P) & = & diff_{\GG}(h:\ol{A_{m}}\Imp P) \cup 
\mbox{}\\
& &
\{h\ (Z_{1}\GG)\dots (Z_{i-1}\GG), N, (Z_{i+1}\GG)\dots (Z_{m}\GG)\mid 
\\
& & N\in\ng(M_{i}:A_{i}), 1\leq i\leq m \} \\
\ng(\lxa M:A\Imp B) &  = & \{ \lxa N \mid N\in (\GG,x:A\prv \mnot(M:B)) \}
\end{array}\]
where the $Z$'s are fresh variables of opportune typing, $m\geq 0$ and
\beq 
diff_{\GG}(h:\ol{A_{m}}\Imp P) & = & \{g\ (Z_{1} \GG)\dots (Z_{n}\GG) \mid 
g\in\Sigma\cup\GG, g : \ol{A_{n}} \Imp P, n\geq 0,h \not\equiv g \}
\eneq
\end{Definition} 
Remark that the definition makes an essential use of the fact that 
$M$ is canonical and thus its matrix has atomic type $P$.

\begin{Corollary}
For $c\in\GG\cup\Sigma,  \ng(c:P) = diff_{\GG}(c:P)$.
\end{Corollary}
\begin{proof}
Consider the $0$-ary application case.
\end{proof}

We will suppress mention of the type in $\ng(M:A)$ when it can be 
inferred from the context.

\begin{Examplen} 
Suppose we want to model predicates on the signature of the (untyped) 
$\l$-calculus.  To distinguish between the former and the 
meta-language we introduce the signature $\Sigma_{lam}$, which 
declares constants of well-known meaning and type (see 
\cite{Pfenning94un}).
\beq
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.  

Imagine we want to negate the identity predicate on unary 
function types:
\[
id(\l x.x).
\]
The intuitive answer is as follows:
\[
\begin{array}{l}
\neg id(\l x. app \ (E_{1} x) (E_{2} x)).\\
\neg id(\l x. lam \ (\l y .\ (E  x)y)).
\end{array}
\]
This follows from the computation of $\cdot\prv\mnot(\of{\lx 
x}{exp\Imp exp})$:
%  we gloss over the type of variables in the context.
\beq
\cdot\prv\mnot(\lx  x) & = & \{\lx N\mid N\in (x:exp\prv\mnot(x))\}\\
& = & \{\lx N\mid N\in diff_{x:exp}(x:exp))\}\\
& = &  \{\lx N\mid N\in \{app \ (E_{1} x) (E_{2} x),lam \ (\l y .\ (E  
x)y) \} \}\\
& = & \{ \lx app \ (E_{1} x) (E_{2} x) , \lx lam \ (\l y .\ (E  x)y)\}
\eneq
\end{Examplen}

If the term to complement is complex, we need to call the \mnot
algorithm recursively as many times as its depth.  Let us see another 
example that requires two calls:
\marginpar{may be dropped}
\newcommand{\lf}{\l f\! . \, }
\begin{Examplen}
Take the signature of numerals:
\beq
N  &\bnfas & 0 \mid s(N)
\eneq
and the problem $\cdot\prv\mnot(\lf  f 0: (nat\Imp nat)\Imp nat)$.  
\beq
\cdot\prv\mnot(\lf  f 0) & = & \{\lf N\mid N\in (\of{f}{n\Imp n}\prv\mnot(f\ 
0))\}\\
& = &   \{\lf N\mid N\in diff_{f}(f)\cup  \{f\ N'\mid N'\in 
(\of{f}{n\Imp n}\prv\mnot(0)) \} \}\\
& = &   \{\lf N\mid N\in \{0,s(N_{1}\ f)\} \cup \{ f\ N' \mid N'\in \{f(N_{2}\ f),s(N_3\ 
f)\} \}\\
& = &   \{\lf 0,\lf s(N_{1}\ f), \lf f(f(N_{2}\ f)), \lf f(s(N_{3}\ f))\}
\eneq
\end{Examplen}


\section{Non-Fully Applied Terms}

Consider a predicate on the  signature $\Sigma_{lam}$ true if a 
unary function does not depend on its argument:
\marginpar{assumes the logic programming application}
\begin{equation}
\label{eq:vac}
vacous(\lx E).
\end{equation}

Intuitively the complement should be a predicate, say \texttt{strict}, 
true when the function does use, somehow, its arguments.
\[
\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 lam (\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 discriminating when a pattern is fully 
applied or not.  It is clear that the simply typed $\l$ calculus, or, 
for that matter, every other intuitionistic type theory is not strong 
enough to represent the complement of non-fully applied 
patterns\footnote{and, I suspect, any other non-fully applied 
expression built out of a 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.

We can instead internalize the (in)dependency constraints in a type 
theory which explicitly take into account the occurrence issue, 
acknowledging the similarity with having type information as 
predicates in logic programs.  The natural choice is a calculus of 
strict types and is formalized in Section \ref{stricttypes}.  We first 
give an informal presentation: we can introduce a strict application 
primitive constructor (and an abstractor), say $F\rapp x$, which 
express the fact that $F$ \emph{must} use an argument $x$ mentioned in 
the context.  Thus for example, the complement of $\mnot(\lx E) = \lx 
F\rapp x$.  Therefore, the complement of (\ref{eq:vac}) is:
\[
\neg vacous(\lx F\rapp x).
\]  

\ignore{We can go farther and recover the above definition of \texttt{strict} 
by `partially evaluating' $E$ against its signature:
\beq
\lefteqn{\cdot\prv\mnot(\lx E)  \Lmap}  \\
% & \lx x \Or \lx app\ (F_{1} \rapp x) (F_{2} x) \Or \lx app\ (F_{3} x) 
% (F_{4}\rapp x) \Or \lx lam\ (\l y.  (F\rapp x)y).
& \{\lx x,   \lx app\ (F_{1} \rapp x) (F_{2}\ x),   \lx app\ (F_{3} \ x) 
(F_{4}\rapp x),   \lx lam\ (\l y.  F\rapp x\ y)\}.
\eneq
thus yielding:
\[
\begin{array}{l}
\neg vacous(\lx x).\\
\neg vacous(\lx app\ (F_{1}\rapp  x) (F_{2}\ x)). \\
\neg vacous(\lx app\ (F_{3}\ x) (F_{4}\rapp x)). \\
\neg vacous(\lx lam\ (\l y. F\rapp x\ y)).
\end{array}
\]
}

Conversely, taking the complement of terms where arguments \emph{must} occur 
yields terms where each argument \emph{may} occur: for example
\beq 
\cdot\prv\mnot(\l xy.  E \rapp y \rapp x) & = & \{\l xy.  F, \l 
xy.F_{1}\rapp x y, \l xy.  F_{2} x \rapp y\} 
\eneq 

\ignore{It is clear that, as far as non-fully applied patterns, 
complementation does not preserve typing, though it induces a neat 
transformation discussed in Proposition \ref{ppn:nottype}.  Indeed, as 
we will see, $\lx E$ has type $exp\ZImp exp$ while its complement $\lx 
F\rapp x$ has typing $exp\RImp exp$.}

\ignore{
\textbf{A first try.} Let $\xn,\ol{y_{m}}$ be two list of variables 
such that for the underlying subsets $\ym\subseteq\xn$.  Let $\zp$ be 
the set-theoretic complement of $\ym$ in $\xn$, that is $\ym\cup\zp = 
\xn$.  We first treat the intuitionistic application  case. The complement of 
$\l \xn.E \ \ym)$ is the set of terms that \emph{may} depend on $\ym$ 
but \emph{has} to depend on one of the $\zp$'s, that is $p$ terms such that
\beq
\GG\prv\mnot(E\ \ol{y_{m}}) & = &  \bigcup\limits_{j=1}^{p} 
\{E_{j}(\ym,z_{1}\mdots z_{j-1}\mbox{} \rapp z_{j},z_{j+1}\mdots 
z_{p})\}
\eneq
While complement of terms with strict application is:
\beq
\GG\prv\mnot(E\rapp \ol{y_{m}}) & = &  \bigcup\limits_{j=1}^{m} 
\{E_{j}(y_{1}\mdots y_{j-1}, y_{j+1}\mdots y_{m})\}
\eneq
\begin{Examplen}
\beq
 \cdot\prv\mnot(\l xyzw.E \ y\ w)& = &\{\l xyzw.F_{1}\ y\ w\rapp x\ z, 
\l xyzw.F_{2}\ y\ w\ x\rapp z\} \\
\cdot\prv\mnot(\l xy.E\rapp x\rapp y) & = & \{\l xy. F_{1} x,   \l 
xy.F_{2} y\}
\eneq
\end{Examplen}
}

Yet, there is a certain asymmetry between strict and intuitionistic 
application: while the former completely determines the occurrence 
status of a variable, the latter leaves the status floating 
indeterminately between the possibility or not of occurrence.  We 
therefore decorate bound variables as well as function types with 
three \emph{occurrence annotations}\ignore{An analogous approach can 
be used to deal with resource management in linear logic 
\cite{Pfenning98notes}.} $1,0,u$ with the intended meaning of: 

\beq 
x^{1} & : & \mbox{$x$ must occur}\\
  x^{0} & : & \mbox{$x$ must \emph{not} occur}\\
x^{u} & : & \mbox{$x$ is undetermined}
\eneq 
Then $\l xy.  E\rapp y$ is written as $\l xy.  F \_^{0} y^{1}$. 
Although the official notation uses an underscore for `empty' 
application, since the variable is required not to occur, we will 
however, by abuse of notation,  \ignore{in  section  \ref{sec:nfa}} retain the name 
of the variable: this is more handy since, as we show next, these annotations 
make every pattern \emph{fully applied}. 


\subsection{The system $\lc$}
\label{stricttypes}

We present a type system can express and check statements about 
whether an expression uses (arbitrarily often) an argument mentioned 
in its binder.  Thus the linear $\l$-calculus is a special case of 
this: the requirement of `occurring only once' can nevertheless be captured 
by introducing the linear connectives.  The peculiarity of this 
formulation is the introduction of a vacuous functional type with its 
respective operators to denote an expression that \emph{ought not} 
to depend from its argument.  For this reason and following Girard's 
and Belnap's \cite{SH?} suggestion we will refer to this calculus as 
\emph{strict} logic, leaving the \emph{relevant} label to other 
calculi which may also satisfy other logical principles such as 
distributivity among the various connectives.

\medskip
\newcommand{\lxla}{\lambda x^{l}\!:\! A.\,}
\newcommand{\lxra}{\lambda x^{1}\!:\! A.\,}
\newcommand{\lxza}{\lambda x^{0}\!:\! A.\,}

Types (formulae) and terms (proofs)  language:
\beq
l & \bnfas & 1\mid 0\mid u\\
A & \bnfas & P\mid A\LImp B \\
M & \bnfas & x \mid c\mid \lxla M\mid M' M^l 
\eneq 

We use an underscore in $M\_^0$ since in the abstraction the argument 
is not used and hence the result of the application does not depend on 
its argument.  Remark that the order in which arguments \emph{do not} 
appear is clearly irrelevant.  Thus, for example a term as $\l 
x^{0}y^{0}.\, (E \_^{0}) \_^{0}$ is not ambiguous.  If a label is $u$ 
it is called \emph{undetermined}, otherwise it is \emph{determined} 
and denoted with the metavariable $d$.  Moreover, we most of the time 
omit the undetermined label.

The typing judgment, depicted in Figure \ref{fig:stricttype} is $\GG \prvs 
M: A$. Given $\GG$, we define $\GG_{l} = \{x^l : A\mid x^l\in dom(\GG)\}$.

\begin{figure}
\label{fig:stricttype}
\[
\begin{array}{c}
\ianc{c\in\Sigma}{\GG  \prvs  c: A}{Idc}
\qquad
\ianc{\GG_1 = \{x^1 : A\}}{\GG \prvs  x:A} {IdR}
\qquad 
\ianc{\GG_1 = \cdot}{\GG,x ^u : A \prvs  x:A}{IdI}\vsk
\ianc{\GG,x^l : A  \prvs M: B}{\GG\prvs(\lxla M) : 
A\LImp B} {\Imp I}
\qquad
\ianc{\GG\prvs M : A \Imp B \quad\quad \GG_{u},\GG_{0} \prvs N  : A}
{\GG \prvs M N :B}{\Imp E}\vsk
% \ianc{\GG ; (\Delta,x : A) \prvs M: B}{\GG;\Delta\prvs(\lxra M ) : 
% A\RImp B}{\RImp I}

\ianc{\GG_{u},\GG_{0},\GG_{1}\prvs M : A \RImp B \quad\quad \GG_{u},\GG_{0},\GG'_{1} \prvs N  : A}
{\GG_{u},\GG_{0},\GG_{1}\cup\GG'_{1}\prvs M N^1 :B}{\RImp E}
% \ianc{\GG ; \Delta \prvs M: B}{\GG;\Delta\prvs(\lxza M) : 
% A\ZImp B}{\ZImp I}
\qquad
\ianc{\GG\prvs M : A \ZImp B}{\GG   \prvs M  \_^0 :B}{\ZImp E}
\end{array}
\]
\caption{Typing rules for $\lc$}
\end{figure}

Note how the strictness constraints is preserved in the elimination 
rules: you can always apply an intuitionistic term to a strict 
function (losing the dependencies), but not viceversa; thus $N:A$ in 
($\Imp E$) is a proof with  empty strict assumptions.  Remark also the 
set-theoretic union $\cup$ of strict contexts in ($\RImp E$), which 
constrains $N:A$ to appear in the first or the second or both 
contexts.  Subtly, his is the only difference compared to the 
\emph{linear} calculus: if instead of uniting sets, we only juxtapose 
the non-intuitionistic context as a multiset, we obtain the 
elimination rule for linear implication\ignore{: the difference between linear 
and strict implication in the difference between multisets and sets in 
a zoned calculus}.  A sample typing derivation can be found in Figure 
\ref{fig:strictex}.  
% Nothing is intuitionistic, hence the latter are 
% not mentioned with in the previous example.  W.r.t.\ the identity 
% rules, you may convince yourself of their validity trying $ \prv A 
% \Imp (B \RImp B)$, $ \prv A\RImp (B \Imp A)$, but $\nprv A \Imp (B 
% \RImp A)$.


\newcommand{\jj}{\justifies}
% \begin{Examplen}
\begin{figure}
\label{fig:strictex}
\prooftree
\[ \mbox{} \jj x^1 : A \RImp A\RImp B \prv x : A \RImp A\RImp B \using 
IdR \]
 \qquad 
 \[ \mbox{} \jj y^1 : A\prv y: A \using IdR\]
 \using \RImp E
\justifies
\[
x^{1} : A \RImp A\RImp B , y^1 :A\prv x y^1 : A\RImp B \qquad y^1 : A\prv y: A
\using \RImp E
\justifies
\[
 x^1 : A \RImp A\RImp B ,y^{1}: A\prv (x y^1)  y^1 : B
 \using \RImp I
 \justifies
 \[
 x^1 : A \RImp A\RImp B  \prv \l y^1 . (x y^1)  y^1 : A\RImp B
 \using \RImp I
 \justifies
\prv \l x^1.\l y^1. (x y^1)  y^1  : (A \RImp A\RImp B)\RImp (A\RImp 
B)
\]
\]
\]
\endprooftree
\caption{Derivation of $(A \RImp A\RImp B)\RImp (A\RImp B)$}
\end{figure}


\subsection{The complement of  non-fully applied patterns}

Observe that the complement operation on terms behaves on 
labels like negation does on truth-values in Kleene's logic, in the 
sense of the following table: 
\beq 
\mnot(1)& = &0\\
\mnot(0)& = &1\\
\mnot(u) & = & u
\eneq
Hence these labels form a three-valued semilattice with the partial 
(information) ordering $u\leq 1, u\leq 0$. 

\bigskip

We now describe how to make every term fully applied: this is achieved 
via a translation from the simply-typed $\l$-calculus into the subset 
of strict types without $1$-types, which we denote with $\l^{\GImp{u,0}}$.  
The latter is the framework where complementation will be performed.

\newcommand{\LBimp}{\longleftrightarrow}
\begin{figure}
\label{fig:trans}  
\[
\begin{array}{c}
\ianc{n,m\geq 0}{\ol{x_{\pi(n)}},\ym\prv  E\ \xn :P\LBimp 
\ol{x^{u}_{\pi(n)}},\ol{y^{0}_{m}}\prv  F\ 
\ol{x^{u}_{\pi(n)}}\ol{y^{0}_{m}}:P}{\mbox{\rm Trn\_Pat}} 
\vsk
\ianc{ \GG,\of{x}{A}\prv  M:B \LBimp  \GG^{\ll},\of{x^{l_{x}}}{A'}\prv  
M':B'}
{\GG\prv \lxa M : A\TImp B \LBimp \GG^{\ll}\prv \l x^{l_{x}}:A'.\, M': 
A'\GImp{l_{x}} B' }{\mbox{\rm Trn\_Lam}}\vsk
\ianc{  \GG\prv  M_{1}:A_{1} \LBimp \GG^{\ll_{1}}_{1}\prv N_{1}:A_{1}
\cdots \GG\prv  M_{n} :A_{n}\LBimp \GG^{\ll_{n}}_{n}\prv N_{n}:A_{n}}
{\GG\prv h\  \Mn :P\LBimp  \GG^{(\Or^{1\leq i\leq n} \ll_{i})}\prv h\ \Nn:P} 
{\mbox{\rm Trn\_App}}
\end{array}
\]
\caption{Translation between $\l^\TImp$ and $\l^{\GImp{u,0}}$}
\end{figure}

The translation is represented by the judgment $\GG\prv M :A\LBimp 
\GG^{\ll}\prv N :A'$ depicted in Figure \ref{fig:trans}.  The rule 
Trn\_App requires a merge of the labeling in the premises.  This is 
achieved taking the `weaker' one.  This operation chooses the context 
labeling most compatible with the various occurrence annotations.  
More formally, if $l_{1}\Or l_{2}$ is the greatest lower bound of two 
labels in the semilattice of labels, extend it to sets of labels 
pairwise, \ie $\ll_{1}\BOr \ll_{2} = \{l_{1}\Or l_{2}\mid l_{1}\in 
\ll_{1}, l_{2}\in\ll_{2} \}$.

\begin{Examplen}
The following is derivable:
\[
\prooftree
(\of{x,y}{exp} \prv E_{1} x)\LBimp(\of{ x^{u},y^{0}}{exp} \prv F_{1}x^{u},y^{0}) \qquad
(\of{x,y}{exp} \prv E_{2})\LBimp(\of{ x^{0},y^{0}}{exp} \prv F_{2}x^{0},y^{0})
\justifies
\[
\of{x,y}{exp} \prv app\ (E_{1}x) \ E_{2}\LBimp\of{ x^{u},y^{0}}{exp} \prv app\ 
(F_{1}x^{u},y^{0}) \ (F_{2}x^{0},y^{0})
 \justifies 
\cdot\prv\l x,y :exp.\, app\ (E_{1}x) \ E_{2} \LBimp 
\cdot\prv\l x^{u},y^{0}: exp.\, app\ (F_{1}x^{u},y^{0}) \  (F_{2}x^{u},y^{0})
\]
\endprooftree
\]
Note the choice of the 'weakest' between context labeling $\of{ x^{u},y^{0}}{exp}$ in 
the application case.
\end{Examplen}

The adequacy of the translation is easily established:

\begin{Ppn}
The judgment $\GG\prv M :A\LBimp \GG^{\ll}\prv N :A'$ represents a 
bijection between $\lc$ and $\l^{\GImp{u,0}}$.
\end{Ppn}
\begin{proof}
A straightforward induction on the structure of the judgment verifies 
that the RHS is the bilateral inverse function of the LHS.
\end{proof}

We can now check that every term can be brought into a fully applied form:

\begin{Ppn} 
For every term $M$ in $\l^\TImp$ such that $\GG\prv M :A\LBimp 
\GG^{\ll}\prv N :A'$, it holds that $\GG^{\ll}\prv N \fa$ in 
$\l^{\GImp{u,0}}$.
\end{Ppn}
\begin{proof}
Again, a straightforward induction on the structure of $M$.
\end{proof}

\smallskip
The idea of complementation a non-fully applied patterns is 
to form a set  of terms in contexts 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 added and the remaining variables are 
set to undetermined, otherwise we do nothing, \ie we do not add a 
term.  Note that we set to undefined even variables in context 
that do not occur in the scope of a logical variable.  This is safe 
for our application, but it needs refining when dealing with 
substructural logics. 

% Def with d
\begin{Definition}[Flexible term complement]
\label{def:ho-compl}
 \beq 
\lefteqn{\GG^{l}, x_{j}^{d}:A_{j}\prv\mnot''(E (x_{1}^{l_{1}}\mdots 
x_{j-1}^{l_{j-1}},x_{j}^{d}, x_{j+1}^{l_{j+1}}\mdots x_n^{l_{n}})) 
=}\\ & & \GG^{u}, x_{j}^{\mnot(d)}:A_{j}\prv F(x_{1}^{u}\mdots 
x_{j-1}^{u},x_{j}^{\mnot(d)}, x_{j+1}^{u}\mdots x_n^{u})) \\
\lefteqn{\GG^{l}, x_{j}^{u}:A_{j}\prv\mnot''(E (x_{1}^{l_{1}}\mdots 
x_{j-1}^{l_{j-1}},x_{j}^{u}, x_{j+1}^{l_{j+1}}\mdots x_n^{l_{n}})) =}\\ & & \eset\\
\lefteqn{\GG^{l}\prv\mnot'(E\ \ol{x_{n}^{l}})  =}\\
 & & \bigcup\limits_{j=1}^{n} \{\GG^{l_{j}}\prv\mnot''(F_{j} (x_{1}^{l_{1}}\mdots 
x_{j-1}^{l_{j-1}},x_{j}^{l_{j}}, x_{j+1}^{l_{j+1}}\mdots 
x_n^{l_{n}}))\}
\eneq
\end{Definition}

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

\begin{Examplen}
\begin{eqnarray}
\mnot'( x^{0}, y^{1}\prv E x^{0} y^{1}) & = & \{ x^{1}, y^{u}\prv F\  
x^{1} y^{u}, \quad x^{u}, y^{0}\prv G\  x^{u} y^{0}\} \label{eq:l}\\
\mnot'( x^{u}, y^{1}\prv E x^{u} y^{1}) & = & \{ x^{u}, y^{0}\prv F\  
x^{u} y^{0}\}\nonumber
\end{eqnarray}
\end{Examplen}

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

\medskip
We are now ready to collect Definition \ref{def:fa-compl} and 
\ref{def:ho-compl}:

 \newcommand{\ngl}{\GG^{l}\prv\mnot}

\begin{Definition}[\ho pattern complement]
\label{def:compl}
Fix a signature $\Sigma$.  For a  \ho linear pattern in canonical 
form $M'$ such that $\GG \prvs M' : A'$ and  $\GG\prv M' :A'\LBimp 
\GG^{\ll}\prv M : A$,  define $\ngl(M: A)$ as:

% \renewcommand{\ngl}{\GG^{l}\prv\mnot}
\[\begin{array}{lll}
\ngl(E\ \ol{x_{n}^{l}} : P) & = & \GG^{l}\prv\mnot'(E\ \ol{x_{n}^{l}})\\ 
\ngl (h\ M_{1}\dots M_{m}: P) & = & diff_{\GG}(h:\ol{A_{m}}\Imp P) \cup 
\mbox{}\\
& &
\{h\ (Z_{1}\GG^l)\dots (Z_{i-1}\GG^l), N, (Z_{i+1}\GG^l)\dots (Z_{m}\GG^l)\mid 
\\
& & N\in\ngl(M_{i}:A_{i}), 1\leq i\leq m \} \\
\ngl(\l x^{l_{x}} \!:\!A.\, M:A\Imp B) &  = & \{ \l x^{u} \!:\!A.\, N \mid N\in 
(\GG^{l},\of{x^{l_{x}}}{A} \prv \mnot(M:B)) \}
\end{array}\]
\end{Definition} 
Remark that in the abstraction case, the label is set to undetermined, 
which is compatible with every occurrence annotation in the matrix.

\begin{Examplen}
\beq
\lefteqn{\mnot(\l x^{1},y^{0}.\, s(M\ x^{1} y^{0}) : nat\RImp nat\ZImp 
nat)  =}\\
 & 
\{ \l  x,y .\, x, \l  x,y .\, y, \l  x,y .\, 0,  \l  x,y .\, s(N\ 
x^{0} y^{u}),  \l  x,y .\, s(N\ x^{u} y^{1}) \}
\eneq
\end{Examplen}

\smallskip We  address the correctness 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.  Again, we need to take into account the current context 
which also gives type information to parameters.  We recall that we assume 
every type to be inhabited, so that every term can be see as the 
intensional representation of the set of its ground instances.  The 
judgments in Figure \ref{fig:grNgr} $\GG\prvs M\in\| N\| : A$ and 
$\GG\prvs M\not\in\| N\| : A$ formalizes the fact that, in a context 
$\GG$ and signature $\S$, $M$ of type $A$ is or is not a ground 
instance of $N$.


\begin{figure}
\label{fig:grNgr}
\[
\begin{array}{c}
\ianc{M\equiv t \ \xn^{l}  \quad \cdot\prvs t : \ol{A_{n}^{l}}\Imp P}
{\GG\prvs  M  \in\| F\ \xn^{l}\| : P}{grFlex} 
\qquad
\ianc{M\equiv t \ \xn^{l}  \quad \cdot\nprvs t : \ol{A_{n}^{l}}\Imp P}
{\GG\prvs  M  \not\in\| F\ \xn^{l}\| : P}{NgrFlex} 
\vsk
\ianc{\GG,x:A\prvs  M  \in\| N\| : B}
{\GG\prvs \lxa M  \in\|\lxa N \|:A\Imp B}{grLam}
\qquad
\ianc{\GG,x:A\prvs  M  \not\in\| N\| : B}{\GG\prvs \lxa M  
\not\in\|\lxa N \|:A\Imp B}{NgrLam}
\vsk
\ianc{\GG\prvs  \Mn  \in\| \Nn\| : \ol{A_n} }
{\GG\prvs h\  \Mn  \in\|h\ \Nn \| : P} {grApp}
%  \qquad   NOT NEEDED
% \ianc{\GG\prvs M\in\|N\| \quad \GG\prvs N\in\|Q\|}{\GG\prvs 
% M\in\|Q\|}{grTrans}
 \vsk
\ianc{\GG\prvs  M_{i}  \not\in\| N_{i}\| : A_{i} }{\GG\prvs h\  \Mn  
\not\in\|h\ \Nn \| : P} {NgrApp_{i}}
\qquad
% \ianc{\prvs h : A\quad h\in\GG\cup\Sigma}{\GG \prvs  h  \in\| h\| : A}{grConst}
% \qquad SUBSUMED
\ianc{ M \in \|diff_{\GG}(h:\ol{A_{n}}\Imp P)\|}{\GG \prvs  M  
\not\in\| h\ \Nn\| : P}{NgrAppdif}
% \vsk
% \ianc{\GG\prvs M \in \|N_{i}\|:A_{i}}{\GG\prvs M \in \|N_{1}\cdots N_{n}\|:A_{1}\cdots A_{n}}{gr_{i}}
% \qquad
% \ianc{\GG\prvs M \not\in \|N_{1}\|:A_{1}\cdots \GG\prvs M \not\in 
% \|N_{n}:A_{n}\|}
% {\GG\prvs M \not \in \|N_{1}\cdots N_{n}\|A_{1}\cdots A_{n}}{Ngr_{n}}
\end{array}
\]
\caption{$M : A$ is or is not a ground instance of $N$}
\end{figure}


\smallskip
We need to extend the above judgment to \emph{sets} of terms: if $1\leq i\leq n$:

\[
\ianc{\GG\prvs M \in \|N_{i}\|:A}{\GG\prvs M \in \|N_{1}\cdots 
N_{n}\|:A}{gr_{i}} 
\qquad 
\ianc{\GG\prvs M \not\in \|N_{1}\|:A\cdots \GG\prvs M \not\in 
\|N_{n}\|:A} {\GG\prvs M \not \in \|N_{1}\cdots N_{n}\|:A}{Ngr_{n}}
\]

\begin{Lemma}[Parameter Context Weakening]
\label{le:pweak}
Fixed a signature $\Sigma$, for parameter contexts $\GG, \GG'$ such 
that $\GG\subseteq\GG'$,  $\GG\prvs M\in 
\|N\| :A$ entails $\GG'\prvs M\in \|N \| :A$.
\end{Lemma}
\ignore{
\begin{proof}
By induction on $N$.  If the latter is $c\in\Sigma\cup\GG$, then a 
fortiori $ M\in\GG\cup\Sigma$ entails $ M\in\GG'\cup\Sigma$, hence 
$M\in\GG'\prv M\in \|N \|$.  Application leaves $\GG$ as is, hence 
simply apply the inductive hypothesis.  Let $N$ be an abstraction 
$\lxa N$.  Then $\GG\prv M\in \|\lxa N\|$ if $\GG,x:A\prv M\in \|N\|$ 
which, by induction hypothesis, entails $\GG', x:A\prv M\in \| N\|$ 
and $\GG'\prv M\in \|\lxa N\|$.
\end{proof}
}
We implicitly use the above lemma to opportunely weaken different 
contexts with common basis to an unique $\GG$.
\smallskip
We use the abridged notation $\GG\prvs M\in\|\mnot(N)\| :A$ for 
$\GG\prvs M\in \|N_{1}\cdots N_{n}\|:A$ where $ \GG\prvs \mnot(N:B) = 
\{N_{1}\cdots N_{n}\}$.  In the following, we may also drop the type 
and signature information from the above judgment in proofs.  Finally 
we abridge $\mnot(l)$ in $-l$.


\begin{Proposition}
\label{ppn:part1}
For a fixed signature $\Sigma$ and $N$ linear, if $\GG^l\prvs M\in \| 
\mnot(N)\| : A$ then $\GG^{l}\prvs M \not\in \| N \| :A$.
\end{Proposition}
\begin{proof}
By induction on $N$.
\begin{itemize}
\item Basis: $N$ is the flexible term $E\ \ol{x_n^{l}}$.
$\GG^l\prv  M\in \|\mnot(E\ \ol{x_n^{l}})\|$ iff there is a $j$ 
such that $\GG^{l_{j}}, x_{j}^{l_j}:A_{j}\prv M\in\|\mnot''(E (x_{1}^{l_{1}}\mdots 
x_{j-1}^{l_{j-1}},x_{j}^{l_j}, x_{j+1}^{l_{j+1}}\mdots x_n^{l_{n}})) 
\|$.  
We proceed by cases on the label $l_{j}$.  If $l_{j}= u$, then $ 
\GG^{l}, x_{j}^{u}:A_{j}\prv M\in \|\mnot''(E (x_{1}^{l_{1}}\mdots 
x_{j-1}^{l_{j-1}},x_{j}^{u}, x_{j+1}^{l_{j+1}}\mdots x_n^{l_{n}}))\| $ 
iff $ \GG^{l}, x_{j}^{u}:A_{j}\prv M \in \eset $, which trivially implies the 
conclusion.  Otherwise $l_{j}$ is a determined label $d$: thus $\GG^{l}, 
x_{j}^{d}:A_{j}\prv M\in \|\mnot''(E (x_{1}^{l_{1}}\mdots 
x_{j-1}^{l_{j-1}},x_{j}^{d}, x_{j+1}^{l_{j+1}}\mdots x_n^{l_{n}})) \|$ 
iff $\GG^{u}, x_{j}^{-d}:A_{j}\prv M\in \|F(x_{1}^{u}\mdots 
x_{j-1}^{u},x_{j}^{-d}, x_{j+1}^{u}\mdots x_n^{u}))\|$.  By rule 
$grflApp$ there is a ground term $t$ such that $t \ \xn^{l} \equiv 
M$ and $\cdot\prv  t : A_{1}^{u}\mdots A_{j-1}^{u},A_{j}^{-d}, 
A_{j+1}^{u}\mdots A_n^{u}\Imp P$.  By uniqueness of typing in $\lc$ we 
have that $\cdot\nprvs t :A_{1}^{l_{1}}\mdots 
A_{j-1}^{l_{j-1}},A_{j}^{d}, A_{j+1}^{l_{j+1}}\mdots A_n^{l_{n}}\Imp 
P$ and by rule $NgrFlex$ $\GG^{l}, x_{j}^{-d}:A_{j}\prv M\not\in \| E 
(x_{1}^{l_{1}}\mdots x_{j-1}^{l_{j-1}},x_{j}^{-d}, 
x_{j+1}^{l_{j+1}}\mdots x_n^{l_{n}}) \|$ and thus $\GG^l\nprvs 
M\in \|E\ \ol{x_n^{l}}\|$.
\item 
Step: 
\ben \item Case: $N$ is an application $(h\ \ol{N_n})$ for $ 
n\geq 0$.
Then $\GG^l\prv M\in\|\mnot(h\ \ol{N_n})\|$ iff by definition of 
$\mnot$, $ M\in \|diff_{\GG^l} (h:\ol{A_{n}}\Imp P)\|$ or $\GG^l\prv 
M\in \|h\ (Z_{1}\GG^l)\dots (Z_{i-1}\GG^l), N, (Z_{i+1}\GG^l)\dots 
(Z_{m}\GG^l) \|)$ for $ N\in\ngl(N_{i}:A_{i})$.  The left horn immediately yields 
 $\GG^{l}\prv M\not\in\|h\ \ol{N_n}\|$ by rule $NgrAppdif$.  
From the right horn, by rule $grApp$ there is an $i$ such that 
$\GG^l\prv M_{i}\in \|N\|$ for $N\in\ngl(N_{i}:A_{i})$; by inductive 
hypothesis $\GG^{l}\prv M_{i}\not\in\|N_{i} \|$, which by rule 
$NgrApp$ yields $\GG^{l}\prv h\ \ol{M_n}\not\in\|h\ \ol{N_n}\|$.
\item 
Case: $N$ is an abstraction $\lxa N$.  Then $\GG^l\prv \lxa 
M\in \|\mnot(\lxa N)\|$ iff, by definition $\GG^l\prv \lxa M\in \| 
\{\lxa S\mid \GG^l,x:A\prv S\in \mnot(N)\} \|$ \ie $M\equiv S$ and 
$\GG^l,x:A\prv S\in\|\mnot(N)\| $ which implies by induction 
hypothesis $\GG^{l}, x :A\prv S\not\in \|N\|$, \ie $\GG^{l}, x :A\prv 
M\not\in \|N\|$. This yields $\GG^{l}\prv\lxa M\not\in\|\l x :A. N\|$.  
\enen
\end{itemize}
\end{proof}


\begin{Proposition}
\label{ppn:part2}
For a fixed signature $\Sigma$ and $N$ linear, if $\GG^l\prvs M 
\not\in \| N \| :A$ then $ \GG^{l}\prvs M\in \| \mnot(N)\| : 
A$.
\end{Proposition}
\begin{proof}
By induction on $N$ analogously to the proof of the above Proposition 
\ref{ppn:part1}.
\end{proof}

\begin{Corollary}[Partition Lemma] For a context $\GG$ 
and a fixed signature $\Sigma$ let $M, N : A$ be linear \ho patterns 
in $\be$-long normal form:
\label{lemma:part}
\ben
\item (Exhaustivity) $\GG\prvs M\in \| N \| :A$ or $\GG\prvs M\in \| 
\mnot(N) \|:A$.
\item (Disjointness) It is not the case that $\GG\prvs M\in \| N \|:A$ and 
$\GG\prvs M\in \| \mnot(N) \|:A$.
\enen
\end{Corollary}
\begin{proof}
Disjointness is equivalent to the Proposition \ref{ppn:part1}, 
exhaustivity to Proposition \ref{ppn:part2}.
\end{proof}


We now go back and address some basic properties of the strict 
$\l$-calculus.


\subsection{Properties of $\lc$}

\newcommand{\ltxa}{\lambda x^{\mbox{\tiny  0}}\!:\! A.\,}
\newcommand{\lrxa}{\lambda x^{\mbox{\tiny  1}}\!:\! A.\,}


% Let us recall that the only allowed applications combinations are R-R, 
% R-I, I-I: hence the following $\beta$-reductions.  
We assume the usual 
notion of free and bound variables, capture-free substitutions and we 
identify $\alpha$-convertible terms. 

We have the following reductions rules:
\[
\begin{array}{llll}
 R-R & (\lrxa M)  N^1 & \Lmap_{\beta} & [N/x]M\\
    I-I & (\lxa M )  N & \Lmap_{\beta} & [N/x]M    \\
     N-N & (\ltxa M)  \_^0 & \Lmap_{\beta} & M
\end{array}
\]
We add the rules for $\eta$-reductions, since they  come handy 
when defining the long $\be$-normal form:
\[
\begin{array}{llll}
  R-R & (\lrxa (M x^1)) & \Lmap_{\eta} & M\\
    I-I    & (\lom x:A.(M x)) & \Lmap_{\eta} & M\\
     N-N      & (\ltxa (M  \_^0)) & \Lmap_{\eta} & M
\end{array}
\]



We now want to check the subject reduction and expansion property 
\marginpar{for the zoned calculus}; 
hence we need to establish the relative inversion and substitution 
lemmata: we follow \cite{Barendregt91}'s account\marginpar{Skip now?}.

\begin{Lemma} [Inversion] 
 \mbox{}
\begin{itemize}
        \item[Iapp] $\GG;\Delta \prvs M N :B \Rightarrow \exists A: \GG;\Delta 
        \prvs M: A \Imp B \And \GG;\Delta \prvs N :A$

        \item[Sapp] $\GG;\Delta \prvs M  N^1:B \Rightarrow \exists 
        A,\Delta_{1},\Delta_{2}: \Delta =_{set} \Delta_{1} \cup \Delta_{2} \ s.t.\ \GG;\Delta_{1} 
        \prvs M: A \RImp B \And \GG;\Delta_{2} \prvs N :A$

        \item[Napp] $\GG;\Delta \prvs M \_^0 :B \Rightarrow \exists A: \GG;\Delta 
        \prvs M: A \ZImp B %\And \GG;\Delta \prvs \_:A
$

        \item[Iabs] $\GG;\Delta\prvs(\lxa M) : C \Rightarrow \exists A,B: 
        C \equiv  A \Imp B \ s.t.\ (\GG,x : A) ; \Delta \prvs M: B$

        \item[Sabs] $\GG;\Delta\prvs(\lxra M) : C \Rightarrow \exists A,B: 
        C \equiv  A \RImp B \ s.t.\ \GG ; (\Delta,x : A) \prvs M: B$ 
         
        \item[Nabs] $\GG;\Delta\prvs(\lxza M) : C \Rightarrow \exists A,B: 
        C \equiv  A \ZImp B \ s.t.\ \GG ; \Delta \prvs M: B$
\end{itemize}
\end{Lemma}
\begin{proof} By inspection
\end{proof}


\begin{Lemma} [Substitution] 
\mbox{}
\begin{enumerate}
        \item  $(\GG, x:A);\Delta \prvs M :B \And \GG;\cdot \prvs  N :B 
        \Rightarrow \GG;\Delta \prvs [N/x]M :A$

        \item  $\GG;(\Delta, x:A) \prvs M :B \And \GG;\Delta' \prvs  N :B 
        \Rightarrow \GG;(\Delta\cup\Delta') \prvs [N/x]M :A$
\end{enumerate}
\end{Lemma}
\begin{proof}
By induction on the structure of $ (\GG, x:A);\Delta \prvs M :B$ and 
$\GG;(\Delta, x:A) \prvs M :B $ respectively.
\end{proof}
\begin{Proposition} [Subject reduction and expansion]
\mbox{}
\ben
        \item $\GG;\Delta \prvs M:A \mbox{\, and $M 
\Lmap^{*}_{\beta} M'$\,}\Rightarrow  \GG;\Delta \prvs M':A$
                \item $\GG;\Delta \prvs M:A \mbox{\, and $M 
\Lmap^{*}_{\eta} M'$\,}\Rightarrow  \GG;\Delta \prvs M':A$.
\enen
\end{Proposition}  
\begin{proof}
(Sketch). (1) By induction on $\Imp^{*}_{\beta}$. In the base case consider in 
turn each kind of $\beta$-redex. Apply  
inversion and conclude by the substitution lemma. Otherwise apply the 
inductive hypothesis. (2)
\end{proof}

\subsection{Canonical forms for $\lc$}

For future use in unification we present the system for 
\emph(canonical) forms, \ie terms in $\be$ long normal form.  This is 
realized by the two mutually recursive judgments depicted in Figure 
\ref{fig:canon}:\marginpar{still zoned calculus}

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

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

\begin{figure}
\label{fig:canon}
\[
\begin{array}{cc}
\ianc{}{\GG;x : A \prvs  x\da A} {cIdR}
& 
\ianc{}{(\GG,x : A); \cdot  \prvs  x\da A}{cIdI}\vsk
\ianc{\GG;\Delta \prvs  x\da P}{\GG;\Delta \prvs  x\bua P} {cAt}
& 
\ianc{c\in\Sigma}{\GG; \Delta  \prvs  c\da A}{cIdc}\vsk
\ianc{(\GG,x : A) ; \Delta \prvs M\bua B}{\GG;\Delta\prvs(\lxa M) \bua 
A\Imp B} {c\Imp I}
&
\ianc{\GG;\Delta\prvs M \da A \Imp B \quad\quad \GG;\cdot \prvs N  \bua A}
{\GG;\Delta \prvs M N \da B}{c\Imp E}\vsk
\ianc{\GG ; (\Delta,x : A) \prvs M\bua B}{\GG;\Delta\prvs(\lxra M) \bua 
A\RImp B}{c\RImp I}
&
\ianc{\GG;\Delta_{1}\prvs M \da A \RImp B \quad\quad \GG;\Delta_{2} \prvs N  \bua A}
{\GG;\Delta_{1}\cup \Delta_{2} \prvs M N^1 \da B}{c\RImp E}\vsk
\ianc{\GG ; \Delta \prvs M\bua B}{\GG;\Delta\prvs(\lxza M) \bua 
A\ZImp B}{c\ZImp I}
&
\ianc{\GG;\Delta\prvs M \da A \ZImp B %\quad\quad \GG;\cdot \prvs \_^0 \bua A
}
{\GG;\Delta  \prvs M  \_^0 \da B}{c\ZImp E}
\end{array}
\]
\caption{Canonical forms for $\lc$}
\end{figure}

\subsection{Strict $\beta_{0}$ unification}

To be inserted: need help on flexrigidcase

% \subsection{More on the complement operation}
\subsection{Extensions}
\label{subsec:ext}

We can extend further the judgment $\GG\prvs M\in\| N\| : A$ to 
simulate non-singleton complement problems (Section \ref{el-rel}) of 
the form $Z - \| N_1 \mdots N_n \|$ as follows:
\[
\ianc{\GG\prvs M\in\| \mnot(N_{1})\|:A \cdots \GG\prvs M\in\| 
\mnot(N_{n})\|:A }{\GG\prvs M\in \| \mnot(N_{1}\mdots N_{n}) \|: 
A}{gr\mnot_{n}}
\]
This judgment can be used as a logic program to search those values of 
$M$ which simultaneously satisfy the conjunctive constraints specified 
in the RHS. To illustrate the idea, we can revisit Example \ref{eqb: 
odd}; the equational problem \[\forall y:z \neq 0 \And z \neq ssy\] 
yields the `query' $\cdot\prvs M \in \|\mnot(0, ssY)\|$ only if 
$\cdot\prvs M \in \|\mnot(0)\|$ and $\cdot\prvs M \in \|\mnot( 
ssY)\|$, so that $M$ is instantiated to the only solution, namely 
$s0$.

\begin{Corollary}
For a fixed signature $\Sigma$ and $N_{1}\mdots N_{n} $ linear, 
$\GG^l\prvs M\in \| \mnot(N_{1}\mdots N_{n})\| : A$ iff $\GG^{l}\prvs 
M \not\in \| N_{1}\mdots N_{n} \| :A$.
\end{Corollary}
\begin{proof}
$\GG\prvs M\in \| \mnot(N_{1})\mdots \mnot(N_{n})\|:A$ iff, by rule 
$gr\mnot_{n}$ , $\GG\prvs M\in\| \mnot(N_{1})\|:A \cdots \GG\prvs 
M\in\| \mnot(N_{n})\| :A$ iff, by $n$ application of the Partition 
Lemma \ref{lemma:part} $\GG\prvs M\not\in\| N_{1}\|:A\cdots\GG\prvs 
M\not\in\| N_{n}|:A$ iff by rule $Ngr_{n}, \GG^{l}\prvs M \not\in \| 
N_{1}\mdots N_{n} \| :A$.
\end{proof}

Note that the logic programming execution of the [non]membership 
judgment is equivalent in the algebraic approach to computing 
sequentially each $\mnot(N_{i})$ and then intersecting them modulo 
unification.  The non-unary character of unification is this setting 
(which by the way make the latter version more problematic) will 
eventually be reflected in the high nondeterminism of the search. For 
now we will not detail any operational refinement of this judgment. We 
will not pursue this further now, as solving singleton complement 
problems is sufficient (\ref{sec:alge}) for our application.  We 
mention only that we can encode \emph{any} relative complement 
problems of the form $\| t_1 \mdots t_n \| - \| u_1 \mdots u_m \|$ as:
\[
\ianc{\GG\prvs M\in \| t_1 \mdots t_n\|:A \quad \GG\prvs M\in \| 
\mnot(u_1 \mdots u_m)\|:A }{\GG\prvs M\in \| t_1 \mdots t_n \| - \| 
u_1 \mdots u_m \|:A}{RelCompl}
\]

Remark also the difference with the way in which \emph{disunification} 
approaches (relative) complement problems: here constraints 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 
complment problems, it maybe argued that disunification is not 
necessarily the master road to the latter.  Moreover the \ho case 
brings in additional complications, as dependencies which are 
orthogonal to the hyper-logical structuring  that 
disunification requires.  On the other hand our approach is similar in 
spirit to Miller's paper ``Unification of Simply Typed Lambda-Terms as 
Logic Programming'' \cite{Miller91iclp} and more in general to the 
experience gained in the design and implementation of \ho programming 
languages as \emph{LambdaProlog} or \emph{Twelf}.  We isolate a 
problem which is well-defined and likely to have a feasible solution 
as the singleton complementation of \ho patterns, say to start with in 
the simply-typed $\l$-calculus.  Then either we specify object level 
programs to solve harder problems--here relative complementation-- or 
we settle for delaying strategies possibly coupled with translations 
to deal with that rare but possible exceptions.  In the case of 
complementation, left-linearization and something like the 
\texttt{noncopy} translation may be employed\footnote{Pointer to 
discussion: for example, to complement the non patterns clause $subst\ 
F\ T\ (F\ T)$, we linearize it into $subst\ F\ T\ New\ \If copy\ New\ 
(F\ T)$ and then complement it via the pre-compiled \texttt{noncopy} 
clauses.}

\subsection{Additional stuff}

We may define a forgetful translation from $\lc$ to a strict calculus 
without empty application: this is given in Figure \ref{fig:forgetful}.
\marginpar{Skip this}

\begin{figure}
\label{fig:forgetful}
\[
\begin{array}{c}
\ianc{\GG, x : A \prvs M \leadsto N\quad l\in\{u,0\}}
{\GG\prvs \l x^{l}:A. M \leadsto  \lxa N} {u0-\l}
\qquad
\ianc{\GG, x : A \prvs M \leadsto N}
{\GG\prvs \l x^{1}:A. M \leadsto  \l^{\#}x:A. N} {1-\#}
\vsk
\ianc{M\in\Sigma\cup\GG\cup\Phi}{\GG \prvs M\leadsto M  }{Id}
\qquad
\ianc{\GG\prvs M \leadsto P \quad \GG\prvs N\leadsto Q}
{\GG \prvs M N^{u}\leadsto P\ Q }{u-app}\vsk
\ianc{\GG\prvs M \leadsto P \quad \GG\prvs N\leadsto Q}
{\GG \prvs M N^{1}\leadsto P\rapp Q }{1app}
\qquad
\ianc{\GG\prvs M \leadsto P}{\GG \prvs M \_^{0}\leadsto P }{0app}\vsk
\end{array}
\]
\caption{Forgetful functor from $\lc$}
\end{figure} 

\bigskip Remark that as far as dependencies are considered the order 
in which argument occurs in the matrix is irrelevant provided that the 
term is linear.  This means that we can consider equivalence classes 
of canonical terms modulo (total) permutation $\pi$ of arguments.  We 
do so in Figure \ref{fig:equiv}.  It is clear from the properties of 
permutations that this is a equivalence relation.  It is convenient to 
agree and name a representative of those classes, say $\rho(M)$ in the 
person of the term whose labeled arguments occur in the matrix in the 
same order as in the context.  This will also disambiguate terms with 
multiple occurrences of $\_^{0}$ by collapsing them in the same class.
\marginpar{I'd like to keep this}

\newcommand{\lequiv}{\stackrel{\mbox{\tiny  $l$}}{\equiv}}

\begin{figure}
\label{fig:equiv}  
\[
\begin{array}{c}
\ianc{}{\GG\prvs  E\ \ol{x_{n}^{l}} \lequiv  E'\ 
\ol{x^{\pi(l)}_{\pi(n)}}}{\lequiv Flex} 
\qquad 
\ianc{ \GG,x:A\prvs  M\lequiv M' }{\GG\prvs \lxa M \lequiv \lxa M' }
{\lequiv Lam}\vsk
\ianc{ h \in\Gamma\cup\Sigma \qquad \GG\prvs  N_{1} \lequiv N'_{1}
\cdots \GG\prvs  N_{n} \lequiv  N'_{n}}
{\GG\prvs h\  \Nn \lequiv h\  \ol{N'_{n}} } {\lequiv App}
\end{array}
\]
\caption{Judgment: $M\lequiv M'$}
\end{figure}

Thus, a consequence of Definition \ref{def:compl} is that 
annotation-equivalent terms have the same complement.

% \begin{Lemma}
% \label{le:eqperm}
% % For every permutation $\pi$ and annotation $l$ of a flexible term 
% If $ E\ \ol{x_{n}^{l}} \lequiv E'\ \ol{x^{\pi(l)}_{\pi(n)}}$ then 
% $\ngl( E\ \ol{x_{n}^{l}}) = \ngl( E'\ \ol{x^{\pi(l)}_{\pi(n)}})$.
% \end{Lemma}
\begin{Lemma}
\label{le:eqperm}
For flexible terms $E,E'$, if $ E \lequiv E'$ then $\ngl( E) = \ngl( E')$.
\end{Lemma}
\begin{proof}
Immediate from the definition of \mnot'.
\end{proof}

\begin{Proposition}
$M \lequiv M'  $ implies $\ngl(M ) = \ngl(M')$.
\end{Proposition}
\begin{proof}
A simple induction on the judgment $M\lequiv M'$ using Lemma \ref{le:eqperm}.
\end{proof}


\section{Conclusions and Future Work}
Blah, blah\ldots

\bit
\item
Pattern complement in dependent types
\item
Term complement in linear frameworks, e.g.\ the simple-typed fragment of 
\emph{LLF}
\item
Implementation: adoption of the spine notation
\enit