霍尔逻辑：严格递减循环变体本身如何证明终止？
参考 完全正确性的 while 规则，WP 似乎告诉我，只需找到一个循环严格减少的变体足以证明终止。我无法接受这一点，要么是因为我遗漏了某些东西，要么是规则是错误的。考虑
int i = 1000;
while(true) i--;
其中变量 i 的值是严格递减循环变体，但循环肯定不会终止。
当然，该规则需要有一个额外的前提条件，例如 i<0 → ØB （其中 B 是公理模式中的循环条件），以便循环条件最终“捕获”循环变体并退出。
或者我错过了什么？
Referring to the while rule for total correctness, WP seems to tell me that just finding a loop variant that strictly decreases is enough to prove termination. I can't accept that, either because I'm missing something or the rule is wrong. Consider
int i = 1000;
while(true) i--;
in which the value of variable i is a strictly decreasing loop variant, but the loop certainly doesn't terminate.
Surely the rule needs to have an additional precondition, something like i<0 → ¬B (where B is the loop condition in the axiom schema) so that the loop condition eventually 'catches' the loop variant and exits.
Or have I missed something?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（3）
循环变量必须是自然数。自然数不能减少到零以上。使用大词，循环变体是一个相对于有充分基础的关系单调递减的值。这是你的推理中缺少的依据。
The loop-variant must be a natural number. A natural number cannot decrease past zero. Using big words, the loop variant is a value that is monotonically decreasing with respect to a well-founded relation. It's the well-foundedness that's missing from your reasoning.
正如维基百科文章中所述：
在本例中，B 为
true，t 为i。true没有暗示i的最小性，因此不满足规则的前提。As noted in the Wikipedia article:
In the case at hand, B is
trueand t isi.truemakes no implication about the minimality ofi, so the premise of the rule is not met.通常的排序“<”在自然数上有充分根据，但在整数上则不然。为了使关系有良好的基础，其域的每个非空子集必须具有最小元素。由于可以证明，对于有充分基础的关系而言，不存在无限的下降链，因此具有变体的循环必须终止。
当然，在元素最小的情况下，循环条件必须为假！
然而，变体不必限于自然数。超限序数也是良序的。
The usual ordering "<" is well-founded on the natural numbers, but not on the integers. In order for a relation to be well-founded, every non-empty subset of its domain must have a minimal element. Since it can be shown that there is no infinite descending chain with respect to a well-founded relation, it follows that a loop with a variant must terminate.
Of course the condition of the loop must be false in the case of a minimal element!
A variant need not be restricted to the natural numbers, however. Transfinite ordinals are also well-ordered.