Abstract of "The Relative Complement Problem for Higher-Order Patterns"

 We address the problem of complementing higher-order unrestricted
patterns, that is without repetitions of free variables.  Differently
from the first-order 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 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 unrestricted patterns
are closed under complement and unification.  Our principal
application is the transformational approach to negation in
higher-order logic programs.