module index where

The StringLab🔗

This website is a fork of the 1Lab that contains a collection of work-in-progress results regarding strings. It was created by Reed Mullanix as his CAS 779 final project. All code and prose written as part of this project live under the StringLab namespace, and are enumerated in this file.

\ Warning

The StringLab is a work in progress, so links to it may not be stable!

How to read this document🔗

The StringLab is entirely written in Literate Agda: this means that we freely intermingle code and prose. All identifiers are hyperlinked, and hovering over them will display their type.

Basic results on strings🔗

The StringLab is all about the mathematics and computer science of strings, so it is only natural that we start with we start with some basic constructions and results on strings. For the most part, these are all elementary, but there are some subtle proof engineering choices here! To read more, click on the following link:

open import StringLab.Data.List

From here, we develop the theory of factors of strings.

open import StringLab.Data.List.Factor

Next, we take some time to define and prove some basic properties of lexicographic orderings.

open import StringLab.Data.List.Lexicographic

Next, we define Lyndon words, and examine their closure properties and standard factorisations.

open import StringLab.Data.List.Lyndon

Appendix🔗

As with any mathematical development, we need some results and definitions that are not directly related to strings; we gather them in the appendix.

Ordering relations🔗

Orderings are somewhat subtle constructively, especially strict orderings, so we must take care when choosing a definition. This module contains our definition of total order, some basic properties, and general commentary on the design choices that I made.

open import StringLab.Order.Trichotomous

Miscellanea🔗

Finally, I needed to prove a grab-bag of tiny lemmas; these are not particularly interesting, which is why they are buried at the end.

open import StringLab.Data.Dec
open import StringLab.Equiv

Technology🔗

The StringLab would not be possible without a myriad other free and open-source projects. Most notably, it is built atop the 1Lab!

The following copyright excerpt is taken from the 1Lab:

  • Fonts: Our monospace typeface is Julia Mono (license), chosen for its excellent unicode coverage. The textual content can be read in either Inria Sans (license) or EB Garamond (license), according to the user’s preference. All of these fonts are distributed under the terms of the SIL Open Font License, v1.1.

  • Prose: We write our textual content in Markdown, which is rendered using Pandoc, then put through a variety of filters to implement things like diagrams, folding equations, highlighted divs/details, etc. Despite our extensive use of Pandoc, no part of the project is distributed.

  • Mathematics: We type-set our mathematics, at build-time, using KaTeX. Even though the rendering is done ahead-of-time, we distribute their CSS and fonts. KaTeX is distributed under the terms of the MIT license: a copy is available here.

  • Iconography: Our favicon is the ice-cube emoji from Noto Emoji, distributed under the terms of the Apache License, 2.0; a copy is available here. Other icons come from octicons, distributed under the terms of the MIT license, which you can find here.

  • Diagrams: Our diagrams are created using quiver, and rendered to SVG using LaTeX and pdftocairo, which is part of the Poppler project. No part of these projects is redistributed.

  • Web: All of the JavaScript we ship is free and open source software, and most of it is developed in-house — you can find it on our GitHub. We use the fast-fuzzy library to power the search dialog, which is distributed under the terms of the ISC license, available here.

    None of our content relies on JavaScript to function, but enabling it does improve the experience — allowing you control over theming, use of the search function, exploring the link graph, type-on-hover, and more. If you have JS disabled for privacy concerns, rest assured: The 1Lab does not track you, or collect any sort of personally identifying information.