循环变体

在计算机科学中，循环变体是在计算机程序的状态空间上定义的一个数学函数，其值在某些不变的条件下，通过while循环的迭代，相对于一个（严格的）有根据的关系单调地减少，从而确保其终止。一个范围被限制在非负整数的循环变体也被称为边界函数，因为在这种情况下，它为循环终止前的迭代次数提供了一个微不足道的上限。然而，一个循环变体可能是无限的，因此不一定限制在整数值上。一个基础良好的关系的特征是其域的每一个非空子集的最小元素的存在。变体的存在证明了计算机程序中的while循环的终止是有根有据的下降。一个有根有据的关系的基本属性是它没有无限的下降链。因此，一个拥有变体的循环将在有限次数的迭代后终止，只要它的主体每次都能终止。一个while循环，或者更一般的，一个可能包含while循环的计算机程序，如果它是部分正确的，并且它终止了，就可以说是完全正确的。

为了正式说明我们在上面展示的关于while循环终止的推理规则，请回忆一下，在Floyd-Hoare逻辑中，表达while循环部分正确性的规则是。其中，V是变体，按照惯例，非绑定符号z被认为是普遍量化的。每个终止的循环都有一个变体变体的存在意味着一个while循环的终止。这似乎令人惊讶，但反过来也是真的，只要我们假设选择公理：每个终止的while循环（给定其不变式）都有一个变体。为了证明这一点，假设循环循环考虑状态空间Σ上的继任关系，该关系是由从满足不变量I和条件C的状态执行语句S所引起的。I和C在状态σ中都为真，并且σ′是在状态σ中执行语句S后产生的状态。因为不然的话，这个循环就无法终止了。接下来考虑继任关系的反射性、传递性闭合。我们称之为迭代：我们说一个状态σ′是σ的一个迭代，如果不是{displaystyle0leqi<n.}。我们注意到，如果σ和σ′是两个不同的状态，并且σ′是σ的迭代，那么σ不可能是σ′的迭代，因为同样，否则循环将无法终止。

换句话说，迭代是反对称的，因此是一个部分顺序。现在，由于while循环在给定不变式I的有限步数后终止，并且除非I在该状态下为真，否则任何状态都没有后继者，我们得出结论，每个状态只有有限个迭代，每个关于迭代的下降链只有有限个不同的值，因此不存在无限的下降链，也就是说，循环迭代满足下降链条件。因此--假设选择公理--我们最初为循环定义的继任关系在状态空间Σ上是成立的，因为它是严格的（非反射的）并且包含在迭代关系中。因此，这个状态空间上的身份函数是while循环的一个变体，因为我们已经表明，在给定不变式I和条件C的情况下，每次执行主体S时，状态必须严格减少--作为一个继承者和一个迭代者。此外，我们可以通过一个计数论证表明，任何变体的存在都意味着存在一个