On the existence of closed terms in the typed lambda calculus II: Transformations of unification problems

DOI10.1016/0304-3975(81)90086-4zbMath0486.03011OpenAlexW2050106235MaRDI QIDQ1164619

Richard Statman

Publication date: 1981

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(81)90086-4

zbMATH Keywords

typed lambda calculusdecidable unification problemspolynomial time decidabletypes of expressions

Mathematics Subject Classification ID

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

Related Items

Rewriting, and equational unification: the higher-order cases, Word operation definable in the typed \(\lambda\)-calculus, A characterization of lambda definable tree operations, Unification under a mixed prefix, Extensional models for polymorphism, Higher-order unification revisited: Complete sets of transformations, \(\lambda\)-definability of free algebras

Cites Work

• Unnamed Item
• Unnamed Item
• The undecidability of the second-order unification problem
• Intuitionistic propositional logic is polynomial-space complete
• The typed lambda-calculus is not elementary recursive
• Completeness, invariance and λ-definability
• Ordering by Divisibility in Abstract Algebras