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 도와주세요 수 :.?이 쪽이 아닌 경우 이런 종류의 질문을하는 장소, 내가 물을 수있는 곳을 알 수 있도록 도와 주시겠습니까? 당신의 도움을 위해 대단히 감사합니다.