Unification Without Occurs Check on a Cellular Tree

[[abstract]]This paper presents the design of a special‐purpose cellular tree architecture for the unification algorithm. The unification algorithm either finds the most general substitution which makes a set of terms identical, or else returns failure. The resulting substitution is permitted to contain loops. Many of the more recent pure logic programs make use of such recursive substitutions to store data structures which are accessed in a lazy fashion. So lack of such an occurs check is intentional. The algorithm involves only integer comparison and shifting operations between adjacent cells in a data‐driven computation mode. The physical design of a VLSI chip, therefore, should be quite easy. Each unification problem runs on the cellular tree in worst‐case time O (n · logn), where n is the number of input symbols. Many unification problems can be run simultaneously on the same chip with no slowdown.[[fileno]]2070502010001[[department]]服務科學研究