Some Properties of Non-Orthogonal Term Graph Rewriting

AbstractThis paper examines left-linear non-orthogonal term graph rewriting systems that allow asymmetric conflicts between redexes. Using a definition of compatibility of sequences based on Boudol's work on the semantics of term rewriting, it shows that two properties associated with functional languages are true of such graph rewriting systems. First, that a notion of standard computation can be defined and that an associated standardisation theorem can be proved. Second, that a set of events can be associated with a reduction sequence and hence event structures modelling all the possible reduction sequences from a given initial graph can be constructed