A factorisation theorem in rewriting theory

Abstract

Some computations on a symbolic term M are more judicious than others, for instance the leftmost outermost derivations in the λ-calculus. In order to characterise generically that kind of judicious computations, [M] introduces the notion of external derivations in its axiomatic description of Rewriting Systems: a derivation e : M → P is said to be external when the derivation e; f : M → Q is standard whenever the derivation f : P → Q is standard.

In this article, we show that in every Axiomatic Rewriting System [M,1] every derivation d : M → Q can be factorised as an external derivation e : M → P followed by an internal derivation m : P → Q. Moreover, this epi-mono factorisation is functorial (i.e there is a nice diagram) in the sense of Freyd and Kelly [FK].

Conceptually, the factorisation property means that the efficient part of a computation can always be separated from its junk. Technically, the property is the key step towards our illuminating interpretation of Berry's stability (semantics) as a syntactic phenomenon (rewriting). In fact, contrary to the usual Lévy derivation spaces, the external derivation spaces enjoy meets.