Lyndon words are words lexicographically minimal in their conjugacy class. We formalize their basic properties and characterizations, in particular the concepts of the longest Lyndon suffix and the Lyndon factorization. Most of the work assumes a fixed lexicographical order. Nevertheless we also define the smallest relation guaranteeing lexicographical minimality of a given word (in its conjugacy class).
- August 17, 2023
- Updated to version v1.10.1.
- Holub, Š., & Starosta, Š. (2021). Lyndon Words Formalized in Isabelle/HOL. Lecture Notes in Computer Science, 217–228. https://doi.org/10.1007/978-3-030-81508-0_18
- Development repository