Paper Info
Title
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.
Year
DOI
Venue
1997
10.1007/BFb0026981
Category Theory and Computer Science
Keywords
Field
DocType
factorisation theorem,rewriting theory
Discrete mathematics,Lambda calculus,Axiomatic system,Axiom,Rewriting,Category theory,Factorization,Mathematics,Computation
Conference
ISBN
Citations 
PageRank 
3-540-63455-X
8
0.67
References 
Authors
5
1
Name
Order
Citations
PageRank
Paul-andré Melliès139230.70