SLDR-resolution: Parallelizing structural recursion in logic programs

AbstractWe introduce a new operational semantics, SLDR-resolution, for a class of recursive logic programs. We establish the soundness and completeness of SLDR-resolution by showing that one SLDR-resolution inference is equivalent to n ≥ 1 SLD-resolution inferences. SLDR-resolution facilitates parallel processing of recursive programs and can exploit parallelism that is not exploitable in SLD-resolution. In contrast with SLD-resolution, where each recursive invocation of a program typically results in a small unification, SLDR-resolution results in large unification computations amenable to optimization and parallelization. Moreover, SLDR-resolution allows a form of AND-parallelism in which the recursive invocations of a procedure start computing simultaneously. Unification in SLDR-resolution can be compiled in a novel way: the unification correspond to solving systems of recurrence equations, and the compilations corresponds to obtaining closed-form expressions for these systems. Another new idea in compilation of SLDR-resolution is to exploit the technique of loop parallelization, which was developed in the context of imperative programming in the early 1970s