Division of Informatics
Forrest Hill & 80 South Bridge
Research Paper #510 | |
|---|---|
| Title: | An Algebraic Semantics of Prolog Program Termination |
| Authors: | Ross,B; Smaill,AD |
| Date: | Oct 1990 |
| Presented: | A shorter version of this paper was submitted to ICLP'91 |
| Keywords: | |
| Abstract: | Formal proofs of termination properties of Prolog programs with cut are presented which make use of an algebraic process semantics of Prolog. The algebraic semantics is written in Milner's CCS. This semantics treats Prolog program components as processes which generate streams of answer substitutions. Such characterisation of logic program computation is ideal for termination proofs because phenomena such as termination, infinite answer generation, and looping are easily modelled as streams. In addition, simple inductive proofs over streams or the structure of argument terms are readily supported. This paper suggests that the process algebra approach is a promising formalism for the semantics of different computational paradigms, since sequential as well as concurrent logic program execution is axiomatisable within it. |
| Download: | NO ONLINE COPY |
![[Search These Pages]](http://www.dai.ed.ac.uk/icons/dai_search.gif){kind=icon}
![[DAI Home Page]](http://www.dai.ed.ac.uk/icons/dai_home.gif){kind=icon}
![[Comment]](http://www.dai.ed.ac.uk/icons/dai_comment.gif){kind=icon}