Combinatorics on Words Basics

Title:	Combinatorics on Words Basics
Authors:	Štěpán Holub, Martin Raška and Štěpán Starosta
Submission date:	2021-05-24
Abstract:	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).
BibTeX:	@article{Combinatorics_Words-AFP, author = {Štěpán Holub and Martin Raška and Štěpán Starosta}, title = {Combinatorics on Words Basics}, journal = {Archive of Formal Proofs}, month = may, year = 2021, note = {\url{https://isa-afp.org/entries/Combinatorics_Words.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Used by:	Combinatorics_Words_Graph_Lemma, Combinatorics_Words_Lyndon
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.