Higher-Order Pattern Complement and the Strict Lambda-Calculus

TL;DR

This paper introduces a generalized lambda-calculus with strict functions to effectively compute complements of higher-order patterns, enabling better handling of negation in higher-order logic programming.

Contribution

It presents a novel calculus that allows finite pattern sets to be closed under complement and intersection, addressing limitations of previous approaches.

Findings

Finite pattern sets are closed under complement and intersection in the new calculus.

The approach improves the transformational handling of negation in higher-order logic programs.

The calculus includes an internal notion of strict functions to express variable dependencies.

Abstract

We address the problem of complementing higher-order patterns without repetitions of existential 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 patterns without repeated variables are closed under complement and intersection. Our principal application is the transformational approach to negation in higher-order logic programs.