?

Log in

No account? Create an account

Previous Entry | Next Entry

fooling people with theorem provers

Занятный доклад на свежем FP Conf про equational reasoning и теорем пруверы:
https://www.youtube.com/watch?v=TRAPqhRdAH0
Докладчик рассказал, почему Liquid Haskell и F* пока не годятся, потом показал как он на Isabelle верифицировал вывод radix sort'a из tree sort'a, взятый из старинной статьи Gibbons'a. Типа, вот у нас реализация сортировки через построение дерева, вот мы тут колдуем-колдуем с эквивалентными преобразованиями кода и вот свели сортировку к foldr по списку, получился радикс сорт, сортирует за один проход, красота.
Только это все неправда.
То, что там названо treesort'ом, внутри себя уже реализует принципы радикссорта. Идея такая. Вот есть у нас список, условно, коротких строк ограниченной длины, [a]. И есть функции извлечения "букв" a -> b, где тип "букв" b принадлежит классам Bounded и Enum, т.е. все его возможные значения можно перечислить по порядку списком
rng = [minBound .. maxBound]
Тогда входной список "строк" можно разбить на подпоследовательности / бакеты - по одной для каждого значения "буквы". Partitioning function:
ptn :: (Bounded b, Enum b) => (a->b) -> [a] -> [[a]]
ptn d xs = [ filter ((m==) . d) xs | m <- rng ]

Здесь d - функция извлечения "буквы" b из "строки" a.
Тогда возьмем набор функций [a->b] по извлечению из условной строки первой буквы, второй буквы, третьей... Разобьем входные данные на бакеты по первой букве, каждый из них - на бакеты по второй, те - по третьей и т.д., получим дерево списков. В каждом узле дерева бакеты идут по порядку возрастания "букв", так что в итоговом дереве все окажется уже отсортированным, останется лишь его сплющить в один выходной список.
data Tree a = Leaf a | Node [Tree a]

mktree :: (Bounded b, Enum b) => [a->b] -> [a] -> Tree [a]
mktree [] xs = Leaf xs
mktree (d:ds) xs = Node (map (mktree ds) (ptn d xs))

treesort :: (Bounded b, Enum b) => [a->b] -> [a] -> [a]
treesort ds xs = flatten (mktree ds xs)

Тут важно, что mktree принимает два списка, ds и xs, первый это короткий список функций по извлечению "букв", второй - сами данные, которые уже будем сортировать, и организована mktree индукцией по списку функций. И flatten имеет очевидное устройство тоже индукцией по дереву. Ну и вот, дальше Gibbons и вслед за ним наш докладчик просто берут эти mktree и flatten и выражают их через foldr, заменяют явную рекурсию стандартным катаморфизмом, плюс избавляются от промежуточной структуры дерева, т.к. собранное mktree дерево тут же flatten'ом разбирается обратно. И, собственнно, весь equational reasoning и вся верификация на Isabelle сводятся к тому, чтобы показать, что реализация на foldr равна процитированной тут реализации на явной рекурсии. Это дело чистой механики и переписывания термов, сам алгоритм там не меняется ни сколько. Получается
radixsort :: (Bounded b, Enum b) => [a->b] -> [a] -> [a]
radixsort = foldr ft id
  where ft d g = concat . ptn d . g

Вот он, один проход по списку, но это проход по списку функций извлечения "букв", а не по входным данным! А вот по входным данным мы будем елозить внутри ptn, в каждом узле дерева входной список данных будет пройден L раз, где L - размер алфавита. Причем Gibbons в статье это понимает и честно отмечает, предлагая в конце альтернативную реализацию функции раскидывания по бакетам ptn. Но исходные рассуждения и доказательства проводятся не с ней, а с наивным вариантом. Докладчик с FPConf же то ли честно не понимал, что делает, то ли решил публику обмануть ради пущего эффекта. Вот, говорит, сортировка за один проход списка foldr'ом. А что совсем не того списка - не сказал. :) Ну и "доказал корректность" довольно простой тавтологии (radixsort == treesort), молодец.

Tags:

Comments

( 5 comments — Leave a comment )
swizard
Dec. 18th, 2017 02:18 pm (UTC)
А его потом, по-моему, кто-то про ptn спросил в кулуарах. Но могу ошибаться, я в тот день страшно не выспался, весь день как в тумане прошёл, вырубало просто адски.

Edited at 2017-12-18 05:28 pm (UTC)
gabriel_irk
Dec. 20th, 2017 06:09 am (UTC)
Нет, про ptn меня никто не спрашивал и вообще, кроме уважаемого thedeemon никто подвоха, к сожалению, не заметил...
gabriel_irk
Dec. 20th, 2017 06:07 am (UTC)
Добрый день!

Докладчик - это я. :D

Во-первых, мне очень приятно, что мой доклад вызвал у Вас интерес. И спасибо огромное за критику!

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

Тем не менее, treesort-то производит (на глаз) квадратичное количество проходов по списку функций, а radixsort - один. Оптимизация налицо! :D И в докладе я указывал, что это не буквальный radixsort, а некоторое обобщение. Строго говоря, конечно, это вообще просто функция, которая нам кажется "похожей" на radixsort. Да, надо было так и сказать.

Но доклад-то был не об этом. :) Я ни в коей мере не пытаюсь приписать себе заслуги Гиббонса, поэтому все алгоритмические трюки и особенности доказательства остаются на его совести. :D

Я попытался понять чего стОят эти "естественные", "прямолинейные", "простые" и "механические" эквациональные преобразования, если выполнять их полностью формально с помощью proof assistant'а. Т.е. по сути, моя часть - это пара слайдов с количесвом строк кода и выводами. К сожалению, без долгого вступления про суть вопроса выводы врядли будут понятны.

Кстати, вот исходники: https://gist.github.com/gabriel-fallen/d4f2a79e88f14a9be3e1ec6beeadca1b
В презентации в доп. материалах эта ссылка имеется, надеюсь PDF'ку тоже скоро опубликуют и она станет доступна общественности.

И если всё ещё считаете тавтологию "treesort == radixsort" простой - приглашаю Вас доказать её формально с помощью Вашего любимого инструмента (Idris, если правильно угадал?). :) Как рассказывал, при помощи Liquid Haskell и F* мне не удалось, а брать Agda или Idris было "страшновато". Но сравнить результаты очень интересно!
thedeemon
Dec. 20th, 2017 07:16 am (UTC)
O, а я смотрю, имя знакомое, но какой ник за ним скрывается не вспомнил. :)
Как обзор инструментов доклад неплохой получился.
Что до Идриса... он наверно не для этого, там все же другие задачи решаются. Не показать равенство двух хаскельных функций, а заимплементить одну так, чтобы в ее типе выразить какие-то нужные свойства. При этом выглядеть она наверняка будет совсем не так, как результат у Гиббонса.
gabriel_irk
Dec. 20th, 2017 10:13 am (UTC)
Спасибо! Хотя обзор инструментов постольку поскольку, поэтому очень ограниченный.

Строго говоря, когда стал доказывать на Isabelle, я тоже перестал доказывать свойства ф-ий Haskell, поскольку в Isabelle семантика ф-ий отличается (тотальность, eager vs. lazy) - просто потом экстракцию в Haskell делаю.

В Idris (как и Agda) с недавних пор завезли equational-style theorem proving, поэтому можно повторить результат относительно близко.

Кроме того, хотел пожаловаться на заголовок поста: то как я дурю людей к использованию theorem prover'а отношения не имеет. Получается fooling people and using theorem prover. :D
( 5 comments — Leave a comment )