MONSTR V - Transitive Coercing Semantics and the Church-Rosser Property
Richard Banach · Zenodo (CERN European Organization for Nuclear Research) · 2020
Abstract: The transitive coercing semantic model for the execution of the MONSTR generalised term graph rewriting language is defined. Of all the operational semantics for MONSTR that one might consider, this one has the cleanest properties. Under intuitively obvious conditions for executions involving redexes permitted to overlap sufficiently to allow the programming of deterministic synchronisations, and despite the failure of exact subcommutativity, a Church-Rosser theorem is proved to hold up to markings and garbage. 1