Abstract
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).
License
History
- August 17, 2023
- Updated to version v1.10.1.
Topics
Related publications
- Holub, Š., & Starosta, Š. (2021). Lyndon Words Formalized in Isabelle/HOL. Developments in Language Theory, 217–228. https://doi.org/10.1007/978-3-030-81508-0_18
- Development repository