** Next:** Sequentiality
**Up:** Foundational models and abstract
** Previous:** Optimal reductions in the

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 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
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).