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".
| Identifer | oai:union.ndltd.org:unt.edu/info:ark/67531/metadc500971 |
| Date | 12 1900 |
| Creators | Wilbanks, John W. (John Winston) |
| Contributors | Yang, Chao-Chih, Conrady, Denis A., Vlach, Frank |
| Publisher | University of North Texas |
| Source Sets | University of North Texas |
| Language | English |
| Detected Language | English |
| Type | Thesis or Dissertation |
| Format | viii, 80 leaves, Text |
| Rights | Public, Copyright, Copyright is held by the author, unless otherwise noted. All rights reserved., Wilbanks, John W. (John Winston) |
Page generated in 0.002 seconds