2

「依存関係ペアを使用した項書き換えの終了」(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ürgen Giesl のグループの博士課程の学生なので、見てみましょう :)

このルールに項 で「到達」した場合を考えてみましょうquot(s(x), s(s(x))。これはまさに「y が s(x) でインスタンス化されている場合」という文が意味することです。

次に、ルールを適用して、 を与えることができますs(quot(minus(x, s(x)), s(s(x))))。ご覧のとおり、元の項は結果の項に埋め込まれています (サブ項のみを考慮することで、元の項を生成できます)。この場合はいつでも、単純化順序を使用して終了を証明することはできません (ただし、依存関係ペアが役立ちます)。

今後の参考のために: このような質問には喜んでお答えします。お気軽に直接お問い合わせください。

于 2012-10-17T15:39:14.627 に答える
0

私にとっても少し奇妙に聞こえますが、もし私があなたなら、J.ギーゼルに直接連絡して、彼のウェブサイトで説明を求めます。verify.rwth-aachen.de/giesl
あなたの報告書には何らかの連絡先情報がありますか?

于 2012-05-16T05:22:47.637 に答える