Decidability of bounded higher-order unification

DOI10.1016/j.jsc.2005.01.005zbMath1126.03017OpenAlexW1985178949MaRDI QIDQ2456577

Manfred Schmidt-Schauss, Klaus U. Schulz

Publication date: 19 October 2007

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: http://publikationen.ub.uni-frankfurt.de/files/4588/bounded_ho5.pdf

zbMATH Keywords

higher-order unificationsimply typed lambda calculusdecision algorithmsexponent of periodicitybounded unification problems

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Decidability of theories and sets of sentences (03B25) Combinatory logic and lambda calculus (03B40)

Related Items

Regular Patterns in Second-Order Unification ⋮ Restricted combinatory unification

Uses Software

• ML
• Haskell
• Miranda
• ETPS
• Curry

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• A unification algorithm for second-order monadic terms
• The undecidability of the second-order unification problem
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Mechanizing \(\omega\)-order type theory through unification
• The typed lambda-calculus is not elementary recursive
• Completion of rewrite systems with membership constraints. I: Deduction rules
• Word unification and transformation of generalized equations
• Isabelle. A generic theorem prover
• Third order matching is decidable
• Proof theory and automated deduction
• Solvability of context equations with two context variables is decidable
• On rewrite constraints and context unification
• On the undecidability of second-order unification
• Decidability of bounded second order unification
• An upper bound for reduction sequences in the typed \(\lambda\)-calculus
• Exact bounds for lengths of reductions in typed λ-calculus
• Decidability of the unification problem for second-order languages with unary functional symbols
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
• Complexity of Makanin's algorithm
• Decidability of fourth-order matching
• Higher Order   Matching is Undecidable
• A Decision Algorithm for Stratified Context Unification
• Linear second-order unification
• On equality up-to constraints over finite trees, context unification, and one-step rewriting
• Automated Deduction – CADE-19
• The Clausal Theory of Types
• Makanin's algorithm for word equations-two improvements and a generalization