\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}
Overview:
  \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$, say $\mnot(t)$,  is the set of 
all ground terms which are not instances of $t$ \ie are not in $\| t 
\|$. 
 \item
 Example: take the  signature of numerals:
\[
\begin{array}{l}
\mnot (s(0))    =    \{0, s(s(Y))\}
\\
\|z_{nat}\| -  \|s(0)\|  = \|0,s(s(Y))\|=\{0, s(s(0)),s(s(s(0)))\dots\}
\end{array}\]
\item 'Multiple Complement': 
\beq
 \|z_{nat}\| - \|0,s(s(Y))\|& =&\mnot(0)\cap\mnot(s(s(Y))=\\
 && \|s(X)\|\cap \|0,s(0)\| =\{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
Example: integer addition modulo $2$.
\beq
% \label{ex:mod2}
s(s(0))&  \Lmap & 0\\
y+0&  \Lmap & y\\
0+y&  \Lmap & y\\
y+y&  \Lmap &
 0
\eneq
\item A relative complement problem (sufficient completeness):
\[
\| x_1 + x_2\| - \|s(s(0)),0+y,y+0,y+y \| = \eset
\]

% \[
% \exists x_1x_2\forall y : (z= x_1 + x_2) \And (z \nq s(s(0)))\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 disjointness 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
% s(s(0))& \Lmap &0\\
% 0+y&  \Lmap & y\\
% y+y&  \Lmap & 0
% \eneq

% We can recover the missing LHS:

% \[
% \| x_1 + x_2\| - \|s(s(0)),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 Answers to negative goals as complement of answers to positive
  ones [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_{ListN}(0)$ in the signature of 
lists of numerals contains not only $s(X)$  but also $nil$ 
and $(cons\ X\ Xs) $.
\item
Complementation must be typed.
\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 a free variable [Lassez \& Marriot 1987]. 

\item
Left-linearization [Plaisted, Stickel].
\item
{\em Constrained terms},  \ie $ 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
 disunification on \ho patterns is decidable [Lugiez $1995$].

\item
Patterns [Miller 1991]: terms where  every free variable is applied to distinct
bound variables. 

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
Complementation  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 Example:
$\l x\l y\l z\,.\, c(E(y,x,z))$
\item Non-Example:
$\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}}, app \hastype exp \Imp exp\Imp exp,  lam\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}{}
\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} {}
\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} {}
\end{array}
\]
% \end{small}

  $(Z\ \GG)$'s denotes the application of a fresh 
variable of correct typing to a  context $\GG$.  
\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$ {\bf does not} depend on $x$ and the term is \emph{not} fully applied. Its 
complement should contain those applications where $E$ {\bf does } 
depend on $x$.

\item

The simply typed 
$\l$-calculus 
 is not strong enough to directly represent the complement of non-fully 
applied patterns  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  (awkward).
\item
We \emph{internalize} strictness in the type-system.

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

%\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} \]
\bit
\item Three form of abstractions, given the label on bound variable.
\item Three form of applications, as a postfix operation.
 \item The calculus is well-behaved (unique canonical forms exist).
\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 allow 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{Embedding the simply-typed $\l$-Calculus}
\bit\item
Example:
\[
\begin{array}{rcl}
\rep{\lambda x.\, \lambda y.\, x} = lam\ (\lamb{x}{exp} lam\ (\lamb{y}{exp} x))
\end{array}
\]
\item
  Argument to the first occurrence of\ `$lam$' is  strict,
 argument to the second is  invariant. Type can only be
$(exp \GImp{u} exp) \GImp{1} exp$.

\item Constants (and bound variables) are strict functions.
\item Second order functions must be undetermined.
\[
\begin{array}{rcl}
 lam\ (\lamb{x}{exp} lam\ (\lamb{y}{exp} x))\Rightarrow
 lam\ (\lamb{x^u}{exp} lam\ (\lamb{y^u}{exp} x)^1)^1
\end{array}
\]
\enit\mends

\begin{slide}{}
\slidetitle{Simple Terms}
\bit
\item
In general:
\ben
\item positive occurrence of function
types are translated to strict functions.
\item  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\ \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\}} {\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 $II$}
\[
\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) = 
(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}



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

\mends

 \begin{slide}{}
\slidetitle{Examples of Complementation}


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^{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^u ))=}\\
& & \{ 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'\}
\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}\}
% \]
\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}{l}
 isredx(app\ (lam\ (\lamb{x^u}{exp} E\ x^u))\ F )\\
 isredx(lam(\lamb{x^u}{exp} app\ (E\ x^0) \ x^u)
\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 \emph{intersecting} $\mmnot(app\ (lam\ (\lamb{x^u}{exp} E\ x^u))\ 
F)$ and $ \mmnot(lam(\lamb{x^u}{exp} app\ (M\ x^0)\ x^u))$
 
 \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}
 non\_isredx(lam(\lamb{x^u}{exp} app\ (H\ x^1)\ H'\ x^{u}))\\
 non\_isredx( lam(\lamb{x^u}{exp} app\ (H\ x^u)\
 (app\ H'\ x^{u} H''\ x^{u})))\\
 non\_isredx(lam(\lamb{x^u}{exp} app\ (H\ x^u)\ ( lam(\lamb{y^u}{exp} H'\ x^u\ y^u))))\\
 non\_isredx(lam(\lamb{x^u}{exp} lam(\lamb{y^u}{exp} H\ x^u\ 
y^u) ))\\
 non\_isredx(lam(\lamb{x^u}{exp}x))\\ 
 non\_isredx( app\ (app\ H_{1}\ H_{2})\ H_{3}\ )
\end{array}\]
\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.

\enit\mends

  \begin{slide}{}
  \slidetitle{Future work}
  \bit
\item
Combine term complementation with clause complementation in \ho hereditary formulae.  
 \item Address the  issue of complement and intersection on \emph{any} strict 
  term.
   \item
Extend to the intuitionistic and linear dependent type case.
 \enit
 \mends
\end{document}


