2

我正在阅读一篇论文“Termination of term rewriting using dependency pairs”（Thomas Arts，Jurgen Giesl）。在示例中：

minus (x,0) -> x
minus (s(x), s(y)) -> minus (x,y)
quot (0, s(y)) -> 0
quote (s(x), s(y)) -> s (quot (minus (x, y), s(y)))

它说： ”However, the TRS above is not compatible with a simplification ordering, because the left-hand side of the last quot-rule is embedded in its right-hand side if y is instantiated with s (x). Therefore these techniques cannot prove termination of this TRS"

我不明白“ if y is instantiated with s (x)”。如果可能的话，你能帮我理解吗？PS：如果这边不是问这种问题的地方，请你帮我知道我在哪里可以问？非常感谢您的帮助

4

2 回答 2

0

对我来说听起来也有点奇怪，但是，如果我是你，我会直接联系 J. Giesl 在他的网站上进行澄清。verify.rwth-aachen.de/giesl
你的文章有任何联系信息吗？

于 2012-05-16T05:22:47.637 回答
0

我是 Jürgen Giesl 小组的博士生，让我们看看 :)

考虑一下您使用 term “到达”此规则的情况quot(s(x), s(s(x))。这正是“如果 y 用 s(x) 实例化”这句话的意思。

然后可以应用规则，给出s(quot(minus(x, s(x)), s(s(x)))). 如您所见，原始术语嵌入在结果术语中（阅读：仅考虑子术语可以产生原始术语）。在这种情况下，不能使用简化顺序来证明终止（但依赖对有帮助）。

供将来参考：我们很乐意回答此类问题，请不要犹豫直接与我们联系！

于 2012-10-17T15:39:14.627 回答