Delaying unification algorithms for lambda calculi

DOI10.1016/0304-3975(88)90135-1MaRDI QIDQ1104776zbMATH OpenOpenAlexFDO

Authors John Staples

Publication date 1988

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

Full work available at URL https://doi.org/10.1016/0304-3975(88)90135-1

zbMATH Keywords

lambda calculusrewriting systemsunification

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Symbolic computation and algebraic computation (68W30)

Review text

Huet proposed delaying some unifications of typed lambda terms, as part of a higher-order resolution method. This paper abstracts that idea from the resolution context. Unification delays are formalized independently of any context, by defining a lambda calculus where a unification constraint forms an integral part of each term. This calculus is shown to support an unusually simple unification theory, where most general unifiers trivially always exist. Attention shifts from the existence of unifiers to the simplification of expressions for most general unifiers. The approach is convenient for discussing the unification of untyped lambda terms and has promise for discussing schematic unification of term schemes. It may also be a convenient format for unification algorithms in rewriting systems which use lazy evaluation to compute with notations for infinite structures.

Recommendations

• A UNIFICATION ALGORITHM FOR THE λΠ-CALCULUS
• Unification for -calculi without propagation rules
• scientific article; zbMATH DE number 1303341
• Unifying lazy and strict computations
• Theorem proving for untyped constructive -calculus: Implementation and application
• Nondeterministic extensions of untyped \(\lambda\)-calculus
• scientific article; zbMATH DE number 3997190
• The lazy lambda calculus in a concurrency scenario
• Initial algebra semantics for lambda calculi
• scientific article; zbMATH DE number 3933030

Cites work

• A unification algorithm for typed -calculus
• Efficient unification of quantified terms
• Graph reduction. Proceedings of a Workshop, Santa Fé, New Mexico, USA, September 29 - October 1, 1986
• Structure sharing for quantified terms: Fundamentals

Cited in

(2)

• Lazy linear combinatorial unification
• scientific article; zbMATH DE number 1303341 (Why is no real title available?)

This page was built for publication: Delaying unification algorithms for lambda calculi

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