Lax Lean Archive

Polynomial automata and Hadamard automata

Lax619925.PolynomialAutomata · concepts/Lax619925/PolynomialAutomata.lean · lax-619925

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    A polynomial automaton (paper appendix) is a weighted automaton whose configuration space is the vector space Qkℚ^k and whose letter actions are polynomial maps. It is the dual of the Hadamard automaton: here the configuration is a point and the final weight is a polynomial, whereas the Hadamard automaton's configuration is a polynomial and its final weight is a point. The main result (paper appendix) is that a series is recognisable by a polynomial automaton if and only if its reversal is Hadamard-recognisable: the duality swaps the configuration and the final weight, and the reversal accounts for the order in which the transitions are composed.

    Concept map
    5 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 39 of this submission's paper

    Lean source view on GitHub

    1import Lax619925.Series
    2import Lax619925.Hadamard
    3import Mathlib.Data.Real.Basic
    4import Mathlib.Data.Fin.Basic
    5import Mathlib.Data.Fintype.Basic
    6import Mathlib.Algebra.MvPolynomial.Basic
    7import Mathlib.Algebra.MvPolynomial.Eval
    8
    9/-!
    10---
    11title: Polynomial automata and Hadamard automata
    12type: theorem
    13---
    14A *polynomial automaton* (paper appendix) is a weighted automaton whose
    15configuration space is the vector space `ℚ^k` and whose letter actions are
    16polynomial maps. It is the dual of the Hadamard automaton: here the
    17configuration is a *point* and the final weight is a *polynomial*, whereas the
    18Hadamard automaton's configuration is a *polynomial* and its final weight is a
    19*point*. The main result (paper appendix) is that a series is recognisable by a
    20polynomial automaton if and only if its reversal is Hadamard-recognisable: the
    21duality swaps the configuration and the final weight, and the reversal accounts
    22for the order in which the transitions are composed.
    23-/
    24
    25namespace Lax619925.PolynomialAutomata
    26
    27open Lax619925.Series Lax619925.Hadamard
    28
    29/-- A *polynomial automaton* over `α`: a dimension `k ≥ 1`, an initial
    30 configuration `qI : ℚ^k`, a final polynomial `F : ℚ[X_1, …, X_k]`, and a
    31 transition `Δ` assigning to each letter `a` a polynomial map
    32 `Δ_a : ℚ^k → ℚ^k` (a `k`-tuple of polynomials). The configuration space is
    33 the vector space `ℚ^k`, and the letter action is `q · a = Δ_a(q)` (evaluate
    34 the transition polynomials at the point `q`). -/
    35structure PolynomialAutomaton (α : Type*) where
    36 dim : ℕ
    37 hdim : 0 < dim
    38 qI : Fin dim → ℚ
    39 F : MvPolynomial (Fin dim) ℚ
    40 Δ : α → Fin dim → MvPolynomial (Fin dim) ℚ
    41
    42/-- The action of a letter `a` on a configuration `q`: `q · a = Δ_a(q)`,
    43 evaluate the transition polynomials at the point `q`. -/
    44noncomputable def PolynomialAutomaton.action {α : Type*} (A : PolynomialAutomaton α)
    45 (q : Fin A.dim → ℚ) (a : α) : Fin A.dim → ℚ :=
    46 fun i => MvPolynomial.eval q (A.Δ a i)
    47
    48/-- The action of a word `w` on a configuration `q`: `q · w`, the letter actions
    49 iterated left-to-right. -/
    50noncomputable def PolynomialAutomaton.wordAction {α : Type*} (A : PolynomialAutomaton α)
    51 (q : Fin A.dim → ℚ) (w : List α) : Fin A.dim → ℚ :=
    52 w.foldl (fun q a => A.action q a) q
    53
    54/-- The series recognised by the automaton at a configuration `q`:
    55 `⟦A⟧_q (w) = F(q · w)`, the final polynomial `F` evaluated at the point
    56 `q · w` reached after reading `w`. -/
    57noncomputable def PolynomialAutomaton.sem {α : Type*} (A : PolynomialAutomaton α)
    58 (q : Fin A.dim → ℚ) : Series α :=
    59 fun w => MvPolynomial.eval (A.wordAction q w) A.F
    60
    61/-- The series recognised by the automaton: the semantics at the initial
    62 configuration `qI`. -/
    63noncomputable def PolynomialAutomaton.recognised {α : Type*} (A : PolynomialAutomaton α) : Series α :=
    64 A.sem A.qI
    65
    66/-- A series is *polynomial-recognisable* if it is recognised by some polynomial
    67 automaton. -/
    68def IsPolynomialRecognisable (α : Type*) (f : Series α) : Prop :=
    69 ∃ A : PolynomialAutomaton α, A.recognised = f
    70
    71/-- A series is recognisable by a polynomial automaton if and only if its
    72 reversal is Hadamard-recognisable (paper appendix). The duality swaps the
    73 configuration (point ↔ polynomial) and the final weight (polynomial ↔
    74 point), and the reversal accounts for the order of composition of the
    75 transitions. -/
    76axiom PolynomialHadamardEquivalence (α : Type*) (f : Series α) :
    77 IsPolynomialRecognisable α f ↔ IsHadamardRecognisable α (reversal α f)
    78
    79end Lax619925.PolynomialAutomata
    80
    Show Proof
    Builds on
    Used by

    none

    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…