Efficient unification over infinite terms
- 42 Downloads
We address the unification problem for expressions over infinite first-order terms. An algorithm which is practically linear in time and space is presented. It is argued that this algorithm is better than some recent algorithms with respect to performance in practice and simplicity in nature. It is further argued that this superiority also holds in comparison with some of the best known algorithms for the more conventional unification problem over finite terms.
KeywordsUnification First-Order Terms Infinite Terms
Unable to display preview. Download preview PDF.
- 1).Aho, A. V., Hopcroft, J. E. and Ullman, J. D.: “Data Structures and Algorithms” (Addison-Wesley) (1983).Google Scholar
- 2).Baxter, L. D.: “A Practically Linear Unification Algorithm,” Report,CS-76-13 (Department of Computer Science, University of Waterloo) (February, 1976).Google Scholar
- 3).Corbin, J. and Bidoit, M.: “A Rehabilitation of Robinson’s Unification Algorithm,” Information Processing 83, R. E. A. Mason (ed.) (Elsevier Science Publishers) (September, 1983) 909–914.Google Scholar
- 4).Colmerauer, A.: “Prolog and Infinite Trees,” in Logic Programming, K. L. Clark and S-Å. Tärnlund (eds.) (Academic Press) (1982) 231–251.Google Scholar
- 7).Mukai, K.: “A Unification Algorithm for Infinite Trees,” Proceedings IJCAI-83 (Karlsruhe) (August, 1983) 547–549.Google Scholar