loops - “必须折叠循环以确保终止”是什么意思？

Question

我在一篇关于形式方法的论文中遇到了“必须折叠循环以确保终止”（准确地说是抽象解释）。我很清楚终止的含义，但我不知道折叠循环是什么，也不知道如何在循环上执行折叠。

有人可以向我解释一下折叠环是什么吗？如果它不是隐含在折叠循环的定义中，或者没有立即遵循，这如何确保终止？

谢谢

Answer 1

折叠一个循环是与众所周知的循环展开相反的动作，它本身就是众所周知的循环展开。给定一个循环，展开它意味着多次重复主体，从而减少执行循环测试的频率。当循环的执行次数提前，循环可以完全展开，留下简单的指令序列。例如，这个循环

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

可以展开到

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

有关部分展开的另一个示例，请参见C++ 循环展开、边界。

比喻是程序被多次折叠。展开意味着去除部分或全部这些褶皱。

在一些静态分析技术中，很难处理循环，因为找到循环入口点的前提条件（即找到循环不变量）需要进行固定点计算，这通常是无法解决的。因此，一些分析展开了循环；这需要对迭代次数有一个合理的限制，这限制了可以分析的程序范围。

在其他静态分析技术中，找到一个好的不变量是分析的关键部分。展开循环无济于事，事实上，部分展开循环会使循环体变大，因此更难确定一个好的不变量；如果迭代次数很大或没有限制，完全展开循环将是不切实际或不可能的。没有看到论文，我觉得这个陈述有点令人惊讶，因为代码可以用展开的形式编写，但是可能有一些程序只能以更折叠的形式进行分析。

Answer 2

我对抽象解释一无所知，所以我将采用函数式编程方法进行折叠。:-)

在函数式编程中，折叠是应用于列表的操作，用于对每个元素执行某些操作，每次迭代更新一个值。例如，您可以map这样实现（在 Scheme 中）：

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

它的作用是它从一个空列表开始（我们称之为结果），然后对于列表的每个元素，从右侧向左移动，调用func元素cons及其结果到结果列表.

就终止而言，这里的关键是折叠，只要列表是有限的，循环就保证终止，因为您每次都迭代到列表的下一个元素，如果列表是有限，那么最终将没有下一个元素。

将此与更 C 风格的for循环进行对比，该循环不在列表上操作，而是具有for (init; test; update). test不能保证永远返回 false，因此不能保证循环完成。