group-telegram.com/covalue/91
Last Update:
Пару недель назад выпустил в открытое плавание (переведя под крыло Coq community) проект, над которым эпизодически работаю c 2021 года: FDSA in SSReflect.
Идея банальна - переписать код из открытой книги Nipkow et al, "Functional Data Structures and Algorithms" (в начале работы книга называлась "Functional Algorithms, Verified") с Isabelle/HOL на полностью типотеоретический язык. Для портирования я выбрал Coq + фреймворк Mathcomp/SSReflect + плагин Equations для компактной записи паттерн-матчинга и доказательств завершимости.
В Isabelle/HOL для ризонинга используется классическая логика, но для работы с корректностью вычислительных структур данных разница с конструктивной логикой невелика, поскольку почти всегда предполагается, что элементы этих структур как минимум дискретны (то есть снабжены разрешимой проверкой на равенство, что соответствует "локальному" исключенному третьему). Основное отличие, пожалуй, только в одном месте - вместо использования равенств на мультимножествах из Isabelle я использую списки и отношение перестановки (perm_eq) на них. Кроме того, в Isabellе функции не обязаны быть тотальными, что влечет за собой необходимость слегка менять определения - дополняя их для всей области определения и давая доказательства завершимости во всех случаях (а не только в избранных, как в книге).
Основная тема книги - формальные доказательства корректности классических чисто функциональных алгоритмов, а для многих алгоритмов также приведены доказательства их рантайм-сложности. Стоит, однако, отметить, что последний момент реализован несколько ad-hoc - вручную строится скелет алгоритма, возвращающий приближенное число итераций, и ризонинг ведется на этом скелете, без проверки его соответствия его изначальному алгоритму.
Книга устроена следующим образом:
0. Вводная глава с основными понятиями.
1. Раздел, посвященный алгоритмам сортировки и выбора: mergesort/quicksort/quickselect. На мой взгляд, глава про алгоритм выбора делает ощутимый скачок в сложности, т.к. для quickselect доказательства завершимости (из-за использования вложенной рекурсии) и комплексити (упрощенный вариант теоремы Акра-Баззи) на порядок (а то и два) замысловатее таковых для сортировок.
2. Крупный раздел об алгоритмах на деревьях - тут и популярные красно-черные/AVL-деревья, и менее известные деревья Брауна, и специализированные квадродеревья.
3. Идеологическое продолжение предыдущего раздела о нескольких способах реализации очередей с приоритетом.
4. Раздел о продвинутых алгоритмических методах, включающий динамическое программирование, амортизационный анализ и косые деревья. До этого раздела я пока еще не добрался, остановился на адаптации поисковых деревьев из предыдущих глав в поисковую таблицу для кэширования результатов в динамическом программировании.
5. Раздел "разное": на текущий момент там есть строковый алгоритм Кнута-Морриса-Пратта, алгоритм сжатия Хаффмана и поисковый алгоритм αβ-отсечения. Тут я пока реализовал только алгоритм Хаффмана.
В целом, книга довольно неплохо объясняет классические иммутабельные алгоритмы (хотя местами слишком сжато, особенно в 4м разделе), этакий пруф-инженерный вариант известной работы Okasaki, [1998] "Purely functional data structures". В книге много упражнений, большинство из которых я прорешал, но в публичном репозитории заменил соответствующие места скелетами определений и теорем, чтобы не спойлить решения для потенциальных студентов.
#datastructures
BY Covalue
Share with your friend now:
group-telegram.com/covalue/91