Documentation

TauCeti.Computability.AutomaticSequence

Automatic sequences #

For a base k, a sequence a : β„• β†’ Ξ” is k-automatic if some deterministic automaton with output (TauCeti.DFAO) with finitely many states and input alphabet Fin k computes a n from the base-k digits of n. The digits are Mathlib's Nat.digits k n, read least significant digit first and without padding zeros. Reading the least significant digit first is the convention that Bridy (Section 2.1) calls reverse reading and that Christol, Kamae, MendΓ¨s France and Rauzy (Section 4) call lecture inverse. Automatic sequences are the subject of Christol's theorem, which identifies the p-automatic sequences with values in 𝔽_p, for a prime p, with the coefficient sequences of the power series over 𝔽_p algebraic over 𝔽_p(X), and of Cobham's theorem, which identifies the sequences automatic in two multiplicatively independent bases with the eventually periodic ones.

The output alphabet is arbitrary; automaticity forces the range of the sequence to be finite. The definition is made for every k β‰  0. For k = 1, Nat.digits 1 n is the unary word of length n, and the constructions below cover this case too.

Main definitions and results #

Implementation notes #

For an eventually periodic sequence with preperiod N and period p, the automaton keeps the value of the digits read so far and the current place value k ^ i, each only through its truncation min Β· N and its residue modulo p. Both are compatible with addition and with multiplication by a natural number, and together they determine the value of the sequence.

References #

source
def TauCeti.IsAutomatic (k : β„•) [NeZero k] {Ξ” : Type u} (a : β„• β†’ Ξ”) :
Prop

A sequence a : β„• β†’ Ξ” is k-automatic if a deterministic automaton with output, with finitely many states and input alphabet Fin k, outputs a n on the base-k digits of n, read least significant digit first (Mathlib's Nat.digits k n, so 0 is the empty word).

Instances For
    source
    theorem TauCeti.isAutomatic_iff {k : β„•} [NeZero k] {Ξ” : Type u} {a : β„• β†’ Ξ”} :
    IsAutomatic k a ↔ βˆƒ (Οƒ : Type) (x : Fintype Οƒ) (M : DFAO (Fin k) Οƒ Ξ”), βˆ€ (n : β„•), a n = M.output (M.eval (List.map (Fin.ofNat k) (k.digits n)))

    Unfolding IsAutomatic: the introduction and elimination rule.

    source
    theorem TauCeti.DFAO.isAutomatic {k : β„•} [NeZero k] {Ξ” : Type u} {Οƒ : Type u_1} [Finite Οƒ] (M : DFAO (Fin k) Οƒ Ξ”) :
    IsAutomatic k fun (n : β„•) => M.output (M.eval (List.map (Fin.ofNat k) (k.digits n)))

    The sequence computed by an automaton with finitely many states on base-k digits is k-automatic. The states may live in any universe: they are relabelled by a Fin type.

    source
    theorem TauCeti.IsAutomatic.map {k : β„•} [NeZero k] {Ξ” : Type u} {Ξ”' : Type v} {a : β„• β†’ Ξ”} (ha : IsAutomatic k a) (f : Ξ” β†’ Ξ”') :
    IsAutomatic k fun (n : β„•) => f (a n)

    Changing the values of a k-automatic sequence along any map keeps it k-automatic.

    source
    theorem TauCeti.IsAutomatic.prodMk {k : β„•} [NeZero k] {Ξ” : Type u} {Ξ”' : Type v} {a : β„• β†’ Ξ”} {b : β„• β†’ Ξ”'} (ha : IsAutomatic k a) (hb : IsAutomatic k b) :
    IsAutomatic k fun (n : β„•) => (a n, b n)

    The pairing of two k-automatic sequences is k-automatic.

    source
    theorem TauCeti.IsAutomatic.finite_range {k : β„•} [NeZero k] {Ξ” : Type u} {a : β„• β†’ Ξ”} (ha : IsAutomatic k a) :
    (Set.range a).Finite

    A k-automatic sequence takes only finitely many values.

    source
    theorem TauCeti.isAutomatic_const {k : β„•} [NeZero k] {Ξ” : Type u} (c : Ξ”) :
    IsAutomatic k fun (x : β„•) => c

    Constant sequences are k-automatic, computed by a one-state automaton.

    Eventually periodic sequences #

    source
    theorem TauCeti.isAutomatic_of_eventually_periodic {k : β„•} [NeZero k] {Ξ” : Type u} {a : β„• β†’ Ξ”} {N p : β„•} (hp : 0 < p) (h : βˆ€ (n : β„•), N ≀ n β†’ a (n + p) = a n) :
    IsAutomatic k a

    Eventually periodic sequences are automatic. A sequence a with a (n + p) = a n for all n β‰₯ N, for some period p > 0, is k-automatic in every base k.

    Checks #