Email Gateway (May 26 2021 at 10:18): Email Gateway (May 26 2021 at 10:18):From: Tobias Nipkow <nipkow@in.tum.de>
Combinatorics on Words Basics
Štěpán Holub, Martin Raška and Štěpán Starosta
We formalize basics of Combinatorics on Words. This is an extension of existing
theories on lists. We provide additional properties related to prefix, suffix,
factor, length and rotation. The topics include prefix and suffix comparability,
mismatch, word power, total and reversed morphisms, border, periods, primitivity
and roots. We also formalize basic, mostly folklore results related to word
equations: equidivisibility, commutation and conjugation. Slightly advanced
properties include the Periodicity lemma (often cited as the Fine and Wilf
theorem) and the variant of the Lyndon-Schützenberger theorem for words. We
support the algebraic point of view which sees words as generators of submonoids
of a free monoid. This leads to the concepts of the (free) hull, the (free)
basis (or code).
https://www.isa-afp.org/entries/Combinatorics_Words.html
Lyndon words
Štěpán Holub and Štěpán Starosta
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).
https://www.isa-afp.org/entries/Combinatorics_Words_Lyndon.html
Graph Lemma
Štěpán Holub and Štěpán Starosta
Graph lemma quantifies the defect effect of a system of word equations. That is,
it provides an upper bound on the rank of the system. We formalize the proof
based on the decomposition of a solution into its free basis. A direct
application is an alternative proof of the fact that two noncommuting words form
a code.
https://www.isa-afp.org/entries/Combinatorics_Words_Graph_Lemma.html
Enjoy!
smime.p7s
Last updated: Apr 24 2024 at 08:20 UTC