Delaying unification algorithms for lambda calculi

Staples J. (1988) Delaying unification algorithms for lambda calculi. Theoretical Computer Science, 56 3: 277-288. doi:10.1016/0304-3975(88)90135-1

Author Staples J.
Title Delaying unification algorithms for lambda calculi
Journal name Theoretical Computer Science   Check publisher's open access policy
ISSN 0304-3975
Publication date 1988-01-01
Sub-type Article (original research)
DOI 10.1016/0304-3975(88)90135-1
Volume 56
Issue 3
Start page 277
End page 288
Total pages 12
Language eng
Subject 1703 Computational Theory and Mathematics
Abstract 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 formalised 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.
Q-Index Code C1
Q-Index Status Provisional Code
Institutional Status Unknown

Document type: Journal Article
Sub-type: Article (original research)
Collections: Scopus Import
Scopus Import - Archived
Version Filter Type
Citation counts: Scopus Citation Count Cited 0 times in Scopus Article
Google Scholar Search Google Scholar
Created: Tue, 26 Jul 2016, 15:03:21 EST by System User