Higher-Order Pattern Complement and the Strict λ-Calculus

Title: Higher-Order Pattern Complement and the Strict λ-Calculus

Research Question: How can we generalize the concept of pattern complementation to higher-order patterns without repetitions of existential variables?

Methodology: The authors propose a generalization of the simply-typed λ-calculus to include an internal notion of strict function. This allows them to directly express that a term must depend on a given variable. They show that, in this more expressive calculus, finite sets of patterns without repeated variables are closed under complement and intersection.

Results: The main result is the development of a method for complementing higher-order patterns without repetitions of existential variables. This is achieved by generalizing the simply-typed λ-calculus to include an internal notion of strict function and invariance, allowing for the expression of dependencies between terms and variables.

Implications: The research has implications for the field of functional and logic programming, where pattern matching and unification play an important role. The proposed method can be applied to problems such as generalization, complementation, and transformation in higher-order logic programs. It may also have applications in other areas such as logical frameworks, term rewriting, and functional logic programming.

Link to Article: https://arxiv.org/abs/0109072v1 Authors: arXiv ID: 0109072v1