[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #2

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 = t1R t2R ⋯ ≤ t = t1R t2R ⋯ if for all i there is a j such that tiR* tj. 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]).


Gérard Berry and Jean-Jacques Lévy. Mimimal and optimal computations of recursive programs. J. of the Association for Computing Machinery, 26:148–175, 1979.
Jan Willem Klop. Combinatory Reduction Systems, volume 127 of Mathematical Centre Tracts. Mathematisch Centrum, Amsterdam, 1980.
Jan Willem Klop. Term rewriting systems. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, chapter 1, pages 1–117. Oxford University Press, Oxford, 1992.
M. Venturini-Zilli. Reduction graphs in the Lambda Calculus. Theoretical Computer Science, 29:251–275, 1984.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]