Higher-order pattern complement and the strict -calculus

DOI10.1145/937555.937559MaRDI QIDQ5267440zbMATH OpenOpenAlexFDO

Authors Alberto Momigliano, Frank Pfenning

Publication date 13 June 2017

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

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)

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.

Recommendations

• Lambda calculus with patterns
• Linear unification of higher-order patterns
• scientific article; zbMATH DE number 1822269
• Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type
• Logic Based Program Synthesis and Transformation

Cited in

(3)

• The undecidability of proof search when equality is a logical connective
• scientific article; zbMATH DE number 2043532 (Why is no real title available?)
• αCheck: A mechanized metatheory model checker

Describes a project that uses

Uses Software

• Elf

This page was built for publication: Higher-order pattern complement and the strict \(\lambda\)-calculus

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