Arctic termination ... below zero

A. Koprowski, J. Waldmann

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    23 Citations (Scopus)
    5 Downloads (Pure)

    Abstract

    We introduce the arctic matrix method for automatically proving termination of term rewriting. We use vectors and matrices over the arctic semi-ring: natural numbers extended with -8,with the operations "max" and "plus". This extends the matrix method for term rewriting and the arctic matrix method for string rewriting. In combination with the Dependency Pairs transformation, this allows for some conceptually simple termination proofs in cases where only much more involved proofs were known before. We further generalize to arctic numbers "below zero": integers extended with -8.This allows to treat some termination problems with symbols that require a predecessor semantics. The contents of the paper has been formally verified in the Coq proof assistant and the formalization has been contributed to the CoLoR library of certified termination techniques. This allows formal verification of termination proofs using the arctic matrix method. We also report on experiments with an implementation of this method which, compared to results from 2007, outperforms TPA (winner of the certified termination competition for term rewriting), and in the string rewriting category is as powerful as Matchbox was but now all of the proofs are certified.
    Original languageEnglish
    Title of host publicationRewriting Techniques and Applications (19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings)
    EditorsA. Voronkov
    Place of PublicationBerlin
    PublisherSpringer
    Pages202-216
    ISBN (Print)978-3-540-70588-8
    DOIs
    Publication statusPublished - 2008

    Publication series

    NameLecture Notes in Computer Science
    Volume5117
    ISSN (Print)0302-9743

    Fingerprint

    Dive into the research topics of 'Arctic termination ... below zero'. Together they form a unique fingerprint.

    Cite this