Jesús Domínguez ; Maribel Fernández - From nominal to higher-order rewriting and back again

lmcs:1610 - Logical Methods in Computer Science, December 14, 2015, Volume 11, Issue 4 - https://doi.org/10.2168/LMCS-11(4:9)2015
From nominal to higher-order rewriting and back againArticle

Authors: Jesús Domínguez ORCID; Maribel Fernández

    We present a translation function from nominal rewriting systems (NRSs) to combinatory reduction systems (CRSs), transforming closed nominal rules and ground nominal terms to CRSs rules and terms, respectively, while preserving the rewriting relation. We also provide a reduction-preserving translation in the other direction, from CRSs to NRSs, improving over a previously defined translation. These tools, together with existing translations between CRSs and other higher-order rewriting formalisms, open up the path for a transfer of results between higher-order and nominal rewriting. In particular, techniques and properties of the rewriting relation, such as termination, can be exported from one formalism to the other.

    https://doi.org/10.2168/LMCS-11(4:9)2015
    Source: arXiv.org:1509.05318
    Volume: Volume 11, Issue 4
    Published on: December 14, 2015
    Submitted on: November 5, 2014
    Keywords: Computer Science - Logic in Computer Science
    Licence: arXiv.org - Non-exclusive license to distribute

    Classifications

    Mathematics Subject Classification 20201
    Sources:
    • [1] zbMATH Open.

    1 Document citing this article

    Share and export

    Consultation statistics

    This page has been seen 1354 times.
    This article's PDF has been downloaded 372 times.