Lax Lean Archive

Hadamard automata and Hadamard-finite series

Lax619925.Hadamard · concepts/Lax619925/Hadamard.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 series is Hadamard-finite if it lies in the Hadamard algebra generated by a finite tuple of series that is closed under left derivatives (paper §5): the Hadamard product is the pointwise product of the underlying functions, so the Hadamard algebra is just the (pointwise) ring of series. Equivalently (the coincidence), it is recognised by a Hadamard automaton (k,F,Δ)(k, F, Δ): a configuration space Q[X1,…,Xk]ℚ[X_1, …, X_k], a final-weight functional FF, and a transition ΔaΔ_a that extends to an endomorphism of the configuration space. The Hadamard-finite series form an effective prevariety, so equality and the commutativity problem are decidable for them; the equality decision reduces to ideal membership in the configuration polynomial ring (the ideal-membership statement).

    Concept map
    4 concepts; 2 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 6 statements. Each proof establishes one of them relative to its assumptions.

    1 HadamardAntiDerivativeClosure proven

    2 HadamardClosure proven

    3 HadamardCoincidence proven

    4 HadamardCommutativityDecidable proven

    5 HadamardEffectivePrevariety proven

    6 HadamardEqualityDecidable proven

    In the paper

    • page 13 of this submission's paper

    Lean source view on GitHub

    1import Lax619925.Series
    2import Lax619925.Prevariety
    3import Lax619925.Commutativity
    4import Mathlib.Data.Real.Basic
    5import Mathlib.Data.Fin.Basic
    6import Mathlib.Data.Fintype.Basic
    7import Mathlib.Data.Finset.Basic
    8import Mathlib.Algebra.MvPolynomial.Basic
    9import Mathlib.Algebra.MvPolynomial.Eval
    10import Mathlib.Algebra.Algebra.Basic
    11
    12/-!
    13---
    14title: Hadamard automata and Hadamard-finite series
    15type: theorem
    16---
    17A series is *Hadamard-finite* if it lies in the Hadamard algebra generated by a
    18finite tuple of series that is closed under left derivatives (paper §5): the
    19Hadamard product is the pointwise product of the underlying functions, so the
    20Hadamard algebra is just the (pointwise) ring of series. Equivalently (the
    21coincidence), it is recognised by a *Hadamard automaton* `(k, F, Δ)`: a
    22configuration space `ℚ[X_1, …, X_k]`, a final-weight functional `F`, and a
    23transition `Δ_a` that extends to an endomorphism of the configuration space.
    24The Hadamard-finite series form an effective prevariety, so equality and the
    25commutativity problem are decidable for them; the equality decision reduces to
    26ideal membership in the configuration polynomial ring (the ideal-membership statement).
    27-/
    28
    29namespace Lax619925.Hadamard
    30
    31open Lax619925.Series Lax619925.Prevariety Lax619925.Commutativity
    32
    33/-- The Hadamard product of two series, defined element-wise:
    34 `(hadamard f g) w = f w * g w`. It is the pointwise product of the
    35 underlying functions, hence associative, commutative, and distributive over
    36 addition, with identity the constant-1 series. -/
    37def hadamard (α : Type*) (f g : Series α) : Series α := fun w => f w * g w
    38
    39/-- The Hadamard-algebra evaluation of the polynomial `p` at the series `fs`:
    40 `hadamardEval fs p = Σ_m p m · ∏_i (fs i)^{m i}`, the interpretation of `p` in
    41 the (pointwise) ring of series, where the variable `X_i` is mapped to `fs i` and
    42 the multiplication is the Hadamard (pointwise) product. -/
    43def hadamardEval (α : Type*) (k : ℕ) (fs : Fin k → Series α) (p : MvPolynomial (Fin k) ℚ) :
    44 Series α :=
    45 fun w => p.support.sum fun m => p.coeff m * ∏ i : Fin k, (fs i) w ^ (m i)
    46
    47/-- A series is *Hadamard-finite* (working definition, paper §5) if it is a Hadamard
    48 polynomial in a finite tuple of series `fs` that is closed under left
    49 derivatives: `f = p(fs)` for some polynomial `p`, and `leftDeriv a (fs i)` is
    50 again a Hadamard polynomial in `fs` for every letter `a` and index `i`. Here
    51 `p(fs)` is the evaluation of `p` in the (pointwise) ring of series, i.e. the
    52 Hadamard algebra. -/
    53def IsHadamardFinite (α : Type*) (f : Series α) : Prop :=
    54 ∃ k : ℕ, ∃ fs : Fin k → Series α, ∃ p : MvPolynomial (Fin k) ℚ,
    55 f = hadamardEval α k fs p ∧
    56 ∀ a : α, ∀ i : Fin k, ∃ q : MvPolynomial (Fin k) ℚ,
    57 leftDeriv α a (fs i) = hadamardEval α k fs q
    58
    59/-- A *Hadamard automaton* over `α`: a dimension `k ≥ 1` (the number of
    60 nonterminals `X_1, …, X_k`), a final-weight functional `F`, and a transition
    61 `Δ` assigning to each letter `a` and nonterminal `X_i` a polynomial `Δ a i` in
    62 the nonterminals. The configuration space is the polynomial ring
    63 `ℚ[X_1, …, X_k] = MvPolynomial (Fin k) ℚ`. -/
    64structure HadamardAutomaton (α : Type*) where
    65 dim : ℕ
    66 hdim : 0 < dim
    67 F : Fin dim → ℚ
    68 Δ : α → Fin dim → MvPolynomial (Fin dim) ℚ
    69
    70/-- The word extension of the transition: `Δ_w` is the endomorphism of the
    71 configuration space obtained by composing the letter endomorphisms
    72 `aeval (Δ a)` along the word, right-to-left. `Δ_ε` is the identity and
    73 `Δ_{a·w} = Δ_w ∘ Δ_a`. -/
    74noncomputable def HadamardAutomaton.Mword {α : Type*} (A : HadamardAutomaton α) (w : List α) :
    75 MvPolynomial (Fin A.dim) ℚ → MvPolynomial (Fin A.dim) ℚ :=
    76 w.foldr (fun a φ => fun β => φ (MvPolynomial.aeval (A.Δ a) β)) id
    77
    78/-- The series recognised by the automaton at a configuration `cfg`:
    79 `⟦A⟧_cfg (w) = F(Δ_w cfg)`, the final-weight functional applied to the
    80 configuration reached after reading `w`. -/
    81noncomputable def HadamardAutomaton.sem {α : Type*} (A : HadamardAutomaton α)
    82 (cfg : MvPolynomial (Fin A.dim) ℚ) : Series α :=
    83 fun w => MvPolynomial.eval (fun i => A.F i) (A.Mword w cfg)
    84
    85/-- The series recognised by the automaton: the semantics at the initial
    86 configuration `X_0` (the first nonterminal). -/
    87noncomputable def HadamardAutomaton.recognised {α : Type*} (A : HadamardAutomaton α) :
    88 Series α :=
    89 A.sem (MvPolynomial.X (Fin.mk 0 A.hdim))
    90
    91/-- A series is *Hadamard-recognisable* if it is recognised by some Hadamard automaton. -/
    92def IsHadamardRecognisable (α : Type*) (f : Series α) : Prop :=
    93 ∃ A : HadamardAutomaton α, A.recognised = f
    94
    95/-- A series is Hadamard-finite if and only if it is Hadamard-recognisable
    96 (paper §5, the coincidence lemma). -/
    97axiom HadamardCoincidence (α : Type*) (f : Series α) :
    98 IsHadamardFinite α f ↔ IsHadamardRecognisable α f
    99
    100/-- The class of Hadamard-finite series is closed under addition, scalar
    101 multiplication, the Hadamard product, and right derivatives (paper §5, the
    102 closure lemma). These four parts hold over any alphabet. -/
    103axiom HadamardClosure (α : Type*) :
    104 (∀ (f g : Series α), IsHadamardFinite α f → IsHadamardFinite α g → IsHadamardFinite α (f + g)) ∧
    105 (∀ (c : ℚ) (f : Series α), IsHadamardFinite α f → IsHadamardFinite α (c • f)) ∧
    106 (∀ (f g : Series α), IsHadamardFinite α f → IsHadamardFinite α g → IsHadamardFinite α (hadamard α f g)) ∧
    107 (∀ (a : α) (f : Series α), IsHadamardFinite α f → IsHadamardFinite α (rightDeriv α a f))
    108
    109/-- The class of Hadamard-finite series over a *finite* alphabet is closed under left
    110 anti-derivatives (paper §5): if `g` is a left anti-derivative of a tuple `f` of
    111 Hadamard-finite series, then `g` is Hadamard-finite. The finiteness of the
    112 alphabet is essential — the witnessing generator tuple is extended by one series
    113 per letter, so it is finite only when the alphabet is. -/
    114axiom HadamardAntiDerivativeClosure (α : Type*) [Fintype α] :
    115 ∀ (g : Series α) (f : α → Series α), IsLeftAntiDerivative α g f →
    116 (∀ a, IsHadamardFinite α (f a)) → IsHadamardFinite α g
    117
    118/-- The class of Hadamard-finite series is an effective prevariety over a finite
    119 alphabet (paper §5, theorem): there is an effective prevariety whose image is
    120 exactly the Hadamard-finite series, with presentations given by Hadamard
    121 automata. -/
    122axiom HadamardEffectivePrevariety (α : Type*) [Fintype α] :
    123 ∃ P : EffectivePrevariety α, ∀ f, IsHadamardFinite α f ↔ ∃ r : P.Rep, P.sem r = f
    124
    125/-- The equality (zeroness) problem is decidable for Hadamard automata over a finite
    126 alphabet (paper §5): there is a procedure that, given a Hadamard automaton,
    127 decides whether the series it recognises is the zero series. The decision
    128 reduces to ideal membership in the configuration polynomial ring, the open
    129 leaf. -/
    130axiom HadamardEqualityDecidable (α : Type*) [Fintype α] :
    131 ∃ d : HadamardAutomaton α → Bool, ∀ A, d A = true ↔ A.recognised = 0
    132
    133/-- In particular, the commutativity problem is decidable for Hadamard-finite series
    134 over a finite alphabet (paper §5): there is a procedure that, given a Hadamard
    135 automaton, decides whether the series it recognises is commutative. This is the
    136 meta-theorem applied to the effective prevariety of Hadamard-finite series. -/
    137axiom HadamardCommutativityDecidable (α : Type*) [Fintype α] :
    138 ∃ d : HadamardAutomaton α → Bool, ∀ A, d A = true ↔ IsCommutative α (A.recognised)
    139
    140end Lax619925.Hadamard
    141
    Show ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…