Algolean is a library of algorithms and complexity theory, defined broadly to include much of the Algorithms and Complexity theory literature. It is written in the lightweight free monad version of what I call the "query-combinator" model. It currently consists of code that lies in several CSLib pull requests. The framework can encompass standard and custom models in algorithms theory, ranging from RAM and Turing machines, to circuits, and even niche models like the Robertson-Webb cake cutting model. The intent is to provide an all-encompassing framework of models and reductions between them. This framework forces formalizers to declare their basic operations and costs upfront and realizes complexity claims as purely structural consequences of the basic costs.
Algolean is a pun. It is intended to be read in two ways.
- "Algo" + "Lean" : A library of algorithms and complexity theory in lean
- "Algol" + "ean" (pronounced like "ene") : To pay homage to Algol which motivates a lot of modern algorithmic pseudocode, and whose simplicity this framework hopes to mimic (hence the "ene").
(so far)
- Shreyas Srinivas - Maintainer and main author.
- Tanner Duve
- Eric Wieser
For timing it builds on top of the Writer monad AddWriter that was proposed in CSLib as the TimeM model by Sorrachai Yingchareonthawornchai and whose API was perfected by Eric Wieser.