\documentclass[landscape]{slides}
%\usepackage{fpslides}
% \usepackage{color}
%%%%%\usepackage{amssymb}
%\usepackage{eepic/epic}
%\usepackage{eepic/eepic}


\usepackage{latexsym}
% \usepackage{amssymb}
%\usepackage{cdsty}
%\usepackage{prooftree}
\usepackage{amsfonts}
%\def\zzctdrawdotedge{\drawdotedge{4pt}0}
%\def\ctabutborderlr{1em}
%\def\ctabutbordertb{1ex}

\newcommand{\ctr}[1]{\begin{array}[c]{c}#1\end{array}}
\newcommand{\rep}[1]{\ulcorner #1\urcorner}
% subset below
 \usepackage{fslide-com}
% \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}{\mnot}
\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 The Relative  Complement Problem\\ for Higher-Order Patterns
} \\[1em]
  Alberto Momigliano\\
Carnegie Mellon University\\[1em]
  joint work with Frank Pfenning \\

September 9 1999
  \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
An open term $t$  as the intensional representation
of its ground instances, denoted  $\| t \|$
\item
The {\em complement} of   $t$ is the set of 
ground terms which are not instances of $t$ \ie are not in $\| t 
\|$. 
 \item
 Take the  signature of numerals:
\[
\begin{array}{l}
\mnot (s(0))    = \{0, s(s(0)),s(s(s(0)))\dots\}=   \{0, s(s(Y))\}
\\
|z_{nat}\| -  \|s(0)\|  = \|0,s(s(Y))\|\qquad\mbox{Notation}
\end{array}\]
\item 'Multiple Complement': 
\beq
 \|z_{nat}\| - \|0,s(s(Y))\| =\mnot(0)\cap\mnot(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
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 \| \]
 \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 Example (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)
% \]

\enit
\vfill
\end{slide}

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

 Functional programming:
\ben
\item
determination of  exhaustivity and disjunctness of a function
definition by patterns
\item improved compilation  by analysis of pattern applicability
\enen
\item Rewriting systems:
\ben
\item {\em Sufficient completeness} 
 of an algebraic (equational) specification. 
\item
Infinite transition systems (temporal analysis of 
communicating processes).
\enen
\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 $II$}

\bit

\item
Machine learning: a concept  as a term with some 
(finite) exceptions: 
\item
inductive theorem proving : 
{\em induction-less induction} or \emph{proof by consistency}
\item Logic Programming
\ben
\item Anserws to negative goal as complement of answers to positive
  one [Kunen 1987]
\item
The transformational approach to negation [Sato\& Tamaki $1985$,
 Barbuti et al.\ $1990$]
\enen\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}
\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. 
Let $\Sigma = a:i, f: i \Imp i \Imp i$: 
\beq
\| z \| - \|f(y,y)\| &  = & \{a\} \cup \{ f(x,z) \mid x \nq z \}
\eneq

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

\item

Correct only for {\em linear} terms, \ie terms without repeated
occurrence of the same variable [ Lassez \& Marriot 1987]. 

\item
Left-linearization [Plaisted, Stickel]
\item
{\em Constrained terms},  as $ f(x,z) \mid x \nq z$.
 \item
 Complement operations based on  disunification [Comon].
\enit

\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{Higher-Order Patterns over simple types.
 }

\renewcommand{\S}{\Sigma}

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

\bit
\item 
\textbf{Note } the 
second-order relative complement  problem is not semi-decidable, but
 higher-order disunification on \ho patterns is decidable [Lugiez $1995$].

\item
Patterns [Miller 1991]: terms where  every free variable is applied to distinct
bound variables. Restriction of $\l$-terms that makes unification unary.
Examples:
$\lx c(E\ x)$, $\l x\l y \,.\,F\ y\ x$
 Non-Examples: 
$\lx E\ c$, $\lx F(E\ x)$, $\lx E\ x\ x$.
\enit
\vfill\end{slide}

 \begin{slide}{}
\slidetitle{Fully Applied Pattern}
\bit
\item
The complement  differentiates depending on whether the term 
is \emph{fully applied}, \ie when all variables
appearing in the binder are mentioned in the scope of a free variable:
\bit
\item Examples:
$\l x\l y\l z\,.\, c(E(y,x,z))$
\item Non-Examples
$\l x\l y\l z\,.\, E\ y$
\enit


% \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:   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 
the occurrence issue.

\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

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

 Complement of the latter:
\beq
\lefteqn{\mmnot(app\ (lam\ (\lamb{x}{exp} (E\ x))\ F)=}\\ 
&& \{ lam\ (\lamb{x}{exp} H\ x), app\ (app\ H_{1}\ H_{2})\ H\}
 \eneq
% %\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}

\[
\begin{array}{c}
\ianc{\GG,x\oftp A\prv  \mnot( M)  =  N \hastype  B}
{\GG\prv  \mnot(\lxa M)  = \lxa N \hastype  A\Imp B}{\l}
\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)) \hastype  P} {Ap^{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 \hastype  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)) \hastype  P} {Ap^{2}}
\end{array}
\]
% \end{small}

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

\beq
 \mmnot(M\hastype A) = \{N\mid\cdot\prv \mnot(M)=N\hastype 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
\rep{\lx E\ x} & = & 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.
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 
given function either will or will not depend on its argument, but in
the presence of existential variables we  need  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 (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)$.


\item How we embed the original $\lambda$-calculus,
and is the calculus now closed under complement?

\item
Exhaustivity does not hold in 
general as we logic variables in NFA terms

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




\enit
\mends

\begin{slide}{}

\slidetitle{ Simple Terms}

\[
\begin{array}{rcl}
\rep{\lambda x.\, \lambda y.\, x} = lam\ (\lamb{x}{exp} lam\ (\lamb{y}{exp} x))
\end{array}
\]
\bit\item
  argument to the first occurrence of\ `$lam$' is  strict,
 argument to the second s  invariant. Type must be
$(exp \GImp{u} exp) \GImp{1} exp$.

\item Constants (and bound variables) are strict functions
\item Second order functions must be undetermined.
\enit\mends
\begin{slide}{}

\slidetitle{ Simple Terms continued}
\bit
\item
In general
\ben
\item positive occurrence of function
types are translated to strict functions,
\item while negative occurrences to
undetermined functions.

\enen
\item Make NFA terms fully applied:
\beq
\l x\l y\l z\,.\, E\ y&\Rightarrow &\l x^u\l y^u\l z^u\,.\,E\ x^0\ y^u\ z^0
\eneq
\item The resulting language:

\[ \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^l
 \end{array} \]
\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 plus the full application translation yields:

% \[ \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^l
% \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  For logic  variables consider each argument in turn
\ben
\item  If an argument variable is undetermined
it does not contribute to the negation. 
\item If an argument variable is strict
 complement the corresponding label from $1$
to $0$ while all other arguments are undetermined.
\item  For vacuous
argument variables we proceed dually
\enen
\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} {}
\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 \hastype  B}
{\GG\prv  \mnot(\lxua M)  = \lxua N \hastype  A\Imp B}{}
\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} \hastype  P} {}
\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 \hastype  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} \hastype  P} {}
\end{array}
\]
% \end{small}


\bit
\item $$\mmnot(M\hastype A) = \{N\mid\cdot\prv \mnot(M)=N\hastype A\}$$
\enit
\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$.

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

\beq
\lefteqn{\mmnot(lam(\lamb{x^{u}}{exp} app\ (E\ x^{0})\ x ))=}\\
& & \{ lam(\lamb{x^u}{exp} app\ (H\ x^1)\ (H'\ x^u)),\\
& & lam(\lamb{x^u}{exp} app\ (H\ x^u)\ (app\ (H'\ x^u) \ (H'' x^u)), \\
& &lam(\lamb{x^u}{exp} app\ (H\ x^u)\ ( lam(\lamb{y^u}{exp} H'\ x^u\ y^u)),\\
& & lam(\lamb{x^u}{exp} lam(\lamb{y^u}{exp} H\ x^u\ y^u) ),\\
& & lam(\lamb{x^u}{exp}x),\\
& & app\ H\ H'\}


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

% \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\hastype A$ then $\GG \prv M\in \| N \| :A$ or $ \GG \prv M\in 
\| \mmnot(N)\| \hastype A$.

\enit\mends

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

\item What about its negation? We can compute $\|Z_{exp}\| -\|app\ (lam\ (\lamb{x^u}{exp} E\ x^u))\ 
F,lam(\lamb{x^u}{exp} app\ (M\ x^0) \ x\|$ by intersecting $\mmnot(app\ (lam\ (\lamb{x^u}{exp} E\ x^u))\ 
F)$ and $ \mmnot(lam(\lamb{x^u}{exp} app\ (M\ x^0)\ x))$
 
 \item We can implement intersection as \emph{unification} of simple 
 terms (not detailed here)
\enit
\mends
\begin{slide}{}
\slidetitle{Elimination of negation in a logical framework, $II$}
\[
\begin{array}{lll}
nb1 & : & non\_isredx(lam(\lamb{x^u}{exp} app\ (H\ x^1)\ H'\ x^{u}))\\
nb2 & : & non\_isredx( lam(\lamb{x^u}{exp} app\ (H\ x^u)\
 (app\ H_4\ x^{u} H_5\ x^{u})))\\
nb3 & : & non\_isredx(lam(\lamb{x^u}{exp} app\ (H\ x^u)\ ( lam(\lamb{y^u}{exp} H'\ x^u\ y^u))))\\
nb4 & : & non\_isredx(lam(\lamb{x^u}{exp} lam(\lamb{y^u}{exp} H\ x^u\ 
y^u) ))\\
nbr & : & non\_isredx(lam(\lamb{x^u}{exp}x))\\ 
nb6 & : & non\_isredx( app\ (app\ H_{1}\ H_{2})\ H_{3}\ )
\end{array}\]
\mends
\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

%  \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
 It is possible to perform any boolean operation on sets of simple 
 terms
\item Future work: complement and intersection on \emph{any} strict term
\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}


