| [Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
Originator: M. Venturini-Zilli [VZ84]
Date: April 1991
Summary: Investigate the properties of spectri for special classes of rewrite systems.
The reduction graph of a term is the set of its reducts structured by the reduction relation. These may be very complicated. The following notion of “spectrum” abstracts away from many inessential details of such graphs: If R is a term-rewriting system and t a term in R, let Spec(t), the “spectrum” of t, be the space of finite and infinite reduction sequences starting with t, modulo the equivalence between reduction sequences generated by the following quasi-order: t = t1 →R t2 →R ⋯ ≤ t = t′1 →R t′2 →R ⋯ if for all i there is a j such that ti →R* t′j. What are the properties of this cpo (complete partial order), in particular for orthogonal (left-linear, non-overlapping) rewrite systems? What influence does the non-erasing property have on the spectrum? (A rewrite system is “non-erasing” if both sides of each rule have exactly the same variables.) The same questions can be asked for the spectrum obtained for orthogonal systems by dividing out the finer notion of “permutation equivalence” due to J.-J. Lévy (see [BL79][Klo80][Klo92]).
| [Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |