Higher Order Matching is Undecidable

DOI10.1093/JIGPAL/11.1.51MaRDI QIDQ4795875zbMATH OpenOpenAlexFDO

Authors Ralph Loader

Publication date 22 July 2003

Published in Logic Journal of the IGPL (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/jigpal/11.1.51

zbMATH Keywords

decidabilityhigher-order matchingsimply typed \(\lambda\)-calculustypesunification

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Combinatory logic and lambda calculus (03B40)

Recommendations

• Higher-order beta matching with solutions in long beta-eta normal form
• Third order matching is decidable
• Decidability of fourth-order matching
• Higher-order matching in the linear -calculus with pairing
• A decidable variant of higher order matching

Cited in

(20)

• The undecidability of pattern matching in calculi where primitive recursive functions are representable
• Third order matching is decidable
• Decidability of bounded higher-order unification
• Model-checking games for typed -calculi
• The inverse lambda calculus algorithm for typed first order logic lambda calculus and its application to translating English to FOL
• Third-order matching in the presence of type constructors (extended abstract)
• Unification for -calculi without propagation rules
• Higher-order beta matching with solutions in long beta-eta normal form
• Recognizability in the Simply Typed Lambda-Calculus
• Decidability of fourth-order matching
• The variable containment problem
• A decidable variant of higher order matching
• Typed answer set programming lambda calculus theories and correctness of inverse lambda algorithms with respect to them
• Higher-order matching in the linear -calculus with pairing
• Matching Modulo Superdevelopments Application to Second-Order Matching
• Fundamentals of Computation Theory
• Automated Deduction – CADE-19
• Simply typed convertibility is \textsc{Tower}-complete even for safe lambda-terms
• Mechanized undecidability of higher-order beta-matching
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility

This page was built for publication: Higher Order   Matching is Undecidable

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