Grandury, Nanevski, Gryzlov, [2025] "Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach"
В прошлом августе у нас наконец-то вышла статья, идею которой я предложил где-то в 2022 году и периодически возился с её имплементацией. В самой статье основная идея в явном виде не выписана, но суть там вот в чём.
В теории типов наиболее общим представлением ориентированного графа обычно полагается функция A → A → U, где A — тип вершин графа, а U — вселенная («тип типов»), то есть гомогенный бинарный предикат. Используя классическую эквивалентность (см. например HoTT book, 4.8.3) ∑[T:U] (T → A) ≃ (A → U), мы можем трансформировать определение графа в пару { edge : A → U, adj : (from : A) → edge from → A }, то есть в представление в виде adjacency map, которое сопоставляет исходным вершинам рёберные конструкции и умеет по ним извлекать конечную вершину. Специализируя эту конструкцию под конечные графы и структуры данных, мы получаем из неё классические представления adjacency matrix/list.
Идея, лежащая в основе статьи, заключается в том, что такое представление удобно и для работы на логическом уровне, по крайней мере, для алгоритмов, работающих как поиск в глубину, то есть стартующих из одной вершины, и транзитивно проходящих по всем исходящим из неё ребрам. В частности, раз мы можем запихнуть орграф в конечное отображение, его можно использовать как частичный коммутативный моноид (Partial Commutative Monoid, PCM) в сепарационной логике. (Частичная) операция моноида - дизъюнктное объединение отображений с непересекающимися областями определения. Чтобы она заработала, достаточно договориться, что графы могут быть частичными, то есть допускать висячие ребра, где исходная вершина лежит в нужном подграфе, а конечная уже за его пределами. При объединении висячие ребра могут склеиваться в обычные ребра, находя свои конечные вершины.
В классической сепарационной логике рассматривается в первую очередь PCM куч (heaps). Как только у нас появился второй PCM, мы можем рассмотреть отображения (морфизмы) между ними, а также эндоморфизмы над самими графами. Морфизм в данном случае это функция, сохраняющая моноидальную операцию, f(γ₁∙γ₂) = fγ₁∙fγ₂. Это позволяет распространить концепцию фрейминга (framing) на графы - в статье мы называем это "контекстной локализацией" (contextual localization). Другими словами, морфизмы позволяют вычленить кусок графа, произвести над ним некоторое действие, и затем автоматически склеить его с незатронутой оставшейся частью, что сильно упрощает ряд доказательств. Морфизмами, в частности, являются высокоуровневые комбинаторы над кодировкой графов как конечных отображений - map, filter, а также более ad-hoc функции вроде взятия множеств конечных вершин sinks. Достижимость (reachability) в графе сама по себе морфизмом не является, но удобно взаимодействует с морфизмом filter, что позволяет "вырезать" фрагменты из достижимых компонент.
Весь этот аппарат мы используем для создания библиотеки работы с графами в Hoare Type Theory, и построения двух формальных доказательств для императивных алгоритмов Шорра-Уэйта (разметка бинарного графа, где стек обхода хранится в самом графе через инверсию рёбер, без выделения отдельной памяти) и union-find (построение непересекающихся классов эквивалентности). Доказательства получились достаточно компактными (110 строк для Шорра-Уэйта, 49 для union-find).
Ограничение описанной техники вытекает из исходной идеи - она естественна для алгоритмов, исследующих граф, следуя по ребрам. Для алгоритмов, работающих с ребрами более "глобально" (например, алгоритм Краскала), скорее всего, потребуются другие представления.
#paper #separationlogic
