Delaying unification algorithms for lambda calculi (Q1104776)

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.