## Paper: A Stability Theorem in Rewriting Theory (at LICS 1998)

**Paul-André Melliès**

### Abstract

One key property of the λ-calculus is that there exists a
minimal computation (the head-reduction) M→^{e}V from a
λ-term M to the set of its head-normal forms. Minimality here
means categorical “reflectivity” i.e. that every reduction
path M→^{f}W to a head-normal form W factors (up to redex
permutation) to a path M→^{e}V→^{h}W. This
paper establishes a stability a la Berry or poly-reflectivity theorem
[D, La, T] which extends the minimality property to rewriting systems
with critical pairs. The theorem is proved in the setting of axiomatic
rewriting systems where sets of head-normal forms are characterised by
their frontier property in the spirit of J. Glauert and Z. Khasidashvili
(1996)

### BibTeX

@InProceedings{Mellis-AStabilityTheoremin, author = {Paul-André Melliès}, title = {A Stability Theorem in Rewriting Theory}, booktitle = {Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1998)}, year = {1998}, month = {June}, pages = {287--298}, location = {Indianapolis, IN, USA}, publisher = {IEEE Computer Society Press} }