Title
From nominal to higher-order rewriting and back again.
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.
Year
DOI
Venue
2015
10.2168/LMCS-11(4:9)2015
LOGICAL METHODS IN COMPUTER SCIENCE
Keywords
Field
DocType
rewriting,nominal syntax,Combinatory Reduction Systems,higher-order syntax,translation tool
Discrete mathematics,Nominal terms,Confluence,Rewriting,Formalism (philosophy),Rotation formalisms in three dimensions,Mathematics
Journal
Volume
Issue
ISSN
11
4
1860-5974
Citations 
PageRank 
References 
0
0.34
13
Authors
2
Name
Order
Citations
PageRank
Jesús Domínguez121.41
Maribel Fernández231523.44