Morphic words

DefinitionExtension of a letter map to finite words#✓fully proved

Given a map \(f\) sending each letter of an alphabet \(A\) to a finite word over \(A\), its extension to finite words sends a word \(a_1 a_2 \cdots a_m\) over \(A\) to the concatenation \(f(a_1) f(a_2) \cdots f(a_m)\) of the images of its letters in order; the empty word is sent to the empty word.

public def morphExtend {A : Type*} (f : A → List A) (w : List A) : List A :=
  w.flatMap f

Used by 7

Used byUniform fixed-point codings via iterates of a uniform map · Dumont–Thomas numeration · Each Kimberling block is a prefix of the next · Lower bound on the length of the Kimberling blocks · Extended letter maps preserve concatenation · Iterates of a letter map · Length of iterates of a uniform letter map

DefinitionIterates of a letter map#✓fully proved

Let \(f\) send each letter of an alphabet \(A\) to a finite word over \(A\), extended to finite words by concatenation. The iterates of \(f\) on finite words over \(A\) are defined by \(f^0(w) = w\) and \(f^{n+1}(w) = f(f^n(w))\) for every finite word \(w\) over \(A\) and every natural number \(n\).

public def morphIterate {A : Type*} (f : A → List A) : Nat → List A → List A
  | 0, w => w
  | n + 1, w => morphExtend f (morphIterate f n w)

Uses 1 · Used by 26

Statement usesExtension of a letter map to finite words

Used byUniform fixed-point codings via iterates of a uniform map · Weighted length of an admissible sequence · Dumont–Thomas numeration · Dumont–Thomas numeration for left-infinite periodic points · Dumont–Thomas numeration for right-infinite periodic points · Quotient and remainder for negative positions · Quotient and remainder for positive Dumont–Thomas representations · Proper prefixes of iterated images have unique admissible expansions · Dumont–Thomas complement representations · Dumont–Thomas representation of minus one · A Dumont–Thomas representation of zero · Substitutions are non-erasing · Two-sided periodic points with growing seed · Substitutions in the sense of Labbé and Lepšová · Two-sided periodic points · Periodic points with growing seed are two-sided periodic points · Admissible sequences are determined by their weighted length · Letters of an iterated image are read by the automaton · Periods of two-sided periodic points are positive · Decomposition of a proper prefix of an iterated image · Tails are injective and order-preserving · Kimberling's blocks · Infinite word as the limit of iterates · Prolongable letter maps · Length of iterates of a uniform letter map · A prefix of the fourth iterate of \(f_1\)

TheoremExtended letter maps preserve concatenation#✓fully proved

Let \(f\) send each letter of an alphabet \(A\) to a finite word over \(A\), extended to finite words by concatenation. Then \(f(uv) = f(u)f(v)\) for all finite words \(u\) and \(v\) over \(A\).

public theorem morphExtend_append {A : Type*} (f : A → List A) (u v : List A) :
    morphExtend f (u ++ v) = morphExtend f u ++ morphExtend f v

Uses 1 · Used by 1

Statement usesExtension of a letter map to finite words

Used byEach Kimberling block is a prefix of the next

TheoremLength of iterates of a uniform letter map#✓fully proved

Let \(k\) be a natural number and let \(f\) send each letter of an alphabet \(A\) to a word of length exactly \(k\) over \(A\), extended to finite words by concatenation, with iterates \(f^n\) (where \(f^0\) is the identity). Then for every natural number \(n\) and every finite word \(w\) over \(A\), the word \(f^n(w)\) has length \(k^n\) times the length of \(w\).

public theorem morphIterate_length_of_uniform {A : Type*} {k : Nat} {f : A → List A}
    (hlen : ∀ x, (f x).length = k) (n : Nat) (w : List A) :
    (morphIterate f n w).length = k ^ n * w.length

Uses 2 · Used by 1

Statement usesIterates of a letter map

Proof usesExtension of a letter map to finite words

Used byUniform fixed-point codings via iterates of a uniform map

DefinitionNon-erasing letter maps#✓fully proved

A map \(f\) sending each letter of an alphabet \(A\) to a finite word over \(A\) is non-erasing when the word \(f(a)\) is nonempty for every letter \(a \in A\).

public def IsNonErasing {A : Type*} (f : A → List A) : Prop :=
  ∀ a : A, f a ≠ []

Used by 2

Used bySubstitutions are non-erasing · Substitutions in the sense of Labbé and Lepšová

DefinitionProlongable letter maps#✓fully proved

Let \(f\) send each letter of an alphabet \(A\) to a finite word over \(A\), extended to finite words by concatenation, with iterates \(f^n\) (where \(f^0\) is the identity). Then \(f\) is prefix-preserving (prolongable) at a letter \(a \in A\) when \(f(a) = a\alpha\) for some finite word \(\alpha\) over \(A\) such that the word \(f^n(\alpha)\) is nonempty for every natural number \(n\), including \(n = 0\).

public def IsPrefixPreserving {A : Type*} (f : A → List A) (a : A) : Prop :=
  ∃ α : List A, f a = a :: α ∧ ∀ n : Nat, morphIterate f n α ≠ []

Uses 1 · Used by 3

Statement usesIterates of a letter map

Used byUniform fixed-point codings are morphic · Uniform fixed-point codings via iterates of a uniform map · Pure morphic words

DefinitionInfinite word as the limit of iterates#✓fully proved

Let \(f\) send each letter of an alphabet \(A\) to a finite word over \(A\), extended to finite words by concatenation, with iterates \(f^n\) (where \(f^0\) is the identity), let \(a \in A\), and let \(w = w_0 w_1 w_2 \cdots\) be an infinite word over \(A\). Then \(w\) is the limit of the iterates of \(f\) at \(a\) when the lengths of the words \(f^n(a)\) (iterates applied to the one-letter word \(a\)) are unbounded as \(n\) ranges over the natural numbers, and for every \(n\) and every position \(i\) of \(f^n(a)\), counted from \(0\), the letter of \(f^n(a)\) at position \(i\) is \(w_i\).

public def IsOmegaLimit {A : Type*} (f : A → List A) (a : A) (w : Nat → A) : Prop :=
  (∀ M : Nat, ∃ n : Nat, M ≤ (morphIterate f n [a]).length) ∧
    ∀ n : Nat, ∀ i : Nat, ∀ h : i < (morphIterate f n [a]).length,
      GetElem.getElem (morphIterate f n [a]) i h = w i

Uses 1 · Used by 7

Statement usesIterates of a letter map

Used byUniform fixed-point codings are morphic · Uniform fixed-point codings via iterates of a uniform map · Gutkovskiy's sequence modulo 2 is generated by a morphism · Pure morphic words · Morphic coding of the Wythoff mex pairs at level one · Morphic coding of the Wythoff mex pairs at level three · Morphic coding of the Wythoff mex pairs at level two

DefinitionPure morphic words#✓fully proved

An infinite word \(w\) over a finite alphabet \(A\) is pure morphic when there are a map \(f\) sending each letter of \(A\) to a finite word over \(A\) and a letter \(a \in A\) such that \(f\) is prolongable at \(a\) and \(w\) is the limit of the iterates of \(f\) at \(a\).

No coding is applied to the limit, and \(f\) is not required to be non-erasing on every letter.

public def IsPureMorphic {A : Type*} [Finite A] (w : Nat → A) : Prop :=
  ∃ (f : A → List A) (a : A), IsPrefixPreserving f a ∧ IsOmegaLimit f a w

Uses 2 · Used by 6

Statement usesInfinite word as the limit of iterates · Prolongable letter maps

Used byUniform fixed-point codings are morphic · A morphic word is the coding of its generator · Building a morphic word from its generator · Morphic words via a coding · Pure morphic words are morphic · The generator of a morphic word is pure morphic

DefinitionMorphic words via a coding#✓fully proved

Let \(A\) be a finite alphabet, \(B\) any alphabet, \(u\) an infinite word over \(A\), \(\tau : A \to B\) a map (a coding) and \(w\) an infinite word over \(B\). Then \(w\) is morphic with generator \(u\) and coding \(\tau\) if \(u\) is a pure morphic word and \(w(n) = \tau(u(n))\) for every \(n \in \mathbb{N}\).

public def IsMorphic {A B : Type*} [Finite A] (u : Nat → A) (coding : A → B) (w : Nat → B) : Prop :=
  IsPureMorphic u ∧ ∀ n, w n = coding (u n)

Uses 1 · Used by 6

Statement usesPure morphic words

Used byUniform fixed-point codings are morphic · Automatic sequences are morphic · A morphic word is the coding of its generator · Building a morphic word from its generator · Pure morphic words are morphic · The generator of a morphic word is pure morphic

TheoremBuilding a morphic word from its generator#✓fully proved

Let \(A\) be a finite alphabet, \(u\) a pure morphic infinite word over \(A\), \(\tau : A \to B\) a map and \(w\) an infinite word over \(B\). If \(w(n) = \tau(u(n))\) for every \(n \in \mathbb{N}\), then \(w\) is morphic with generator \(u\) and coding \(\tau\).

public theorem IsMorphic.intro {A B : Type*} [Finite A] {u : Nat → A} {coding : A → B}
    {w : Nat → B} (hPure : IsPureMorphic u)
    (hCode : ∀ n, w n = coding (u n)) : IsMorphic u coding w

Uses 2

Statement usesMorphic words via a coding · Pure morphic words

TheoremThe generator of a morphic word is pure morphic#✓fully proved

Let \(A\) be a finite alphabet, \(u\) an infinite word over \(A\), \(\tau : A \to B\) a map and \(w\) an infinite word over \(B\). If \(w\) is morphic with generator \(u\) and coding \(\tau\), then \(u\) is a pure morphic word.

public theorem IsMorphic.pure {A B : Type*} [Finite A] {u : Nat → A} {coding : A → B}
    {w : Nat → B} (h : IsMorphic u coding w) : IsPureMorphic u

Uses 2

Statement usesMorphic words via a coding · Pure morphic words

TheoremA morphic word is the coding of its generator#✓fully proved

Let \(A\) be a finite alphabet, \(u\) an infinite word over \(A\), \(\tau : A \to B\) a map and \(w\) an infinite word over \(B\). If \(w\) is morphic with generator \(u\) and coding \(\tau\), then \(w(n) = \tau(u(n))\) for every \(n \in \mathbb{N}\).

public theorem IsMorphic.coding_eq {A B : Type*} [Finite A] {u : Nat → A} {coding : A → B}
    {w : Nat → B} (h : IsMorphic u coding w) (n : Nat) : w n = coding (u n)

Uses 2

Statement usesMorphic words via a coding

Proof usesPure morphic words

TheoremPure morphic words are morphic#✓fully proved

Let \(A\) be a finite alphabet and \(u\) a pure morphic infinite word over \(A\). Then \(u\) is morphic with generator \(u\) and the identity coding of \(A\).

public theorem IsMorphic.ofPureMorphic {A : Type*} [Finite A] {u : Nat → A}
    (hu : IsPureMorphic u) : IsMorphic u id u

Uses 2

Statement usesMorphic words via a coding · Pure morphic words

13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.