Formal Power Series for Weighted Languages

Stream: new members

[Rudy Peterson]

Hello,

I would like to formalize the notion of a formal power series for weighted languages.

In Mathlib4, I see there are a few definitions for formal power series, such as PowerSeriesBasic, MvPowerSeries, and FormalMultilinearSeries.

However, I am not sure these are the definitions I am looking for.

For a weigted language, I have an alphabet $\Sigma$ with strings $\mathbf{y} \in \Sigma^*$, and a semiring $\mathcal{W} = (\mathbb{K}, +, \times, \mathbf{0}, \mathbf{1})$.

The weighted language $L$ is described by a function $f : \Sigma^* \to \mathbb{K}$, such that:

$$L = \{ (f(\mathbf{y}), \mathbf{y}) \mid \mathbf{y} \in \Sigma^* \}$$

Which can be written as:

$$L = \sum_{\mathbf{y} \in \Sigma^*} f(\mathbf{y}) \mathbf{y}$$

$f(\mathbf{y})$ is the weight for string $\mathbf{y}$.

Is there a formalization of this in Mathlib4 already? Or are one of the formal power series definitions in Mathlib4 suitable for this?

Thank you!

[Aaron Liu]

Is the weighted language $L$ a set of ordered pairs or a sum?

[Rudy Peterson]

Aaron Liu said:

Is the weighted language $L$ a set of ordered pairs or a sum?

That's a good question... I am not sure if it is actually a sum... it may just be a function.

If it is just a function I am not sure why it is written as a sum...

[Philippe Duchon]

This looks like a multivariate power series, but with noncommuting indeterminates. I looked for them in Mathlib a few weeks ago (I wanted to try formalizing the beginining of the Berstel-Reutenauer book on them), but did not find them.

As a starting point, they could be defined as mappings from the free monoid on your alphabet, to your semiring $W$ - this is similar to the way MvPowerSeries are defined, the free monoid $W^*$ replacing finite support mappings from the alphabet to the naturals. I didn't go much further than that :)

As to whether they would be sums... you'd need to extend the work on the PiTopology of MvPowerSeries (power series are the sum of their monomials). They should be sums. I'm not sure how much of this would depend on the finiteness of the alphabet, or details of the topology on $W$ you're using (most likely, the discrete topology).

[Scott Carnahan]

I would guess that you are writing the formal sum to make it easier to think about termwise addition and convolutional multiplication. You can express this using the existing Hahn series framework by imposing a suitable partial ordering on the set of strings, but it's possible that a more specialized set of tools would serve you better.

[Aaron Liu]

Philippe Duchon said:

This looks like a multivariate power series, but with noncommuting indeterminates. I looked for them in Mathlib a few weeks ago (I wanted to try formalizing the beginining of the Berstel-Reutenauer book on them), but did not find them.

Isn't this just the docs#FreeAlgebra

[Aaron Liu]

Or maybe not, since it's a series

[Philippe Duchon]

Aaron Liu said:

Philippe Duchon said:

This looks like a multivariate power series, but with noncommuting indeterminates. I looked for them in Mathlib a few weeks ago (I wanted to try formalizing the beginining of the Berstel-Reutenauer book on them), but did not find them.

Isn't this just the docs#FreeAlgebra

That's quite possible; my knowledge of algebra is rather dated and limited (and quite possibly, even more limited than it was when I learned about it). The Mathlib definition, though, doesn't seem to match what I had in mind; it's defined through a quotient, whereas I had a concrete definition in mind.

I'll try to have a look at the API for this and see if I can make it click for me.

[Aaron Liu]

docs#FreeAlgebra is the multivariate polynomial with noncommuting indeterminates, not the series

[Rudy Peterson]

I think fundamentally want I need is just functions from elements of a free monad to elements of a semiring.

So maybe I don't need any of this stuff?