星游戏与九头蛇
Star Games and Hydras
AI总结：
本文通过引入星游戏简化递归路径排序的表述，并直接证明了九头蛇战役的终止性，同时提供了量化版本及未来研究方向。
摘要：
递归路径排序是项重写中用于证明终止性的一个成熟且关键的工具。我们通过一些简单的规则重新审视其表述，这些规则作用于带有“星”作为控制符号的树（或相应的项），表示使该树（或项）在所定义的序中变小的命令。这导致了星游戏，对于证明许多重写任务的终止性非常方便。例如，仅使用有限无标号树上最简单的星游戏，我们就获得了著名的九头蛇战役终止性的非常直接的证明，直接性体现在无需通常提及序数。我们还包含了建立星游戏的另一条途径，使用Buchholz的证明方法，经van Oostrom改编，产生了星作为控制符号的量化版本。最后，我们提出了一些问题和未来的研究方向。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
