History and basic features of the critical-pair/completion procedure (Q1103414)

The paper is an interesting survey of the basic ideas and major advances in critical-pair/completion (clause based language when recursive predicates, possibly with function symbols, are present. The proposed approach takes the naive fixed point computation that realizes the minimum model semantics of the given program and transforms it into a computation that terminates and executes efficiently. Rule rewriting scripts, called methods, are used for these transformations; different methods are selected according to the patterns of free and bound variables appearing in the given recursive goal. One method, known as seminaive fixed point, applies to the situation where no argument is bound in the recursive goal. The remaining methods are meant for queries where the initial bindings of the arguments in the recursive goal can be used to improve the efficiency and, often, to guarantee the termination of the computation. The general solution used for these queries consists of implementing the recursive predicate as a cascade of two fixed point computations. Various methods proposed along these lines are studied and compared, including the magic set method, the counting method and the magic counting method. These methods are implemented as rule rewriting transformations which compile a given program into a safe and efficient implementation.