一句话:提出以自由半模 monad 为代数基础的加权搜索框架,并实现 Dijkstra 与高效概率采样。
加权搜索是许多基础算法的重要组件,但作为计算效应,其研究远少于深度优先或广度优先搜索。本文探索加权搜索的代数基础,并展示如何将其实现为 monad transformer。作者首先将广度优先搜索表达为半环上的多项式,再推广到自由半模 monad,以涵盖概率 monad、多项式 monad 及加权搜索等广泛应用。随后,基于自由半模 monad 引入 monad transformer,通过优化该类型得到配对堆,并用于实现 Dijkstra 算法和高效概率采样。该构造在 Cubical Agda 中形式化,并在 Haskell 中实现。
Weighted search is an essential component of many fundamental and useful algorithms. Despite this, it is relatively under explored as a computational effect, receiving not nearly as much attention as either depth- or breadth-first search. This paper explores the algebraic underpinning of weighted search, and demonstrates how to implement it as a monad transformer. The development first explores breadth-first search, which can be expressed as a polynomial over semirings. These polynomials are generalised to the free semimodule monad to capture a wide range of applications, including probability monads, polynomial monads, and monads for weighted search. Finally, a monad transformer based on the free semimodule monad is introduced. Applying optimisations to this type yields an implementation of pairing heaps, which is then used to implement Dijkstra's algorithm and efficient probabilistic sampling. The construction is formalised in Cubical Agda and implemented in Haskell.