Proving termination of GHC programs

Krishna Rao, M. R. K. ; Kapur, D. ; Shyamasundar, R. K. (1997) Proving termination of GHC programs New Generation Computing, 15 (3). pp. 293-338. ISSN 0288-3635

Full text not available from this repository.

Official URL: http://www.springerlink.com/content/3305886g1777l8...

Related URL: http://dx.doi.org/10.1007/BF03037949

Abstract

A transformational approach for proving termination of parallel logic programs such as GHC programs is proposed. A transformation from GHC programs to term rewriting systems is developed; it exploits the fact that unifications in GHC-resolution correspond to matchings. The termination of a GHC program for a class of queries is implied by the termination of the resulting rewrite system. This approach facilitates the applicability of a wide range of termination techniques developed for rewrite systems in proving termination of GHC programs. The method consists of three steps: (a) deriving moding information from a given GHC program, (b) transforming the GHC program into a term rewriting system using the moding information, and finally (c) proving termination of the resulting rewrite system. Using this method, the termination of many benchmark GHC programs such as quick-sort, merge-sort, merge, split, fair-split and append, etc., can be proved.

Item Type:Article
Source:Copyright of this article belongs to Springer.
Keywords:Parallel Logic Programming; Verification; Termination
ID Code:56604
Deposited On:24 Aug 2011 10:58
Last Modified:24 Aug 2011 10:58

Repository Staff Only: item control page