Top-down semantics of fair computations of logic programs. (English) Zbl 0592.68019

van Emden, M. H.; Abdallah, M. A. Nait

J. Logic Program. 2, 67-75 (1985).

The title of this paper is somewhat confusing. Top-down semantics is not to be associated with top-down design in any way. It merely indicates that the semantics is built upon a reverse set-inclusion rather than just set-inclusion as is done traditionally in logic programming. Approximations start with the Herbrand base B (top) instead of \(\emptyset\) (bottom). To make thing work this Herbrand base is extended with formulas with infinite terms. This approach is strongly related to that of using the Smyth ordering [M. B. Smyth, J. Comput. Syst. Sci. 16, 23-36 (1978; Zbl 0391.68011)] in the denotational semantics of standard (i.e. not-logic) programming.
The result the authors obtain is an extension of that of [M. A. Nait Abdallah, Lect. Notes Comput. Sci. 172, 358-370 (1984; Zbl 0557.68030)]: Every k-fairly (informally expressing that the shortest computation that is not yet successful, has length k) SLD-derived result can be obtained by iteration of the transformation associated with the program from B. (This should be contrasted with the well-known fact that every successful computation can be obtained by iteration from \(\emptyset)\). This theorem provides semantic justification for derivations independent whether they are successful or failed, finite or infinite. As a consequence it enables infinite (\(\omega\)-)fair computation to be characterized by means of greatest models or fixpoints, yielding a ”top-down” semantics.

Reviewer: J.-J.Ch.Meyer

MSC:

68Q60	Specification and verification (program logics, model checking, etc.)
68N01	General topics in the theory of software

Keywords:

fixpoint semantics; fairness; logic programming; Herbrand base

Citations:

Zbl 0391.68011; Zbl 0557.68030