thedeemon | Entries tagged with ats

Акт 5. Мемоизация доказательств

Для обеспечения коррекности структур и убеждения компилятора в том, что мы не делаем ничего предосудительного, у нас используются доказательства утверждений LEON(k,sz) о том, что sz - действительно k-е число Леонардо, L[k]=sz. В одном из прошлых постов этой серии мы видели, как построить функцию, вычисляющую нужное число Леонардо и поставляющую вместе с ним доказательство того, что это правильное число. Там было несколько вариантов, и лучший из них имел сложность O(k). Если такую функцию задействовать в smoothsort'e, его сложность резко возрастет и из O(n * log n) превратится во что-то вроде O(n * log n * log n). Нужна мемоизация, и оригинальный алгоритм подразумевает использование массива с уже вычисленными числами Леонардо, так получение нужного числа отнимает O(1) операций. Но такой массив имеет размер опять же O(log n), поэтому рассказы про потребление памяти О(1) - враки. Попытка добавить мемоизацию в функцию вычисления чисел Леонардо сталкивается с проблемой. Функция определена как

fun leon {n:nat} (n : int n) : [x:nat] (LEON(n,x) | int x)

тип ее результата зависит от значения аргумента. Зависимые типы, понимаш. Если мы захотим сохранить результаты в массиве, то каждый его элемент будет иметь свой тип! А так нельзя - в массивах все элементы одного типа.( Read more... )

Церебральный секс в 7 актах.

В ЖЖ модно проходить психологические тесты, один из них в этом посте, суть его раскрывается ниже.

Введение

Для тренировки своего ATS-фу я решил реализовать и доказать на нем алгоритм smoothsort - сортировку, имеющую сложность O(n * log n) как в среднем, так и в худшем случае, O(n) в лучшем, и вроде как плавно изменяющую скорость по мере перехода от лучшего случая к среднему (по мере увеличения числа элементов не на своих местах), отсюда ее название. Моей задачей было получить корректно работающую реализацию, содержащую в явном виде доказательство отсортированности получаемого массива. Заставить ее работать супер быстро я задачу не ставил, т.к. по-любому константа в сложности этого алгоритма так велика, что на практике он проигрывает по скорости более простым методам на малых объемах и гибридным на больших. Поэтому я позволил себе неэффективную реализацию с использованием O(log n) памяти под вспомогательные структуры. В интернетах пишут, что Аллах послал нам эту сортировку через пророка своего Дейкстру в варианте с О(1) дополнительной памяти, но это все равно враки, потом расскажу подробней почему.

Акт 1. Алгоритм

Алгоритм строится вокруг упоминавшихся тут ранее чисел Леонардо. Напомню, что определяются они так:
L[0] = 1, L[1] = 1, L[k] = L[k-1] + L[k-2] + 1
Вводится понятие кучи Леонардо - это неявная структура, содержащая L[k] элементов. Для k=0 и k=1 она состоит из единственного элемента. Для k > 1 куча Леонардо состоит из трех идущих подряд частей: кучи размером L[k-1], кучи размером L[k-2] и одного элемента, называемого корнем (для кучи из одного элемента ее корнем считается он сам). Такая куча имеет размер L[k-1] + L[k-2] + 1 = L[k], т.е. ее устройство повторяет определение чисел Леонардо. Структура неявная, т.е. все элементы лежат подряд в обычном массиве, просто мы мысленно разбиваем их на группы и интерпретируем как кучи.

Не каждое натуральное число является числом Леонардо, но любое натуральное число можно представить в виде суммы чисел Леонардо с разными индексами. Мы это вскоре докажем конструктивно в нашем коде. Поэтому массив любой длины мы можем "покрыть" идущими подряд кучами Леонардо с убывающими индексами (k). Такую последовательность кучек Леонардо назовем рядом куч (heap string). И чтобы это все было не зря, потребуем от этих неявных структур несколько свойств. Свойством кучи Леонардо (heap property) сделаем требование, чтобы ее корень всегда был не меньше, чем корни двух входящих в нее подкуч (если они есть). А свойством ряда куч (heap string property) сделаем требование неубывания корней кучек, из которых этот ряд состоит. Вот так, например, выглядит ряд куч Леонардо на массиве из 10 элементов:

В этом ряду две кучи, одна имеет размер sz=9, индекс k=4, ее корнем является элемент с индексом r=8. Вторая куча состоит из одного элемента с позицией r=9, имеет размер sz=1 и индекс k=1. Первая куча размером L[4] внутри имеет две подкучи размерами L[3] и L[2], которые содержат подкучи меньшего размера и т.д. Для каждой кучи выполнено ее свойство - корень не меньше корней подкуч, и для всего ряда выполнено свойство ряда - корни входящих в него куч не убывают. В итоге сам массив еще не отсортирован, но уже какой-то порядок в нем есть. Можно заметить, что следствием свойства кучи является тот факт, что среди всех входящих в нее элементов максимальный - самый правый. Такое же следствие и у свойства ряда куч - самый правый элемент больше всех (не меньше, если быть точным).

Отсюда уже несложно угадать устройство smoothsort'a. Мы берем массив и сперва проходимся по нему слева-направо, постепенно с нуля строя ряд куч, добавляя в него по одному элементу и обеспечивая выполнение требуемых свойств. В результате максимальный элемент занимает свое место - самое правое. Потом мы идем обратно справа-налево, выкидывая по элементу и сокращая ряд куч, так же обеспечивая выполнение обоих свойств. Тогда на каждом шагу этого обратного хода максимальный элемент из всех, входящих в ряд, оказывается справа, а ряд на каждом шагу сокращается. В результате, если у нас массив A из n элементов, то после построения ряда из n элементов у нас элементы A[0..n-2] не больше, чем A[n-1], потом после сокращения ряда на 1 элементы A[0..n-3] не больше, чем A[n-2], ..., и когда ряд сократится до двух элементов, получится, что A[0] <= A[1] <= A[2] ... <= A[n-1], т.е. массив окажется отсортированным. Всего будет почти 2n шагов, каждый из которых потребует не более O(log n) действий, что доказано elsewhere (любимое слово Hongwei Xi), поэтому общая сложность O(n * log n).

Неупомянутые детали. Каким образом происходит рост ряда куч при добавлении одного элемента? Мы смотрим на две самых правых кучи. Если их индексы - соседние убывающие числа (например, 3 и 2 или 1 и 0), то из двух этих куч и нового элемента мы делаем одну кучу большего размера. В противном случае просто добавляем кучу из одного этого нового элемента, а индексом ее считаем 0, если последняя куча в ряду имела индекс 1 (чтобы получились подряд идущие кучи с индексами 1 и 0), и 1 иначе. Сокращение ряда на один элемент еще проще. Если самая правая куча имеет размер 1, то просто ее выкидываем. Если ее размер больше 1, то она состоит из двух подкуч и корневого элемента. Ставим вместо нее в ряд две эти подкучи, а корневой элемент оказывается выкинутым. После каждой такой операции нужно восстановить требуемые свойства, об этом позже.

Теперь давайте запишем это все на ATS. Мы хотим описать функцию с таким заголовком:

fn {a:t@ype} smoothsort {n:nat | n > 0} 
 (A : array(a,n), n : int n, gt : gt(a)): (SORTED(0,n-1) | void)

где

typedef gt (a:t@ype) = (a,a) -> bool // x > y

Для любого типа данных a наша полиморфная функция smoothsort принимает массив А из n элементов типа a, количество элементов n и функцию сравнения элементов gt, возвращающую true, когда первый аргумент больше второго. Функция сортирует массив на месте, и ничего не возвращает (void), а вместе с этим ничего она возвращает доказательство утверждения SORTED(0, n-1), т.е. что элементы массива с индексами от 0 до n-1 включительно теперь отсортированы. Будем считать, что сортируем массив по возрастанию, сортировка по убыванию получается просто передачей на вход другой функции сравнения.
( Read more... )

Сегодня тема попроще.

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

fn search {n,m:nat | m <= n}
  (str : string n, sub : string m) : [p:int | p <= n - m] int p = let
  val n = int1_of_size1 (string_length str)
  val m = int1_of_size1 (string_length sub)
  fun cmp {i,j:nat | i < n-m; j <= m} .<m-j>. 
    (i : int i, j : int j) :<cloref0> bool = 
      if j = m then true 
      else if str[i+j] = sub[j] then cmp(i, j+1) else false
    
  fun search_loop {k:nat | k <= n-m} .<n-k>. 
    (k : int k):<cloref0> [r:int | r <= n-m] int r = 
      if cmp(k, 0) then k 
      else if k < n - m then search_loop(k+1) else ~1
in
  if m <= n then search_loop(0) else ~1
end

Видите ошибку?
Что делает компилятор. ( Read more... )

В прошлой серии мы увидели, как зависимые типы в 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... )

For you, when one sees emptiness
In terms of the meaning of dependent origination,
Then being devoid of intrinsic existence and
Possessing valid functions do not contradict.

-- Дже Цонкапа, "Сборник цитат для привлечения внимания", Союзпечать, 1402 г. (src)

В нашем детском саду всякий слышал о зависимых типах, что они умеют параметризоваться не только другими типами (как List a), но и значениями. Классический пример, который все приводят (и обычно на этом останавливаются), - это список с длиной. В синтаксисе ATS он описывается так:

datatype list (a:t@ype+, int) =
| list_nil (a, 0) 
| {n:nat} list_cons (a, n+1) of (a, list (a, n))

Для удобства рядом определяют

#define :: list_cons
#define nil list_nil

После чего выражение 5::6::7::nil будет иметь тип list(int, 3).
Т.е. list - это конструктор типа с двумя аргументами. Но в отличие от иных языков, где его kind был бы чем-то вроде * -> * -> *, здесь вместо звездочек более конкретные и информативные сущности: сорта. Тут стоит сделать небольшое отступление. Обычно языки программирования содержат в себе два подъязыка: один оперирует объектами времени выполнения (числа, строки, структуры...) и описывает поведение программы, второй оперирует объектами времени компиляции (типы, модули, шаблоны в С++...). Динамика и статика. В ряде динамически-типизированных языков второй подъязык почти отсутствует, поэтому они называются scripting languages, не будучи достойными называться programming languages.

В статически-типизированных языках мы привыкли во втором подъязыке оперировать в основном типами: применяем конструктор типов List к типу Int, получаем тип List Int. В ATS мир статических конструкций намного богаче, и не все из них являются типами данных. Например, утверждения (props). Возникает понятие сорта статического терма (конструкции). Так, type - сорт, к которому относятся все типы размером со слово (указатель), включая все boxed типы. t@ype - сорт, к которому относятся типы других размеров, например unboxed структуры, а также банальный тип int, ибо на 64-битной платформе его размер отличается от размера указателя. prop - сорт логических утверждений, view - сорт утверждений в линейной логике, viewtype - сорт для типов, с которыми связаны некоторые линейные утверждения... Сортов всяких много, плюс можно еще определять свои. Есть также сорта int и bool, к которым относятся статические целочисленные и булевы термы. Например, в типе list(int, 3) тройка - это не рантайм-значение типа int, которое будет где-то в памяти во время исполнения программы, а компайлтайм-значение (терм) сорта int, существующее только во время компиляции. Оба аргумента list здесь - статические термы, но разных сортов: первый терм имеет сорт t@ype, второй - сорт int. Именно это указано при описании datatype list(a:t@ype+, int). Плюс после t@ype означает ковариантность, на ней сейчас останавливаться не будем.
( Read more... )

Занялся я тут изучением ATS и в качестве учебного примера взял задачку nponeccop'a про фильтрацию IP адресов. Дабы не изобретать колеса, взял простое и красивое решение antilamer'a и попытался его почти дословно перевести.

Получилось 108 строк на ATS. Собранное версией ATS 0.2.5 под Cygwin'ом оно работает у меня в полтора раза быстрее, чем антиламерское решение, собранное GHC 6.12.1 (с ключом -О2). На тысяче интервалов и миллионе адресов работает 0.8 секунды (версия на хаскеле - 1.2 с), на 10 миллионах адресов - 8 секунд (а решение на хаскеле 12 с). Ради корректности сравнения оба варианта выдают один и тот же результат (вообще говоря, ошибочный - IP адрес, совпадающий с концом интервала, выкидывается, а интервал из одного адреса и вовсе игнорируется).

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

/home/user/ats/bin/atsopt --output ips_dats.c --dynamic ips.dats
/home/user/ips.dats: 3287(line=89, offs=9) -- 3293(line=89, offs=15): error(3):
mismatch of static terms (tyleq):
The needed term is: S2Eapp(S2Ecst(at_viewt0ype_addr_view); S2Eapp(S2Ecst(bytes);
 S2EVar(1284)), S2EVar(1285))
The actual term is: S2Eapp(S2Ecst(at_viewt0ype_addr_view); S2Eapp(S2Ecst(b0ytes)
; S2EVar(1267)), S2Evar(l$3484$3485(6817)))
/home/user/ips.dats: 3287(line=89, offs=9) -- 3293(line=89, offs=15): error(3):
mismatch of static terms (tyleq):
The needed term is: S2Etyarr(S2Ecst(byte); S2EVar(1284))
The actual term is: S2Etyarr(S2Etop(0; S2Ecst(byte_t0ype)); S2EVar(1267))
/home/user/ips.dats: 3287(line=89, offs=9) -- 3293(line=89, offs=15): error(3):
mismatch of static terms (tyleq):
The needed term is: S2Ecst(byte_t0ype)
The actual term is: S2Etop(0; S2Ecst(byte_t0ype))
exit(ATS): uncaught exception: _2fhome_2ffac2_2fhwxi_2fresearch_2fATS_2fIMPLEMEN
T_2fGeizella_2fAnairiats_2fsvn_2fats_2dlang_2fsrc_2fats_error_2esats__FatalError
Exception(1233)
exit(ATS): [ccomp_file_to_file(ips.dats, ips_dats.c)] failed.

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

На первый вариант у меня ушло два дня, но он работал на порядок медленнее хаскелевского. Дело было в том, что удобная для использования функция input_line основана на fgetc и сильно тормозит. А чтобы заменить ее на более быструю fgets ушло еще несколько часов, т.к. там типы сильно сложнее, и то не обошлось без читерства (приведение указателя).

Впечатлений масса, чуть позже распишу подробнее и объясню, что все эти закорючки в исходнике означают. Пока лишь замечу, что мой план начать писать на ATS в стиле ML, а потом постепенно вводить зависимые типы провалился: без зависимых типов и доказательств работать со строками, массивами или вводом-выводом нельзя.