The coneptual distinction between logic and control is an important tenet of logic programing. In practice, however, logic program languages use control strategies which profoundly affect the computational behavior of programs. For example, sequential Prolog's depth-first-left-first control is an unfair strategy under which nontermination can easily arise if programs are ill-structured. Formal analyses of logic programs therefore require an explicit formalisation of the control scheme. To this ends, this research introduces an algebraic proccess semantics of sequential logic programs written in Milner's calculus of Communicating Systems (CCS). the main contribution of this semantics is that the control component of a logic programming language is conciesly modelled. Goals and clauses of logic programs correspond semantically to sequential AND and OR agents respectively, and these agents are suitably defined to reflect the control strategy used to traverse the AND/OR computation tree for the program. The main difference between this and other process semantics which model concurrency is that the processes used here are sequential. The primary control strategy studied is standard Prolog's left-first-depth-first control. CCS is descriptively robust, however, and a variety of other sequential control schemes are modelled, including breadth-first, predicate freezing, and nondeterministic strategies. The CCS semantics for a particular control scheme is typically defined hierarchically. For example, standard Prolog control is initially defined in basic CCS using two control operators which model goal backtracking and clause sequencing. Using these basic definitions, higher-level bisimilarities are derived, ehich are more closely mappable to Prolog program constructs. By using variuos algebraic properties of the control operators, as well as the stream domain and theory of observational equivalence from CCS, a programming calculus approach to logic program analysis is permitted. Some example applications using the semantics include proving program termination, verifying transformations which use cut, and characterising some control issues of partial evaluation. Since progress algebras have already been used to model concurrency, this thesis suggests that they are an ideal means for unifying the operational semantics of the sequential and concurrent paradigms of logic programming.
| Identifer | oai:union.ndltd.org:bl.uk/oai:ethos.bl.uk:561622 |
| Date | January 1992 |
| Creators | Ross, Brian James |
| Contributors | Smaill, Alan |
| Publisher | University of Edinburgh |
| Source Sets | Ethos UK |
| Detected Language | English |
| Type | Electronic Thesis or Dissertation |
| Source | http://hdl.handle.net/1842/585 |
Page generated in 0.0019 seconds