Dependency graph

Legend

Boxes: definitions
Ellipses: theorems and lemmas
Blue border: the statement of this result is ready to be formalized; all prerequisites are done
Orange border: the statement of this result is not ready to be formalized; the blueprint needs more work
Blue background: the proof of this result is ready to be formalized; all prerequisites are done
Green border: the statement of this result is formalized
Green background: the proof of this result is formalized
Dark green background: the proof of this result and all its ancestors are formalized
Dark green border: this is in Mathlib

Definition 11

The critical exponent $\mathrm{ce}(w)$ of an infinite word $\mathbf{w}$ is defined by

\[ \mathrm{ce}(w) = \sup \{ \alpha \in \mathbb Q \mid \mathbf{w} \text{ contains some $\alpha $-power}\} . \]

LaTeX

Theorem 20

Let $x$ be a word in a finite alphabet $\Sigma $. We have $A^-(x)\le A(x)$. If $\lvert x\rvert =1$ and $\lvert \Sigma \rvert {\gt}1$ then $A^-(x)=1{\lt}2=A(x)$.

LaTeX

Definition 15

Let $\Sigma $ be a finite alphabet and let $Q$ be a finite set whose elements are called states. A nondeterministic finite automaton (NFA) is a 5-tuple $ M=(Q,\Sigma ,\delta ,q_0,F). $ The transition function $\delta :Q\times \Sigma \to \mathcal P(Q)$ maps each $(q,b)\in Q\times \Sigma $ to a subset of $Q$. Within $Q$ we find the initial state $q_0\in Q$ and the set of final states $F\subseteq Q$. The function $\delta $ is extended to a function $\delta ^*:Q\times \Sigma ^*\to \mathcal P(Q)$ by structural induction:

\begin{eqnarray*} \delta ^*(q,\varepsilon ) & =& \{ q\} ,\\ \delta ^*(q,\sigma \mathbin {{:}{;}}i)& =& \bigcup _{s\in \delta ^*(q,\sigma )}\delta (s,i). \end{eqnarray*}

Overloading notation, we may also write $\delta =\delta ^*$. The language accepted by $M$ is

\[ L(M)=\{ x \in \Sigma ^*\mid \delta (q,x)\cap F\ne \emptyset \} . \]

A deterministic finite automaton (DFA) is also a 5-tuple $ M=(Q,\Sigma ,\delta ,q_0,F). $ In this case, $\delta :Q\times \Sigma \to Q$ is a total function and is extended to $\delta ^*:Q\times \Sigma ^*\to Q$ by

\begin{equation} \label{eq:recursion} \delta ^*(q,\sigma \mathbin {{:}{;}}i)=\delta (\delta ^*(q,\sigma ),i). \end{equation}

If the domain of $\delta $ is a subset of $Q\times \Sigma $, $M$ is an incomplete DFA. In this case, $M$ coincides with an NFA with a special property which we can check for effectively. We denote a partial function $f$ from $A$ to $B$ by $f:(\subseteq A)\to B$ or $f\mathrel {\vdots }A\to B$.

Finally, the set of words accepted by $M$ is

\[ L(M)=\{ x \in \Sigma ^*\mid \delta (q,x)\in F\} . \]

LaTeX

Definition 19

Let $\Sigma $ be an alphabet. Let DFA$_\Sigma $ denote the class of all DFAs over $\Sigma $ and let partDFA$_\Sigma $ denote the class of all partial DFAs over $\Sigma $. If a DFA $M$ over $\Sigma $ has the property that it accepts a string $x$, but no other strings of length $\lvert x\rvert $, i.e.,

\[ L(M)\cap \Sigma ^{\lvert x\rvert }=\{ x\} , \]

then we say that $M$ accepts $x$ uniquely. Let $x\in \Sigma ^*$ with $\lvert x\rvert =n$. Define $A(x,\Sigma )$, the automatic complexity of $x$ (with respect to $\Sigma $) to be the least number of states in any $M\in \mathrm{DFA}_\Sigma $ such that $M$ accepts $x$ uniquely.

If we consider $x$ to be a function $x:[n]\to \Sigma $, then $x\in \Sigma ^*$ where $\Sigma =\mathrm{range}(x)$. We define $\tilde A(x)=A(x,\mathrm{range}(x))$.

Similarly, we define $A^-(x,\Sigma )$, the partial automatic complexity of $x$, to be the least number of states in any $M\in \mathrm{partDFA}_\Sigma $ such that $L(M)\cap \Sigma ^n=\{ x\} $.

LaTeX

Definition 21 [ 7 , 19 ]

Let $L(M)$ be the language recognized by the automaton $M$. Let $x$ be a finite word. The (unique-acceptance) nondeterministic automatic complexity $A_N(w)=A_{Nu}(w)$ of $w$ is the minimum number of states of an NFA $M$ such that $M$ accepts $w$ and the number of walks along which $M$ accepts words of length $\lvert w\rvert $ is 1.

The exact-acceptance nondeterministic automatic complexity $A_{Ne}(w)$ of $w$ is the minimum number of states of an NFA $M$ such that $M$ accepts $w$ and $L(M)\cap \Sigma ^{\lvert w\rvert }=\{ w\} $.

LaTeX Lean

Definition 8

A de Bruijn word of order $n$ over an alphabet $\Sigma $ is a sequence $y$ such that every $x\in \Sigma ^n$ occurs exactly once as a cyclic substring of $y$.

LaTeX

Definition 16

A digraph $D=(V,E)$ consists of a set of vertices $V$ and a set of edges $E\subseteq V^2$. Let $s,t\in V$. Let $n\ge 0$, $n\in \mathbb Z$. A walk of length $n$ from $s$ to $t$ is a function $\Delta :\{ 0,1,\dots ,n\} \to V$ such that $\Delta (0)=s$, $\Delta (n)=t$, and $(\Delta (k),\Delta (k+1))\in E$ for each $0\le k{\lt}n$.

A cycle of length $n=\lvert \Delta \rvert \ge 1$ in $D$ is a walk from $s$ to $s$, for some $s\in V$, such that $\Delta (t_1)=\Delta (t_2), t_1\ne t_2\implies \{ t_1,t_2\} =\{ 0, n\} $. Two cycles are disjoint if their ranges are disjoint.

LaTeX

Definition 4

Two occurrences of words $a$ (starting at position $i$) and $b$ (starting at position $j$) in a word $x$ are disjoint if $x=uavbw$ where $u,v,w$ are words and $\lvert u\rvert =i$, $\lvert uav\rvert =j$.

LaTeX

Definition 1

The length of a word $s\in \Sigma ^*$ is defined by induction:

\begin{eqnarray*} \lvert \varepsilon \rvert & =& 0\\ \lvert s \mathbin {{:}{;}}a\rvert & =& \lvert s\rvert + 1. \end{eqnarray*}

LaTeX

Definition 10

Let $\alpha $ be a word of length $n$, and let $\alpha _i$ be the $i^{\text{th}}$ letter of $\alpha $ for $1\le i\le n$. We define the $u^{\text{th}}$ power of $\alpha $ for certain values of $u\in \mathbb Q_{\ge 0}$ (the set of nonnegative rational numbers) as follows. For $u\in \mathbb {N} $:

\begin{eqnarray*} \alpha ^0 & =& \varepsilon ,\\ \alpha ^{n+1} & =& \alpha ^n \mathbin {{+}{+}}\alpha . \end{eqnarray*}

If $u=v+k/n$ where $0{\lt}k{\lt}n$, and $k$ is an integer, then $\alpha ^u$ denotes $\alpha ^v \alpha _1\dots \alpha _k$ and is called a $u$-power.

The word $w$ is $u$-power-free if no nonempty $v$-power, $v\ge u$, occurs (Definition 5) in $w$. In particular, 2-power-free is called square-free and 3-power-free is called cube-free. Let $\mathbf{w}$ be an infinite word over the alphabet $\Sigma $, and let $x$ be a finite word over $\Sigma $. Let $u{\gt}0$ be a rational number. The word $x$ is said to occur in $\mathbf{w}$ with exponent $u$ if $x^{u}$ occurs in $\mathbf{w}$ (Definition 5).

LaTeX

Theorem 9

Let $k,t\in \mathbb {N} $ with $k\ge 1$. In an alphabet of cardinality $k$, there exists a $t$-rainbow word of length $k^t+t-1$.

LaTeX

Theorem 23Hyde [ 6 ]

The nondeterministic automatic complexity $A_N(x)$ of a string $x$ of length $n$ satisfies

\[ A_N(x) \le b(n):={\lfloor } n/2 {\rfloor } + 1\text{.} \]

LaTeX Lean

Lemma 6

Suppose $n,t$ are positive integers with $t\le n+1$. A word of length $n$ has $n+1-t$ occurrences of subwords of length $t$.

LaTeX

Theorem 14Lyndon and Schützenberger [ 16 ] ; see [ 18 , Theorem 2.3.3 ]

Let $x,y\in \Sigma ^+$. Then the following four conditions are equivalent:

$xy=yx$.
There exists $z\in \Sigma $ and integers $k,l{\gt}0$ such that $x=z^k$ and $y=z^l$.
There exist integers $i,j{\gt}0$ such that $x^i=y^j$.

LaTeX

Theorem 17

Let $B$ be a set and let $P$ be the set of all partial functions from $\mathbb {N} $ to $B$. For each $F:\mathbb {N} \times P\to B$, there is a unique function $G:\mathbb {N} \to B$ such that

\[ G(n)=F(n,G\upharpoonright n) \]

for all $n\in \mathbb {N} $.

LaTeX

Theorem 7

Let $k,t\in \mathbb {N} $ with $k\ge 1$. In an alphabet of cardinality $k$, a $t$-rainbow word has length at most $k^t+t-1$.

LaTeX

Theorem 12Krieger [ 14 ]

The critical exponent of $\mathbf w$ is equal to

\[ \inf \{ \alpha \in \mathbb Q \mid \mathbf{w} \text{ is $\alpha $-power-free}\} . \]

LaTeX

Lemma 13Lyndon and Schützenberger [ 16 ] ; see [ 18 , Theorem 2.3.2 ]

Let $c,d,e\in \Sigma ^+$. The equation $cd=de$ holds iff there exist a nonempty word $u$, a word $v$, and a natural number $p$ such that $c=uv$, $d=(uv)^p u$, and $e=vu$.

LaTeX

Theorem 22Shallit and Wang [ 19 , Theorem 9 ]

Suppose $w\in \Sigma ^*$ is $k$th-power-free for some integer $k\ge 2$, i.e., $w$ contains no subword of the form $x^k$ with $x\ne \varepsilon $. Then $A(w)\ge \frac{\lvert w\rvert +1}k$.

LaTeX

Definition 5

A word $x=x_0\dots x_{n-1}$, or an infinite word $x=x_0x_1\dots $, with each $x_i\in \Sigma $, is viewed as a function $f_x:n\to \Sigma $ with $f_x(i)=x_i$. An occurrence of $y=y_0\dots y_{m-1}$ in $x$ is a function $f_x\upharpoonright [a,a+m-1]$ such that $f_x(a+i)=y_i$ for each $0\le i{\lt} m$.

For $a,b\in \mathbb {N} $, let $[a,b]=\{ x\in \mathbb {N} \mid a\le x\le b\} $. Two occurrences $f_x\upharpoonright [a,b]$, $f_x\upharpoonright [c,d]$ are disjoint if $[a,b]\cap [c,d]=\emptyset $.

If moreover $[a,b+1]\cap [c,d]=\emptyset $ then the occurrences are strongly disjoint.

A subword that occurs at least twice in a word $w$ is a repeated subword of $w$. Let $k\in \mathbb {N} $, $k\ge 1$. A word $x=x_0\dots x_{n-1}$, $x_i\in \Sigma $, is $k$-rainbow if it has no repeated subword of length $k$: there are no $0\le i{\lt}j{\lt}n-k$ with $x\upharpoonright [i,i+k-1]=x\upharpoonright [j,j+k-1]$. A 1-rainbow word is also known simply as rainbow.

LaTeX