文章基本信息

标题：Formalization of Basic Combinatorics on Words
本地全文：下载
作者：Holub, {S}t {e}p'{a}n ; Starosta, {S}t {e}p'{a}n
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2021
卷号：193
页码：22:1-22:17
DOI：10.4230/LIPIcs.ITP.2021.22
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：combinatorics on words; formalization; Isabelle/HOL