Заметки о ФП: формальное доказательство свойств программы

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

В этой статье я продолжу наводить мосты между математикой и программированием и покажу как формально доказывать свойства программ. Кроме того мы разберемся что значит словосочетание “корректная программа”.

Математическая индукция и корректность

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

предположим, что нужно установить истинность бесконечной последовательности утверждений \(P_{1}, P_{2}, ..., P_{n}, P_{n+1}, ...\). Тогда если

• верно утверждение \(P_{1}\) (база индукции)
• утверждение \(P_{n+1}\) (шаг индукции) верно, если верно \(P_{n}\) для любого n (предположение индукции)

то вся последовательность утверждений \(P_{1}, P_{2}, P_{3} ...\) верна. Аналогично можно установить истинность конечной последовательности.

Как мы видели ранее, выполнение программы - это просто последовательность вызовов методов. Каждый метод возвращает определенное значение, множество ограничений на которое можно записать в виде математического утверждения. Таким образом, выполнение программы можно представить как последовательность утверждений. Для определения истинности некоторого утверждения о программе остается доказать два момента. Первый - это доказать то, что первый метод в программе возвращает верное значение. Второй - что любой вызов метода в программе возвращает верное значение, при условии что предыдущий метод также вернул верное значение. В качестве примера докажем следующее утверждение о коде расчета факториала: \(factorial(n) \geq 2^{n}\, для\, n \geq 4\).

Определение метода следующее:

def factorial(n: Int): Int =
        if (n == 0) 1
        else n * factorial(n - 1)

Докажем для начала базу индукции. Просто посчитаем: \(factorial(4) = 24 \geq 16; 16 = 2^{4}\). База индукции доказана. Теперь докажем, что шаг индукции не меняет истинности нашего утверждения. Предполагаем, что неравенство \(factorial(n) \geq 2^n\) верно. Тогда в соответствии с кодом выше для n > 4 получаем \(factorial(n+1) \geq (n+1) * factorial(n) > 2 * factorial(n) \geq 2*2^{n}; 2*2^{n} = 2^{n+1}\). Видим, что \(factorial(n+1) \geq 2^{n+1}\). Таким образом мы формально доказали, что в результате выполнения нашей программы утверждение \(factorial(n) \geq 2^{n}\, для\, n \geq 4\) всегда остается справедливым.

Заметим, что для нашей модели подстановок (определенной тут) каждый шаг программы просто заменяет часть терма другим термом. Между всеми состояниями программы мы можем поставить знак равенства. Это свойство называется ссылочной прозрачностью.

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

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

• если n > 0, то мы будем выполнять вызов factorial(n-1). На каждом шаге программы n только уменьшается до тех пор, пока не станет равным 0;
• если n == 0, то программа завершается;
• если n < 0, то мы будем выполнять вызов factorial(n-1) бесконечно.

Последний случай ясно показывает, что наша программа некорректна, так как не всегда завершается. Вспомним, что факториал определен только для натуральных чисел и исправим нашу реализацию, воспользовавшись классом натуральных чисел из прошлой статьи:

val One = new Succ(Zero)
def factorial(n: Nat): Nat =
        if (n.isZero) One
        else n * factorial(n - One)

Структурная индукция

Принцип структурной индукции - это частный случай принципа математической индукции. Определить его можно так.

Для доказательства истинности свойства P(xs) для любого списка xs достаточно:

• доказать, что истинна база индукции P(Nil)
• для списка xs и некоторого элемента x доказать истинность шага индукции, принимая гипотезу индукции: если P(xs) истинно, то и P(x::xs) также истинно

В качестве примера докажем корректность метода concat (или просто ++) из класса List, служащего для объединения двух списков. Доказывать будем следующее свойство: \((xs ⧺ ys) ⧺ zs = xs ⧺ (ys ⧺ zs)\).

Реализация метода concat такая:

def concat[T](xs: List[T], ys: List[T]) = xs match {
        case List() => ys // 1-й случай
        case x :: xs1 => x :: concat(xs1, ys) //2-й случай
}

Видим, что вместо ++ может быть подставлен один из двух термов (в коде отмечены комментариями). Далее воспользуемся принципом структурной индукции. Для начала докажем базу индукции для xs.

Воспользовавшись определением метода мы доказали базовый случай. Теперь аналогично докажем истинность шага индукции по xs. Предполагаем, что \((xs ⧺ ys) ⧺ zs = xs ⧺ (ys ⧺ zs)\).

Случай доказан. Для завершения доказательства осталось провести идентичные рассуждения по индукции для ys и zs. Теперь давайте разберем более сложный пример. Рассмотрим метод reverse:

def reverse = this match {
        case Nil => Nil
        case x::xs => xs.reverse ++ List(x)
}

Доказывать будем утверждение \(xs.reverse.reverse = xs\). База индукции доказывается просто:

Провести доказательство истинности шага индукции уже не так легко:

С этим выражением мы больше ничего не можем сделать. Раз мы не смогли свести выражение к нужной формуле простыми преобразованиями, то будем хитрее. Заметим, что на самом деле нам нужно доказать выражение \((xs.reverse ⧺ List(x)).reverse = x \mathrel{::} xs\). Кроме того, по предположению индукции, \(x \mathrel{::} xs = x \mathrel{::} xs.reverse.reverse\). Таким образом нам нужно доказать, что \((xs.reverse ⧺ List(x)).reverse = x \mathrel{::} xs.reverse.reverse\). После нескольких попыток доказать это утверждение становится понятно, что весьма удобно заменить \(xs.reverse\) на \(ys\). Такая замена называется обобщением (не знаю точен ли перевод, на английском он пишется generalize). Теперь нам нужно доказать следующую лемму:

Докажем эту лемму индукцией по ys. Базовый случай:

Базовый случай доказан, займемся доказательством для шага индукции.

Положим \(y \mathrel{::} ys = zs\), тогда видим что \((zs ⧺ List(x)).reverse = x \mathrel{::} zs.reverse\). Таким образом лемма доказана и доказать первоначальное утверждение не составит труда. Данный метод доказательства является достаточно общим и иногда его называют fold/unfold. Доказательство этим методом проводится в три шага.

• определяем часть утверждения двумя разными путями (шаг fold)
• приравниваем одно определение другому, упрощаем и применяем предположение индукции
• еще раз применяем определение и переходим к первоначальной постановке задачи (шаг unfold)

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

Подведем итоги

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