Петлевой вариант

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

Хорошо обоснованное отношение характеризуется существованием минимального элемента в каждом непустом подмножестве его области определения. Существование варианта доказывает завершение цикла while в компьютерной программе вполне обоснованным спуском . ^[1] Основное свойство хорошо обоснованного отношения состоит в том, что оно не имеет бесконечных нисходящих цепочек . Следовательно, цикл, имеющий вариант, завершится после конечного числа итераций, пока его тело каждый раз завершается.

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

Правило вывода правильности для полной

Чтобы формально сформулировать правило вывода для завершения цикла while, которое мы продемонстрировали выше, вспомните, что в логике Флойда-Хоара правило выражения частичной корректности цикла while таково:

{\frac {\{I\land C\}\;S\;\{I\}}{\{I\}\;{\mathtt {while}}\;C\;{\mathtt {do}}\;S\;\{I\land \lnot C\}}},

где $I$ — инвариант , C — условие , а S — тело цикла. Чтобы выразить полную правильность, мы пишем вместо этого:

{\frac {<{\text{ is well-founded}},\;[I\land C\land V=z]\;S\;[I\land V<z]}{[I]\;{\mathtt {while}}\;C\;{\mathtt {do}}\;S\;[I\land \lnot C]}},

где, кроме того, V — это вариант , и по соглашению несвязанный символ z считается универсальным .

У каждого завершающегося цикла есть вариант [ править ]

Существование варианта подразумевает, что цикл while завершается. Это может показаться удивительным, но верно и обратное, если мы принимаем аксиому выбора : каждый цикл while, который завершается (с учетом его инварианта), имеет вариант. Чтобы доказать это, предположим, что цикл

{\mathtt {while}}\;C\;{\mathtt {do}}\;S

завершается с учетом инварианта $I$ , где мы имеем утверждение полной корректности

[I\land C]\;S\;[I].

Рассмотрим отношение «преемник» в пространстве состояний $Σ,$ индуцированное выполнением оператора S из состояния, удовлетворяющего как инварианту $I$ , так и условию C . То есть мы говорим, что состояние $σ'$ является «преемником» $σ$ тогда и только тогда, когда

$I$ и C оба верны в состоянии $σ$ и
$σ’$ — это состояние, возникающее в результате выполнения оператора S в состоянии $σ$ .

Мы отмечаем, что $\sigma '\neq \sigma ,$ иначе цикл не сможет завершиться.

Далее рассмотрим рефлексивное, транзитивное замыкание отношения «наследник». Назовем эту итерацию : мы говорим, что состояние $σ'$ является итерацией σ $,$ если либо $\sigma '=\sigma ,$ или существует конечная цепочка $\sigma _{0},\sigma _{1},\,\dots \,,\sigma _{n}$ такой, что $\sigma _{0}=\sigma ,$ $\sigma _{n}=\sigma '$ и $\sigma _{i+1}$ является «преемником» $\sigma _{i};$ за все $я$ , $0\leq i<n.$

Заметим, что если $σ$ и $σ’$ — два различных состояния, а $σ’$ — это итерация $σ$ , то $σ$ не может быть итерацией $σ’,$ поскольку в противном случае цикл не сможет завершиться. Другими словами, итерация антисимметрична и, следовательно, является частичным порядком .

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

Следовательно, если принять аксиому выбора , отношение «преемник», которое мы первоначально определили для цикла, хорошо обосновано в пространстве состояний $Σ$ , поскольку оно строгое (иррефлексивное) и содержится в «итерационном» отношении. Таким образом, функция идентичности в этом пространстве состояний является вариантом цикла while, поскольку мы показали, что состояние должно строго уменьшаться — как «преемник» и «итерация» — каждый раз, когда тело S выполняется с учетом инварианта $I$ и условие С.

Более того, мы можем показать счетным рассуждением, что существование любого варианта влечет за собой существование варианта в ω ₁ , первом несчетном ординале , т. е.

V:\Sigma \rightarrow \omega _{1}.

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

соображения Практические

На практике варианты цикла часто считаются неотрицательными целыми числами или даже должны быть таковыми. ^[2] но требование, чтобы каждый цикл имел целочисленный вариант, лишает выразительной силы неограниченной итерации язык программирования . Если такой (формально проверенный) язык не допускает трансфинитное доказательство завершения для какой-либо другой столь же мощной конструкции, такой как рекурсивный вызов функции , он больше не способен к полной µ-рекурсии , а только к примитивной рекурсии . Функция Аккермана — канонический пример рекурсивной функции, которую нельзя вычислить в цикле с целочисленным вариантом .

Однако с точки зрения вычислительной сложности функции, которые не являются примитивно-рекурсивными, лежат далеко за пределами того, что обычно считается управляемым . Учитывая даже простой случай возведения в степень как примитивно-рекурсивной функции и тот факт, что композиция примитивно-рекурсивных функций является примитивно-рекурсивной, можно начать понимать, насколько быстро может расти примитивно-рекурсивная функция. И любая функция, которая может быть вычислена машиной Тьюринга за время выполнения, ограниченное примитивно-рекурсивной функцией, сама по себе является примитивно-рекурсивной. Поэтому трудно представить себе практическое применение полной µ -рекурсии, где примитивная рекурсия не подойдет, тем более, что первая может моделироваться второй до чрезвычайно длительного времени выполнения.

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

Пример [ править ]

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

/** condition-variable, which is changed in procedure S() **/
bool C;
/** function, which computes a loop iteration bound without side effects **/
inline unsigned int getBound();

/** body of loop must not alter V **/ 
inline void S(); 

int main() {
    unsigned int V = getBound(); /* set variant equal to bound */
    assert(I); /* loop invariant */
    while (C) {
        assert(V > 0); /* this assertion is the variant's raison d'être (reason of existence) */
        S(); /* call the body */
        V = min(getBound(), V - 1); /* variant must decrease by at least one */
    };
    assert(I && !C); /* invariant is still true and condition is false */

    return 0;
};

Зачем вообще рассматривать нецелочисленный вариант? [ редактировать ]

Зачем вообще рассматривать нецелочисленный или трансфинитный вариант? Этот вопрос возник потому, что во всех практических случаях, когда мы хотим доказать, что программа завершается, мы также хотим доказать, что она завершается через разумный промежуток времени. Есть как минимум две возможности:

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

См. также [ править ]

Ссылки [ править ]

^ Винскель, Глинн (1993). Формальная семантика языков программирования: введение . Массачусетский технологический институт. стр. 32–33, 174–176.
^ Бертран Мейер, Михаэль Швейцер (27 июля 1995 г.). «Почему варианты цикла являются целыми числами» . Страницы поддержки Eiffel . Эйфелева программа . Проверено 23 февраля 2012 г.

[1] Винскель, Глинн (1993). Формальная семантика языков программирования: введение . Массачусетский технологический институт. стр. 32–33, 174–176.

[2] Бертран Мейер, Михаэль Швейцер (27 июля 1995 г.). «Почему варианты цикла являются целыми числами» . Страницы поддержки Eiffel . Эйфелева программа . Проверено 23 февраля 2012 г.

[1]

[2]