In this part we develop the basic theory of formal series in noncommuting variables. The results in this part are valid for every product rule. This is the fundation upon which, in the next part, we will develop the theory of special product rules.

This is part is structured as follows.

  • In Series we define formal series and their vector space structure.
  • In Terms we define the notion of terms and develop their basic properties. Terms are used to define product rules, which are developed next.
  • In ProductRules we define the notion of a product rule P, which is then used in Products to define the P-product operation on formal series.
  • In FinitelyGenerated we study the resulting notion of P-finite series.
  • In Automata we study P-automata. This culminates with a proof of the coincidence of P-finite series and series recognized by P-automata.
  • Finally, in Reversal we study right derivatives and reversals of formal series, and in ReversalEnd we study what happens when reversal is an endomorphism.
{-# OPTIONS --guardedness --sized-types #-}

module General.index where

import General.Series
import General.Terms
import General.ProductRules
import General.Products
import General.FinitelyGenerated
import General.Automata
import General.Reversal
import General.ReversalEnd

References