Third order matching is decidable

DOI10.1016/0168-0072(94)90083-3zbMath0822.03010OpenAlexW1988246540MaRDI QIDQ1337691

Gilles Dowek

Publication date: 8 November 1994

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0168-0072(94)90083-3

zbMATH Keywords

interpolationdecidabilitymatching problemthird ordersimply typed \(\lambda\)-calculus

Mathematics Subject Classification ID

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

Related Items (12)

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 ⋮ Nominal syntax with atom substitutions ⋮ Decidability of bounded higher-order unification ⋮ The variable containment problem ⋮ Third-order matching in the polymorphic lambda calculus ⋮ Decidability of all minimal models ⋮ Typed answer set programming lambda calculus theories and correctness of inverse lambda algorithms with respect to them ⋮ Decidable higher-order unification problems ⋮ A colored version of the λ-calculus ⋮ On the undecidability of second-order unification ⋮ Model-Checking Games for Typed λ-Calculi

Cites Work

• The lambda calculus, its syntax and semantics
• Unification under a mixed prefix
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Proving and applying program transformations expressed with second-order patterns
• Higher-order unification revisited: Complete sets of transformations
• Completeness, invariance and λ-definability
• The Clausal Theory of Types
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Third order matching is decidable