无圈项图的Kruskal树定理
Kruskal's Tree Theorem for Acyclic Term Graphs
摘要：
在本文中，我们研究的终止项图重写，我们限制我们的注意力非循环项图。出于先前的工作丰满，我们的目标是在定义的概念，简化顺序的非循环项图。为此，我们适应同胚嵌入关系的长期图。与早期的扩展相比，我们的概念受到态射的启发。在此基础上，我们建立了非循环项图的Kruskal树定理的一个变体。在证明中，我们依赖于嵌入的新概念，并遵循纳什-威廉姆斯的最小坏序列论证。最后，我们提出了一个变种的字典路径顺序的非循环项图。
英文摘要：
In this paper we study termination of term graph rewriting, where we restrict our attention to acyclic term graphs. Motivated by earlier work by Plump we aim at a definition of the notion of simplification order for acyclic term graphs. For this we adapt the homeomorphic embedding relation to term graphs. In contrast to earlier extensions, our notion is inspired by morphisms. Based on this, we establish a variant of Kruskal's Tree Theorem formulated for acyclic term graphs. In proof, we rely on the new notion of embedding and follow Nash-Williams' minimal bad sequence argument. Finally, we propose a variant of the lexicographic path order for acyclic term graphs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
