Higher Order Matching is Undecidable

DOI10.1093/jigpal/11.1.51zbMath1014.03017OpenAlexW2126489583MaRDI QIDQ4795875

Ralph Loader

Publication date: 22 July 2003

Published in: Logic Journal of 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)

Related Items

The Inverse Lambda Calculus Algorithm for Typed First Order Logic Lambda Calculus and Its Application to Translating English to FOL, 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, Typed answer set programming lambda calculus theories and correctness of inverse lambda algorithms with respect to them, Recognizability in the Simply Typed Lambda-Calculus, Model-Checking Games for Typed λ-Calculi