A fast parallel algorithm for N-ary unification with AI applications
M. P. Cine · 1989
Unification is the central primitive used in all Resolution based Automated Theorem Proving systems (Robinson65a) and Logic Programming (Kowalski74) environments. Almost all the efforts in this area has been focused on the special case of unifying just two terms (binary unification (Kowalski79)), which is only sufficient when the theorem prover's input language is restricted (ex: to Horn logic (Horn51), (Henschen74)) or when additional inference rules are provided (such as Factoring (Wos64)). Fast (linear time) binary unification algorithms have existed for a decade (Martelli77), (Paterson78b), but when more than two terms are unified (n-ary unification), the typical solution is quadratic, the original algorithm being exponential (Robinson65a). We show that n-ary unification can be reduced to binary unification, resulting in efficient sequential and parallel algorithms. In particular, if N is the size of the input graph (nodes + edges), the parallel algorithm has a time cost of O(N) with processors proportional to the number of terms in the unified set. Adopting the popular computational complexity view that sublinear unification is impossible even with infinite processors (Yasuura84), (Dwork84), our algorithm is popularly optimal (Dwork86). It is the Literature's first linear parallel n-ary unifier. The sequential algorithm is also asymptotically efficient: it has a time cost bounded by O(N logN) which is within a factor of logN from optimal. As well as theoretical efficiency, our system has minimal startup and overhead costs, pragmatic concerns which have plagued other unification algorithms (DeChampeaux86a), (Martelli82), (Escalada88). Asymptotic time cost analysis of unification in the recent Literature has contained ambiguities. We show how different authors have stated the same time cost for their algorithms, yet the actual efficiencies vary all the way from linear to exponential time. We present a new categorization schema intended to remove this confusion. A flexible binary unifier is developed which is combined with an implementation of our n-ary unification theory. The n-ary unifier is ported to a number of hardware platforms, including several monoprocessors and a tightly coupled MIMD multiprocessor (the Sequent B21). A suite of tests is performed on the implementations, results confirming the time cost analysis. We also discuss the relative fitness of SIMD architectures (such as the Connection machine) for a class of algorithms such as ours. The simplicity of our algorithm not only implies a very small startup cost, but it also means the theory might be realizable in hardware. We discuss the importance of this (the Literature's first hardware n-ary unifier), then present a solution. We keep the presentation at the conceptual level, broad enough to allow implementations to be based on any number of existing hardware primitives. Finally, the new n-ary unification framework is shown to be flexible, promising other avenues of application.