In this section we define the class of P-finite series, which are series that belong to a finitely generated algebra of series that is closed under left derivatives.

To this end, we fix the coefficient ring R, the alphabet Σ, and a product rule P.

{-# OPTIONS --guardedness --sized-types #-}

open import Preliminaries.Base renaming (_,,_ to _,_)
open import General.ProductRules

module General.FinitelyGenerated
    (R : CommutativeRing)
    (Σ : Set)
    (P : ProductRule R)
    where

open import Preliminaries.Vector
open import Preliminaries.Algebra R

open import General.Terms R
    renaming (_+_ to _[+]_; _*_ to _[*]_; _·_ to _[·]_)

open import General.Series R Σ
open import General.Products R Σ
open Product P

private variable
    X : Set
    m n : ℕ
    c : A
    f g h : A ⟪ Σ ⟫
    gs : Vec (A ⟪ Σ ⟫) n
    ϱ : SEnv X

Finitely genereated algebras of series

For a series f and a vector of generators gs, we write f ∈[ gs ] to denote that f can be obtained from the generators gs by a finite sequence of algebra operations. In other words, if any of the following holds:

  • f is the zero series 𝟘,
  • f is one of the generators in gs,
  • f is obtained by scalar multiplication from a series g s.t. g ∈[ gs ],
  • f is obtained by addition from two series g and h s.t. g ∈[ gs ] and h ∈[ gs ],
  • f is obtained by multiplication from two series g and h s.t. g ∈[ gs ] and h ∈[ gs ].

This leads to the following formal definition.

infix 4 _∈[_]
infixr 8 _·∈_
infixr 6 _+∈_
infixr 7 _*∈_
infixr 8 _≈∈_

data _∈[_] : A ⟪ Σ ⟫ → Vec (A ⟪ Σ ⟫) n → Set where
    𝟘∈ : 𝟘 ∈[ gs ]
    gen∈ : g ∈ gs → g ∈[ gs ]
    _·∈_ : ∀ c → f ∈[ gs ] → c · f ∈[ gs ]
    _+∈_ : f ∈[ gs ] → g ∈[ gs ] → f + g ∈[ gs ]
    _*∈_ : f ∈[ gs ] → g ∈[ gs ] → f * g ∈[ gs ]

    -- we need closure under equivalence of series
    -- since the base ring is parametrised by an equivalence relation
    _≈∈_ : f ≈ g → g ∈[ gs ] → f ∈[ gs ]

Closure under algebra operations

If the series environment ϱ maps variables to series in the algebra generated by gs, then also ⟦ p ⟧ ϱ belongs to this algebra. In other words, the algebra generated by gs is closed under the algebra operations.

subalgebra : ∀ p → (∀ x → ϱ x ∈[ gs ]) → ⟦ p ⟧ ϱ ∈[ gs ]
subalgebra 0T _ = 𝟘∈
subalgebra (var x) ass = ass x
subalgebra (c [·] p) ass = _ ·∈ subalgebra p ass
subalgebra (p [+] q) ass = subalgebra p ass +∈ subalgebra q ass
subalgebra (p [*] q) ass = subalgebra p ass *∈ subalgebra q ass

We specialise the subalgebra property to vector series environments.

subalgebraᵥ : ∀ p → ⟦ p ⟧ᵥ gs ∈[ gs ]
subalgebraᵥ p = subalgebra p λ x → gen∈ (∈-lookup x _)

Viceversa, for every element in the algebra generated by gs we can compute a term α witnessing membership.

extract :
    ∀ f (gs : Vec (A ⟪ Σ ⟫) n) →
    f ∈[ gs ] →
    ----------------------------
    ∃[ α ] f ≈ ⟦ α ⟧ᵥ gs

The proof proceeds by structural induction on the witness for f ∈[ gs ]

extract {n} f gs f∈[gs] = go f f∈[gs] where

    -- there are n variables
    Y : Set
    Y = Fin n

    -- if f belongs to a finitely generated algebra,
    -- then it can be expressed as a polynomial in the generators
    go : ∀ f → f ∈[ gs ] → ∃[ α ] f ≈ ⟦ α ⟧ (lookup gs)
    go f 𝟘∈ = 0T , ≈-refl
    go f (gen∈ f∈gs) = var i , f≈⟦i⟧ϱ where

        -- index of f in gs
        i : Y
        i with lookup-∈ f∈gs
        ... | i , _ = i

        -- proof that f indeed is element i of gs′
        f≡ϱi : f ≡ lookup gs i
        f≡ϱi with lookup-∈ f∈gs
        ... | _ , eq = eq

        f≈⟦i⟧ϱ : f ≈ ⟦ var i ⟧ (lookup gs)
        f≈⟦i⟧ϱ = ≡→≈ f≡ϱi

    go f (c ·∈ f∈[gs])
        with go _ f∈[gs]
    ... | α , f≈⟦α⟧ = c [·] α , ·-cong R-refl f≈⟦α⟧

    go f (f∈[gs] +∈ g∈[gs])
        with go _ f∈[gs] | go _ g∈[gs]
    ... | α , f≈⟦α⟧ | β , g≈⟦β⟧ = α [+] β , +-cong f≈⟦α⟧ g≈⟦β⟧
    
    go f (f∈[gs] *∈ g∈[gs])
        with go _ f∈[gs] | go _ g∈[gs]
    ... | α , f≈⟦α⟧ | β , g≈⟦β⟧ = α [*] β , *-cong f≈⟦α⟧ g≈⟦β⟧

    go f (f≈g ≈∈ f∈[gs])
        with go _ f∈[gs]
    ... | α , g≈⟦α⟧ = α , ≈-trans f≈g g≈⟦α⟧

P-finite series

We present two, equivalent, definitions for P-finite series. The first is more intuitive, while the second is more convenient to work with. In particular, the second definition will yield simpler proofs for the closure properties of P-finite series.

First definition

We start with the intuitive definition. We say that a series is P-finite if it belongs to a finitely generated algebra of series that is closed under left derivatives. This is formalised as follows.

module FirstDefinition where

    infix 3 P-fin[_,_,_]
    record P-fin (f : A ⟪ Σ ⟫) (n : ℕ) : Set where
        constructor P-fin[_,_,_]
        field
            gen : Vec (A ⟪ Σ ⟫) n
            memb : f ∈[ gen ]
            closed : ∀ a {g} → g ∈[ gen ] → δ g a ∈[ gen ]

        elem : A ⟪ Σ ⟫
        elem = f

    open P-fin

In other words, P-fin f n holds if

  • there exists a vector of generators gen of size n,
  • we have a witness memb : f ∈[ gen ] that f indeed belongs to the algebra generated by gen, and
  • whenever g ∈[ gen ] we also have δ g a ∈[ gen ].

Second definition

We now present a more convenient definition of P-finite series, which will be our working definition for the rest of the document.

The working definition requires closure under left derivatives only for the generators (instead for all elements of the algebra), and thus it is definitionally more restrictive.

module SecondDefinition where

    infix 3 P-fin[_,_,_]
    record P-fin (f : A ⟪ Σ ⟫) (n : ℕ) : Set where
        constructor P-fin[_,_,_]
        field
            gen : Vec (A ⟪ Σ ⟫) n
            memb : f ∈[ gen ]
            closed : ∀ a {g} → g ∈ gen → δ g a ∈[ gen ]

        elem : A ⟪ Σ ⟫
        elem = f

Note the difference in the closed field, where we only require that g ∈ gen (instead of g ∈[ gen ]) implies δ g a ∈[ gen ].

Equivalence of the two definitions

Before proceeding, we show that the two definitions are in fact equivalent.

module EquivalenceOfDefinitions where

    open SecondDefinition
    open FirstDefinition renaming (P-fin to P-fin′; P-fin[_,_,_] to P-fin′[_,_,_])
    open P-fin public

From the first to the second definition

The second definition is a special case of the first one, so one direction is immediate.

    first→second : P-fin′ f n → P-fin f n
    first→second P-fin′[ gen , f∈[gen] , cl′ ] =
        P-fin[ gen , f∈[gen] , cl ] where
            cl :  ∀ a {g} → g ∈ gen → δ g a ∈[ gen ]
            cl a g∈gen = cl′ a (gen∈ g∈gen)

From the second to the first definition

For the other direction, we will use the following auxiliary lemma. It says that the algebra generated by the generators of a P-finite series (in the second sense) is closed under left derivatives. We state it separately because it is interesting in its own right, for instance it will be used in the section about closure under anti-derivatives.

    δ-closed :
        ∀ (F : P-fin f n) a {g} →
        g ∈[ gen F ] →
        -------------------------
        δ g a ∈[ gen F ]

With this lemma in hand, it is easy to show that the second definition implies the first one.

    second→first : P-fin f n → P-fin′ f n
    second→first F = P-fin′[ gen F , memb F , δ-closed F ]

We conclude by proving the auxiliary lemma. The proof is by structural induction on the witness for g ∈[ gen F ].

    δ-closed F a = go where
        go : ∀ {g} → g ∈[ gen F ] → δ g a ∈[ gen F ]
        go 𝟘∈ = 𝟘∈
        go (gen∈ g∈gen) = closed F a g∈gen
        go (c ·∈ g∈[F]) = c ·∈ go g∈[F]
        go (g∈[F] +∈ h∈[F]) = go g∈[F] +∈ go h∈[F]
        go (_*∈_ {f = g} {g = h} g∈[gen] h∈[gen]) = subalgebra P ass where

            ass : ∀ x → lookup (g ∷ δ g a ∷ h ∷ δ h a ∷ []) x ∈[ gen F ]
            ass zero = g∈[gen]
            ass (suc zero) = go g∈[gen]
            ass (suc (suc zero)) = h∈[gen]
            ass (suc (suc (suc zero))) = go h∈[gen]
            
        go (f≈g ≈∈ f∈[F]) = (δ-≈ f≈g a) ≈∈ go f∈[F]

Therefore, from now on we use the second definition as the notion of P-finiteness.

open SecondDefinition public
open EquivalenceOfDefinitions using (δ-closed) public
open P-fin public

Closure properties of P-finite series

In this section we show some natural closure properties for the class of P-finite series. The use of the second definition makes the proofs easier.

Preliminary properties

In the proofs we will use the following auxiliary properties, which will be proved at the end. First we define a function _++-gen_ that concatenates the generators of two P-finite series.

_++-gen_ : P-fin f m → P-fin g n → Vec (A ⟪ Σ ⟫) (m +ℕ n)
F ++-gen G = gen F ++ gen G

The auxiliary properties are:

  • _++-memb-+_, saying that the sum of two P-finite series belongs to the algebra generated by the concatenation of their generators,
  • _++-memb-*_, saying the same for products, and
  • _++-closed_, saying that the algebra generated by the concatenation of the generators of two P-finite series is itself closed under left derivatives.

The formal statements are as follows.

_++-memb-+_ : (F : P-fin f m) (G : P-fin g n) → elem F + elem G ∈[ F ++-gen G ]
_++-memb-*_ : (F : P-fin f m) (G : P-fin g n) → elem F * elem G ∈[ F ++-gen G ]
_++-closed_ : ∀ (F : P-fin f m) (G : P-fin g n) a {h} → h ∈ (F ++-gen G) →
    δ h a ∈[ F ++-gen G ]

We are now ready to show the closure properties of P-finite series.

Zero

The zero series 𝟘 is P-finite, for the empty tuple of generators.

P-fin-𝟘 : P-fin 𝟘 0
P-fin-𝟘 = P-fin[ [] , 𝟘∈ , (λ a {g} ()) ]

Scalar multiplication

P-finite series are closed under scalar multiplication. We use the same set of generators.

P-fin-· : 
    P-fin f n →
    ----------------
    P-fin (c · f) n

P-fin-· F = P-fin[ gen F , _ ·∈ memb F , closed F ]

Addition

P-finite series are closed under addition. The set of generators is the concatenation of generators.

P-fin-+ :
    P-fin f m →
    P-fin g n →
    ----------------------
    P-fin (f + g) (m +ℕ n)

P-fin-+ F G = P-fin[ F ++-gen G , F ++-memb-+ G , F ++-closed G ]

Multiplication

P-finite series are closed under multiplication. The set of generators is the concatenation of generators.

P-fin-* :
    P-fin f m →
    P-fin g n →
    ----------------------
    P-fin (f * g) (m +ℕ n)

P-fin-* F G = P-fin[ F ++-gen G , F ++-memb-* G , F ++-closed G ]

The previous closure properties can be aggregated by saying that, for every term, if each variable evaluates to a P-finite series, then the whole term evaluates to a P-finite series too.

Left derivatives

P-finite series are closed under left derivatives. The set of generators does not change.

P-fin-δ :
    P-fin f m →
    ∀ a →
    ---------------
    P-fin (δ f a) m

P-fin-δ F a = P-fin[ gen F , δ-closed F a (memb F) , closed F ]

Left anti-derivatives

When the alphabet Σ is finite, we can also show that P-finite series are closed under left anti-derivatives. This is elaborated in a separate section, where we can make the required assumption on the alphabet.

This concludes the basic development for P-finite series. In the next section we will introduce P-automata and show that P-finite series are precisely those series recognized by P-automata.

Appendix

We prove here the auxiliary lemmas used in the closure properties.

++-∈ˡ : ∀ {fs : Vec (A ⟪ Σ ⟫) m} {gs : Vec (A ⟪ Σ ⟫) n} → f ∈[ fs ] → f ∈[ fs ++ gs ]
++-∈ˡ 𝟘∈ = 𝟘∈
++-∈ˡ (gen∈ f∈fs) = gen∈ (∈-++⁺ˡ f∈fs)
++-∈ˡ (c ·∈ f∈[fs]) = c ·∈ ++-∈ˡ f∈[fs]
++-∈ˡ (f∈[fs] +∈ g∈[fs]) = ++-∈ˡ f∈[fs] +∈ ++-∈ˡ g∈[fs]
++-∈ˡ (f∈[fs] *∈ g∈[fs]) = ++-∈ˡ f∈[fs] *∈ ++-∈ˡ g∈[fs]
++-∈ˡ (f≈g ≈∈ g∈[fs]) = f≈g ≈∈ ++-∈ˡ g∈[fs]

++-∈ʳ : ∀ {fs : Vec (A ⟪ Σ ⟫) m} {gs : Vec (A ⟪ Σ ⟫) n} → f ∈[ gs ] → f ∈[ fs ++ gs ]
++-∈ʳ 𝟘∈ = 𝟘∈
++-∈ʳ (gen∈ f∈fs) = gen∈ (∈-++⁺ʳ _ f∈fs)
++-∈ʳ (c ·∈ f∈[fs]) = c ·∈ ++-∈ʳ f∈[fs]
++-∈ʳ (f∈[fs] +∈ g∈[fs]) = ++-∈ʳ f∈[fs] +∈ ++-∈ʳ g∈[fs]
++-∈ʳ (f∈[fs] *∈ g∈[fs]) = ++-∈ʳ f∈[fs] *∈ ++-∈ʳ g∈[fs]
++-∈ʳ (f≈g ≈∈ g∈[fs]) = f≈g ≈∈ ++-∈ʳ g∈[fs]

F ++-memb-+ G = ++-∈ˡ (memb F) +∈ ++-∈ʳ (memb G)
F ++-memb-* G = ++-∈ˡ (memb F) *∈ ++-∈ʳ (memb G)
   
_++-closed_ F G a h∈fs++gs with ∈ᵥ-++ h∈fs++gs
... | inj₁ h∈fs = ++-∈ˡ (closed F a h∈fs)
... | inj₂ h∈gs = ++-∈ʳ (closed G a h∈gs)

References