Lax Lean Archive

Shuffle automata and shuffle-finite series

Lax619925.Shuffle · concepts/Lax619925/Shuffle.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 shuffle-finite if it belongs to a finitely generated differential shuffle algebra (paper §6.2.2): it is a shuffle polynomial in a finite tuple of series that is closed under left derivatives. Equivalently (the coincidence), it is recognised by a shuffle 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 a derivation of the configuration space (the paper's differential- algebra structure, §6). The shuffle-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), via the same ideal-chain argument as for the Hadamard and infiltration automata.

    Concept map
    4 concepts; 1 descendant 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 ShuffleAntiDerivativeClosure proven

    2 ShuffleClosure proven

    3 ShuffleCoincidence proven

    4 ShuffleCommutativityDecidable proven

    5 ShuffleEffectivePrevariety proven

    6 ShuffleEqualityDecidable proven

    In the paper

    • page 24 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.Data.Finsupp.Basic
    9import Mathlib.Algebra.MvPolynomial.Basic
    10import Mathlib.Algebra.MvPolynomial.Eval
    11
    12/-!
    13---
    14title: Shuffle automata and shuffle-finite series
    15type: theorem
    16---
    17A series is *shuffle-finite* if it belongs to a finitely generated differential
    18shuffle algebra (paper §6.2.2): it is a shuffle polynomial in a finite tuple of
    19series that is closed under left derivatives. Equivalently (the coincidence),
    20it is recognised by a *shuffle automaton* `(k, F, Δ)`: a configuration space
    21`ℚ[X_1, …, X_k]`, a final-weight functional `F`, and a transition `Δ_a` that
    22extends to a *derivation* of the configuration space (the paper's differential-
    23algebra structure, §6). The shuffle-finite series form an effective prevariety,
    24so equality and the commutativity problem are decidable for them; the equality
    25decision reduces to ideal membership in the configuration polynomial ring (the
    26ideal-membership statement), via the same ideal-chain argument as for the Hadamard and
    27infiltration automata.
    28-/
    29
    30namespace Lax619925.Shuffle
    31
    32open Lax619925.Series Lax619925.Prevariety Lax619925.Commutativity
    33
    34/-- The recursive core of the shuffle product, defined by primitive recursion on the
    35 word: `(f ⧢ g) ε = f ε · g ε` and
    36 `(f ⧢ g) (a·w) = ((leftDeriv a f) ⧢ g) w + (f ⧢ (leftDeriv a g)) w`, the Leibniz
    37 rule. This is the unique series satisfying the characterisation. The recursion
    38 measure is the word length (the series arguments `f`, `g` change at each step, so
    39 structural recursion on the word alone does not apply). -/
    40noncomputable def shuffleRec (α : Type*) (f g : Series α) (w : List α) : ℚ :=
    41 match w with
    42 | [] => f [] * g []
    43 | a :: w' => shuffleRec α (leftDeriv α a f) g w' + shuffleRec α f (leftDeriv α a g) w'
    44 termination_by w.length
    45
    46/-- The shuffle product of two series, characterised by the Leibniz rule
    47 `leftDeriv a (f ⧢ g) = (leftDeriv a f) ⧢ g + f ⧢ (leftDeriv a g)` and the
    48 initial condition `(f ⧢ g) ε = f ε · g ε`. Equivalently,
    49 `(f ⧢ g) w = Σ_{u·v = w} f u · g v`, the sum over all interleavings of `u`
    50 and `v` that yield `w`. -/
    51noncomputable def shuffle (α : Type*) (f g : Series α) : Series α :=
    52 fun w => shuffleRec α f g w
    53
    54/-- The unit of the shuffle product: the delta series, `1` on the empty word and `0`
    55 elsewhere. Unlike the constant-`1` series (the unit of the pointwise product), the
    56 delta series is the unit of the *shuffle* product. -/
    57def shuffleUnit (α : Type*) : Series α := fun w => if w = [] then 1 else 0
    58
    59/-- The `n`-fold iterated shuffle power of `f`: `shufflePow α f 0 = shuffleUnit α` (the
    60 shuffle unit) and `shufflePow α f (n+1) = f ⧢ shufflePow α f n`. This is the shuffle
    61 analogue of the pointwise power `f ^ n` used in `hadamardEval`. -/
    62noncomputable def shufflePow (α : Type*) (f : Series α) (n : ℕ) : Series α :=
    63 match n with
    64 | 0 => shuffleUnit α
    65 | n + 1 => shuffle α f (shufflePow α f n)
    66
    67/-- The shuffle product of the iterated shuffle powers `fs 0 ⧢^[d 0] ⧢ ⋯ ⧢ fs (k-1) ⧢^[d (k-1)]`,
    68 where `⧢` is the shuffle product and `⧢^[n]` is the iterated shuffle power
    69 (`shufflePow`). This is the shuffle analogue of the pointwise monomial product
    70 `∏ i, (fs i) ^ (d i)` used in `hadamardEval`; it is the shuffle fold of the
    71 commutative-associative shuffle operation over all indices (the zero-exponent terms
    72 contribute the shuffle unit, which is the identity). It is computed as a right-fold
    73 over the index list, so that the definition does not depend on the `Std.Commutative`/
    74 `Std.Associative` instances (which the axiom-free concept package cannot carry); the
    75 proof package shows it equals the corresponding `Finset.fold` (`shuffleProd_eq_fold`). -/
    76noncomputable def shuffleProd (α : Type*) (k : ℕ) (fs : Fin k → Series α) (d : Fin k →₀ ℕ) : Series α :=
    77 (((Finset.univ : Finset (Fin k)).toList).map (fun i => shufflePow α (fs i) (d i))).foldr
    78 (fun x acc => shuffle α x acc) (shuffleUnit α)
    79
    80/-- The evaluation of the polynomial `p` in the *shuffle* algebra, sending `X_i` to
    81 `fs i`: `shuffleEval α k fs p = ∑ d ∈ p.support, p.coeff d · (fs 0 ⧢^[d 0] ⧢ ⋯ ⧢
    82 fs (k-1) ⧢^[d (k-1)])`, where `⧢` is the shuffle product and `⧢^[n]` is the iterated
    83 shuffle power. This is the shuffle analogue of `hadamardEval` (which evaluates in the
    84 pointwise ring); because the shuffle ring cannot be a `CommRing` instance on `Series α`
    85 (which already carries the pointwise ring), it is defined directly as the sum over the
    86 polynomial's support of the coefficients times the shuffle product of the iterated
    87 powers. -/
    88noncomputable def shuffleEval (α : Type*) (k : ℕ) (fs : Fin k → Series α)
    89 (p : MvPolynomial (Fin k) ℚ) : Series α :=
    90 p.support.sum fun m => p.coeff m • shuffleProd α k fs m
    91
    92/-- The unique derivation of the polynomial ring `MvPolynomial σ R` sending the
    93 variable `X i` to `φ i`, defined by the Leibniz rule on monomials:
    94 `δ_φ(X^m) = Σ_i m_i · X^{m - e_i} · φ i`. This is the extension of the
    95 letter transition `Δ_a` (a map on the variables) to a derivation of the whole
    96 configuration space. -/
    97noncomputable def derivationExt {σ : Type*} [Fintype σ] {R : Type*} [CommRing R]
    98 (φ : σ → MvPolynomial σ R) : MvPolynomial σ R → MvPolynomial σ R :=
    99 fun p => p.support.sum fun m =>
    100 p.coeff m • (∑ i : σ, ((m i : R) • MvPolynomial.monomial (m - Finsupp.single i 1) 1) * φ i)
    101
    102/-- A *shuffle automaton* over `α`: a dimension `k ≥ 1` (the number of
    103 nonterminals `X_1, …, X_k`), a final-weight functional `F`, and a transition
    104 `Δ` assigning to each letter `a` and nonterminal `X_i` a polynomial `Δ a i` in
    105 the nonterminals. The configuration space is the polynomial ring
    106 `ℚ[X_1, …, X_k] = MvPolynomial (Fin k) ℚ`. -/
    107structure ShuffleAutomaton (α : Type*) where
    108 dim : ℕ
    109 hdim : 0 < dim
    110 F : Fin dim → ℚ
    111 Δ : α → Fin dim → MvPolynomial (Fin dim) ℚ
    112
    113/-- The word extension of the transition: `Δ_w` is the map of the configuration
    114 space obtained by composing the letter derivations `derivationExt (Δ a)` along
    115 the word, right-to-left. The law is unchanged from the Hadamard case:
    116 `Δ_ε` is the identity and `Δ_{a·w} = Δ_w ∘ Δ_a`; the only difference is that
    117 each `Δ_a` is now a derivation rather than an endomorphism. -/
    118noncomputable def ShuffleAutomaton.Mword {α : Type*} (A : ShuffleAutomaton α) (w : List α) :
    119 MvPolynomial (Fin A.dim) ℚ → MvPolynomial (Fin A.dim) ℚ :=
    120 w.foldr (fun a φ => fun β => φ (derivationExt (A.Δ a) β)) id
    121
    122/-- The series recognised by the automaton at a configuration `cfg`:
    123 `⟦A⟧_cfg (w) = F(Δ_w cfg)`, the final-weight functional applied to the
    124 configuration reached after reading `w`. -/
    125noncomputable def ShuffleAutomaton.sem {α : Type*} (A : ShuffleAutomaton α)
    126 (cfg : MvPolynomial (Fin A.dim) ℚ) : Series α :=
    127 fun w => MvPolynomial.eval (fun i => A.F i) (A.Mword w cfg)
    128
    129/-- The series recognised by the automaton: the semantics at the initial
    130 configuration `X_0` (the first nonterminal). -/
    131noncomputable def ShuffleAutomaton.recognised {α : Type*} (A : ShuffleAutomaton α) :
    132 Series α :=
    133 A.sem (MvPolynomial.X (Fin.mk 0 A.hdim))
    134
    135/-- A series is *shuffle-finite* (working definition, paper §6.2.2) if it belongs to a
    136 finitely generated differential shuffle algebra: it is a shuffle polynomial in a
    137 finite tuple of series `fs` that is closed under left derivatives, i.e.
    138 `f = shuffleEval k fs p` for some polynomial `p`, and `leftDeriv a (fs i)` is again a
    139 shuffle polynomial in `fs` for every letter `a` and index `i`. Here `shuffleEval k fs`
    140 is the evaluation in the shuffle algebra generated by `fs`. -/
    141def IsShuffleFinite (α : Type*) (f : Series α) : Prop :=
    142 ∃ k : ℕ, ∃ fs : Fin k → Series α, ∃ p : MvPolynomial (Fin k) ℚ,
    143 f = shuffleEval α k fs p ∧
    144 ∀ a : α, ∀ i : Fin k, ∃ q : MvPolynomial (Fin k) ℚ,
    145 leftDeriv α a (fs i) = shuffleEval α k fs q
    146
    147/-- A series is *shuffle-recognisable* if it is recognised by some shuffle automaton. -/
    148def IsShuffleRecognisable (α : Type*) (f : Series α) : Prop :=
    149 ∃ A : ShuffleAutomaton α, A.recognised = f
    150
    151/-- A series is shuffle-finite if and only if it is shuffle-recognisable
    152 (paper §6, the coincidence lemma): the finitely generated differential shuffle
    153 algebras are exactly the languages of shuffle automata. -/
    154axiom ShuffleCoincidence (α : Type*) (f : Series α) :
    155 IsShuffleFinite α f ↔ IsShuffleRecognisable α f
    156
    157/-- The class of shuffle-finite series is closed under addition, scalar
    158 multiplication, the shuffle product, and right derivatives (paper §6, the
    159 closure lemma). These four parts hold over any alphabet. -/
    160axiom ShuffleClosure (α : Type*) :
    161 (∀ (f g : Series α), IsShuffleFinite α f → IsShuffleFinite α g → IsShuffleFinite α (f + g)) ∧
    162 (∀ (c : ℚ) (f : Series α), IsShuffleFinite α f → IsShuffleFinite α (c • f)) ∧
    163 (∀ (f g : Series α), IsShuffleFinite α f → IsShuffleFinite α g → IsShuffleFinite α (shuffle α f g)) ∧
    164 (∀ (a : α) (f : Series α), IsShuffleFinite α f → IsShuffleFinite α (rightDeriv α a f))
    165
    166/-- The class of shuffle-finite series over a *finite* alphabet is closed under left
    167 anti-derivatives (paper §6): if `g` is a left anti-derivative of a tuple `f` of
    168 shuffle-finite series, then `g` is shuffle-finite. The finiteness of the
    169 alphabet is essential — the witnessing generator set is extended by one series
    170 per letter, so it is finite only when the alphabet is. -/
    171axiom ShuffleAntiDerivativeClosure (α : Type*) [Fintype α] :
    172 ∀ (g : Series α) (f : α → Series α), IsLeftAntiDerivative α g f →
    173 (∀ a, IsShuffleFinite α (f a)) → IsShuffleFinite α g
    174
    175/-- The class of shuffle-finite series is an effective prevariety over a finite
    176 alphabet (paper §6, theorem): there is an effective prevariety whose image is
    177 exactly the shuffle-finite series, with presentations given by shuffle
    178 automata. -/
    179axiom ShuffleEffectivePrevariety (α : Type*) [Fintype α] :
    180 ∃ P : EffectivePrevariety α, ∀ f, IsShuffleFinite α f ↔ ∃ r : P.Rep, P.sem r = f
    181
    182/-- The equality (zeroness) problem is decidable for shuffle automata over a finite
    183 alphabet (paper §6): there is a procedure that, given a shuffle automaton,
    184 decides whether the series it recognises is the zero series. The decision
    185 reduces to ideal membership in the configuration polynomial ring, the open
    186 leaf. -/
    187axiom ShuffleEqualityDecidable (α : Type*) [Fintype α] :
    188 ∃ d : ShuffleAutomaton α → Bool, ∀ A, d A = true ↔ A.recognised = 0
    189
    190/-- In particular, the commutativity problem is decidable for shuffle-finite series
    191 over a finite alphabet (paper §6): there is a procedure that, given a shuffle
    192 automaton, decides whether the series it recognises is commutative. This is the
    193 meta-theorem applied to the effective prevariety of shuffle-finite series. -/
    194axiom ShuffleCommutativityDecidable (α : Type*) [Fintype α] :
    195 ∃ d : ShuffleAutomaton α → Bool, ∀ A, d A = true ↔ IsCommutative α (A.recognised)
    196
    197end Lax619925.Shuffle
    198
    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…