Algebraic computational models of OR-parallel execution of Prolog (Q1920217)

A specification of the OR-parallel execution of Prolog programs, using CHOCS (calculus of higher order communicating systems), is presented in this paper. A translation is defined from Prolog programs and goals to CHOCS processes: the execution of the CHOCS process corresponding to a goal mimics the OR-parallel execution of the original Prolog goal. In the translation, clauses and predicate definitions of a Prolog program correspond to processes. To model OR-parallelism, the processes \(P^1, \dots, P^n\), corresponding to clauses \(C_1, \dots, C_n\) (having the same head predicate \(p\)) start their execution concurrently, but, in order to respect to depth-first search rule, each \(P^i\) is guarded by the termination of the executions of processes \(P^j\)'s, \(j<i\). The computational model is proved correct with respect to the semantics of Prolog. Our model, because of its algebraic specification, can be easily used to prove properties of the parallel execution of Prolog programs. Moreover, the model exploits the maximum degree of parallelism, by giving the Prolog solutions in parallel, without any order among them. However, this model, being close to the Prolog semantics definition, contains sources of inefficiency which make it unpractical as a guide for the implementation. To overcome these problems, a new computational model is defined. This model is obtained by modifications of the basic one and thus its correctness can be easily proved. Finally, we show how to obtain models of different real implementations of OR-parallel Prolog by slight modification of the new model. The relations among all these results, in terms of parallelism degree, are studied by using of the concepts of bisimulation and simulation, developed for concurrent calculi.