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

typesdecidabilityunificationsimply typed \(\lambda\)-calculushigher-order matching

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
• Computer Science Logic
• scientific article; zbMATH DE number 2090083

Cited in

(18)

• Recognizability in the Simply Typed Lambda-Calculus
• Computer Science Logic
• Matching Modulo Superdevelopments Application to Second-Order Matching
• The variable containment problem
• scientific article; zbMATH DE number 2185677 (Why is no real title available?)
• Unification for \(\lambda\)-calculi without propagation rules
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility
• Decidability of bounded higher-order unification
• Simply typed convertibility is \textsc{Tower}-complete even for safe lambda-terms
• Higher-order beta matching with solutions in long beta-eta normal form
• Fundamentals of Computation Theory
• Third order matching is decidable
• scientific article; zbMATH DE number 2090083 (Why is no real title available?)
• Typed answer set programming lambda calculus theories and correctness of inverse lambda algorithms with respect to them
• The undecidability of pattern matching in calculi where primitive recursive functions are representable
• Automated Deduction – CADE-19
• The inverse lambda calculus algorithm for typed first order logic lambda calculus and its application to translating English to FOL
• Model-checking games for typed \(\lambda\)-calculi

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)