Huet and Levy showed 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 Levy introduced the subclass of strongly sequential TRSs and showed that strong sequentiality is a decidable property of orthogonal TRSs. Several authors proposed decidable extensions of the class of strongly sequential TRSs. Since Comon's and Jacquemard's work, all the corresponding decidability proofs have been expressed using tree automata techniques: typically a property is satisfied if and only if some associated automaton recognizes the empty language. A uniform framework for the study of sequentiality is described in [3] where classes of TRSs are parameterized by approximation mappings. Nowdays the best known approximation for which sequentiality is decidable is the growing approximation studied in [10]. We assume that the reader is familiar with the basics of term rewriting. Familiarity with the theory of sequentiality is helpmf. Autowrite is an experimental tool written in Common Lisp for checking properties of TRSs. It was initially designed to check sequentiality properties of TRSs. For this purpose, it implements the tree automata constructions used in [7,3,4, 10] and many useful operations on terms, TRSs and tree automata (unfortu-naletly not all yet integrated into the graphical interface). A graphical interface (still under construction) is written using FreeCLIM, the free implementation of the CLIM specification. Using this interface, one can check sequentiality of the different approximations of a given system. Many other functionalities are available directly from the Common Lisp interactive environment and could easily be integrated into the graphical interface. The Autowrite tool was used to check sequentiality for most of the examples presented in [5].
展开▼
机译：Huet和Levy表明，对于一类正交项重写系统（TRS），每个非常规形式的项都包含所需的redex（即，在每个规范化重写序列中都收缩的redex），并且反复收缩所需的redex会生成常规形式如果存在。但是，需求通常是不确定的。为了获得对需求的可确定的近似值，Huet和Levy引入了强顺序TRS的子类，并表明强顺序是正交TRS的可确定的性质。几位作者提出了强序TRS类的可确定扩展。自从Comon和Jacquemard开展工作以来，所有相应的可判定性证明都是使用树自动机技术表达的：通常，当且仅当某些关联的自动机识别出空语言时，才满足属性。在[3]中描述了一个统一的顺序研究框架，其中TRS的类通过近似映射进行参数化。如今，可确定连续性的最著名的近似是[10]中研究的增长近似。我们假设读者熟悉术语重写的基础。熟悉顺序理论是helpmf。自动写入是一种用Common Lisp编写的实验工具，用于检查TRS的属性。它最初旨在检查TRS的顺序属性。为此，它实现了[7,3,4,10]中使用的树自动机构造以及术语，TRS和树自动机（不幸的是，尚未全部集成到图形界面中）的许多有用操作。图形界面（仍在构建中）是使用FreeCLIM（CLIM规范的免费实现）编写的。使用此接口，可以检查给定系统的不同近似值的顺序。 Common Lisp交互环境直接提供了许多其他功能，并且可以轻松地集成到图形界面中。 [5]中介绍的大多数示例都使用自动写入工具来检查顺序。
展开▼
