PROVING TERMINATION OF GHC PROGRAMS

A transformational approach for proving termination of parallel logic programs such as GHC programs is proposed. A transformation from GHC p rograms to term rewriting systems is developed; it exploits the fact t hat unifications in GHC-resolution correspond to matchings. The termin ation of a GHC program for a class of queries is implied by the termin ation of the resulting rewrite system. This approach facilitates the a pplicability of a wide range of termination techniques developed for r ewrite systems in proving termination of GHC programs. The method cons ists 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 ma ny benchmark GHC programs such as quick-sort, merge-sort, merge, split , fair-split and append, etc., can be proved.