Return to search

Linear Unification

Efficient unification is considered within the context of logic programming. Unification is explained in terms of equivalence classes made up of terms, where there is a constraint that no equivalence class may contain more than one function term. It is demonstrated that several well-known "efficient" but nonlinear unification algorithms continually maintain the said constraint as a consequence of their choice of data structure for representing equivalence classes. The linearity of the Paterson-Wegman unification algorithm is shown largely to be a consequence of its use of unbounded lists of pointers for representing equivalences between terms, which allows it to avoid the nonlinearity of "union-find".

Identiferoai:union.ndltd.org:unt.edu/info:ark/67531/metadc500971
Date12 1900
CreatorsWilbanks, John W. (John Winston)
ContributorsYang, Chao-Chih, Conrady, Denis A., Vlach, Frank
PublisherUniversity of North Texas
Source SetsUniversity of North Texas
LanguageEnglish
Detected LanguageEnglish
TypeThesis or Dissertation
Formatviii, 80 leaves, Text
RightsPublic, Copyright, Copyright is held by the author, unless otherwise noted. All rights reserved., Wilbanks, John W. (John Winston)

Page generated in 0.0024 seconds