Что означает "петли должны быть сложены, чтобы обеспечить завершение"?

В статье о формальных методах (абстрактная интерпретация, если быть точным) я наткнулся на "петли должны быть свернуты до конца". Мне ясно, что означает завершение, но я не знаю, что такое свернутая петля, и как выполнять складывание на петле.

Может кто-нибудь объяснить мне, пожалуйста, что такое свернутая петля? И если это не подразумевается или не следует сразу за определением свернутого цикла, как это обеспечивает завершение?

Спасибо

Источник

2 ответа

Решение

У меня нет знаний об абстрактной интерпретации, поэтому я прибегну к подходу функционального программирования к свертыванию.:-)

В функциональном программировании сгиб - это операция, применяемая к списку, чтобы что-то делать с каждым элементом, обновляя значение на каждой итерации. Например, вы можете реализовать map таким образом (на схеме):

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

То, что это делает, - то, что это начинается с пустого списка (давайте назовем это результатом), и затем для каждого элемента списка, с правой стороны, перемещающейся влево, вы вызываете func на элементе и cons его результат на список результатов.

Ключевым моментом здесь в том, что касается завершения, является то, что при сгибе цикл гарантированно завершается до тех пор, пока список конечен, поскольку вы каждый раз переходите к следующему элементу списка, и если список конечно, тогда со временем следующего элемента не будет.

Contrast this with a more C-style for loop, that doesn't operate on a list, but instead have the form for (init; test; update), test is not guaranteed to ever return false, and so the loop is not guaranteed to complete.

Источник

Складывание цикла - это действие, противоположное более известному развертыванию цикла, которое само по себе больше известно как развертывание цикла. Для данного цикла раскрытие означает повторение тела несколько раз, чтобы тест цикла выполнялся реже. Когда количество выполнений цикла заранее, цикл можно полностью развернуть, оставив простую последовательность инструкций. Например, этот цикл

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

можно развернуть до

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

Посмотрите разворачивание цикла C++, границы для другого примера с частичным разворачиванием.

Метафора заключается в том, что программа складывается сама по себе много раз; Развертывание означает удаление некоторых или всех этих складок.

В некоторых методах статического анализа трудно иметь дело с циклами, потому что нахождение предусловия для точки входа в цикл (то есть нахождение инварианта цикла) требует вычисления с фиксированной точкой, которое вообще неразрешимо. Поэтому некоторые анализы раскрывают петли; для этого требуется разумное ограничение количества итераций, что ограничивает объем программ, которые можно анализировать.

В других методах статического анализа поиск хорошего инварианта является критической частью анализа. Это не помогает развернуть цикл, фактически частичное развертывание цикла увеличило бы тело цикла и затруднило бы определение хорошего инварианта; и полное развертывание цикла было бы непрактичным или невозможным, если бы число итераций было большим или неограниченным. Не видя статьи, я нахожу это утверждение несколько удивительным, потому что код мог бы быть написан с развернутой формой, но могут быть программы, над которыми анализ работает только в более сложенной форме.

Источник
Другие вопросы по тегам