Combinatorics on Words Basics

Štěpán Holub 🌐, Martin Raška and Štěpán Starosta 🌐

May 24, 2021

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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, including its full parametric solution. 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). We also provide relevant proof methods and a tool to generate reverse-symmetric claims.


BSD License


August 17, 2023
Updated to version v1.10.1.
August 24, 2022
Many updates and additions. New theories: Border_Array, Morphisms, Equations_Basic, and Binary_Code_Morphisms.


Related publications

Session Combinatorics_Words