Termination of logic programs via labelled term rewrite systems
Thjj Thomas Arts, Hans Zantema · 1994
We propose proving left-termination of well-moded logic programs by transforming them into term rewrite systems (TRSs). We introduce the new notions single-redex reduction, a reduction in which exactly one redex occurs in each term, and single-redex normalising, normalising with respect to the single-redex reduction. We describe a transformation of wellmoded logic programs into TRSs for which termination of the logic program follows from single-redex normalisation of the TRS, which is far stronger than previous results, since termination, innermost normalisation etc., all imply single-redex normalisation. A powerful tool for proving termination of TRSs that are obtained by the proposed transformation is semantic labelling. We use it for proving termination of implementations of quick-sort and generation of permutations. 1. Introduction A proof of the correctness of a program normally consists of a proof that the program meets the specification (often called `partial correctn...