Square-free words

DefinitionSquare word#✓fully proved

A word \(w\) over an alphabet \(\alpha\) is a square if \(w = xx\) for some nonempty word \(x\), where \(xx\) denotes the concatenation of \(x\) with itself.

public def IsWordSquare {α : Type*} (w : List α) : Prop :=
  ∃ x : List α, x ≠ [] ∧ w = x ++ x

Used by 3

Used byCrochemore's square-freeness test · Square-free finite word · Square-freeness via prefixes of suffixes

DefinitionSquare-free finite word#✓fully proved

A finite word \(w\) over an alphabet \(\alpha\) is square-free if no factor of \(w\) is a square, where a factor of \(w\) is a word \(s\) with \(w = psq\) for some words \(p\) and \(q\), and a square is a word \(xx\) with \(x\) nonempty.

public def IsSquareFreeWord {α : Type*} (w : List α) : Prop :=
  ∀ s : List α, s.IsInfix w → ¬ IsWordSquare s

Uses 1 · Used by 4

Statement usesSquare word

Used byCrochemore's square-freeness test · Square-freeness via prefixes of suffixes · Square-free ternary words of length \(n\) · Factors of square-free words are square-free

DefinitionSquare-free infinite word#✓fully proved

An infinite word \(u = u_0 u_1 u_2 \cdots\) over an alphabet \(\alpha\) is square-free if it contains no two adjacent equal nonempty blocks: for all \(i \ge 0\) and all \(k \ge 1\) there is some \(j < k\) with \(u_{i+j} \ne u_{i+k+j}\).

public def IsInfiniteSquareFreeWord {α : Type*} (u : Nat → α) : Prop :=
  ∀ i k : Nat, 0 < k → ∃ j, j < k ∧ u (i + j) ≠ u (i + k + j)

Used by 1

Used bySquare-free infinite ternary word

AbbreviationThe ternary alphabet for square-free words#✓fully proved

The ternary alphabet is the set \(\{0, 1, 2\}\) of natural numbers less than \(3\); its three letters play the role of \(a\), \(b\) and \(c\).

public abbrev TernaryAlphabet := Fin 3

Used by 3

Used byCrochemore's square-freeness test · Square-free infinite ternary word · Square-free ternary words of length \(n\)

DefinitionSquare-free ternary words of length \(n\)#✓fully proved

For a natural number \(n\), a finite word \(w\) over the ternary alphabet is a square-free ternary word of length \(n\) if \(w\) is square-free and \(w\) has length exactly \(n\).

public def IsTernarySquareFreeLength (n : Nat) (w : List TernaryAlphabet) : Prop :=
  IsSquareFreeWord w ∧ w.length = n

Uses 2

Statement usesSquare-free finite word · The ternary alphabet for square-free words

DefinitionSquare-free infinite ternary word#✓fully proved

An infinite word \(u = u_0 u_1 u_2 \cdots\) over the ternary alphabet is a square-free infinite ternary word if it is square-free as an infinite word.

public def IsInfiniteTernarySquareFreeWord (u : Nat → TernaryAlphabet) : Prop :=
  IsInfiniteSquareFreeWord u

Uses 2

Statement usesSquare-free infinite word · The ternary alphabet for square-free words

TheoremFactors of square-free words are square-free#✓fully proved

If a finite word \(v\) is square-free and \(u\) is a factor of \(v\), that is, \(v = puq\) for some words \(p\) and \(q\), then \(u\) is square-free.

public theorem IsSquareFreeWord.of_isInfix {α : Type*} {u v : List α}
    (hv : IsSquareFreeWord v) (huv : u.IsInfix v) : IsSquareFreeWord u

Uses 1 · Used by 1

Statement usesSquare-free finite word

Used byCrochemore's square-freeness test

TheoremSquare-freeness via prefixes of suffixes#✓fully proved

A finite word \(w\) is square-free if and only if, for every prefix \(s\) of a suffix of \(w\) and every nonempty prefix \(x\) of \(s\), we have \(s \ne xx\), where \(xx\) denotes the concatenation of \(x\) with itself.

This form is directly decidable when letter equality is decidable.

public theorem isSquareFreeWord_iff_inits_tails {α : Type*} {w : List α} :
    IsSquareFreeWord w ↔
      ∀ s ∈ w.tails.flatMap List.inits, ∀ x ∈ s.inits, x ≠ [] → s ≠ x ++ x

Uses 2

Statement usesSquare-free finite word

Proof usesSquare word

TheoremCrochemore's square-freeness test#✓fully proved

Let \(f\) map each letter of the three-letter alphabet \(\{a, b, c\}\) to a finite word over a set \(T\), and extend \(f\) to words by concatenation, \(f(x_1 \cdots x_n) = f(x_1) \cdots f(x_n)\). Then \(f\) maps every square-free word over \(\{a, b, c\}\) to a square-free word if and only if it maps every square-free word over \(\{a, b, c\}\) of length at most \(5\) to a square-free word.

A word is square-free when no factor has the form \(uu\) with \(u\) nonempty. No non-erasing hypothesis is assumed: the image of a letter may be empty.

Proof: reduce erasing morphisms first, then apply Currie's synchronization method to a shortest square occurrence and its shortest source-word cover.

public theorem crochemore_squarefree_test_set
    {T : Type*} (f : TernaryAlphabet → List T) :
    (∀ w : List TernaryAlphabet, IsSquareFreeWord w → IsSquareFreeWord (w.flatMap f)) ↔
      ∀ w : List TernaryAlphabet, w.length ≤ 5 →
        IsSquareFreeWord w → IsSquareFreeWord (w.flatMap f)

Sources

• Currie, lines 99-100 of https://cs.uwaterloo.ca/journals/JIS/VOL22/Currie/currie20.tex; primary reference Crochemore, Theoret. Comput. Sci. 18(2) (1982), DOI 10.1016/0304-3975(82)90023-8.

Uses 4

Statement usesSquare-free finite word · The ternary alphabet for square-free words

Proof usesFactors of square-free words are square-free · Square word

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.