Productivity of non-orthogonal term rewrite systems

M. Raffelsieper

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

    1 Citation (Scopus)

    Abstract

    Productivity is the property that finite prefixes of an infinite constructor term can be computed using a given term rewrite system. Hitherto, productivity has only been considered for orthogonal systems, where non-determinism is not allowed. This paper presents techniques to also prove productivity of non-orthogonal term rewrite systems. For such systems, it is desired that one does not have to guess the reduction steps to perform, instead any outermost-fair reduction should compute an infinite constructor term in the limit. As a main result, it is shown that for possibly non-orthogonal term rewrite systems this kind of productivity can be concluded from context-sensitive termination. This result can be applied to prove stabilization of digital circuits, as will be illustrated by means of an example.
    Original languageEnglish
    Title of host publicationProceedings 10th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2011, Novi Sad, Serbia, May 29, 2011)
    EditorsS. Escobar
    PublisherEPTCS
    Pages53-67
    DOIs
    Publication statusPublished - 2012

    Publication series

    NameElectronic Proceedings in Theoretical Computer Science
    Volume82
    ISSN (Print)2075-2180

    Fingerprint Dive into the research topics of 'Productivity of non-orthogonal term rewrite systems'. Together they form a unique fingerprint.

    Cite this