Delaying unification algorithms for lambda calculi

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

Author Staples, John
Title Delaying unification algorithms for lambda calculi
Journal name Theoretical Computer Science   Check publisher's open access policy
ISSN 0304-3975
Publication date 1988-03-01
Year available 1988
Sub-type Article (original research)
DOI 10.1016/0304-3975(88)90135-1
Open Access Status DOI
Volume 56
Issue 3
Start page 277
End page 288
Total pages 12
Place of publication Amsterdam, Netherlands
Publisher Elsevier
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 UQ

Document type: Journal Article
Sub-type: Article (original research)
Collection: 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 on behalf of Learning and Research Services (UQ Library)