Third order matching is decidable

DOI10.1016/0168-0072(94)90083-3MaRDI QIDQ1337691zbMATH OpenOpenAlexFDO

Authors 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

decidabilityinterpolationmatching problemsimply typed \(\lambda\)-calculusthird order

Mathematics Subject Classification ID

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

Review text

The matching problem in the simply typed \(\lambda\)-calculus has been shown decidably by Huet in the case of at most second order, but it is open in general. The author shows that it is decidable in the case of third order. The main idea is that if a problem \(a=b\), where \(b\) is ground, has a solution, then it also has a solution whose depth (of Böhm tree) is bounded by some integer depending only on the problem. This is first shown for an interpolation problem as an intermediate stage. The proof is very neatly described.

Recommendations

• Third-order matching in the polymorphic lambda calculus
• scientific article; zbMATH DE number 2185677
• Higher Order   Matching is Undecidable
• Computer Science Logic
• Decidability of fourth-order matching

Cites work

• A unification algorithm for typed -calculus
• Completeness, invariance and λ-definability
• Higher-order unification revisited: Complete sets of transformations
• scientific article; zbMATH DE number 3935004 (Why is no real title available?)
• scientific article; zbMATH DE number 3993540 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• Proving and applying program transformations expressed with second-order patterns
• The Clausal Theory of Types
• The lambda calculus, its syntax and semantics
• Unification under a mixed prefix

Cited in

(17)

• On the undecidability of second-order unification
• Decidability of bounded higher-order unification
• Nominal syntax with atom substitutions
• 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
• scientific article; zbMATH DE number 2185677 (Why is no real title available?)
• Unification for -calculi without propagation rules
• Higher-order beta matching with solutions in long beta-eta normal form
• scientific article; zbMATH DE number 1223619 (Why is no real title available?)
• The variable containment problem
• Third-order matching in the polymorphic lambda calculus
• Decidability of all minimal models
• Higher Order   Matching is Undecidable
• 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
• Fundamentals of Computation Theory

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

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