### 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

BSD License

### History

August 17, 2023
  Updated to version v1.10.1.

### Topics

- Computer science/Automata and formal languages

### Related publications

- 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

### Session Combinatorics_Words_Lyndon

- Lyndon
- Lyndon_Addition

### Depends on

- Combinatorics on Words Basics
- Order Extension and Szpilrajn’s Extension Theorem

## Cite

×

Combinatorics_Words_Lyndon-AFP

    @article{Combinatorics_Words_Lyndon-AFP,
      author  = {Štěpán Holub and Štěpán Starosta},
      title   = {Lyndon words},
      journal = {Archive of Formal Proofs},
      month   = {May},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Combinatorics_Words_Lyndon.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- May 26, 2021 : Isabelle2021