「循環必須摺疊以確保終止」是什麼意思？

Question

在一篇關於形式化方法（抽象解釋是精確的）的論文中，我遇到了「循環必須摺疊以終止終止」。我很清楚終止是什麼意思，但我不知道摺疊循環是什麼，也不知道如何在循環中執行摺疊。

請問有人請向我解釋一下什麼是摺疊的循環？如果它沒有隱含在摺疊循環的定義中，或者沒有立即遵循，如何確保終止？

感謝

Answer 1

我沒有抽象解釋的知識，所以我會好好函數式編程的方法來摺疊。 :-)

在函數式編程中，fold是應用於列表的操作，用於對每個元素執行某些操作，每次迭代更新一次值。例如，可以實現map這種方式（方案）：

(define (map1 func lst) 
    (fold-right (lambda (elem result) 
       (cons (func elem) result)) 
       '() lst)) 

什麼，做的是，它與空列表開始（我們稱之爲的結果），然後在列表中的每個元素，從右側向左移動，您將元素上的func和cons的結果調用到結果列表上。

就終止而言，關鍵在於，只要列表是有限的，就保證循環終止，因爲每次迭代到列表中的下一個元素，並且如果列表是有限的，那麼最終不會有下一個元素。

將此與C風格的for循環進行對比，該循環不在列表中操作，而是以for (init; test; update)的形式運行。 test不保證永遠返回false，因此循環不能保證完成。

Answer 2

摺疊的環是從較知名環展開，其本身更好地稱爲loop unrolling相反的動作。給定一個循環，展開它意味着重複幾次，這樣循環測試執行的次數就減少了。當預先執行循環的次數時，循環可以完全展開，留下簡單的指令序列。例如，這個循環

for i := 1 to 4 do 
    writeln(i); 

可以展開到

writeln(1); 
writeln(2); 
writeln(3); 
writeln(4); 

參見C++ loop unfolding, bounds用於與部分解摺疊的另一個例子。

這個比喻是，程序被摺疊了很多次，展開意味着去除部分或全部這些褶皺。

在一些靜態分析技術中，很難處理循環，因爲找到循環入口點的前提條件（即找到循環不變量）需要通常不能解決的定點計算。因此一些分析展開了循環;這要求對迭代次數有合理的限制，這限制了可以分析的程序的範圍。

在其他靜態分析技術中，找到一個好的不變量是分析的關鍵部分。這對展開循環沒有幫助，實際上部分展開循環會使循環體更大，因此會更難確定好的不變量;並且如果迭代次數很大或無限，完全展開循環將是不切實際的或不可能的。沒有看到這篇論文，我覺得這個說法有點令人驚訝，因爲代碼可能是用展開的表單編寫的，但是可以有一些程序只能以更摺疊的形式進行分析。