Higher-order pattern complement and the strict λ-calculus

DOI10.1145/937555.937559zbMATH Open1365.68155arXivcs/0109072OpenAlexW2077870744MaRDI QIDQ5267440FDOQ5267440

Frank Pfenning, Alberto Momigliano

Publication date: 13 June 2017

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/cs/0109072

zbMATH Keywords

complementhigher-order patternsstrict \(\lambda\)-calculus

Mathematics Subject Classification ID

Logic programming (68N17) Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Cited In (3)

• αCheck: A mechanized metatheory model checker
• The undecidability of proof search when equality is a logical connective
• Title not available (Why is that?)

Uses Software

• Elf

This page was built for publication: Higher-order pattern complement and the strict λ-calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5267440)