From nominal to higher-order rewriting and back again
Jes\'us Dom\'inguez (King's College London), Maribel Fern\'andez, (King's College London)

TL;DR
This paper introduces bidirectional translation methods between nominal rewriting systems and combinatory reduction systems, enabling transfer of properties like termination between these formalisms.
Contribution
It provides a novel, reduction-preserving translation from NRSs to CRSs and an improved translation from CRSs to NRSs, facilitating interoperability.
Findings
Translation preserves rewriting relations.
Enables transfer of properties like termination.
Improves upon previous translation methods.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
