Axiomatic Rewriting Theory I - A Diagrammatic Standardization Theorem
Paul-André Melliès, Equipe Preuves, Programmes Et Systèmes, Université Paris, Denis Diderot, Dedicated Jan, Willem Klop · 2001
By extending nondeterministic transition systems with concurrency and copy mechanisms, Axiomatic Rewriting Theory provides a uniform framework for a variety of rewriting systems, ranging from higher-order systems to Petri nets and process calculi. Despite its generality, the theory is surprisingly simple, based on a mild extension of transition systems with independence: an axiomatic rewriting system is defined as a 1-dimensional transition graph equipped with 2-dimensional transitions describing the redex permutations of the system, and their orientation. In this article, we formulate a series of elementary axioms on axiomatic rewriting systems, and establish a diagrammatic standardization theorem.