\documentclass{rtaloop}
\rtalabel{spectrum}

\begin{document}
\begin{problem}{M. Venturini-Zilli}{\cite{V84:tcs}}{April 1991}

\begin{abstract}
Investigate the properties of \emph{spectri} for special classes of rewrite
systems. 
\end{abstract}

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 = t_1 \rightarrow_R t_2
\rightarrow_R \cdots \leq t = t'_1 \rightarrow_R t'_2 \rightarrow_R \cdots$ if
for all $i$ there is a $j$ such that $t_i \rightarrow_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\'evy (see \cite{BL79:jacm}\cite{K80:mct}\cite{K92:ox}).

\end{problem}
\end{document}