Занятный доклад на свежем 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), молодец.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
![[livejournal.com profile]](https://www.dreamwidth.org/img/external/lj-userinfo.gif){kind=small}
