Axiomatic Rewriting Systems

Melliès pursues his work on abstract rewriting systems which are an axiomatic presentation of rewriting systems with bound variables. This year he obtained a factorisation theorem in the sense of Freyd & Kelly. The theorem means that the efficient part of a computation can always be separated from its useless part modulo redex permutations, and that this separation is categorically functorial. This work was presented at the Confer workshop in Bologna and at the CTCS `97 conference in Santa Margherita.

Subsequently, Melliès has obtained a stability result in the sense of Berry expressing the existence of a cone $(e_i:M\to V_i)_{i\in I}$ of minimal computations from any term M to the set of its values V_i. The result whose proof relies heavily on the factorisation theorem is verified by any axiomatic rewriting system. In the lambda-calculus, it extends the result by Wadsworth that the head-reduction is the minimal reduction path from a lambda-term to its head-normal form. In the call-by-value lambda-calculus, the cone $(e_i:M\to V_i)_{i\in I}$ contains at most a singleton which describes the strategy of Landin SECD machine. In the lambda-sigma calculus, the existence of a cone and its finiteness implies the completeness of various weak strategies and the corresponding abstract machines. A paper containing these results has been submitted to LiCS `98.

[[M97]] P.-A. Melliès, A factorisation theorem in Rewriting Theory. Proc. of the Category Theory and Computer Science symposium (CTCS'97).