\documentclass[landscape]{slides}
%\usepackage{fpslides}
% \usepackage{color}
%\usepackage{amssymb}
%\usepackage{eepic/epic}
%\usepackage{eepic/eepic}
% \usepackage{amssymb}
%\usepackage{cdsty}
%\usepackage{prooftree}
%\def\zzctdrawdotedge{\drawdotedge{4pt}0}
%\def\ctabutborderlr{1em}
%\def\ctabutbordertb{1ex}

\usepackage{latexsym}
 \usepackage{fslide-com}

\newcommand{\ctr}[1]{\begin{array}[c]{c}#1\end{array}}
\newcommand{\rep}[1]{\ulcorner #1\urcorner}
% subset below

% \newcommand{\xn}{\overline{x_n}}
%\newcommand{\Imp}{\rightarrow}
\newcommand{\UImp}{\GImp{u}}
%\newcommand{\ZImp}{\stackrel{\mbox{\tiny  $0$}}{\Imp}}
%\newcommand{\GImp}[1]{\stackrel{\mbox{\tiny  ${#1}$}}{\Imp}}
%\newcommand{\RImp}{\stackrel{\mbox{\tiny  1}}{\Imp}}
\newcommand{\god}{\Gamma; \Omega;\Delta}
\newcommand{\betared}{\stackrel{\beta}{\longrightarrow}}
\newcommand{\etaexp}{\stackrel{\bar\eta}{\longrightarrow}}
\newcommand{\lxua}{\lambda x^{u}\!:\!  A.\, }
\newcommand{\D}{\Delta}
\newcommand{\mmnot}{\neg}
\newcommand{\lf}{\l f\! . \, }
\newcommand{\gdo}{(\GG,\Delta);\Omega;\cdot}
\newcommand{\ctx}{\GG^{+};\cdot;\cdot}
\renewcommand{\O}{\Omega}
\newcommand{\cM}{{\cal M}}

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

\newcommand{\mends}{\vfill\end{slide}}
\renewcommand{\theslide}{\arabic{slide}}

\input fpsfonts.def
%
% Normal Width (61)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Extra Width (70)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Small (73)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Small, Extra Width (85)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Height:
%   Normal: 17 or 18 lines?
%   Small: ??

\pagestyle{plain}
\sloppy
\raggedright
\renewcommand{\arraystretch}{1.5}

\begin{document}

 \begin{slide}{}
  \begin{center}
  {\bf Higher-Order Pattern Complement\\ and Strict
Lambda-Calculus} \\[1em]
  Alberto Momigliano\\
Department of Philosophy\\
  joint work with Frank Pfenning \\[1em]
  Automated Deduction Seminar \\
\today
  \end{center}

  \vspace{1em}
  \begin{enumerate} \itemsep 0pt
   \item The Relative Complement Problem
   \item Higher-Order Patterns
   \item A Strict $\l$-Calculus
   \item The Complement Algorithm
   \item (Intersection and Other Boolean Operations)
	%\item (Relative Complement Revisited)
  \end{enumerate}
  \vfill
 \end{slide}

 \begin{slide}{}
  \slidetitle{Complement Problem}
 \begin{itemize} \itemsep 0pt
 \item
 Take the  signature of numerals:

\beq
\neg(s(0))  =   \{0, s(s(Y))\}  = \{0, s(s(0)),s(s(s(0)))\dots\}
\eneq
\item
An open term $t$  as the intensional representation
of its ground instances, say  $\| t \|$
\item
The {\em complement} of   $t$ is the set of 
ground terms which are not instances of $t$ \ie are not in $\| t 
\|$. Notation (commas represent (set theoretic) union) :
\beq
\|z_{nat}\| -  \|s(0)\| & = &\|0,s(s(Y))\|
\eneq
\item 'Multiple Complement': 
\beq
 \|z_{nat}\| - \|0,s(s(Y))\| & = & \{s(0)\}
\eneq
 %\item Logical specification:
%$$\forall y:z \neq 0 \And  z \neq ssy$$
\end{itemize}
  \vfill
 \end{slide}


\begin{slide}{}
 \slidetitle{Relative Complement}
 \begin{itemize} \itemsep 0pt
  \item
integer addition modulo $2$
\beq
% \label{ex:mod2}
ss0&  \Lmap & 0\\
y+0&  \Lmap & y\\
0+y&  \Lmap & y\\
y+y&  \Lmap &
 0
\eneq
\item The Following Relative Complement problem is related to the issue of 
sufficient completeness.
\[
\| x_1 + x_2\| - \|ss0,0+y,y+0,y+y \| = \eset
\]

\[
\exists x_1x_2\forall y : (z= x_1 + x_2) \And (z \nq ss0)\And (z \nq 
y+0)\And (z \nq 0+y)\And (z \nq y+y)
\]
 \item
All the ground 
instances of a given (finite) set of terms which are not instances of 
another given one. 
\[ \| t_1 \mdots t_n \| - \| u_1 \mdots u_m \| \]
\enit
\vfill
\end{slide}

\begin{slide}{}\slidetitle{Applications}
 \begin{itemize} \itemsep 0pt
  \item

 Functional programming:
\ben
\item
 to determine, modulo pattern 
matching, if a function definition is 
exhaustive and disjunct; even further to produce a non-ambiguous set 
of patterns.  
\item
using the given sequential order of application of clauses to 
provide an improved compiled code:  if a second clause applies, 
the first one does not, \ie terms reducible by  second rule are in the 
complement of the LHS of the first.
\enen
\item Rewriting systems:
\bit
\item
{\em Ground reducibility} and {\em sufficiently completeness} 
 of an algebraic (equational) specification. 
   If not 
complete, the algorithm my lead to recover the missing cases.
\enit\enit\mends
\begin{slide}{}\slidetitle{Applications, $II$}
 \begin{itemize} \itemsep 0pt
  \item
\begin{quote}
``Stop losing sleep over incomplete specifications''
\end{quote}

\item
 Back to  integer addition modulo $2$. Suppose we omit $ y+0  \Lmap  y$

\beq
ss0& \Lmap &0\\
0+y&  \Lmap & y\\
y+y&  \Lmap & 0
\eneq

We can recover the missing LHS:

\[
\| x_1 + x_2\| - \|ss0,y+0,y+y \| = y+0
\]

\item
Infinite transition systems:
the complement of a LHS returns the states from which no transition 
is achievable ( temporal analysis of 
communicating processes).


\end{itemize}
  \vfill
 \end{slide}

 \begin{slide}{} \slidetitle{Applications $III$}

\bit
\item
In machine learning, a concept can be captured by a term with some 
(finite) exceptions: its computation is the search for an explicit 
representation of the former.
\item
inductive theorem proving : 
{\em induction-less induction} or \emph{proof by consistency}

\item
The transformational approach to negation [Sato\& Tamaki $1985$,
 Barbuti et al.\ $1990$]
\enit


Our Aim: extend the latter to Logical Frameworks
  \vfill
 \end{slide}

% \begin{slide}{}
%  \slidetitle{Elimination of Negation in \lp}
%  
% 
% Consider the following fragment of a program for evaluation in Mini-ML:
% 
% \[\begin{array}{lcl}
% eval &:& exp \Imp o.\\
% evalclo & : & eval (E) \If closed (E) \If \ldots\\
% evalop & : & eval (E) \If \neg closed (E) \If \ldots
% \vsk
% closed &:& exp \Imp o.\\
% cloz & : & closed\ z\\
% clolam &: & \Pi E:exp.\ closed\ (lam\ E) \If \PI {x } {exp}\ (closed\ x) 
% \Imp closed\ (E\ x)\\
% cloapp &: & \Pi E_{1}E_{2}:exp.\ closed\ (app\ E_{1} E_{2}) \If 
% closed\ E_1 \And closed\ E_{2}
% \end{array}\]
% 
% Last clause not legal: $\neg closed (E)$ not a predicate (type 
% family).
% \mends
% 
% 
%  \begin{slide}{}
%  \slidetitle{Elimination of Negation in \lp, $II$}
% 
% \[\begin{array}{lcl}
% evalclo & : & eval (E) \If closed (E) \If \ldots\\
% evalop & : & eval (E) \If \emph{open} (E) \If \ldots
% \\
% cloz & : & closed\ z\\
% clolam &: & \Pi E:exp.\ closed\ (lam\ E) \If \PI {x } {exp}\ (closed\ x) 
% \Imp closed\ (E\ x)\\
% cloapp &: & \Pi E_{1}E_{2}:exp.\ closed\ (app\ E_{1} E_{2}) \If 
% closed\ E_1 \And closed\ E_{2}\\
% oplam &: & \Pi E : exp.\ open\ (lam\ E)  \If \PI {x } {exp}\ open\ (E\ x)\\
% opapp &: & \Pi E_{1}E_{2}:exp.\ open\ (app\ E_{1} E_{2}) \If open\ E_1 \Or open\ E_{2}
% \end{array}\]
% where definition of \texttt{open} has been synthesized by the user.
% 
% 
% Aim: mechanize this transformation (when possible) so that
%      % for every ground term $t\hastype exp$:
% $$ def(open)\vd open(E) \mbox{ iff it not the case that } def(closed)\vd open(E)$$
% 
% \vfill
% \end{slide}
 \begin{slide}{} \slidetitle{Elimination of Negation in \fo\lp}
 
\bit
\item
Consider the following fragment of a Prolog program:

\[\begin{array}{l}
p(X,XS) \If member(X,XS) \If \ldots\\
p(X,XS) \If \neg member(X,XS) \If \ldots 
\vsk
member(X,X.XS).\\
member(X,Y.XS)\If member(X,XS)
\end{array}\]

\item
Last clause not a legal Horn clause: $\neg member(X,XS)$ not an atom.

\item Prolog solution: interpret $\neg$ as \emph{negation as 
failure}: ``$\neg A$ holds if $A$ \emph{finitely fails} to hold.

\item Problems (among others): an operational, not declarative notion 
which does not return answer substitutions:

\item Unsuitable for Logical Frameworks

\item Solution: eliminate negation through program transformation
\enit  
 \mends

 \begin{slide}{}
 \slidetitle{Elimination of Negation in \lp, $II$}

\[\begin{array}{l}
p(X,XS) \If member(X,XS) \If \ldots\\
p(X,XS) \If non\_member(X,XS) \If \ldots 
\vsk
member(X,X.XS).\\
member(X,Y.XS)\If member(X,XS)\vsk
non\_member(X,nil).\\
non\_member(X,Y.XS)\If diff(X,Y)\If non\_member(X,XS)
\end{array}\]where definition of \texttt{non\_member} has been synthesized by the user.

\mends
\begin{slide}{}
 \slidetitle{Elimination of Negation in \lp, $III$}
\bit\item
Aim: mechanize this transformation (when possible) so that for every 
ground $x,xs$:
\ben
\item
$def(member),def(non\_member)\vd member(x,xs)$ or 
$def(member),def(non\_member)\vd non\_member(x,xs)$
\item
It is not the case that both
$def(member),def(non\_member)\vd member(x,xs)$ and 
$def(member),def(non\_member)\vd member(x,xs)$
\enen\enit\vfill
\end{slide}

 \begin{slide}{}
\slidetitle{ENLP, $IV$}
\bit
\item
two major steps
\ben
\item
Compute complement of heads in $def(member)$
\item 
Bring definition in negation normal form respecting operational 
semantics (not detailed here)
\enen

\item
Given
$p(t) \If G$, rewrite to
$p(Z) \If Z = t \If G$. 

If $p(t) 
\If G\nprv p(s)$ for $s\neq t$ then 
$\neg p(Z) \If Z\neq t\vd p(s)$
\item
Compute the complement of $t\hastype A$. More in general for 
$ 
p(t_{1})\If G_{1},
\ldots,
p(t_{n}) \If G_{n}$


Compute $\|Z_{A}\| - \| t_{1}\ldots t_{n}\|$
\ie, here $\|Z_{list}\| -\|X.XS\| = nil$
\enit
\vfill
\end{slide}
 
\begin{slide}{}

\slidetitle{First-Order Term Complement,[Lassez\&Marriot, $1987$]}
\bit
\item
Consider a finite (untyped) signature  $\Sigma$ and a term $t$.  
\[ \begin{array} {lll}
\mnot_\Sigma(x  ) & =   \emptyset  \\
\mnot_\Sigma(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_\Sigma(t_{i}), i \in [1,n] \}
\end{array} \]

\item


The ' \mnot'  function tends to produce irrelevant 
outcomes; $\mnot_{\Sigma}(0)$ in the signature of 
lists of numerals contains not only $s(z)$  but also $nil$ 
and $(cons\ z\ zs) $.
\enit
\vfill
\mends

 \begin{slide}{}
\slidetitle{Linearity}
\bit
\item
{\bf CAUTION}:  the intensional representation of terms is not 
closed under complementation. 
Take
$\Sigma = a:i, f: i \Imp i \Imp i$: 

intuitively:
\begin{equation}
\| z \| - \|f(y,y)\|  =  \{a\} \cup \{ f(x,z) \mid x \nq z \}
\end{equation}

But, incorrectly
\[
\mnot(f(y,y)) \stackrel{?}{=} \{a\} 
\]

\item


 Lassez \& Marriot   have shown that the latter 
is correct only for {\em linear} terms, \ie terms without repeated occurrence of the same variable: complement of non-linear 
ones do not have a straightforward finite representation
\enit
\vfill
\mends

\begin{slide}
\slidetitle{Linearity, $II$}
\bit
\item
The restriction to linearity seems to be 
almost immaterial in \lp thanks to the idea of {\em 
left-linearization} [Plaisted, Stickel]:

\item
Allowing only heads with linear terms as argument 
and constraining equal occurrences in the body by a new predicate, say 
$eq$, whose definition is $eq(x,x)$:  it opens 
the road to transformation of the source program 

\item


Other 
approaches include:
\ben

\item
{\em Constrained terms}, where terms as $ f(x,z) \mid x \nq z$  are allowed
\item
Complement operations based on  disunification [Comon, Lugiez].
\enen\enit\vfill
\end{slide}


 \begin{slide}{}
\slidetitle{Complementing Higher-Order Patterns over simple types.
 }

\renewcommand{\S}{\Sigma}



\[ \begin{array}{rrcl}
 \mbox{\textit{Simple Types}} & A & \bnfas &o\bnfalt 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} \]

\bit
\item Restrictions:
% \begin{sloppypar}
All terms are linear and 
Types do not contain occurrences of the primitive type $o$ (see \emph{LF})

\item 
The main difference \wrt the \fo case is twofold: first, the 
second-order (relative) complement  problem is not semi-decidable, but
 higher-order disunification on \ho patterns is decidable [Lugiez $1995$].

\enit\vfill\end{slide}

 \begin{slide}{}
\slidetitle{Fully Applied Pattern}
\bit
\item
Secondly, the treatment  differentiates depending on whether the term 
to be complemented is \emph{fully applied}: 


\renewcommand{\fa}{ \,\ \mbox{\rm {f.a.}}}
 
\[
\begin{array}{c}
\ianc{\ol{x_{\pi(n)}}=dom(\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}}
\end{array}
\]
\item
For fully applied terms proceed similarly to \fo with an additional 
case for bound variables, collected in a context $\GG$, so 
that the complement    is taken \wrt both the signature 
and the current context.
 \item
In the non-fully applied case the complement has to take into account  
% different status of free (logical) and bound variables: the crux lies 
% in the presence of \emph{dependency constraints}, \ie 
whether some of the variables mentioned in a lambda binder does appear in 
the matrix.  

\enit\vfill\end{slide}


 \begin{slide}{}
\slidetitle{Encoding the the (untyped) 
$\l$-calculus}


\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
\bit\item
Encoding a $\beta$-redex:
\beq
\mid (\lx E\ x)\ F\mid & = & app\ (lam\  (\lamb{x}{exp} (E\ x))\ F
\eneq

%  $\lamb{x} {exp} app \ (E_{1}\ x) (E_{2}\ x)$ represents the set
% of all unary functions which return an application (in the object language).

\item
Its complement 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\}
 \]
% %\item
% %Signature of numerals: $
% %N  \bnfas  0 \mid s(N)
% %$
%   \enit
% \beq
% \cdot\prv\mmnot(\lf  f 0: (nat\Imp nat)\Imp nat) =\\
%    \{\lf 0,\lf s(N_{1}\ f), \lf f(f(N_{2}\ f)), \lf f(s(N_{3}\ f))\}
% \eneq
\enit
\mends

\begin{slide}
\slidetitle{FAHP Complement}
 For a linear  
$M$ such that $\GG \prv  M \hastype  A$ define $\GG\prv  \mnot(M) = N : A$ as:

\[
\begin{array}{c}
\ianc{\GG,x\oftp A\prv  \mnot( M)  =  N : B}
{\GG\prv  \mnot(\lxa M)  = \lxa N : A\Imp B}{\mnot\_Lam}
\vsk
\ianc{g\in\Sigma\cup\GG, g \oftp A_{1}\Imp\dots\Imp A_{m}\Imp 
P\quad m\geq 0,h \not\equiv g   } 
{\GG\prv  \mnot (h\ \Mn) = 
(\dots (g\ (Z_{1} \GG))\dots (Z_{m}\GG)) : P} {\mnot\_App^{1}}
\vsk
\ianc{ h\in\Sigma\cup\GG, \GG\prv h\oftp A_{1}\Imp\dots\Imp A_{n}\Imp P, 1\leq i\leq n, \GG\prv \mnot( M_i) = N : A_i } 
{\GG\prv  \mnot (h\ \Mn^1) = 
(\dots (h\ (Z_{1}\GG ))\dots (Z_{i-1}\GG ) \ N\ 
(Z_{i+1}\GG )\dots (Z_{m}\GG)) : P} {\mnot\_App^{2}}
\end{array}
\]
% \end{small}

 $m\geq 0$ and  $(Z\ \GG)$'s denotes the application of a fresh 
variable of opportune typing to a  context.  

\beq
 \mmnot(M\hastype A) = \{N\mid\cdot\prv \mnot(M)=N:A\}
 \eneq
\mends


 \begin{slide}{}
\slidetitle{NFA Patterns}
\bit
\item

%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
Encoding a $\eta$-redex, where $x\not\in FV(E)$:
\beq
\mid \lx E\ x\mid & = & lam(\lamb{x}{exp} app\ E\ x)
\eneq

\item Hence $E$ {\em does not} depend on $x$.  Intuitively its 
complement should contain those applications where $E$ {\em does } 
depend on $x$.

\item

The simply typed 
$\l$-calculus 
theory is not strong enough to directly represent the complement of non-fully 
applied patterns. For patterns which are not fully applied, the complement cannot
be expressed as a finite set of patterns

\item
 This 
cannot be avoided similarly 
to left-linearization
We need to have a notion of \emph{strictness} in the language.
\enit\mends

\begin{slide}
\slidetitle{Strictness}
\bit
\item
 Lugiez modifies the language 
of terms to promote constraints to first-class objects, 
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.
 

 \item

 We 
generalize our language to include 
\ben
\item
\emph{strict functions} of type $A
\RImp B$ (which are guaranteed to depend on their argument) 
\item

\emph{invariant functions} of type $A \ZImp B$ (which are guaranteed
\textbf{not} to depend on their argument). 
\item The full
function space $A \UImp B$.
\enen
\enit
\mends

\begin{slide}{}
\slidetitle{The language of strict types}
\bit
\item 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. 

\[ \begin{array}{rrcl}
 \mbox{\textit{Labels}} & k & \bnfas & 1 \bnfalt 0 \bnfalt u \\
 \mbox{\textit{Types}} & A & \bnfas & o\bnfalt 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} \]
 \item Typing judgment: $\god\vd M\hastype A$.
\enit
\mends

 \begin{slide}{}
\slidetitle{Typing rules}

\[ \begin{array}{c}
 \ianc{c\oftp A \in \Sigma}{\Gamma; \Omega; \cdot \vd c \hastype A}{Con}
\quad
 \mbox{\textit{no $Id^0$ rule}}
\vsk
 \ianc{}{(\Gamma, x\oftp A); \Omega; \cdot \vd x \hastype A}{Id^u}
 
 \quad
 \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]
\end{array}
\]\mends

\begin{slide}{}
\slidetitle{Typing rules, continued}

\[ \begin{array}{c}
 \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} \]
\mends



% \newcommand{\jj}{\justifies}
% 
% \prooftree
% \[ \mbox{} \jj\cdot;y : A; x  : A \RImp A\RImp B \prv x : A \RImp A\RImp B \using 
% Id^1 \]
%  \qquad 
% \[ \mbox{} \jj \cdot ; x: A \RImp A\RImp B ; y  : A\prv y: A \using Id^1\using \RImp E\]
% \justifies
% \[
% \cdot; y : A; x  : A \RImp A\RImp B , y  :A\prv x y^1 : A\RImp B \jj\]
% \qquad 
% \[\mbox{} \jj \cdot; x :A \RImp A\RImp B, y: A; y  : A\prv y: A
% \using \RImp E\]
% \justifies
% \[
%  \cdot;\cdot; x  : A \RImp A\RImp B ,y^{1}: A\prv (x y^1)  y^1 : B
%  \using \RImp I
%  \justifies
%  \[
%  \cdot;\cdot; x  : A \RImp A\RImp B  \prv \l y^1 . (x y^1)  y^1 : A\RImp B
%  \using \RImp I
%  \justifies
% \cdot;\cdot;\cdot\prv \l x^1.\l y^1. (x y^1)  y^1  : (A \RImp A\RImp B)\RImp (A\RImp 
% B)
% \]
% \]
% \]
% \endprooftree

 \begin{slide}{}
\slidetitle{Properties}
\bit
\item
 {\bf Theorem [Weakening]} \mbox{}
 \begin{enumerate}
  \item (Weakening$^{u}$) If $\Gamma; \Omega; \Delta\vd M \hastype C$ then $(\Gamma, 
  x\oftp A); \Omega; \Delta\vd M \hastype C$. 
  \item (Weakening$^{0}$) 
  If $\Gamma; \Omega; \Delta\vd M \hastype C$ then $\Gamma
  ; (\Omega, x\oftp A); \Delta\vd M \hastype C$. 
  \end{enumerate}


\item
{\bf Theorem [Loosening$^{0}$]}

If $\Gamma; (\Omega,\Phi); \Delta\vd M \hastype A$ then $(\Gamma, 
\Phi); \Omega; \Delta\vd M \hastype A$. 

\item
{\bf Theorem [Loosening$^{1}$]}

If $\Gamma; \Omega; \Delta\vd M \hastype A$ then $\gdo\vd M \hastype A$. 
\enit
\mends
 \begin{slide}{}
\slidetitle{Properties, $II$}

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


\item
{\bf Theorem [Contraction}]
  (Contraction$^{u}$)
  If $(\Gamma, x\oftp A, y\oftp A);\Omega;\Delta \vd M
\hastype C$ then $(\Gamma, z\oftp A) ;\Omega;\Delta\vd [z/x][z/y]M \hastype C$.
etc...
 \enit
\mends

 \begin{slide}{}
\slidetitle{Subject Reduction and Expansion}
\bit
\item
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} \]
 
%\item
%One of the main reason to introduce irrelevant variables, as 
%ones which \emph{may} occur but \emph{must not} be used, is to 
%well-type $\eta$-expansion of invariant functions:
%\[ \begin{array}{rcl}
  
%   M \hastype A \GImp{0} B & \etaexp & \lam x^0\oftp A\ldot M\, x^0 \\
% \end{array} \]
  
\item
%The subject reduction and expansion theorems are a direct consequence 
%of the structural and substitution properties.

{\bf Theorem [Subject Reduction]} \mbox{}

If $\Gamma;\Omega; \Delta \vd M \hastype A$ and $M \betared M'$ then 
$\Gamma;\Omega; \Delta \vd M' \hastype A$.

\item
{\bf Theorem [Subject   Expansion]} \mbox{}

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$.
\enit
\mends
 \begin{slide}{}

\slidetitle{Canonical forms for $\lc$}


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

\[
\begin{array}{c}
\ianc{}{\GG;\Omega; x\oftp A \prv  x\da A} {cId^{1}}
\vsk
\ianc{}{(\GG,x\oftp A);\Omega; \cdot  \prv  x\da A}{cId^{u}}\vsk
 \mbox{\textrm{no rule for }}cId^{0}\vsk
\ianc{c\oftp A\in\Sigma}{\GG; \Omega;\cdot  \prv  c\da A}{cIdc}
\end{array}\]
\mends
\begin{slide}{}

\slidetitle{Canonical forms for $\lc$, $II$}

\[
\begin{array}{c}

%\ianc{}{\GG;\Omega;\Delta\vd E\ \ol{x_{n}^{l}}\da P}{cPat}
%\qquad
\ianc{\GG;\Omega;\Delta \prv  M\da P}{\GG;\Omega;\Delta \prv  M\bua P} 
{cAt}\vsk
\ianc{(\GG,x\oftp A) ; \Omega;\Delta \prv M\bua B}{\GG;\Omega;\Delta\prv(\lamb{x^u}{A} M) \bua 
A\TImp B} {c\TImp I}
\vsk
\ianc{\GG ; \Omega; (\Delta,x\oftp A) \prv M\bua B}{\GG;\Delta\prv(\lamb{x^1}{A} M) \bua 
A\RImp B}{c\RImp I}
\vsk
\ianc{\GG ;(\Omega, x\oftp A) ;\Delta \prv M\bua B}{\GG;\Omega;\Delta\prv(\lamb{x^0}{A} M) \bua 
A\ZImp B}{c\ZImp I}
\end{array}\]
\mends
\begin{slide}{}

\slidetitle{Canonical forms for $\lc$, continued}


\[
\begin{array}{c}
\vsk
 \ibnc{\Gamma; \Omega; \Delta \vd M \da A \TImp B}{\Gamma;
(\Omega, \Delta); \cdot \vd N \bua A}{\Gamma; \Omega; \Delta
\vd M\, N^u \da B}{c\GImp{u}E}
\vsk
\ianc{\GG;\Omega;\Delta\prv M \da A \ZImp B \quad (\GG,\Omega);\Delta;\cdot \prv N \bua A
}
{\GG;\Omega;\Delta  \prv M  \ N^0 \da B}{c\ZImp E}\vsk
 \ibnc{\Gamma; (\Omega, \Delta_N); (\Delta_M, \Delta_{MN}) \vd M
\da A \RImp B}{\Gamma; (\Omega, \Delta_M); (\Delta_N, \Delta_{MN})
\vd N \bua A}{\Gamma; \Omega; (\Delta_M, \Delta_N, \Delta_{MN}) \vd
M\, N^1 \da B}{c\RImp E}
\end{array}
\]


Typing rule and the the canonical form for logic 
variables:

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



%{\bf Theorem [Canonical Form Theorem]}

%Assume $\god\vd M\hastype A$ and $M$ 'reduces' to $N$. Then 
%\ben 
%\item $\GG;\Omega;\Delta\prv N\da A$.
%\item $\GG;\Omega;\Delta\prv N \bua A$.
%\enen
\mends

 \begin{slide}{}
\slidetitle{Complement Desiderata}
\bit
\item
The complement operator must satisfy the usual boolean 
rules for negation, that is:

\ben
\item (Disjointness) It is not the case that $M$ is both a ground 
instance of $N$  and of $\mmnot(N)$.

\item (Exhaustivity) $M$ is a ground instance of $N$ or $M$ is a 
ground instance of $\mmnot(N)$.
\enen
 

%\enit
%\mends
%\begin{slide}{}
%\slidetitle{Complement desiderata, $II$}
%\bit
\item
The second property does not hold in 
general as we allowed intuitionistic functions. 

\[
\begin{array}{l}
y\oftp ((a\Imp a)\Imp a)\Imp a, x\oftp a\vd y(\lamb{f}{a\Imp a} f\ 
x) \\
y\oftp ((a\Imp a)\Imp a)\Imp a, x\oftp a\vd y(\lamb{f}{a\Imp a} x)
\end{array}
\]
 

% $y$ is well-typed but the above term does not satisfy exhaustivity. 
\enit
\mends

\begin{slide}{}

\slidetitle{ Simple Terms}
\bit
\item
 We 
must therefore isolate the right fragment of the strict calculus: 



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

Note that the first item is not required for disjointness.

%\item
%Existential variables:

%\[ M \in \|E\ z^{1}\|  \mbox{\textrm{ or }}  M \in \|\mmnot (E\ 
%z^{1})\|\]
%\ie
%\[ M \in \|E\ z^{1}\|  \mbox{\textrm{ or }}  M \in \|F\ 
%z^{0}\|\]

 \item
Idea:  make the status of terms as determined as possible, 
while preserving the possibility of well-typing sub-terms as $y$ 
above. 
\item

Trick is to keep undetermined every negative occurrence of 
the arrow, while making determined the positive ones.
\enit\mends

 \begin{slide}{}
\slidetitle{Embedding}

\beq
(A\Imp B)^{-} & = & A^{+} \TImp B^{-}\\
(A\Imp B)^{+} & = & A^{-} \RImp B^{+}\\
P^{\pm} & = & P
\vsk
(\lxa M)^{-} & = & \lamb{x^{u}}{A^{+}} M^{-}\\
M^{-} & = & M^{+}\\
x^{+} & = & x\\
(E_A\ \xn)^{+} &=& F_{A^{-}} \ \xn^u\\
(M\ N)^{+} & = & (M^{+}\ N^{-})^{1}\\
[1em]
(\cdot)^{+} & = & \cdot\\
(\GG,x\oftp A)^{+} & = & \GG^{+}, x\oftp A^{+}\\
(\Sigma,P\oftp type)^{+} & = & \Sigma^{+}, P\oftp type\\
(\Sigma,c\oftp A)^{+} & = & \Sigma^{+}, c\oftp A^{+}
\eneq
\mends
 \begin{slide}{}
\slidetitle{Simple Terms, $II$}

\beq
\lefteqn{(y\oftp ((a\Imp a)\Imp a)\Imp a, x\oftp a)^{+}\vd (y(\lamb{f}{a\Imp a} f\ 
x))^{+}  = }\\
& & y\oftp ((a\RImp a)\TImp a)\RImp a, x\oftp a\vd y(\lamb{f^{u}}{a\RImp a} f\ 
x^{1})^{1}\\
\lefteqn{(y\oftp (a\Imp a)\Imp a, x\oftp a)^{+}\vd (y(\lamb{f}{a\Imp a} x))^{+}  = }\\
& & y\oftp ((a\RImp a)\TImp a)\RImp a, x\oftp a\vd 
y(\lamb{f^{u}}{a\RImp a} x)^{1}
\eneq

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

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


{\bf Theorem 
}
If $\GG\vd M\buda A$ then $\ctx\vd M^{-}\buda A^{-}$.
\mends
 \begin{slide}{}

\slidetitle{Full Application}

\bit
\item
Make every term fully: a translation from simple terms

\item
Write $Z\ \GG^{u}$ for $Z\ x_{1}^{u}\dots x_{n}^{u}$, where 
$x_{1}\dots x_{n}\in dom(\GG)$.


\newcommand{\LBimp}{\longleftrightarrow}
\newcommand{\emp}{;\cdot;\cdot}

 
\[
\begin{array}{c}
\ianc{}{(\GG,\Omega)\emp\prv  E\ \pi(\GG^{u}) \LBimp F\ \GG^{u} \
 \Omega^{0}}{\mbox{\rm Trn\_Pat}} 
\vsk
\ianc{ (\GG,x\oftp A)\emp \prv  M \LBimp  N }
{\GG\emp\prv \lxua M \LBimp  \lamb{x^u}{A }N }{\mbox{\rm Trn\_Lam}}\vsk
\ianc{  \GG\emp\prv  M_{1}  \LBimp   N_{1}\cdots \GG\emp\prv  M_{n} \LBimp   N_{n} }
{\GG\emp\prv h\  \Mn^{1} \LBimp   h\ \Nn^{1}} {\mbox{\rm Trn\_App}}
\end{array}
\]
\[ \begin{array}{rrcl}
\mbox{\textit{Simple Terms}} & M & \bnfas &  \lam x^{u}\oftp
A^{+}\ldot M \bnfalt (\dots (h\ M_1)^{1} \dots M_n)^{1}\bnfalt E\ 
\ol{x^{l}_{n}}
\end{array} \]

{\bf Theorem }
% \label{thm:fat}
If  $\GG\emp \vd N 
\LBimp Q$, then $\GG\emp\vd M\in\|N\|\hastype A$ iff $\GG\emp \vd M\in 
\|Q\|\hastype A$.
\enit\mends

 \begin{slide}{}

\slidetitle{The Complement Algorithm}
\bit
\item
Idea: form 
a set of terms  according to the occurrence status of every 
variable; if  determined  a term 
with the given variable annotated with the complement of the 
annotation is built where the remaining variables are set to 
undetermined, otherwise we do nothing 
 \item
Observe that the complement operation on terms behaves on 
labels like negation does on truth-values in Kleene's logic

\beq 
\mnot(1)=0 \quad
\mnot(0)=1 \quad
\mnot(u) = u
\eneq
\enit

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


Define $\mmnot(M\hastype A) = \{N\mid\cdot\prv \mnot(M)=N:A\}$

\mends

 \begin{slide}{}
\slidetitle{Examples of Complementation}
\bit
\item
If $E$ is a variable, it has the canonical form $\l 
\ol{x_{n}^{u}}.E\ \ol{x_{n}^{u}}$: hence $\mmnot(E) = \eset$.

\beq
\mmnot( E\ x^{0} y^{1}) & = & \{  F\  
x^{1} y^{u},   G\  x^{u} y^{0}\} \label{eq:l}\\
\mmnot(  E\ x^{u} y^{1}) & = & \{  F\  x^{u} y^{0}\}\nonumber
\eneq

\item
Members of a complement set  are not 
mutually disjoint, due to the indeterminacy of $u$. 
Above equation  can be made explicit into:
\[
\{F_{1} \ x^{1} y^{1} ,    G_{1} \ x^{1} y^{0} ,   G_{2} \ x^{0} y^{0}\}
\]


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

\enit
\beq
\lefteqn{\mmnot(\l x^{u}\l y^{u}.\, s(M\ x^{1} y^{0})^{1} \hastype
  nat\Imp nat\Imp nat)  =}\\
& \{ \l x^u\l y^u .\, x, \l x^u\l y^u .\, y, \l x^u\l y^u .\, 0, \l 
x^u\l y^u .\, s(N\ x^{0} y^{u})^{1}, \l x^u\l y^u .\, s(N'\ x^{u} 
y^{1})^{1} \} 
\eneq

\mends

 \begin{slide}{}
\slidetitle{Results}
\bit
\item
{\bf Theorem }
If $M$ is a simple term, so is $N$, for all $N\in\mmnot(M)$.


\item

{\bf Theorem }
It is not the case that both $\GG\vd M \in \| N\|:A$ and $\GG\vd M \in 
\| \mmnot(N)\|:A$.




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

\item
{\bf Lemma}  Let $M$ be a simple patterns:

If $\cu\vd M\buda A$ then $\cxtr\vd M\buda A$ or $\cxto\vd M\buda A$.
\item


{\bf Theorem }

if $\cD::\GG\vd M\buda A$ then $\GG \prv M\in \| N \| :A$ or $ \GG \prv M\in 
\| \mmnot(N)\| : A$.

\enit\mends

\begin{slide}{}
\slidetitle{Elimination of negation in a logical framework}
\bit
\item Consider the following program:
\[
\begin{array}{lrl}
betarx & : & isredx(app\ (lam\ (\lamb{x}{exp} E\ x))\ F )\\
etarx & : & isredx(lam(\lamb{x}{exp} app\ M\ x))
\end{array}\]

\item What about its negation? Compute the complement of its clause and 
combine:

\beq
\mmnot(app\ lam \ (\lamb{x}{exp} E\ x)\ F)= 
\{ lam(\lamb{x}{exp} H\ x), app\ (app\ H_{1}\ H_{2})\ H\}\\
\eneq
\enit
\mends
\begin{slide}{}
\slidetitle{Elimination of negation in a logical framework, $II$}
\[\begin{array}{l}
\mmnot(lam(\lamb{x}{exp} app\ M\ x))=\\
app\ H_1\ H_2, lam(\lamb{x}{exp} lam(\lamb{y}{exp} H_3\ x\ y) ),\\
 lam(\lamb{x}{exp} app\ (H\ x^1)\ (app\ H_4\ H_5)),  \\
lam(\lamb{x}{exp} app\ (H\ x^1)\ ( lam(\lamb{y}{exp} H_6\ x\ y))
\end{array}
\]
\bit
\item We can compute $\|Z_{exp}\| -\|app\ (lam\ (\lamb{x}{exp} E\ x))\ 
F,lam(\lamb{x}{exp} app\ M\ x)\|$ by intersecting $\mmnot(app\ (lam\ (\lamb{x}{exp} E\ x))\ 
F)$ and $ \mmnot(lam(\lamb{x}{exp} app\ M\ x))$
 
 \item We can implement intersection as \emph{unification} of simple 
 terms (next time)
 \enit
 \mends
 
 \begin{slide}{}
 \slidetitle{Conclusions}
 \bit
 \item
 The (relative) complement problem is interesting
 \item
 Even restricted to patterns, it does not generalize immediately to 
 the \ho case: we need to have an intrinsic notion of strictness
 \item
 We have presented a strict $\l$- calculus, which  we think gives a 
 contribution to the understanding of sub-structural calculi
 \item
 We have shown how to perform any boolean operation on sets of simple 
 terms
\enit\mends
 \begin{slide}{}
 \slidetitle{Future work}
 \bit
 \item Address the  issue of complement and intersection on \emph{any} strict 
 term
  \item Formulate a Strict LF
\item Apply to \emph{LLF}
\enit

All items  are non-trivial.

\mends
\end{document}


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

Compatibility of labeling are compatible:
the symmetric and idempotent extension of the following partial 
operation: $1\cap u = 1, 0\cap u = 0, u\cap u = u$. 

Extend 
it  to lists (contexts) of labeled variables;

\beq
\cdot\mcap \cdot & = &  \cdot\\
x^k,xs\mcap x^{k'},ys & = &  x^{k\mcap k'},(xs\mcap ys)
\quad\mbox{\textrm{if $k\mcap k'$ is defined}}
\eneq


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


% \begin{small}
\[
\begin{array}{c}
\ianc{\Phi_1\mcap \Phi_2 = \Phi%\quad \Phi\not = nil
 }
{\GG\prv  E \ \Phi_1\mcap   F\ \Phi_2= H\ \Phi : P} 
{\mcap\_FlexFlex}
\vsk
\mbox{\textrm{no rule for flex-flex same}}
\vsk
\ianc{\GG,x\oftp A\prv   M  \mcap  N = Q: B}
{\GG\prv   \lxua M  \mcap \lxua N =\lxua Q : A\Imp B}{\mcap\_Lam}
\vsk
\ianc{c\in\Sigma\quad \GG\prv  H_1 \ \Phi_{1}\mcap 
M_{1}=N_{1}:A_{1}\cdots \GG\prv  H_n \ \Phi_{n}\mcap 
M_{n}=N_{n}:A_{n}  } 
{ \GG\prv  E \ \Phi \mcap c\ \Mn^{1}= c\ \Nn^{1}: P} {\mcap\_FlexRgd_c^{*}}
\vsk
\ianc{y\in\GG\quad  \quad \GG\prv  H_1 \ \Phi_{1}\mcap 
M_{1}=N_{1}:A_{1}\cdots \GG\prv  H_n \ \Phi_{n}\mcap 
M_{n}=N_{n}:A_{n} } 
{\GG\prv E\ \Phi \mcap y\ \Mn^{1}= y\ \Nn^{1} : P} {\mcap\_FlexRgd_y^{\#}}
\vsk
\ianc{ h\in\GG\cup\Sigma\quad \GG\prv  M_1 \mcap N_{1} = Q_1: A_1 \cdots \GG\prv  M_n \mcap 
N_{n}= Q_n : A_n} 
{\GG\prv   h\ \Mm^{1}\mcap h\ \Nn^{1} = h\ \ol{Q_{n}^{1}} : P} {\mcap\_App}
\end{array}
\]
% \end{small}

 \begin{slide}{}
 The rule 
$\mcap\_FlexRgd_c^{*}$ has the following proviso: 
\beq
\forall x. \Phi(x) = 0 & \Imp & \forall i:1\leq i\leq n. \Phi_{i}(x) = 0\\ 
\forall x. \Phi(x) = u & \Imp & \forall i. \Phi_{i}(x) = u\\ 
\forall x. \Phi(x) = 1 & \Imp & \exists i. \Phi_{i}(x) = 1
\And \forall j, j\not = i. \Phi_{j}(x)\not = u
\eneq
The rule 

$\mcap\_FlexRgd_y^{\#}$ has the additional proviso: 
\beq
\Phi(y) \not = 0\And . \Phi(y)=1& \Imp & \forall i. \Phi_{i}(y) = u\ignore{\\
\forall x. \Phi(x) = 0 & \Imp & \forall i. \Phi_{i}(x) = 0\\ 
\forall x. \Phi(x) = u & \Imp & \forall i. \Phi_{i}(x) = u\\ 
\forall x. \Phi(x) = 1 & \Imp & \exists i. \Phi_{i}(x) = 0
\And \forall j, j\not = i. \Phi_{j}(x)\not = u
}\eneq


$M\mbigcap N :A  = \{Q\mid\cdot\prv  M\mcap N = Q : A\}$


  Rule $\mcap\_FlexFlex$  assumes  the same list 
of variables,  with different labeling is the argument of $E,F$ 
and $G$, since simple terms are fully-applied and due to linearity we 
can always reorder the context to the same list. 

 Thanks to linearity 
 the flex-flex same variable case does not occur. 

In the rule $\mcap\_FlexRgd$ the proviso is compelled by the typing 
rules not to leave the status of $x$ undetermined in the antecedent, 
when $a$ is a constant.  If instead $y$ is the projected variable, it 
\textbf{does} occur in the RHS: hence it \emph{ought to} occur in the 
LHS: moreover, since it did occur, it is set to $u$ in the rest of the 
computation.


The  example illustrates how   unification on simple terms can be finitary.

\begin{example}
\beq
\lefteqn{x^{u}\oftp A\prv E\ x^{1}\mbigcap\  c\ (F_{1}\  x^{u})^{1} \ (F_{2}\  
x^{u})^{1} = }\\
& \{c\ (H_{1}\  x^{1})^{1} \ (H_{2}\  x^{0})^1,c\ (H_{1}\  x^{0})^1 \ (H_{2}\  
x^{1})^1,c\ (H_{1}\  x^{1})^1 \ (H_{2}\  x^{1})^1\}
\eneq
\end{example}


 \begin{slide}{}

\begin{Lemma}
\label{le:flexunif}
$\GG\prv M\in\|E\ \Phi_{1}\|:P$ and $\GG\prv M\in\|F\ \Phi_{2}\|:P$ iff $\GG\prv 
M\in\|H\ \Phi_{1}\mcap \Phi_{2}\|:P$.
\end{Lemma}

\begin{Corollary}
\label{co:unif}
 $\GG\prv M\in\|N_{1}\|:A$ and $\GG\prv M\in\|N_{2}\|:A$, where $\GG\vd 
N_{1}\mcap N_{2}= N$, iff $\GG\prv M\in\|N\|:A$.
\end{Corollary}

We now extend the intersection operators to \emph{sets} of terms: if 
$\cM$ and $\cN$ are sets of terms of type $A$, define:

 \beq
\cM \bigcap_{A} \cN & = & \bigcup_{M\in \cM}^{N\in \cN} M\mbigcap N:A
 \eneq

Furthermore we may do the same \wrt complementation:

\beq 
\mmnot_{A} \cM & = & \bigcap_{M\in\cM} \mmnot M:A 
\eneq

Note that the former definition implicitly uses De Morgan laws: it 
is therefore possible to organize the set of finite sets of terms of a 
given type say $\mathbf{\cal T}_{A}$ in a boolean algebra
$
\la \mathbf{\cal T}_{A},\eset_{A}, 
\bigcup_{A},\bigcap_{A},\mmnot_{A}\ra
$
under set union, patterns intersection and complementation.
This means also that any other boolean operation in definable: indeed 
complementation and intersection  alone allows to define the 
\emph{relative} complement operation: if 
$\cM$ and $\cN$ are sets of terms of type $A$, define:
\beq
\cM - \cN & = & \cM\bigcap_{A} (\mmnot_{A} \cN)
\eneq
 \begin{slide}{}

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


\end{document}