\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{\myslidetitle}[2]{
 \begin{tabbing} {\large #1} \` #2 \end{tabbing}
 \vspace{.1cm} \par          \hrule
 }
\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{\yield}{\Rightarrow}
\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 \\

ICLP'99, December 1st,  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}
 \begin{itemize} \itemsep 0pt

\item
A term $t$  with free variables as the intensional representation
of its \emph{ground} instances.
%, denoted  $\| t \|$
\item
\emph{Unification} of two terms $t=s$ as \emph{intersection} $t\cap s$ 
of the (ground instances of) $s$ and $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
 Example:  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 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 Notation: a term stands for the set of its instances, ','
  represents union.
\item 'Multiple Complement': by De Morgan rules:
\beq
 \mnot\{0,s(s(Y))\}& =& \mnot(0)\cap\mnot(s(s(Y)))\\
&=&  s(X)\cap \{0,s(0)\}\\
&=&  \{s(0)\}
\eneq
  \item 'Relative Complement':
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:
\beq
s(X) - \{0,s(s(Y)))\}& =& s(X)\cap\mnot\{0,s(s(Y))\} \\
&=& s(X)\cap s(0)= s(0)
\eneq
%  \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}{}\myslidetitle{Applications}{ 1/2}
 \begin{itemize} \itemsep 0pt
  \item

 Functional programming:
\ben
\item
Determination of  exhaustivity and exclusivity 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}{} \myslidetitle{Applications}{2/2}

\bit
\item Logic Programming: 
\ben
\item Answers to negative goal as the complement of answers to its
  positive version [Kunen 1987].
\item Compilation of constructive negation [Chan 1989, Stuckey 1995].
\item The transformational approach to negation [Sato\& Tamaki $1985$,
  Barbuti et al.\ $1990$].  
\enen
\item Our Aim: extend the latter to the \ho case, both for
  higher-order languages ($\l$-Prolog) and Logical Frameworks
  (\emph{Twelf}). 
\enit \vfill
 \end{slide}


\begin{slide}{}

\slidetitle{First-Order Term Complement}
\newcommand{\cL}{{\cal L}}

Consider a finite (untyped) language  $\cL$ and a \emph{linear} term $t$:
\[ \begin{array} {lll}
\mnot_\cL(x  ) & =   \emptyset  \\
\mnot_\cL(f(\tn)  ) & =  \\
 & \{g(\vz)   \mid  \mbox{for all $g \in \cL$ distinct from } 
f\} \cup \mbox{} 
\\
& \{f(z_1 \mdots z_{i-1},s,z_{i+1}, \dots,z_n) \mid \\
&
s\in\mnot_\cL(t_{i}), i \in [1,n] \}
\end{array} \]
\bit
\item
Problem: irrelevant outcomes. Example:
\beq
\mnot(0.nil) & = & \{0,s(X),nil,s(X).L,0.X.L\}
%lists of numerals contains not only $s(z)$  but also $nil$ and $(cons\ z\ zs) $.
\eneq
\item  Solution: typing.
\enit
\vfill
\mends



% Complement operations based on  disunification [Comon, Lugiez].



 \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 (full)
second-order relative complement  problem is not semi-decidable.


\item
Patterns [Miller 1991]: terms where  every logic 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$.
\item  Higher-order disunification (which encompasses complement
  problems) on \ho patterns is decidable [Lugiez $1995$].
\enit
\vfill\end{slide}

%  \begin{slide}{}
% \slidetitle{Fully Applied Pattern}
% \bit
% \item


% \enit\vfill\en% d{slide}

\renewcommand{\lx}{\mbox{\boldmath $\Lambda$} x\,.\,}
 \begin{slide}{}
\myslidetitle{Encoding the (untyped) $\l$-calculus} {1/2}

\beq
e & \bnfas & x \mid  (\lx e) \mid  e_1\  e_{2}\\
\Sigma  & \bnfas & exp\hastype \mbox{\textrm{type}}, lam\hastype (exp\Imp 
exp)\Imp exp, app \hastype exp \Imp exp\Imp exp
\eneq
\bit
\item
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
\item
The encoding a $\beta$-redex  as a pattern using logic variables
 $E_{exp\Imp exp}$ and $F_{exp}$:
\beq
\rep {(\lx e)\ f} & = & app\ (lam\  (\lamb{x}{exp} (E\ x))\ F)
\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
\enit\mends

%\begin{slide}


 \begin{slide}{}
\myslidetitle{Encoding the (untyped) $\l$-calculus }{ 2/2}
\bit
\item
Complement of the $\beta$-redex in the \textbf{empty} context:
 $\lx e, (e_1 \ e_2) \ e_3$, that is
\beq
\lefteqn{\cdot\vd\mmnot(app\ (lam\ (\lamb{x}{exp} (E\ x))\ F)=}\\ 
&& \{ lam\ (\lamb{x}{exp} H\ x), app\ (app\ H_{1}\ H_{2})\ H_3\}
 \eneq

\item
Encoding a $\eta$-redex, where $x\not\in FV(e)$:
\beq
\rep{\lx (e\ x)} & = & lam(\lamb{x}{exp} (\fbox{$app\ E$}) \ x)
\eneq

\item Hence $e$ {\em does \textbf{not}} depend on $x$.  Intuitively
  its complement should contain those application sub-terms where $E$
  {\bf does} depend on $x$:
$$lam(\lamb{x}{exp} (\fbox{$app\ F\# x$}) \ (H\ x))$$



\enit\mends
\begin{slide}
\slidetitle{Fully vs. Non-Fully Applied Patterns}
\bit
\item The crux of the matter is whether a pattern is \emph{fully
    applied}, \ie if  all bound variables appearing in the binder are
  mentioned in the scope of a logic variable. Example: $\l x\l y\l
  z\,.\, (E \ y\ x\ z)$.  Non-example:
 $\l x\l y\l z\,.\, E\ y$.

\item
Complement of fully applied terms is  similar to the  \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 
% variable occurrence constraints.
\item
    The simply typed $\l$-calculus theory is not strong enough to
  directly represent the complement of non-fully applied patterns.



\enit\mends

\begin{slide}
\slidetitle{Strictness}
\bit
\item We need to have a notion of \emph{strictness} in the language to
  express variable occurrence constraints.
 
\item We \emph{internalize} strictness as a type system, rather than
  promote constraints to first-class objects 
  as in [Lugiez 1995] (technically 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}


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

\bit
\item Three labels: 1 'must occur', 0 'must not occur', u 'undetermined'.
\item Three different forms of abstraction and application. 
\item Calculus is well-behaved (unique canonical forms exist).
\enit
\mends




 \begin{slide}{}
\slidetitle{Complementing Patterns in the Strict Calculus}
\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 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 must be $(exp \GImp{u} exp)
  \GImp{1} exp$.

\item Constants (and bound variables) are strict functions, negative
  [positive] occurrences of \ho  functions must be undetermined [strict].
\enit\mends

\begin{slide}{}
\slidetitle{Simple Terms}
\bit
\item Example:
\beq
\lefteqn{lam\ (\lamb{x}{exp} lam\ (\lamb{y}{exp} x))\yield}\\
& &  lam\
(\lamb{x^u}{exp} lam\ (\lamb{y^u}{exp} x)^1)^1
\eneq

\item Bring to full application:
\beq
\lefteqn{lam(\lamb{x^y}{exp} (app\ \fbox{$E$})^1 \ x^1)\yield}\\
& & lam(\lamb{x^u}{exp} (app\ (\fbox{$E\ x^0$})^1 \ x^1))
\eneq
\item The resulting language:
\enit
\[ \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} \]
\mends
\begin{slide}{}

 \myslidetitle{The Complement Algorithm}{}
 \bit
\item  For logic  variables consider each argument in turn:
\ben
\item  If an argument variable is \textbf{undetermined}
it does not contribute to the negation. 
\item If an argument variable is \textbf{strict},
 complement the corresponding label from $1$
to $0$ while all other arguments are undetermined.
\item  For \textbf{vacuous}
argument variables  proceed dually.
\enen
\item Example:
\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}\} 
\eneq
\enit\mends


 \begin{slide}{}
\slidetitle{Complement of $\mmnot(lam(\lamb{x^{u}}{exp} app\ (E\ x^{0})\  x ))$ }

\[
\begin{array}{l}
\mbox{different from first coordinate \fbox{$E\ x^{0}$ }}\\
 \qquad \{ lam(\lamb{x^u}{exp} app\ (\fbox{$H\ x^1$})\ (H'\ x^u)),\vsk
\mbox{different from second coordinate \fbox{$x$}}\\
\qquad lam(\lamb{x^u}{exp} app\ (H\ x^u)\ \fbox{$(app\ (H'\ x^u) \ (H'' x^u))$}) \\
\qquad lam(\lamb{x^u}{exp} app\ (H\ x^u)\  \fbox{$lam(\lamb{y^u}{exp} H'\ x^u\
y^u)$}),
\vsk
\mbox{different from \fbox{$(app\ (E\ x^{0})\  x )$}}\\
\qquad  lam(\lamb{x^u}{exp} \fbox{$lam(\lamb{y^u}{exp} H\ x^u\ y^u)$} ),\\
\qquad  lam(\lamb{x^u}{exp} \fbox{$x$}),\vsk
\mbox{different from top \fbox{$lam(\dots)$} functor}\\
\qquad  \fbox{$app\ H\ H'$}\}
\end{array}
\]

\mends

\begin{slide}
\slidetitle{Unification of Simple Terms}
\bit
\item Unification as \emph{intersection} of labels, (analogous to conjunction 
in  three-valued logic).
\item  \emph{Finite} sets of most general unifiers exist.
\item Example: since $x$ is strict in 
the LHS, it can be strict either in the first or second subterm of $c$:
\begin{eqnarray*}
%\label{eq:int}
\lefteqn{x\oftp A\prv E\ x^{1}\cap\  c\ (F\  x^{u})^{1} \ (G\  
x^{u})^{1} = }\\
& &  \{c\ (G\  x^{1})^{1} \ (H\  x^{u})^1, c\ (G\  x^{u})^1 \ (H\  
x^{1})^1\}
\end{eqnarray*}
\enit
\mends

 \begin{slide}{}
\slidetitle{Results}
\bit
\item
{\bf Theorem }
If $M$ is a simple term, so is $\mnot(M)$.

\item

{\bf Theorem }
$M$ is a ground instance of $\mnot(N)$ if and only if $M$ is
\textbf{not} a ground instance of $N$.


\item

{\bf Theorem }
$M$ is a ground instance of $N_1$ and $N_2$ if and only if $M$ is a ground
instance of $N_1\cap N_2$.

\item \textbf{Corollary }  \emph{Finite} sets of simple terms form a boolean algebra.

\enit
\mends

\begin{slide}{}
\myslidetitle{Towards Intensional Negation}{ }

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

Infer its negation by computing: 
$$\mnot(app\ (lam\ (\lamb{x^u}{exp} E\ x^u))\ F)
\cap\mnot(lam(\lamb{x^u}{exp} app\ (M\ x^0) \ x))$$

\[
\begin{array}{ll}
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'\ x^{u} H''\ 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) ))\\
nb5  : & non\_isredx(lam(\lamb{x^u}{exp}x))\\ 
nb6  : & 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, the \fo algorithm 
 does not generalize immediately to 
 the \ho case: we need to have an intrinsic notion of strictness.
 \item
 We have formulated a strict $\l$-calculus, which  we think gives an 
independent  
 contribution to the understanding of sub-structural calculi.
 \item
 We have shown how to perform \emph{any} boolean operation on \emph{finite}
sets of simple  terms.
\enit\mends

  \begin{slide}{}
  \slidetitle{Future work}
  \bit
\item Combine term complement with clause complement to obtain intensional
negation in \ho\lp  [Done].
  \item Address the  issue of unrestricted complement and intersection on \emph{any} strict
  term.
   \item Extend to the intuitionistic and linear dependently-typed case.
 \enit
 \mends
\end{document}


