A deterministic PROLOG fixpoint semantics. (English) Zbl 0592.68021

Fitting, Melvin

J. Logic Program. 2, 111-118 (1985).

This article presents a fixpoint semantics for a core subset of PROLOG (without unification, backtracking or meeting a goal) that deals with deterministic control structures as well as logical features. To this end a kind of computation sequence are employed to model the execution of a PROLOG program given some goal. More or less classical fixedpoint theory is used to prove that such an execution sequence can be obtained as the least fixedpoint of a semantical operator associated with the program in question. In fact, this result amounts to the equivalence proof of the denotational and the operational semantics presented. The proof of this theorem is rather informal and may provide the non-theoreticist more intuition about these matters than a strictly formal one, the more so as the paper illustrates every move by means of examples.

Reviewer: J.-J.Ch.Meyer

MSC:

68Q60

Specification and verification (program logics, model checking, etc.)

Keywords:

operational semantics; fixpoint semantics; PROLOG; deterministic control structures