MONSTR V - Transitive Coercing Semantics and the Church-Rosser Property

Richard Banach (Computer Science Dept., Manchester University, UK)

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 on e might consider, this one has the cleanest properties. Under intuitively obvious conditions fo r 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.