A π-calculus specification of prolog

Abstract

A clear and modular specification of Prolog using the π-calculus is presented in this paper. Prolog goals are represented as π-calculus processes, and Prolog predicate definitions are translated into π-calculus agent definitions. Prolog’s depth-first left-right control strategy as well as the cut control operator are modeled by the synchronized communication among processes, which is similar in spirit to continuation-passing style implementation of Prolog. Prolog terms are represented by persistent processes, while logical variables are modeled by complex processes with channels that, at various times, can be written, read, and reset. Both unifications with and without backtracking are specified by π-calculus agent definitions. A smooth merging of the specification for control and the specification for unification gives a full specification for much of Prolog. Some related and further works are also discussed.