Infinite Words and Morphic Languages Formalized in Isabelle/HOL
\v{S}t\v{e}p\'an Starosta
TL;DR
This paper formalizes concepts of infinite words, morphic languages, and Sturmian words within Isabelle/HOL, contributing to the rigorous mathematical foundation of combinatorics on words.
Contribution
It introduces a formalization of infinite words, morphic languages, and Sturmian words in Isabelle/HOL, advancing the mechanized verification of combinatorial properties.
Findings
Formalization of infinite words in Isabelle/HOL
Definition and elementary properties of Sturmian words
Framework for future formalization of combinatorics on words
Abstract
We present a formalization of basics related to infinite words in the generic proof assistant Isabelle/HOL. Furthermore, we present a formalization of purely morphic and morphic languages. Finally, we present a formalized definition of Sturmian words as lower mechanical words and prove some very elementary facts. The formalization is based on an ongoing larger project of formalization of combinatorics on words.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · semigroups and automata theory · Advanced Algebra and Logic