Recursion equation sets computing logic programs

AbstractThis paper establishes a method of constructing a recursion equation set computing a given logic program. The recursion equation set is regarded as a dataflow program and transformable into a Lisp-like program for the dataflow. The recursion equation set constructible from a logic program expresses the procedure to form the minimal Herbrand model of the original logic program by means of inferences and is defined over a sequence domain. The domain is the set of all finite and infinite sequences of ground atoms. The recursion equation set contains functions corresponding to the inferences caused by definite clauses, and fair merge functions necessary for the purpose of taking set unions in terms of variables denoting ground atom sequences. The functions in accordance with the inferences concerning definite clauses areobtained by eliminating the nondeterminism usually involved. By the fair merge function, we mean a device to provide a sequence variable acquired by interleaving input infinite sequence variables without neglecting any part of any input sequence. It is shown that the recursion equation set defines a continuous function from a direct product of a sequence domain to itself, therefore there exists a least fixpoint of the function. The fixpoint completely denotes the minimal Herbrand model of the original logic program, which is essential for its finite computation. Finally it is shown that the recursion equation set can be expressed as a Lisp-like program