Algebras for weighted search
File(s) 3473577.pdf (364.17 KB)
Published version
Author(s)
Kidney, Donnacha Oisín
Wu, Nicolas
Type
Journal Article
Abstract
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 semi module monad to capture a wide range of applications, including probability monads, polynomial monads, and monads for weighted search. Finally, a monad trans-former based on the free semi module 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.
Date Issued
2021-08-18
Date Acceptance
2021-06-19
Citation
Proceedings of the ACM on Programming Languages, 2021, 5, pp.1-30
ISSN
2475-1421
Publisher
Association for Computing Machinery (ACM)
Start Page
1
End Page
30
Journal / Book Title
Proceedings of the ACM on Programming Languages
Volume
5
Copyright Statement
© 2021 Copyright held by the owner/author(s). This work is licensed under a Creative Commons Attribution 4.0 International License.
License URL
Sponsor
Engineering & Physical Science Research Council (EPSRC)
Identifier
https://dl.acm.org/doi/10.1145/3473577
Grant Number
EP/S028129/1
Subjects
Science & Technology
Technology
Computer Science, Software Engineering
Computer Science
Haskell
Agda
graph search
monad
Science & Technology
Technology
Computer Science, Software Engineering
Computer Science
Haskell
Agda
graph search
monad
MONAD TRANSFORMERS
BACKTRACKING
Publication Status
Published
Article Number
72
Date Publish Online
2021-08-18
