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

### License

BSD License

### History

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.

### Topics

- Computer science/Automata and formal languages

### Related publications

- Holub, Š., & Starosta, Š. (2021). Formalization of Basic Combinatorics on Words. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPICS.ITP.2021.22
- Producing symmetrical facts for lists induced by the list reversal mapping in Isabelle/HOL
- Development repository

### Session Combinatorics_Words

- Arithmetical_Hints
- Reverse_Symmetry
- CoWBasic
- Border_Array
- Submonoids
- Morphisms
- Periodicity_Lemma
- Lyndon_Schutzenberger
- Binary_Code_Morphisms
- Equations_Basic

### Used by

- Binary codes that do not preserve primitivity
- Intersection of two monoids generated by two element codes
- Graph Lemma
- Lyndon words

## Cite

×

Combinatorics_Words-AFP

    @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},
    }

Download

## Download

× Download latest

Older releases:

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