We show that for every term graph in a left-linear but non-orthogonal term graph rewrite system, one can construct an event structure that represents all the possible reductions that can occur in reduction sequences starting from that term graph. Every finite reduction sequence from that graph corresponds to a configuration of the event structure, and Lévy-equivalent sequences correspond to the same configuration.Garbage collection is modelled in the event structure by an ‘erases’ relation. The asymmetric conflicts that arise in non-orthogonal rewrite systems are modelled by introducing a ‘prevents’ relation. The configurations of the event structure then form the state space of an event automaton. Taking the directed completion of this space yields a prime algebraic domain.
Event structures and non-orthogonal term graph rewriting
