Понять о прекращении

Question

Я читаю статью «Прекращение перезаписи терминов с использованием пар зависимостей» (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:.?, Если эта сторона не место, чтобы задать этот вопрос, не могли бы вы помочь мне узнать, где я могу спросить? Большое спасибо за вашу помощь

Answer 1

Я аспирант в группе Юргена Giesl, так что давайте посмотрим :)

Рассмотрим случай, когда вы «прибыть» в это правило с термином quot(s(x), s(s(x)). Это именно то, что означает предложение «если y isantantiated с s (x)».

Тогда правило может быть применено, давая s(quot(minus(x, s(x)), s(s(x)))). Как вы можете видеть, исходный термин встроен в результирующий термин (читай: только учитывая подтермы, можно дать исходный термин). Всякий раз, когда это так, порядок доказательства упрощения не может быть использован для подтверждения завершения (но помощь по паре зависимостей).

Для справок в будущем: Мы будем рады ответить на такие вопросы, не стесняйтесь обращаться к нам напрямую!

Answer 2

Звучит немного странно для меня, однако, если бы я был вами, я бы связался с J. Giesl прямо для уточнения на своем сайте. verify.rwth-aachen.de/giesl
Есть ли у вашей записи какие-либо контактные данные?