×

Autowrite: A tool for checking properties of term rewriting systems. (English) Zbl 1045.68579

Tison, Sophie (ed.), Rewriting techniques and applications. 13th international conference, RTA 2002, Copenhagen, Denmark, July 22–24, 2002. Proceedings. Berlin: Springer (ISBN 3-540-43916-1). Lect. Notes Comput. Sci. 2378, 371-375 (2002).
Summary: Huet and Lévy have shown that for the class of orthogonal term rewriting systems (TRSs) every term not in normal form contains a needed redex (i.e., a redex contracted in every normalizing rewrite sequence) and that repeated contraction of needed redexes results in a normal form if it exists. However, neededness is in general undecidable. In order to obtain a decidable approximation to neededness Huet and Lévy introduced the subclass of strongly sequential TRSs and showed that strong sequentiality is a decidable property of orthogonal TRSs.
For the entire collection see [Zbl 0992.00043].

MSC:

68Q42 Grammars and rewriting systems

Software:

Autowrite
PDFBibTeX XMLCite
Full Text: Link