ATS: какие ваши доказательства?

В прошлой серии мы увидели, как зависимые типы в ATS помогают избежать грубых ошибок вроде выхода за пределы строки или массива. А можно ли продвинуться еще дальше в деле обеспечения корректности? Можно ли полностью доказать статически, что функция делает ровно то, что надо, и всегда выдает верный результат? В ряде случаев можно. В ATS мы можем формулировать логические утверждения о данных и функциях программы и конструировать их доказательства, а компилятор их проверит. Утверждения являются одним из сортов статических термов (prop) и подобны типам данных, но только они служат типами не для данных, а для доказательств. Лучше всего рассмотреть на примере. Числа Фибоначчи нынче не в моде, они всем надоели, поэтому возьмем нечто новое, необычное и волнующее: числа Леонардо. Определяются они так:
L[0] = 1, L[1] = 1, L[n] = L[n-2] + L[n-1] + 1

Мы можем сформулировать логическое утверждение LEON(n,x), гласящее, что число x есть n-ное по счету число Леонардо (считая с нуля):

dataprop LEON(int, int) =
| {n:nat | n <= 1} LEONbase(n, 1)
| {n:nat | n > 1; a,b:int} LEONind(n, a+b+1) of (LEON(n-2, a), LEON(n-1,b))

Выглядит это похоже на определение алгебраического типа данных, но смысл несет несколько другой. В первой ветке говорится, что для любого натурального n <= 1 (т.е. 0 или 1) мы можем сконструировать факт-доказательство LEONbase(n, 1), доказывающий утверждение LEON(n,1), причем нам для этого никаких пререквизитов не требуется, мы можем его сконструировать из ничего, постулировать, это наша база индукции. Если бы это был алгебраический тип данных, мы бы сказали, что выражение LEONbase(0,1) имеет тип LEON(0,1). Но это не тип (type), а утверждение (prop), поэтому мы говорим, что факт LEONbase(0,1) служит доказательством утверждения LEON(0,1). Во второй ветке говорится, что если для натурального n > 1 и целых чисел a и b у нас имеется на руках доказательство утверждения LEON(n-2, a) и доказательство утверждения LEON(n-1,b) (т.е. мы знаем, что L[n-2]=a и L[n-1]=b), то из них мы можем вывести факт LEONind(n, a+b+1), доказывающий утверждение LEON(n, a+b+1), т.е. что L[n]=a+b+1. Это шаг индукции.
( Read more... )