ATS: какие ваши доказательства?
Nov. 26th, 2011 08:55 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
thedeemonВ прошлой серии мы увидели, как зависимые типы в ATS помогают избежать грубых ошибок вроде выхода за пределы строки или массива. А можно ли продвинуться еще дальше в деле обеспечения корректности? Можно ли полностью доказать статически, что функция делает ровно то, что надо, и всегда выдает верный результат? В ряде случаев можно. В ATS мы можем формулировать логические утверждения о данных и функциях программы и конструировать их доказательства, а компилятор их проверит. Утверждения являются одним из сортов статических термов (prop) и подобны типам данных, но только они служат типами не для данных, а для доказательств. Лучше всего рассмотреть на примере. Числа Фибоначчи нынче не в моде, они всем надоели, поэтому возьмем нечто новое, необычное и волнующее: числа Леонардо. Определяются они так:
L[0] = 1, L[1] = 1, L[n] = L[n-2] + L[n-1] + 1
Мы можем сформулировать логическое утверждение LEON(n,x), гласящее, что число x есть n-ное по счету число Леонардо (считая с нуля):
Выглядит это похоже на определение алгебраического типа данных, но смысл несет несколько другой. В первой ветке говорится, что для любого натурального 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. Это шаг индукции.
Как эту штуку можно использовать? Мы можем описать функцию, вычисляющую n-ное число Леонардо и доказать, что она делает именно это, что возвращаемое значение действительно является n-ным числом Леонардо. Простой вариант выглядит так:
Тип ее читается так: функция leon для любого натурального n принимает его, и существует такой натуральный х, что функция возвращает целое число х, а вместе с ним доказательство утверждения LEON(n,x), т.е. что L[n]=x. Внутри происходит следующее. Если n < 2, то возвращаем результат (1), а вместе с ним факт-доказательство LEONbase, доказывающее LEON(n,1). Что именно оно доказывает, компилятор понимает по типу функции. Если же аргумент не меньше двух, то вызывая себя рекурсивно, мы получаем значение a=L[n-2] вместе с сопутствующим доказательством утверждения LEON(n-2,a), аналогично значение b=L[n-1] с сопутствующим доказательством утверждения LEON(n-1,b) и строим из них факт-доказательство LEONind, доказывающий утверждение LEON(n, a+b+1), который и возвращаем вместе с вычисленным ответом a+b+1. Такой вариант компилируется успешно, но если мы в выражении-ответе заменим 1 на другое число или a на b или еще что поменяем, то компилироваться уже не будет.
Но тут мы совсем уж изображали капитана Очевидность, вычисляющий код и вывод доказательства дублировали друг друга. Давайте сделаем другой вариант, более эффективный. Вместо двухкратного рекурсивного вызова будем все считать за О(n) простым линейным циклом. Без доказательств код будет выглядеть так:
Нерекурсивная функция leon2 для любого натурального n возвращает некое целое х. Если n меньше 2, то возвращаем 1. Иначе запускаем цикл от 2 до n, передавая в переменной cur текущее (i-ное) число Леонардо, а в переменной prev - предыдущее. Дошли до n - вернули текущее. Еще не дошли - вычисляем следующее (prev + cur + 1) и повторяем цикл. Функция-цикл использует значение n из внешней функции, поэтому это замыкание, помечаем как cloref. Сайд-эффектов нет, поэтому пишем cloref0. Чтобы доказать отсутствие эффекта nontermination, ставим терминационную метрику - .<n-i>. - это натуральное число с каждым рекурсивным вызовом уменьшается, а значит цикл гарантированно завершится.
Теперь расставим утверждения и доказательства. В типе внешней функции будет все как в прошлый раз: мы утверждаем, что она возвращает L[n], поэтому
Когда аргумент меньше двух, мы так же возвращаем единицу и факт - базу индукции
Чтобы индуктивно получить доказательство для L[n+1], нам потребуются доказательства для L[n] и L[n-1] - cur и prev. Поэтому перед аргументами loop ставим
pf_cur: LEON(i,c), pf_prev: LEON(i-1,p)
т.е. добавляем два аргумента-доказательства.
Теперь при самом первом ее вызове loop(2, 3, 1) нам нужно предоставить доказательства, что 3 действительно является L[2], а 1 - L[1]. Их конструируем из LEONbase и LEONind, только нужно явно указать, какое именно утверждение доказывается (там, где это не очевидно). В итоге вся функция целиком выглядит так:
prval - это как val, только для proofs. Пробуем скомпилировать, но компилятор ругается в месте LEONind(pf_prev, pf_cur): кое-что должно быть больше единицы! В чем дело? Вспомним определение LEONind: это доказательство определено для натурального n > 1. Мы же его используем для idx+1, где idx - натуральное число от 0 до n, а значит неравенство (idx+1) > 1 не всегда выполнено. Добавим в тип loop условие i > 1 (мы ведь начинаем цикл с 2), теперь все нормально, компилятор доволен, теорема доказана.
Итак, у нас в программе завелись статические сущности, похожие на типы, - утверждения - и динамические сущности, похожие на значения, - доказательства. Про статику мы знаем, что это чисто объекты времени компиляции, во время работы программы их нет. А как в рантайме выглядят динамические объекты-доказательства? А никак. Их тоже нет, при трансляции в Си они полностью исчезают, остается только настоящий код, делающий реальную работу. Именно для этого в ATS не пошли до конца по пути Карри-Говарда и не стали объединять типы с утверждениями, а значения с доказательствами. Они хоть и похожи, но имеют важное отличие - одни попадают в скомпилированную программу, а вторые остаются в мире идей, эдакие мнимые динамические значения.
Есть ли у этого механизма реальное применение помимо вычисления столь нужных каждому факториалов, Фибоначчи и Леонардо? О да. Прошу еще раз теперь уже новыми глазами посмотреть на пример реальной задачи. Такой раскрашенный HTML генерирует сам компилятор. Красное - это динамические значения, то, чем реально оперирует работающий код. Синее - это статические термы (в том числе типы данных), используемые при компиляции для проверок корректности. А зеленое - это доказательства. Мы выделяем буфер вызовом malloc_gc(BUFSZ), который имеет такой тип:
Он возвращает указатель на адрес l, а вместе с ним два факта-доказательства. Первый доказывает, что n байт по адресу l были выделены в управляемой куче, и о них должен заботиться сборщик мусора. Второй доказывает, что по адресу l находятся n непроинициализированных байтов (блин, все время мучаюсь, склонять ли это слово). Второе доказательство нам очень понадобится при вызове fgets. Функция чтения строки fgets_err имеет следующий тип:
Помимо того, что число запрашиваемых байтов обязано быть не больше размера передаваемого буфера (и это проверяется статически!), функция требует доказательство того, что файл открыт на чтение, а также доказательство того, что по указанному адресу действительно есть sz байт, которые не обязаны быть проинициализированны. Возвращает она вместе с указателем на прочитанную строку доказательство утверждения fgets_v, которое определено так:
Смысл его такой. Если функция вернула нулевой указатель, то по переданному ей адресу по-прежнему находятся sz непроинициализированных байтов. Если же вернулся ненулевой указатель, то по данному адресу находится строка длины n, причем n меньше числа запрошенных у fgets_err байтов n0. Чтобы работать с буфером как со строкой нам потребуется доказательство, что это именно строка (strbuf (sz, n)), а не случайные байты (b0ytes (sz)).
Здесь использовано ключевое слово dataview, а не dataprop, потому что это не просто утверждение (prop), а линейное утверждение (view). Имеется в виду линейная логика: доказательство линейного утверждения существует в единственном экземпляре и может быть съедено (consumed). Поскольку это в данном случае утверждение о содержимом некоторого буфера, то если какая-то функция это содержимое меняет, то утверждение больше не актуально, поэтому доказательство его больше недействительно. Такая функция съедает доказательство старого утверждения и выдает в обмен новое доказательство нового утверждения о новом статусе буфера. Функция fgets_err как раз такая. Причем реально-то это обычная fgets из libc, оперирующая голыми указателями и числами. Просто в ATS ее обвешали типами так, что программист просто вынужден работать с ней корректно, передавая правильные данные и проверяя возвращаемый результат. Сила зависимых типов не в том, что они сделают работу за нас, а в том, что они заставят нас писать хороший код, а плохой не писать вовсе.
Ладно, на сегодня хватит.
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. Это шаг индукции.
Как эту штуку можно использовать? Мы можем описать функцию, вычисляющую n-ное число Леонардо и доказать, что она делает именно это, что возвращаемое значение действительно является n-ным числом Леонардо. Простой вариант выглядит так:
fun leon {n:nat} (n : int n) : [x:nat] (LEON(n,x) | int x) =
if n < 2 then (LEONbase | 1)
else let
val (pa | a) = leon(n-2)
val (pb | b) = leon(n-1)
in
(LEONind(pa, pb) | a + b + 1)
endТип ее читается так: функция leon для любого натурального n принимает его, и существует такой натуральный х, что функция возвращает целое число х, а вместе с ним доказательство утверждения LEON(n,x), т.е. что L[n]=x. Внутри происходит следующее. Если n < 2, то возвращаем результат (1), а вместе с ним факт-доказательство LEONbase, доказывающее LEON(n,1). Что именно оно доказывает, компилятор понимает по типу функции. Если же аргумент не меньше двух, то вызывая себя рекурсивно, мы получаем значение a=L[n-2] вместе с сопутствующим доказательством утверждения LEON(n-2,a), аналогично значение b=L[n-1] с сопутствующим доказательством утверждения LEON(n-1,b) и строим из них факт-доказательство LEONind, доказывающий утверждение LEON(n, a+b+1), который и возвращаем вместе с вычисленным ответом a+b+1. Такой вариант компилируется успешно, но если мы в выражении-ответе заменим 1 на другое число или a на b или еще что поменяем, то компилироваться уже не будет.
Но тут мы совсем уж изображали капитана Очевидность, вычисляющий код и вывод доказательства дублировали друг друга. Давайте сделаем другой вариант, более эффективный. Вместо двухкратного рекурсивного вызова будем все считать за О(n) простым линейным циклом. Без доказательств код будет выглядеть так:
fn leon2 {n:nat} (n: int n) : [x:nat] int x =
if n < 2 then 1
else let
fun loop {i,c,p:nat | i <= n} .<n-i>.
(idx: int i, cur : int c, prev: int p):<cloref0> [x:nat] int x =
if idx = n then cur
else loop(idx+1, prev + cur + 1, cur)
in
loop(2, 3, 1)
endНерекурсивная функция leon2 для любого натурального n возвращает некое целое х. Если n меньше 2, то возвращаем 1. Иначе запускаем цикл от 2 до n, передавая в переменной cur текущее (i-ное) число Леонардо, а в переменной prev - предыдущее. Дошли до n - вернули текущее. Еще не дошли - вычисляем следующее (prev + cur + 1) и повторяем цикл. Функция-цикл использует значение n из внешней функции, поэтому это замыкание, помечаем как cloref. Сайд-эффектов нет, поэтому пишем cloref0. Чтобы доказать отсутствие эффекта nontermination, ставим терминационную метрику - .<n-i>. - это натуральное число с каждым рекурсивным вызовом уменьшается, а значит цикл гарантированно завершится.
Теперь расставим утверждения и доказательства. В типе внешней функции будет все как в прошлый раз: мы утверждаем, что она возвращает L[n], поэтому
fn leon2 {n:nat} (n: int n) : [x:nat] (LEON(n,x) | int x) =Когда аргумент меньше двух, мы так же возвращаем единицу и факт - базу индукции
if n < 2 then (LEONbase | 1)
Чтобы индуктивно получить доказательство для L[n+1], нам потребуются доказательства для L[n] и L[n-1] - cur и prev. Поэтому перед аргументами loop ставим
pf_cur: LEON(i,c), pf_prev: LEON(i-1,p)
т.е. добавляем два аргумента-доказательства.
Теперь при самом первом ее вызове loop(2, 3, 1) нам нужно предоставить доказательства, что 3 действительно является L[2], а 1 - L[1]. Их конструируем из LEONbase и LEONind, только нужно явно указать, какое именно утверждение доказывается (там, где это не очевидно). В итоге вся функция целиком выглядит так:
fn leon2 {n:nat} (n: int n) : [x:nat] (LEON(n,x) | int x) =
if n < 2 then (LEONbase | 1)
else let
fun loop {i,c,p:nat | i <= n} .<n-i>. (pf_cur: LEON(i,c), pf_prev: LEON(i-1,p) |
idx: int i, cur : int c, prev: int p):<cloref0> [x:nat] (LEON(n,x) | int x) =
if idx = n then (pf_cur | cur)
else loop(LEONind(pf_prev, pf_cur), pf_cur | idx+1, prev + cur + 1, cur)
prval p0 : LEON(0,1) = LEONbase
prval p1 : LEON(1,1) = LEONbase
prval p2 = LEONind(p0, p1)
in
loop(p2, p1 | 2, 3, 1)
end
prval - это как val, только для proofs. Пробуем скомпилировать, но компилятор ругается в месте LEONind(pf_prev, pf_cur): кое-что должно быть больше единицы! В чем дело? Вспомним определение LEONind: это доказательство определено для натурального n > 1. Мы же его используем для idx+1, где idx - натуральное число от 0 до n, а значит неравенство (idx+1) > 1 не всегда выполнено. Добавим в тип loop условие i > 1 (мы ведь начинаем цикл с 2), теперь все нормально, компилятор доволен, теорема доказана.
Итак, у нас в программе завелись статические сущности, похожие на типы, - утверждения - и динамические сущности, похожие на значения, - доказательства. Про статику мы знаем, что это чисто объекты времени компиляции, во время работы программы их нет. А как в рантайме выглядят динамические объекты-доказательства? А никак. Их тоже нет, при трансляции в Си они полностью исчезают, остается только настоящий код, делающий реальную работу. Именно для этого в ATS не пошли до конца по пути Карри-Говарда и не стали объединять типы с утверждениями, а значения с доказательствами. Они хоть и похожи, но имеют важное отличие - одни попадают в скомпилированную программу, а вторые остаются в мире идей, эдакие мнимые динамические значения.
Есть ли у этого механизма реальное применение помимо вычисления столь нужных каждому факториалов, Фибоначчи и Леонардо? О да. Прошу еще раз теперь уже новыми глазами посмотреть на пример реальной задачи. Такой раскрашенный HTML генерирует сам компилятор. Красное - это динамические значения, то, чем реально оперирует работающий код. Синее - это статические термы (в том числе типы данных), используемые при компиляции для проверок корректности. А зеленое - это доказательства. Мы выделяем буфер вызовом malloc_gc(BUFSZ), который имеет такой тип:
fun malloc_gc {n:nat} (n: size_t n)
:<> [l:agz] (freebyte_gc_v (n, l), b0ytes n @ l | ptr l)
Он возвращает указатель на адрес l, а вместе с ним два факта-доказательства. Первый доказывает, что n байт по адресу l были выделены в управляемой куче, и о них должен заботиться сборщик мусора. Второй доказывает, что по адресу l находятся n непроинициализированных байтов (блин, все время мучаюсь, склонять ли это слово). Второе доказательство нам очень понадобится при вызове fgets. Функция чтения строки fgets_err имеет следующий тип:
fun fgets_err
{sz,n0:int | 0 < n0; n0 <= sz}
{m:fm} {l_buf:addr} (
pf_mod: file_mode_lte (m, r)
, pf_buf: b0ytes (sz) @ l_buf
| p: ptr l_buf, n0: int n0, f: &FILE m
) :<> [l:addr] (fgets_v (sz, n0, l_buf, l) | ptr l)
Помимо того, что число запрашиваемых байтов обязано быть не больше размера передаваемого буфера (и это проверяется статически!), функция требует доказательство того, что файл открыт на чтение, а также доказательство того, что по указанному адресу действительно есть sz байт, которые не обязаны быть проинициализированны. Возвращает она вместе с указателем на прочитанную строку доказательство утверждения fgets_v, которое определено так:
dataview
fgets_v (sz:int, n0: int, addr, addr) =
| {l_buf:addr}
fgets_v_fail (sz, n0, l_buf, null) of b0ytes (sz) @ l_buf
| {n:nat | n < n0} {l_buf:addr | l_buf > null}
fgets_v_succ (sz, n0, l_buf, l_buf) of strbuf (sz, n) @ l_buf
Смысл его такой. Если функция вернула нулевой указатель, то по переданному ей адресу по-прежнему находятся sz непроинициализированных байтов. Если же вернулся ненулевой указатель, то по данному адресу находится строка длины n, причем n меньше числа запрошенных у fgets_err байтов n0. Чтобы работать с буфером как со строкой нам потребуется доказательство, что это именно строка (strbuf (sz, n)), а не случайные байты (b0ytes (sz)).
Здесь использовано ключевое слово dataview, а не dataprop, потому что это не просто утверждение (prop), а линейное утверждение (view). Имеется в виду линейная логика: доказательство линейного утверждения существует в единственном экземпляре и может быть съедено (consumed). Поскольку это в данном случае утверждение о содержимом некоторого буфера, то если какая-то функция это содержимое меняет, то утверждение больше не актуально, поэтому доказательство его больше недействительно. Такая функция съедает доказательство старого утверждения и выдает в обмен новое доказательство нового утверждения о новом статусе буфера. Функция fgets_err как раз такая. Причем реально-то это обычная fgets из libc, оперирующая голыми указателями и числами. Просто в ATS ее обвешали типами так, что программист просто вынужден работать с ней корректно, передавая правильные данные и проверяя возвращаемый результат. Сила зависимых типов не в том, что они сделают работу за нас, а в том, что они заставят нас писать хороший код, а плохой не писать вовсе.
Ладно, на сегодня хватит.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
no subject
Date: 2011-11-26 08:41 pm (UTC)no subject
Date: 2011-11-26 10:12 pm (UTC)no subject
Date: 2011-11-27 12:39 am (UTC)no subject
Date: 2011-11-27 04:54 am (UTC)no subject
Date: 2011-11-27 08:25 am (UTC)no subject
Date: 2011-11-27 09:32 am (UTC)no subject
Date: 2011-11-27 11:37 am (UTC)I/O эффектом не считается, и это действительно довольно странно.
no subject
Date: 2011-11-27 10:07 pm (UTC)