星星游戏和九头蛇
摘要：递归路径排序是在术语重写中用于证明终止性的一种已经建立且关键的工具。我们通过对树（或相应的术语）施加带有“*”标记的简单规则来重新考虑其表达方式，“*”表示将该树（或术语）在定义的顺序中变小的命令。这导致了非常方便用于证明许多重写任务终止性的星形游戏。例如，使用已经最简单的带有有限无标签树的星形游戏，我们可以直接证明著名的Hydra战斗的终止性，这里的“直接”是指没有通常的序数提及。我们还提供了一种设置星形游戏的替代方法，使用了Buchholz的证明方法，并由van Oostrom调整，得到了星形作为控制符的定量版本。最后，我们提出了一些问题和未来的研究方向。
作者：J"org Endrullis, Jan Willem Klop, Roy Overbeek
论文ID：2001.08478
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22