\documentclass{cameraagp99}
\usepackage{amsfonts}
\usepackage{cdsty}
\usepackage{mit-com}

\def\zzctdrawdotedge{\drawdotedge{4pt}0}
\def\ctabutborderlr{1em}
\def\ctabutbordertb{1ex}
\pagestyle{headings} %change to empty
\bibliographystyle{plain}

\newcommand{\eqdef}{\stackrel{\mbox{\tiny  def}}{=}}
\newcommand{\mmnot}{\neg}
\newcommand{\rep}[1]{\ulcorner #1\urcorner}  % amsfonts.sty
\newcommand{\arv}[2]{\begin{array}{c} #1\\#2\end{array}}
\newcommand{\UImp}{\GImp{u}}
\newcommand{\god}{\Gamma; \Omega;\Delta}
\newcommand{\godemp}{(\GG,\O,D)\emp}
\newcommand{\betared}{\stackrel{\beta}{\longrightarrow}}
\newcommand{\etaexp}{\stackrel{\bar\eta}{\longrightarrow}}
\newcommand{\lxua}{\lambda x^{u}\!:\!  A.\, }
\newcommand{\D}{\Delta}
\renewcommand{\O}{\Omega}
\newcommand{\dmn}{(\D_{M},\D_{N})}
\newcommand{\Mns}{\overline{M_n^1}}
\newcommand{\Nns}{\overline{N_n^1}}
\newcommand{\emp}{;\cdot;\cdot}
\newcommand{\itc}{\item[\textbf{case}]}
\newcommand{\btab}{\begin{tabbing}}
\newcommand{\etab}{\end{tabbing}}
\newcommand{\cF}{{\cal F}}
\newcommand{\xnl}{\overline{x_{n}^{k}}}
\newcommand{\cM}{{\cal M}}
\newcommand{\mbc}{\sqcap}
\newcommand{\mna}{\mmnot} %overloaded notation: may be changed
\newcommand{\mcap}{\cap}
\newcommand{\mbigcap}{\hat\cap}
\newcommand{\da}{\downarrow}
\newcommand{\bua}{\Uparrow}
\newcommand{\buda}{\Uparrow\!\downarrow}

\newtheorem{Theorem}{Theorem}
\newtheorem{Example}[Theorem]{Example}
\newtheorem{Lemma}[Theorem]{Lemma}
\newtheorem{Corollary}[Theorem]{Corollary}
\newtheorem{Definition}[Theorem]{Definition}


\title{The Relative Complement Problem for Higher-Order Patterns
\thanks{A version of this paper will appear in ICLP99}}

\author{ Alberto Momigliano\\
Department of Philosophy\\
           Carnegie Mellon University\\
           Pittsburgh, PA 15213, U.S.A.\\
 \texttt{mobile@cs.cmu.edu}
\and
  Frank Pfenning\\
 Department of Computer Science \\
           Carnegie Mellon University\\
           Pittsburgh, PA 15213, U.S.A.\\
 \texttt{fp@cs.cmu.edu}}

\begin{document}
\maketitle
\runningtitle{The Relative Complement Problem for Higher-Order Patterns}
\begin{abstract}
We address the problem of complementing \ho patterns without repetitions of
free variables.  Differently from the \fo case, the complement of a pattern
cannot, in general, be described by a pattern, or even by a finite set of
patterns.  We therefore generalize the simply-typed $\lambda$-calculus to
include an internal notion of \emph{strict function} so that we can directly
express that a term must depend on a given variable.  We show that, in this
more expressive calculus, finite sets of patterns without repeated variables
are closed under complement and unification.  Our principal application is
the transformational approach to negation in higher-order logic programs.
\end{abstract}

\begin{keywords}
Relative complement, strict $\l$-calculus, \ho logics, intensional negation.
\end{keywords}

\section{Introduction}
\label{sec:intro}

In most functional and logic programming languages the notion of a pattern,
together with the requisite algorithms for matching or unification, play an
important role in the operational semantics.  Besides unification other
problems such as generalization or complement also arise frequently.  In
this paper we are concerned with the problem of pattern complement in a
setting where patterns may contain binding operators, so-called
\emph{higher-order patterns}~\cite{Miller91jlc}.  Higher-order
patterns have found applications in logic
programming~\cite{Miller91jlc}, logical
frameworks~\cite{Pfenning91lf}, term rewriting~\cite{Nipkow93tlca}, and
functional logic programming~\cite{Hanus96RTA}.  Higher-order patterns
inherit many pleasant properties from the first-order case.  In particular,
most general unifiers~\cite{Miller91jlc} and least general
generalizations~\cite{Pfenning91lics} exist, even for complex type theories.

Unfortunately, the complement operation does not generalize as
smoothly.  Lugiez \cite{Lug95} has studied the more general problem of
higher-order disunification and had to go outside the language of
patterns and terms to describe complex constraints on sets of
solutions.  We can isolate one basic difficulty: a pattern such as
$\lambda x\ldot E\ x$ for an existential variable $E$ matches any term
of appropriate type, while $\lambda x\ldot E$ matches precisely those
terms $\lambda x\ldot M$ where $M$ does not depend on $x$.  The
complement then consists of all terms $\lambda x\ldot M$ such that $M$
\emph{does} depend on $x$.  However, this set cannot be described by a
pattern, or even a finite set of patterns.

This formulation of the problem suggests that we should consider a
$\lambda$-calculus with an internal notion of \emph{strictness} so that we
can directly express that a term must depend on a given variable.  For
reasons of symmetry and elegance we also add the dual concept of
\emph{invariance} expressing that a given term does not depend on a given
variable.  As in the first-order case, it is useful to single out the case
of \emph{linear patterns}, namely those where no existential variable
occurs more than once.\footnote{This notion of linearity should not
be confused with the eponymous concept in linear logic and $\lambda$-calculus.}
We show that patterns in our calculus have the
following properties: 
\begin{enumerate}
 \item The complement of a linear pattern is a finite set of linear
patterns.
 \item Unification of two patterns is decidable and leads to a finite set of
most general unifiers.
\end{enumerate}
 Consequently, finite sets of linear patterns in the strict
$\lambda$-calculus are closed under complement and unification.  If we think
of finite sets of linear patterns as representing the set of all their
ground instances, then they form a boolean algebra under simple union,
intersection (implemented via unification) and the complement operation.

The paper is organized as follows: Section \ref{sec:related} briefly reviews
related work, while Section \ref{sec:facomp} introduces some preliminary
definitions.  In Section \ref{sec:strict} we introduce a strict
$\l$-calculus and note some basic properties such as the existence of
canonical forms.  Section \ref{sec:strictcomp} introduces a restriction of
the language for which complementation is possible.  The algorithm for
negation is presented in Section \ref{sec:compl}.  In Section
\ref{sec:sunif} we give a unification algorithm for our fragment.  We
conclude in Section \ref{sec:concl} with some applications and speculation
on future research.  For reasons of space, a number of lemmas and proofs are
omitted here and can be found in \cite{Momigliano99phd}.


\section{Related Work}
\label{sec:related}

Complement problems have a number of applications in theoretical computer
science (see \cite{Comon91} for a list of references).  For example, they
are used in functional programming to produce non-ambiguous function
definitions by patterns and to improve their compilation and in rewriting
systems to check whether an algebraic specification is sufficiently
complete.  They can also be employed to analyze communicating processes
expressed by infinite transition systems.  Other applications lie in the
areas of machine learning and inductive theorem proving.  In \lp Kunen
\cite{Kunen87} used term complement to represent infinite sets of answers to
negative queries.  Our main motivation has been the explicit synthesis of
the negation of higher-order logic programs, as discussed in Section
\ref{sec:concl}.

Lassez and Marriot \cite{Lassez87} proposed the seminal {\em uncover}
algorithm for computing relative complements and introduced the now
familiar restriction to linear terms.  We quote the
definition of the ``$\mmnot$'' algorithm for the (singleton) complement
problem given in \cite{Bar90} which we generalize in
Definition \ref{def:compl}.  Given a finite signature $\Sigma$ and a
linear term $t$ we define:
\[ \begin{array} {lll}
\mmnot_\Sigma(x ) & = \emptyset \\ \mmnot_\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\mmnot_\Sigma(t_{i}), i \in [1,n] \}
\end{array} \]

An alternative solution to the relative complement problem is
\emph{disunification} (see \cite{Comon91} for a survey and \cite{Lug95} for
an extension to the simply-typed $\l$-calculus): here operations on sets of
terms are translated into conjunctions or disjunctions of equations and
disequation under explicit quantifiers.  Non-deterministic application of a
few dozen rules eventually turns a given problem into a solved form.
Though a reduction to a significant subset of the disunification rules is
likely to be attainable for complement problems, control is a major problem.
We argue that using disunification for this purpose is unnecessarily
general.  Moreover the \ho case results in additional complications, such as
restrictions on the occurrences of bound variables, which fall outside an
otherwise clean framework.  As we show in this paper, this must not
necessarily be the case.  We believe that our techniques can also be applied
to analyze disunification, although we have not investigated this
possibility at present.


\section{Preliminaries}
\label{sec:facomp}

In this section we introduce some preliminary definitions and examples which
guide our development.  We write $P$ for atomic types, $c$ for term-level
constants, and $x$ for term-level variables.

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

We require that signatures and contexts declare each constant or variable at
most once.  Furthermore, we identify contexts which differ only in their
order and promote ``,'' to denote disjoint set union.  As usual we identify
terms which differ only in the names of their bound variables.  We restrict
attention to well-typed terms, omitting the standard typing rules.

In applications such as logic programming or logical frameworks,
$\lambda$-abstraction is used to represent binding operators in some
object language.  In such a situation the most useful notion of normal
form are long $\beta\eta$-normal forms (which we call \emph{canonical
forms}), since the canonical forms are almost always the terms in
bijective correspondence with the objects we are trying to represent.
Every well-typed term in the simply-typed $\lambda$-calculus has a
unique canonical form---a property which persists in the strict
$\lambda$-calculus introduced in Section~\ref{sec:strict}.

We denote existential variables of type $A$ (also called logical
variables, meta-variables, or pattern variables) by $E_A$, although we
mostly omit the type $A$ when it is clear from the context.  We think of
existential variables as syntactically distinct from bound variables or
free variables declared in a context.  A term possibly containing some
existential variables is called a \emph{pattern} if each occurrence of
an existential variable  appears in a subterm of the form $E\ x_1\ldots x_n$, where the
arguments $x_i$ are distinct occurrences of free or bound variables (but
not existential variables).

Semantically, an existential variable $E_A$ stands for all canonical terms
$M$ of type $A$ in the empty context with respect to a given signature.  We
extend this to arbitrary well-typed terms in the usual way, and write $\GG
\prv M\in\| N\| : A$ when a term $M$ is a ground instance of a pattern $N$
at type $A$.  In this setting, unification of two patterns without shared
existential variables corresponds to an intersection of the set of terms
they denote~\cite{Miller91jlc,Pfenning91lics}.  This set is always either
empty, or can be expressed again as the set of instances of a single
pattern.  That is, patterns admit most general unifiers.

The class of higher-order patterns inherits many properties from
first-order terms.  However, as we will see, it is \emph{not} closed
under complement, but a special subclass is.  We call a canonical
pattern $\Gamma \vd M \hastype A$ \emph{fully applied} if each
occurrence of an existential variable $E$ under binders $y_1,\ldots,y_m$
is applied to some permutation of the variables in $\Gamma$ and
$y_1,\ldots,y_m$.  Fully applied patterns play an important role in
functional logic programming and rewriting~\cite{Hanus96RTA} because any
fully applied existential variable $\Gamma \vd E\ x_1\ldots x_n$
denotes all canonical terms with free variables from $\Gamma$.
It is this property which makes complementation particularly simple.

\begin{Example}
\label{ex:lam}
Consider the untyped $\l$-calculus.
\beq
e & \bnfas & x \mid \lx e \mid e_1\, e_2
\eneq
We encode these expressions using the usual techniques of higher-order abstract
syntax (see, for example, \cite{Michaylov91}) as canonical forms
over the following signature.
\beq
\Sigma  & = & exp\hastype \mbox{\textrm{type}}, lam\hastype (exp\Imp 
exp)\Imp exp, app \hastype exp \Imp exp\Imp exp
\eneq
The representation function is given by.
\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
The representation of an object-language $\beta$-redex then has
the form
\beq
\rep{ (\lx e)\ f} & = & app\ (lam\  (\lamb{x}{exp} \rep{e}))\ \rep{f}
\eneq
 where $\rep{e}$ my have free occurrences of $x$.  When written as a pattern
with variables $E_{exp \arrow exp}$ and $F_{exp}$ ranging over \emph{closed}
terms, this is expressed as $app\ (lam\ (\lamb{x}{exp} (E\ x))\ F)$.  The
complement of the right-hand side considered as a pattern with respect to
the empty context contains every top-level $\lambda$-abstraction plus every
application where the first argument is not an abstraction:
\[
\mmnot(app\ (lam\ (\lamb{x}{exp} (E\ x))\ F)= 
\{ lam\ (\lamb{x}{exp} H\ x), app\ (app\ H_{1}\ H_{2})\ H_{3}\}
 \]
\end{Example}

For patterns which are not fully applied, the complement cannot
be expressed as a finite set of patterns, as the following example
illustrates.

\begin{Example}
\label{ex:etardx}
The encoding of an $\eta$-redex takes the form
\beq
\rep{\lx e\ x} & = & lam(\lamb{x}{exp} app\ \rep{e}\ x)
\eneq
 where $\rep{e}$ may contain no free occurrence of $x$.  The side condition
is expressed in a pattern by introducing an existential variable $E_{exp}$
which {\em does not} depend on $x$.  Hence, its complement with respect to
the empty context should contain, among others, also all terms
 \[ lam\ (\lamb{x}{exp} app\ (E x)\ x) \]
where $E$ {\em does}
depend on $x$.
\end{Example}

Note that there is no finite set of patterns which has as its ground
instances exactly those terms $M$ which depend on a given variable $x$.
Following standard terminology, we call such terms \emph{strict in $x$} and
the corresponding function $\lamb{x}{A} M$ a \emph{strict function}.  As the
example above shows, the complement of patterns which are not fully applied
can therefore not be represented as a finite set of patterns.  This failure
of closure under complementation cannot be avoided similarly to the way in
which left-linearization bypasses the limitation to linear patterns and it
needs to be addressed directly.

One approach is taken by Lugiez \cite{Lug95}: he modifies the language of
terms to permit occurrence constraints.  For example $\l xyz.\ M\{1,3\}$
would denote a function which depends on its first and third argument.  The
technical handling of those objects then becomes awkward as they require
specialized rules which are foreign to the issues of complementation.

Since our underlying $\lambda$-calculus is typed, we use typing to express
that a function \emph{must} or \emph{must not} depend on its argument.  In
the next section we develop such a $\lambda$-calculus and generalize the
complement algorithm to work on such terms.

\section{A Strict $\lambda$-Calculus}
\label{sec:strict}

As we have seen in the preceding section, the complement of some patterns in
the simply-typed $\lambda$-calculus cannot be expressed in a finitary manner
within the same calculus.  We thus generalize our language to include
\emph{strict functions} of type $A \RImp B$ (which are guaranteed to depend
on their argument) and \emph{invariant functions} of type $A \ZImp B$ (which
are guaranteed \textbf{not} to depend on their argument).  Of course, 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.  Therefore our calculus also contains the full function
space $A \UImp B$.  

\[ \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_1 \ M_2}^k \\
 \mbox{\textit{Contexts}} & \Gamma & \bnfas & \cdot \bnfalt \Gamma, x\oftp A
 \end{array} \]

Note that there are three different forms of abstractions and applications,
where the latter are distinguished by different labels on the argument.  It
is not really necessary to distinguish three forms of application
syntactically, since the type of function determines the status of the
application, but it is convenient for our purposes.  A label $u$ it is
called \emph{undetermined}; other labels are \emph{determined} and denoted
by $d$.

We use a formulation of the typing judgment with three zones, 
containing the undetermined, irrelevant and strict hypotheses, denoted 
by $\Gamma$, $\Omega$, and $\Delta$, respectively.
  \[ \Gamma; \Omega; \Delta \vd M \hastype A \]
 We implicitly assume a fixed signature $\Sigma$ which would otherwise
clutter the presentation.

\begin{figure}[th]
% \begin{small}
\[ \begin{array}{c}
 \ianc{c\oftp A \in \Sigma}{\Gamma; \Omega; \cdot \vd c \hastype A}{Con} \\[1em]

 \ianc{}{(\Gamma, x\oftp A); \Omega; \cdot \vd x \hastype A}{Id^u}
 \hspace{2em}
 \mbox{\textit{no $Id^0$ rule}}
 \hspace{2em}
 \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]

 \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} \]
% \end{small}
\caption{Typing rules for $\lc$}
\end{figure}


Our system is biased towards a bottom-up reading of the rules in that 
variables never disappear, i.e., they are always propagated from the 
conclusion to the premises, although their status might be changed.

Let us go through the typing rules in detail.  The requirement for the
strict context $\Delta$ to be empty in the $Id^u$ and $Id^1$ rules expresses
that strict variables must be used, while undetermined variables in $\Gamma$
or irrelevant variables in $\Omega$ can be ignored.  Note that there is no
rule for irrelevant variables, which expresses that they cannot be used.

The introduction rules for undetermined, invariant, and strict functions
simply add a variable to the appropriate context and check the body
of the function.

The difficult rules are the three elimination rules.  First, the
undetermined context $\Gamma$ is always propagated to both premises.
This reflects that we place no restriction on the use of these variables.

Next we consider the strict context $\Delta$.  Recall that this contains
the variables which should occur strictly in a term.  An
undetermined function $M\hastype A \GImp{u} B$ may or may not use
its argument.  An occurrence of a variable in the argument to such
a function can therefore not be guaranteed to be used.  Hence we
must require in the rule $\GImp{u}E$ for an application
$M\ N^u$ that all variables in $\Delta$ occur strictly in $M$.  This
ensures at least one strict occurrence in $M$ and no further
restrictions on occurrences of strict variables in the argument
are necessary.  This is reflected in the rule by adding $\Delta$ to
the undetermined context while checking the argument $N$.  The
treatment of the strict variables in the vacuous application $M\ N^0$
is similar.

In the case of a strict application $M\ N^1$ each strict variable should
occur strictly in either $M$ or $N$.  We therefore split the context into
$\Delta_M$ and $\Delta_N$ guaranteeing that each variable has at least one
strict occurrence in $M$ or $N$, respectively.  However, strict variables
can occur more than once, so variables from $\Delta_N$ can be used freely
in $M$, and variables from $\Delta_M$ can occur freely in $N$.  As before,
we reflect this by adding these variables to the undetermined context.

Finally we consider the irrelevant context $\Omega$.  Variables
declared in $\Omega$ cannot be used \emph{except} in the argument
to an irrelevant function (which is guaranteed to ignore its argument).
We therefore add the irrelevant context $\Omega$ to the undetermined
context when checking the argument of a vacuous application $M\ N^0$.

Our strict $\lambda$-calculus satisfies the expected properties, culminating
in the existence of canonical forms which is critical for the intended
applications.  A full account can be found in
\cite{Momigliano99phd}.

Let us examine the structural properties of contexts.  Exchange is directly
built into the formulation.  Weakening is allowed in the undetermined and in
the irrelevant contexts.  Contraction holds anywhere.  We also have the
possibility to lose track of occurrences, if we are so
inclined.  This follows by structural inductions on the typing
judgment.
\newpage
\begin{Theorem}[Loosening]
\label{thm:Oloose}
\mbox{}
\ben
\item
If $\Gamma; (\Omega, x\oftp C); \Delta \vd M \hastype A$
then $(\Gamma, x\oftp C); \Omega; \Delta \vd M \hastype A$.
\item
If $\Gamma; \Omega; (\Delta, x\oftp C) \vd M \hastype A$
then $(\Gamma, x\oftp C); \Omega; \Delta \vd M \hastype A$.
\enen
\end{Theorem}

%\begin{Theorem}[Substitution Properties] \mbox{}
%\label{thm:substitution}
%\begin{enumerate}
%\item (Substitution$^u$) If $(\Gamma, x\oftp A);\Omega;\Delta\vd M 
%\hastype C$ and $(\Gamma,\D); \Omega;\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, \Delta,\Omega) ;\cdot;\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}
%\end{Theorem}

The notions of 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} \]
 
The subject reduction and expansion theorems are an immediate consequence of
the structural and substitution properties generalized to this three-zoned
calculus.  The substitution properties again follow by straightforward
structural inductions.

\begin{Theorem}
[Subject Reduction and Expansion]
 \mbox{}
\label{thm:subred}
\ben
 \item If $\Gamma;\Omega; \Delta \vd M \hastype A$ and $M \betared M'$ then 
$\Gamma;\Omega; \Delta \vd M' \hastype A$.
 \item If $\Gamma;\Omega; \Delta \vd M \hastype A$ and $ M \hastype A
\etaexp M'$ then $\Gamma;\Omega; \Delta \vd M' \hastype A$.
\enen
\end{Theorem}

The above results culminate in the canonical form theorem: for every term
$M$ such that $\god\vd M\hastype A$, there exists a unique $N$ in canonical
(= $\beta$-normal $\eta$-long) form, denoted $\god\vd N\bua A$, such that
$M$ is convertible to $N$.  The proof employs the standard method of logical
relations, adapted to the specific $\lambda$-calculus we consider.

The following lemma establishes a consistency property of the type system
relevant to complementation.

\begin{Lemma}[Exclusivity]
\label{le:disj}
It is not the case that both $\GG;\O;(\D,x\oftp A)\vd M\hastype 
C$ and $\GG;(\O,x\oftp A);\D\vd M\hastype C$.
\end{Lemma}

\newcommand{\er}[1]{\mid #1\mid_{\mbox{\tiny \textrm{er}}}}


\section{Embedding the Simply-Typed $\lambda$-Calculus}
\label{sec:strictcomp}

Now that we have developed a calculus which is potentially strong
enough to represent the negation of linear patterns, we need to
answer two questions: how do we embed the original $\lambda$-calculus,
and is the calculus now closed under complement?

In this paper, we do not answer the second question
conclusively.  However, our algorithm is sound and
complete for the fragment which results from the natural embedding of the
original simply-typed $\lambda$-calculus which is sufficient for all
applications we have presently considered (see Section
\ref{sec:concl}).

Recall that we introduced strictness to capture occurrence conditions on
variables in canonical forms.  This means that constants (and by extension
bound variables) should be considered \emph{strict} functions of their
argument, since these arguments will indeed occur in the canonical form.  On
the other hand, if we have a second order constant, we cannot restrict the
argument function to be either strict or vacuous, since this would render
our representations inadequate.

\begin{Example}
 Continuing Example \ref{ex:lam}, we see
\[
\begin{array}{rcl}
\rep{\lambda x.\, \lambda y.\, x} = lam\ (\lamb{x}{exp} lam\ (\lamb{y}{exp} x))
\end{array}
\]
 so the argument to the first occurrence of\ `$lam$' is a strict function,
while the argument to the second occurrence is an invariant function.
If we can give only one type to `$lam$' it must therefore be
$(exp \GImp{u} exp) \GImp{1} exp$.
\end{Example}

Generalizing this observation means that positive occurrence of function
types are translated to strict functions, while negative occurrences to
undetermined functions.  We can formalize this as an embedding of the
simply-typed $\l$-terms into a fragment of strict terms via two mutually
recursive functions $()^{-}$ and $()^{+}$.  First, the definition on
types.
\beq
(A\Imp B)^{-} & = & A^{+} \TImp B^{-}\\
(A\Imp B)^{+} & = & A^{-} \RImp B^{+}\\
P^{-} = P^{+} & = & P
\eneq
We extend it to canonical terms (including existential variables), signatures,
and contexts as follows:
\beq
(\lxa M)^{-} & = & \lamb{x^{u}}{A^{+}} M^{-}\\
M^{-} & = & M^{+} \qquad \mbox{for $M$ of base type}\\
x^{+} & = & x\\
c^{+} & = & c\\
(E_A\ x_1\dots x_n)^{+} &=& F_{A^{-}} \ x_1^u\dots x^u_n \\
(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

The image of the embedding of the canonical forms of the simply-typed 
$\lambda$-calculus gives rise to the following fragment, which we 
call \emph{simple terms}.

\[ \begin{array}{rrcl}
\mbox{\textit{Simple Terms}} & M & \bnfas &  \lam x^{u}\oftp
A^{+}\ldot M \bnfalt h\ {M_1}^{1} \dots {M_n}^{1} \bnfalt E_{A^{-}}\
x^{u}_{1}\dots{x^u_{n}} \end{array} \] We sometimes abbreviate $h\ {M_1}^{1}
\dots {M_n}^{1}$ as $h\ \Mns$.  Note that by the restriction to long normal
forms such terms and applications of pattern variables must be of base type.
For every judgment $\cal J$ on simple terms,
 we will shorten  $\GG\emp\vd \cal J$ into $\GG\vd \cal J$.

\newcommand{\ctx}{\GG^{+}}

The correctness of the embedding is easily established by
induction over the structure of canonical forms.

\begin{Theorem}
\label{thm:embed}
If $\GG\vd M\bua A$ then $\ctx\vd M^{-}\bua A^{-}$. 
\end{Theorem}

From now on we drop the $\pm$ embedding annotations from terms, 
types and contexts.  We may also hide the $()^1$ decoration
from strict application of constants in examples.
\smallskip

Simple terms enjoy the tightening property which is related to loosening
(Theorem \ref{thm:Oloose}) and exclusivity (Theorem \ref{le:disj}) and is
crucial for the correctness proof of our complement algorithm.  It expresses
that every closed \emph{simple} term is either strict or vacuous in a given
undetermined variable.  After appropriate generalization, the result follows by induction
on the given derivation.

\newcommand{\cu}{(\GG, x\oftp C);\Omega;\Delta}
\newcommand{\cxtr}{\GG;\O; (\D, x\oftp C)}
\newcommand{\cxto}{\GG; (\O,x\oftp C);\D}

\begin{Theorem}[Tightening]
\label{le:exh} 
Let $M$ be a simple term  without existential variables 
such that $\cu\vd M\bua A$. Then 
 $\cxtr\vd M\bua A$ or $\cxto\vd M\bua A$.
\end{Theorem}

\newcommand{\LBimp}{\longleftrightarrow}

It simplifies the presentation of the algorithms for complement and later
unification if we extend every existentially quantified variable
 to be applied to all bound variables in
their declaration order.  This is possible for simple linear patterns
without changing the set of its ground instances.  We just insert vacuous
applications, which guarantees that the extra variables are not used.
We furthermore permute the argument to the standard order, which also
does not affect the set of ground instances of linear patterns.
In slight abuse of notation we call the resulting terms \emph{fully
applied}.

\begin{Example}
The simple term from Example \ref{ex:etardx},
$$lam\ (\lamb{x^u}{exp} app\ E\ x)$$, has fully applied form
$$lam\ (\lamb{x^u}{exp} app\ (Z\ x^0)\ x)$$ for a fresh existential
variable $Z$ of type $exp \GImp{0} exp$.
\end{Example}

The translation to fully applied terms is proven correct by induction
over the structure of the given canonical form, using a few
straightforward lemmas regarding variable occurrences in simple
terms. We use the judgment $\GG\vd M\in\|N\|\hastype A $ to denote
that a term $M$ of type $A$ is a ground instance of $N$ in context
$GG$.

\begin{Theorem}
\label{thm:fat}
Let $N$ be a simple term and $Q$ its fully applied translation.  Then
$\GG\vd M\in\|N\|\hastype A$ iff $\GG\vd M\in \|Q\|\hastype A$.
\end{Theorem}

From now on we tacitly assume that all simple terms are fully applied.
We call a term $E\, x_1^{l_1}\ldots x_n^{l_n}$ (of base type) a
\emph{generalized variable}.

\section{The Complement Algorithm}
\label{sec:compl}

The idea of complementation for applications and abstractions is quite
simple and similar to the first-order case.  For generalized variables
we consider each argument in turn.  If an argument variable is undetermined
it does not contribute to the negation.  If an argument variable is strict
then any term where this variable does not occur contributes to
the negation.  We therefore complement the corresponding label from $0$
to $1$ while all other arguments are undetermined.  For vacuous
argument variables we proceed dually.  In preparation for the rules
we define.
\beq 
\mnot(1)  =  0\quad
\mnot(0)  =  1\quad
\eneq
If $\Gamma = x_1\oftp A_1,\ldots, x_n\oftp A_n$, we write $E\ \Gamma^u$ for
the application of $E\ {x_1}^u\ldots{x_n}^u$.  Such an application represents
the set of all terms without existential variables and free variables
from $\Gamma$.
  
\newcommand{\blip}{\Rightarrow}

\begin{Definition}[Higher-Order Pattern Complement]
\label{def:compl}

Fix a signature $\Sigma$.  For a linear simple term  
$M$ such that $\GG \prv  M \hastype  A$ define $\GG\prv  \mnot(M) \blip N : A$
by the following rules.  Note that a given $M$ may be related to several
terms $N$ all of which belong to the complement of $M$.

\begin{small}
\[
\begin{array}{c}
\ianc{1\leq i\leq n\quad k\in\{1,0\}} {\GG\prv \mnot(E \ x_{1}^{l_{1}}\dots x_{i-1}^{l_{i-1}} \ 
x_{i}^{k}\ x_{i+1}^{l_{i+1}}\dots x_n^{l_{n}}) \blip H\ x_{1}^{u}\dots 
x_{i-1}^{u}\ x_{i}^{\mnot(k)}\ x_{i+1}^{u}\dots x_n^{u} : P} {\mnot\_Flx}
\vsk
% \mbox{\textrm{no rule for } $k=u$}
% \vsk
\ianc{\GG, x\oftp A \prv \mnot(M) \blip  N : B}
{\GG \prv \mnot(\lxua M)  \blip \lxua N : A\GImp{u} B}{\mnot\_Lam}
\vsk
\ianc{g\in\Sigma\cup\GG, g \hastype A_{1}\RImp\dots\RImp A_{m}\RImp 
P, m\geq 0,h \not\equiv g} 
{\GG\prv  \mnot (h\ \Mn^1) \blip 
g\ (H_{1} \GG^{u})^{1}\dots (H_{m}\GG^{u})^{1} : P} {\mnot\_App^{1}}
\vsk
\ianc{\GG\prv \mnot( M_i) \blip N : A_i\qquad 1\leq i\leq n } 
{\GG\prv  \mnot (h\ \Mn^1) \blip 
h\ (H_{1}\GG^{u})^{1}\dots (H_{i-1}\GG^{u})^{1} \ N^{1}\ 
(H_{i+1}\GG^{u})^{1}\dots (H_{n}\GG^{u})^{1} : P} {\mnot\_App^{2}}
\end{array}
\]
\end{small}

\noindent where the $H$'s are fresh generalized variables,
$h\in\Sigma\cup\GG$, and $\GG\prv h\hastype A_{1}\RImp\dots\RImp 
A_{n}\RImp P$. Finally we define $\GG\vd\mmnot(M)= \cN\hastype A$ if 
$\cN=\{N\mid\GG\prv \mnot(M)\blip N\hastype A\}$.
%\beq 
%\mmnot(M\hastype A) & =&  \{N\mid\cdot\prv \mnot(M)\blip N:A\}
%\eneq
\end{Definition} 

Note that if $E_A$ is a generalized variable considered in the empty context,
 it has the canonical form $\l \ol{x_{n}^{u}}\,.\,E\ \ol{x_{n}^{u}}$. Hence
$\cdot\vd\mmnot(E_{A}) = \eset\hastype A$ as expected.

\begin{Example} Let $\GG$ be $x\oftp B,y\oftp C$:
\begin{eqnarray}
\GG\vd\mmnot( E\ x^{u} y^{1}) & = & \{ F\ x^{u} y^{0}\}\nonumber \\
\GG\vd\mmnot( E\ x^{0} y^{1}) & = & \{ F\ x^{1} y^{u}, G\ x^{u} y^{0}\} 
\label{eq:l}
\end{eqnarray}
\end{Example}

We remark that the members of a complement set are not mutually disjoint,
due to the indeterminacy of $u$.  We can achieve a representation by
exclusive patterns if we resolve this indeterminacy, that is, by considering
for every argument $x^{u}$ the two possibilities $x^{1}$ and $x^{0}$.  Thus,
for example, the set from equation (\ref{eq:l}) may be transformed into
 \[ \{F \ x^{1} y^{1}, G \ x^{1} y^{0}, H \ x^{0} y^{0}\} \]
 It is clear that in the worst case scenario the number of terms in a
complement set is bound by $2^{n}$; hence the usefulness of this further
step needs to be pragmatically determined.

%\begin{Example}
%Let $\Sigma$ be the signature of numerals:
%\beq
%\lefteqn{\mmnot(\l x^{u}\l y^{u}.\, s(E\ x^{1} y^{0}) \hastype
%  nat\TImp nat\TImp 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}), \l x^u\l y^u .\, s(N'\ x^{u} 
%y^{1}) \} 
%\eneq
%\end{Example}

We can now revisit\footnote{To avoid too many indices on existential variables,
we adopt a convention that the scope of existential variables is
limited to each member of a complement set.}
 Example \ref{ex:etardx}:
\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'\}
\eneq
% \beq
% \lefteqn{\mmnot(lam(\lamb{x^{u}}{exp} app\ (E\ x^{0})\ x^{1} ))=}\\
% & & \{ lam(\lamb{x^u}{exp} app\ (H\ x^1)\ H'),\\
% & & 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)),\\
% & & app\ H\ H',lam(\lamb{x^u}{exp} lam(\lamb{y^u}{exp} H\ x^u\ y^u) )\}
% \eneq

We can show that simple terms are closed under complementation by
induction over the construction of the complement.

\begin{Theorem}
If $M$ is a simple term, so is $N$, for all $N\in\GG\vd\mmnot(M)\hastype A$.
\end{Theorem}
 
We address the soundness and completeness of the complement algorithm.
Termination is obvious as the algorithm is syntax-directed and only finitely
branching.  We write $\GG\prv  M\in \| \mmnot(N) \|\hastype A$ if 
$\GG\vd\mnot(N)\blip Q\hastype A$ and $\GG\prv  M\in \| Q \|\hastype A$.

\begin{Theorem}[Partition] For a fixed signature $\Sigma$, let 
$\GG\vd N \hastype A$ be a simple linear term.  Then:
\label{lemma:part}
\ben
\item (Exclusivity) It is not the case that both $\GG\prv  M\in \| N \|\hastype A$ and 
$\GG\prv  M\in \| \mmnot(N) \|\hastype A$.
\item (Exhaustivity) If $\GG \vd M \hastype A$ then either
$\GG\prv  M\in \| N \| \hastype A$ or $\GG\prv  M\in \|
\mmnot(N) \|\hastype A$.
\enen
\end{Theorem}

Note that exclusivity is based on Theorem \ref{le:disj}, which holds for
\emph{any} strict term.  In contrast, exhaustivity requires tightening
(Theorem \ref{le:exh}) which holds only for simple terms.

\section{Unification of Simple Terms}
\label{sec:sunif}

We now address the issue of unification, i.e., intersection of simple 
linear \ho patterns.  We start by determining when two labels are 
compatible and define their intersection as follows:
\beq
1 \cap 1 = u \cap 1 = 1\cap u = 1\\
0 \cap 0 = u \cap 0 = 0\cap u = 0\\
u\cap u = u
\eneq
The remaining cases $1 \cap 0$ and $0 \cap 1$ are undefined since
no variable can be both strict and vacuous in a given term.

We use $\Phi$ for sequences of labeled bound variables and
write $\Phi(x) = k$ if $x^k\in\Phi$.  We then 
extend the intersection operations to these contexts:
\beq 
\cdot\mcap \cdot & = & 
\cdot\\
(x^k\ \Phi)\mcap (x^{k'}\ \Phi') & = &  x^{k\mcap k'}\ (\Phi\mcap \Phi')
\quad\mbox{\textrm{if $k\mcap k'$ is defined.}}
\eneq
Following standard terminology with call atomic terms whose head is
a free or bound variable \emph{rigid}, while terms whose head is
an existential variable is called \emph{flexible}.

\begin{Definition}[Higher-Order Pattern Intersection]
Fix a signature $\Sigma$.  For simple linear terms $M$ and $N$ 
 without shared variables such that $\GG \prv M \hastype A$ and $\GG
\prv N \hastype A$, we define $\GG\prv M \mcap N \blip Q \hastype A$ by the
following rules.

\begin{small}
\[
\begin{array}{c}
\ianc{}
{\GG\prv  E \ \Phi_1\mcap   F\ \Phi_2\blip  H\ (\Phi_{1}\mcap \Phi_{2}) \hastype  P} 
{\mcap\_FlxFlx}
\vsk
\mbox{\textrm{no rule for flex-flex with same variable}}
\vsk
\ianc{c\in\Sigma\quad \GG\prv  H_1 \ \Phi_{1}\mcap 
M_{1}\blip N_{1}\hastype A_{1}\cdots \GG\prv  H_n \ \Phi_{n}\mcap 
M_{n}\blip N_{n}\hastype A_{n}  } 
{ \GG\prv  E \ \Phi \mcap c\ \Mns\blip  c\ \Nns\hastype  P} {\mcap\_FlxRgd^c }
\vsk
\ianc{y\in\GG\quad  \quad \GG\prv  H_1 \ \Phi_{1}\mcap 
M_{1}\blip N_{1}\hastype A_{1}\cdots \GG\prv  H_n \ \Phi_{n}\mcap 
M_{n}\blip N_{n}\hastype A_{n} } 
{\GG\prv E\ \Phi \mcap y\ \Mns\blip  y\ \Nns \hastype  P} {\mcap\_FlxRgd^y }
\vsk
\ianc{ h\in\GG\cup\Sigma\quad \GG\prv  M_1 \mcap N_{1} \blip  Q_1\hastype  A_1 \cdots \GG\prv  M_n \mcap 
N_{n}\blip  Q_n \hastype  A_n} 
{\GG\prv   h\ \Mns\mcap h\ \Nns \blip  h\ \ol{Q_{n}^{1}} \hastype  P} {\mcap\_App}
\vsk
\ianc{\GG,x\oftp A\prv   M  \mcap  N \blip  Q\hastype  B}
{\GG\prv   \lxua M  \mcap \lxua N \blip \lxua Q \hastype  A\Imp B}{\mcap\_Lam}
\end{array}
\]
\end{small}
where  the $H$'s are fresh variables of correct  typing and $n\geq 0$.

We have omitted two rules $\mcap\_RgdFlx^c$ and $\mcap\_RgdFlx^y$ which are
symmetric to $\mcap\_FlxRgd^c$ and $\mcap\_FlxRgd^y$.  The rules
$\mcap\_FlxRgd^c$ and $\mcap\_RgdFlx^c$ have the following proviso: for all
$x\in \Phi$ and $1\leq i\leq n$:
\beq
\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) = 1
\And \forall j, j\not = i. \Phi_{j}(x) = u
\eneq
The rules $\mcap\_FlxRgd^y$ and $\mcap\_RgdFlx^y$ are subject to the
proviso
\beq
\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. x \not= y \And \Phi(x) = 1  \Imp  \exists i\,.\, \Phi_{i}(x) = 1
\And \forall j, j\not = i. \Phi_{j}(x) = u \\
\Phi(y) = u \Or
(\Phi(y)=1 \And  \forall i. \Phi_{i}(y) = u)
\eneq
Finally define $\GG\vd M\mbigcap N \hastype A = {\cal Q}$ if ${\cal Q}=
 \{Q\mid\GG\prv  M\mcap N \blip  Q \hastype  A\}$.
%\beq
%M\mbigcap N \hastype A & =& \{Q\mid\cdot\prv  M\mcap N \blip  Q \hastype  A\}
%\eneq
\end{Definition} 

Some remarks are in order:
\bit
\item
In rule $\mcap\_FlxFlx$ we can assume that the same list of variables,
though possibly with different labeling, is the argument of $E,F$ and $H$,
since simple terms are fully applied and due to linearity we can always
reorder the context to the same list.  Since patterns are linear and $M$ and
$N$ share no pattern variables, the flex-flex case arises only with distinct
variables.  This also means we do not have to apply substitutions or perform
the customary occurs-check.
\item 
In the flex/rigid and rigid/flex rules, the proviso enforces the typing
discipline since each strict variable $x$ must be strict in some premise.
The modified condition on $y$ takes into account that the head of an
application constitutes a strict occurrence.
\enit

The following example illustrates how the Flex-Rigid rules, in this 
case $\mcap\_FlxRgd^c$, make unification on simple terms finitary.

\begin{Example}
Consider the unification problem $x\oftp A\prv E\ x^{1}\mbigcap\ 
c\ (F\ x^{u})^{1} \ (F'\ x^{u})^{1}$.  Since $x$ is strict in 
the LHS, there are two ways in which $\Phi$ can be split leading 
to the following sub-problems:
\[
\begin{array}{lrr}
x\oftp A\prv E' \ x^{1}\mcap\  F\  x^{u} \blip  H\  x^{1}
& & x\oftp A\prv E''\ x^{u}\mcap\  F'\  x^{u} \blip  H'\  x^{u}
\\
x\oftp A\prv E' \ x^{u}\mcap\  F\  x^{u} \blip  H\  x^{u}
& & x\oftp A\prv E''\ x^{1}\mcap\  F'\  x^{u} \blip  H'\  x^{1}
\end{array}
\]
Hence the result:
\beq
x\oftp A\prv E\ x^{1}\mbigcap\  c\ (F\  x^{u})^{1} \ (F'\  
x^{u})^{1}= \{c\ (H\  x^{1})^{1} \ (H'\  x^{u})^1,c\ (H\  x^{u})^1 \ (H'\  
x^{1})^1\}
\eneq
\end{Example}

Note that, similarly to complementation, intersection returns a
solution with possible overlaps between the patterns.  Again it
is possible, in a post-processing phase, to transform the results
into disjoint form.

As for complement, the termination of the algorithm is straightforward since
the judgment is term-directed with finite branching.  The adequacy proof
for the unification algorithm on linear simple terms requires two
implications which follow inductively, at the heart relying on properties of
strict typing derivations.

\begin{Theorem}[Adequacy of Pattern Intersection]
\label{co:unif}
Fix a signature $\Sigma$.  For simple linear terms $N_1$ and $N_2$ 
 without shared variables such that $\GG \prv N_1 \hastype A$ and $\GG
\prv N_2 \hastype A$, $\GG\prv 
M\in\|N_{1}\|\hastype A$ and $\GG\prv M\in\|N_{2}\|\hastype A$  iff $\GG\prv 
M\in\|N_1\mbigcap N_2\|\hastype A$.
\end{Theorem}

\section{Conclusion}
\label{sec:concl}

We have shown that the complement of linear higher-order patterns cannot
be expressed as a finite union of such patterns.  To close the language
under complement we generalized to a $\lambda$-calculus
in which strict and vacuous functions can be expressed in the type system.
The original language can be embedded compositionally into \emph{simple
patterns}.  On this language, both complement and intersection (that is,
unification) can be expressed as a finite union of simple linear patterns.
From this it is easy to see that finite sets of simple linear patterns
form a boolean algebra. Indeed, we can trivially define the {\em relative complement}
of two terms via complement and intersection; namely, extending as
expected the latter operation to operate on sets of terms, we have:
\beq
\cM-\cN & = & \cM\mbigcap \neg \cN
\eneq

Our main application lies in higher-order logic programming, where pattern
complement is a necessary component in any algorithm to synthesize the
negation of a given program.  This synthesis includes two basic operations:
negation to compute the complements of heads of clauses in the
definition of a predicate, and intersection to combine results of
negating individual clause  heads.  In this paper we have
provided algorithms to compute both.

While this approach has been investigated for \fo Horn clauses 
\cite{Bar90} and CLP programs \cite{Bruscoli94}, the field
has been little explored with respect to \ho logics and logical frameworks.
This is the most important future work we are considering;
the algorithms presented here provide the central foundation.

We also plan to extend the results to dependent types to
endow intentionally weak frameworks such as Twelf \cite{Schurmann98cade}
with a logically meaningful notion of 
negation along the lines of \cite{Bar90}.  Finally, we hope to address the 
general case of complementation and unification in the strict 
$\lambda$-calculus which is likely to be useful in linear logical 
frameworks as {\em LLF} \cite{Cervesato96lics}.

\medskip
\noindent
{\bf Acknowledgments}. We are grateful to Iliano Cervesato, Carsten Sch\"{u}rmann and Roberto Virga for useful comments on previous versions of this paper.
This work has been partially supported by NSF Grant CCR-9619584.

\bibliography{iclp,not,framework,strict}
 
\end{document}
