Cobham's theorems on recognizable sets

DefinitionValue of a base-k digit word#✓fully proved

The value of a word \(w = d_1 d_2 \cdots d_m\) of base-\(k\) digits \(d_i \in \{0, \dots, k - 1\}\), read with the most significant digit first, is \(\sum_{i=1}^{m} d_i k^{m-i}\). The empty word has value \(0\).

def baseWordValue {k : ℕ} (w : List (Fin k)) : ℕ :=
  w.foldl (fun value digit ↦ value * k + digit.val) 0
Used by 3
Used byCobham's theorem · Cobham's gap theorem without a separate base hypothesis · Sets recognizable in base k

DefinitionCanonical base-k words#✓fully proved

A word of base-\(k\) digits is canonical when it is empty or its first (most significant) digit is nonzero.

def IsCanonicalBaseWord {k : ℕ} : List (Fin k) → Prop
  | [] => True
  | digit :: _ => digit.val ≠ 0
Used by 3
Used byCobham's theorem · Cobham's gap theorem without a separate base hypothesis · Sets recognizable in base k

DefinitionSets recognizable in base k#✓fully proved

For a natural number \(k\), a set \(S\) of natural numbers is recognizable in base \(k\) when \(k \ge 2\) and some deterministic finite automaton with a nonempty finite set of states, reading words of base-\(k\) digits from the most significant digit, accepts a word \(w = d_1 d_2 \cdots d_m\) exactly when \(w\) is canonical (empty, or with \(d_1 \neq 0\)) and its value \(\sum_{i=1}^{m} d_i k^{m-i}\) lies in \(S\).

def IsBaseRecognizable (k : ℕ) (S : Set ℕ) : Prop :=
  2 ≤ k ∧
    ∃ numStates : ℕ, 0 < numStates ∧
      ∃ init : Fin numStates,
        ∃ transition : Fin numStates → Fin k → Fin numStates,
          ∃ accept : Fin numStates → Bool,
            ∀ w : List (Fin k),
              (accept (w.foldl transition init) = true ↔
                IsCanonicalBaseWord w ∧ baseWordValue w ∈ S)
Uses 2 · Used by 4
Statement usesCanonical base-k words · Value of a base-k digit word
Used byCobham's theorem · Cobham's theorem for characteristic sequences · Cobham's gap theorem · Cobham's gap theorem without a separate base hypothesis

DefinitionBase-k expansion#✓fully proved

For a natural number \(k \ge 2\) and a natural number \(n\), the base-\(k\) expansion of \(n\) is the word \(d_1 d_2 \cdots d_m\) of base-\(k\) digits, most significant digit first, with \(n = \sum_{i=1}^{m} d_i k^{m-i}\) and \(d_1 \neq 0\); for \(n = 0\) it is the empty word.

def baseDigits {k : ℕ} (hk : 2 ≤ k) (n : ℕ) : List (Fin k) :=
  (Nat.digits k n).reverse.map fun d ↦ ⟨d % k, Nat.mod_lt _ (by omega)⟩
Used by 2
Used byCobham's theorem · Cobham's gap theorem without a separate base hypothesis

DefinitionMultiplicatively independent bases#✓fully proved

Two natural numbers \(k\) and \(l\) are multiplicatively independent when \(k^m \ne l^n\) for all positive natural numbers \(m\) and \(n\).

def BasesMultiplicativelyIndependent (k l : ℕ) : Prop :=
  ∀ m n : ℕ, 0 < m → 0 < n → k ^ m ≠ l ^ n
Used by 2
Used byCobham's theorem · Cobham's theorem for characteristic sequences

DefinitionUltimately periodic sets of natural numbers#✓fully proved

A set \(S\) of natural numbers is ultimately periodic when there are natural numbers \(N\) and \(p > 0\) such that, for every \(n \ge N\), \(n \in S\) if and only if \(n + p \in S\).

def IsUltimatelyPeriodicSet (S : Set ℕ) : Prop :=
  ∃ N p : ℕ, 0 < p ∧ ∀ n : ℕ, N ≤ n → (n ∈ S ↔ n + p ∈ S)
Used by 3
Used byCobham's theorem · Cobham's theorem for characteristic sequences · Ultimately periodic sets and their characteristic sequences

TheoremCobham's theorem#✓fully proved

Let \(k\) and \(l\) be multiplicatively independent natural numbers with \(l \ge 2\), and let \(S\) be a set of natural numbers that is recognizable in base \(k\) and is not ultimately periodic. Then \(S\) is not recognizable in base \(l\).

public theorem cobham_base_dependence {k l : ℕ} {S : Set ℕ}
    (hl : 2 ≤ l)
    (hindependent : BasesMultiplicativelyIndependent k l)
    (hrecognizable : IsBaseRecognizable k S)
    (haperiodic : ¬ IsUltimatelyPeriodicSet S) :
    ¬ IsBaseRecognizable l S
Sources
  • proved via T. J. P. Krebs, A more reasonable proof of Cobham's theorem, arXiv:1801.06704, Section 3.
  • T. Kärki, A. Lacroix, and M. Rigo, On the Recognizability of Self-Generating Sets, especially the remark invoking Cobham's theorem: https://cs.uwaterloo.ca/journals/JIS/VOL13/Rigo/rigo6.tex.
Uses 6 · Used by 1
Statement usesMultiplicatively independent bases · Sets recognizable in base k · Ultimately periodic sets of natural numbers
Proof usesCanonical base-k words · Base-k expansion · Value of a base-k digit word
Used byCobham's theorem for characteristic sequences

TheoremUltimately periodic sets and their characteristic sequences#✓fully proved

A set \(S\) of natural numbers is ultimately periodic if and only if its characteristic sequence \(n \mapsto (n \in S)\), a sequence of truth values, is ultimately periodic.

public theorem isUltimatelyPeriodicSet_iff_isUltimatelyPeriodic (S : Set ℕ) :
    IsUltimatelyPeriodicSet S ↔ IsUltimatelyPeriodic (fun n => n ∈ S)
Uses 2 · Used by 1
Statement usesUltimately periodic sequences · Ultimately periodic sets of natural numbers
Used byCobham's theorem for characteristic sequences

TheoremCobham's theorem for characteristic sequences#✓fully proved

Let \(k\) and \(l\) be multiplicatively independent natural numbers with \(l \ge 2\), and let \(S\) be a set of natural numbers that is recognizable in base \(k\) and whose characteristic sequence \(n \mapsto (n \in S)\), a sequence of truth values, is not ultimately periodic. Then \(S\) is not recognizable in base \(l\).

public theorem cobham_base_dependence_isUltimatelyPeriodic {k l : ℕ} {S : Set ℕ}
    (hl : 2 ≤ l)
    (hindependent : BasesMultiplicativelyIndependent k l)
    (hrecognizable : IsBaseRecognizable k S)
    (haperiodic : ¬ IsUltimatelyPeriodic (fun n => n ∈ S)) :
    ¬ IsBaseRecognizable l S
Uses 6
Statement usesMultiplicatively independent bases · Sets recognizable in base k · Ultimately periodic sequences
Proof usesUltimately periodic sets of natural numbers · Cobham's theorem · Ultimately periodic sets and their characteristic sequences

TheoremCobham's gap theorem without a separate base hypothesis#✓fully proved

Let \(k\) be a natural number and let \(x_0 < x_1 < x_2 < \cdots\) be a strictly increasing sequence of natural numbers whose set of values is recognizable in base \(k\). Then either the limit superior, as \(i \to \infty\), of the ratios \(x_{i+1} / x_i\) computed in the extended nonnegative reals \([0, \infty]\) (where a ratio with denominator \(0\) is \(\infty\)) is greater than \(1\), or there is a natural number \(C\) with \(x_{i+1} - x_i \le C\) for every \(i\).

Recognizability in base \(k\) already requires \(k \ge 2\), so no separate hypothesis on \(k\) is needed.

theorem cobham_gap_theorem_general {k : ℕ} {x : ℕ → ℕ}
    (hx : StrictMono x)
    (hX : IsBaseRecognizable k (Set.range x)) :
    Filter.limsup
      (fun i => ((x (i + 1) : ENNReal) / (x i : ENNReal)))
    Filter.atTop > 1 ∨
    ∃ C : ℕ, ∀ i : ℕ, x (i + 1) - x i ≤ C
Uses 4 · Used by 1
Statement usesSets recognizable in base k
Proof usesCanonical base-k words · Base-k expansion · Value of a base-k digit word
Used byCobham's gap theorem

TheoremCobham's gap theorem#✓fully proved

Let \(k \ge 2\) be a natural number and let \(x_0 < x_1 < x_2 < \cdots\) be a strictly increasing sequence of natural numbers whose set of values is recognizable in base \(k\). Then either the limit superior, as \(i \to \infty\), of the ratios \(x_{i+1} / x_i\) computed in the extended nonnegative reals \([0, \infty]\) (so an unbounded limit superior is \(\infty\), and a ratio with denominator \(0\) is \(\infty\)) is greater than \(1\), or there is a natural number \(C\) with \(x_{i+1} - x_i \le C\) for every \(i\).

theorem cobham_gap_theorem {k : ℕ} {x : ℕ → ℕ}
    (hx : StrictMono x)
    (hk : 2 ≤ k)
    (hX : IsBaseRecognizable k (Set.range x)) :
    Filter.limsup
      (fun i => ((x (i + 1) : ENNReal) / (x i : ENNReal)))
    Filter.atTop > 1 ∨
    ∃ C : ℕ, ∀ i : ℕ, x (i + 1) - x i ≤ C
Sources
Uses 2
Statement usesSets recognizable in base k
Proof usesCobham's gap theorem without a separate base hypothesis
11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.