2026-07-23T21:44:50Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13917 2024-03-06T10:53:07Z ddc:004 open_access

Formalization of Basic Combinatorics on Words Holub, Štěpán Starosta, Štěpán combinatorics on words formalization Isabelle/HOL Combinatorics on Words is a rather young domain encompassing the study of words and formal languages. An archetypal example of a task in Combinatorics on Words is to solve the equation x ⋅ y = y ⋅ x, i.e., to describe words that commute. This contribution contains formalization of three important classical results in Isabelle/HOL. Namely i) the Periodicity Lemma (a.k.a. the theorem of Fine and Wilf), including a construction of a word proving its optimality; ii) the solution of the equation x^a ⋅ y^b = z^c with 2 ≤ a,b,c, known as the Lyndon-Schützenberger Equation; and iii) the Graph Lemma, which yields a generic upper bound on the rank of a solution of a system of equations. The formalization of those results is based on an evolving toolkit of several hundred auxiliary results which provide for smooth reasoning within more complex tasks. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Štěpán Holub and Štěpán Starosta 2021 Is Part Of LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2021.22 urn:nbn:de:0030-drops-139177 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.22 eng https://creativecommons.org/licenses/by/4.0/legalcode