论文标题
星际游戏和九头蛇
Star Games and Hydras
论文作者
论文摘要
递归路径排序是在术语重写以证明终止方面已建立的至关重要的工具。我们通过在树（或相应的术语）上的一些简单规则（或配备了“星形”作为控制符号）的一些简单规则来重新审视其演示文稿，这表示命令在定义的顺序中使该树（或术语）较小。这导致明星游戏非常方便地证明终止许多重写任务。例如，在有限的未标记树上使用最简单的明星游戏，我们可以直接获得著名的Hydra Battle的终止证明，这是直接的，因为没有通常提到序数。我们还提供了使用Buchholz的证明方法（由Van Oostrom改编）来设置Star Games的替代道路，从而将Star的定量版本作为控制符号。我们以许多问题和未来的研究方向结束。
The recursive path ordering is an established and crucial tool in term rewriting to prove termination. We revisit its presentation by means of some simple rules on trees (or corresponding terms) equipped with a 'star' as control symbol, signifying a command to make that tree (or term) smaller in the order being defined. This leads to star games that are very convenient for proving termination of many rewriting tasks. For instance, using already the simplest star game on finite unlabeled trees, we obtain a very direct proof of termination of the famous Hydra battle, direct in the sense that there is not the usual mention of ordinals. We also include an alternative road to setting up the star games, using a proof method of Buchholz, adapted by van Oostrom, resulting in a quantitative version of the star as control symbol. We conclude with a number of questions and future research directions.
