关于变窄树到生成置换范围的正则树文法的转化
On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions
摘要：
一个语法确定性条件项重写系统和一对项的缩小树的语法表示是一个正则树语法，它生成由所有可能的最内缩小推导获得的替换表达式，这些推导以该对项开始，以特定的非缩小项结束。在本文中，在一定的句法条件下，我们展示了一个转换的语法表示的缩小树到另一个正规树文法，过近似生成的范围内的地面替代所产生的语法表示。在我们以前的工作中，这样的变换仅限于w.r.t.给定的单一变量，因此，有用性是有限的。我们扩展了以前的变换表示的范围作为一个元组的条件，这是通过有限树的编码。我们展示了一个精确的定义的转换，并证明了语言的转换定期树文法是一个overapproximation的范围内产生的地面置换的语法表示。我们留下一个实验来评估转换的有用性作为未来的工作。
英文摘要：
The grammar representation of a narrowing tree for a syntactically deterministic conditional term rewriting system and a pair of terms is a regular tree grammar that generates expressions for substitutions obtained by all possible innermost-narrowing derivations that start with the pair and end with particular non-narrowable terms. In this paper, under a certain syntactic condition, we show a transformation of the grammar representation of a narrowing tree into another regular tree grammar that overapproximately generates the ranges of ground substitutions generated by the grammar representation. In our previous work, such a transformation is restricted to the ranges w.r.t. a given single variable, and thus, the usefulness is limited. We extend the previous transformation by representing the range of a ground substitution as a tuple of terms, which is obtained by the coding for finite trees. We show a precise definition of the transformation and prove that the language of the transformed regular tree grammar is an overapproximation of the ranges of ground substitutions generated by the grammar representation. We leave an experiment to evaluate the usefulness of the transformation as future work.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
