Delaying unification algorithms for lambda calculi (Q1104776)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Delaying unification algorithms for lambda calculi |
scientific article |
Statements
Delaying unification algorithms for lambda calculi (English)
0 references
1988
0 references
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.
0 references
lambda calculus
0 references
unification
0 references
rewriting systems
0 references
0 references