The University of Edinburgh -
Division of Informatics
Forrest Hill & 80 South Bridge

Research Paper #469

Title:An Algebraic Semantics of Sequential Prolog Control
Authors:Ross,B; Wilk,P
Date:Mar 1990
Presented:A shorter version of this paper was submitted to NACLP, 1990
Abstract:This work introduces a new algebraic semantics of sequential Prolog. The semantics is based on a process interpretation of logic program computation, and is written in Milner's Calculus of Communicating Systems (CCS) [Mil89]. The motivation for this semantics is that meta-interpretive and denotational semantics of Prolog are not useful as programming calculi, as the declarative semantics of source programs is lost within their abstract mathematical domains. Our approach, on the other hand, defines the operational semantics at the language level, while at the same time maintaining the first-order declarative interpretation of the program. The CCS semantics is presented in two stages, first showing how Prolog's control mechanism is axiomatised, and then showing how dataflow is handled. Program clauses and predicates have corresponding AND and OR agents derived for them, which are defined as CCS agent expressions. Two algebraic operators define the main control characteristics in Prolog, namely clause sequencing and goal backtracking. We derive some algebraic properties of Prolog control using the CCS formalism. This semantics should prove useful as a calculus for logic program analysis.

[Search These Pages] [DAI Home Page] [Comment]