循環變體

在計算機科學中，循環變體是在計算機程序的狀態空間上定義的一個數學函數，其值在某些不變的條件下，通過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時，狀態必須嚴格減少--作為一個繼承者和一個迭代者。此外，我們可以通過一個計數論證表明，任何變體的存在都意味著存在一個