ORDER-INDEPENDENT UNIFICATION AND BACKTRACKING

Abstract

Two algorithms for order-independent unification are presented. Both assume that unifications are timestamped, giving a natural ordering on unifications from lowest timestamp to highest. The first algorithm permits lower-timestamped unifications to be performed after higher-timestamped unifications have already been done, without requiring previous unifications to be backtracked and later redone. The binding state that results is indistinguishable from that produced by a lowest-to-highest execution. The second algorithm extends the first by allowing intermediate unifications to be undone, again avoiding work in undoing and redoing unifications with higher timestamps. These algorithms are designed for distributed, fully AND-parallel Prolog execution; asynchronous events occurring on different CPSs can be reconciled without too much overhead.