(version 04/04/2019 - Awali 1.0.2)

Awali deals with weighted automata. The weights are taken in sets that are called internally `WeightSets`

and that are, in a first approximation, *semirings*.
This first document (which is cut in two parts indeed) presents the *numerical* semirings that are available in the current version of Awali.
A next document will present more complex `WeightSets`

, and another one how a user can define its own `WeightSet`

and integrate it in Awali.

The list of numerical semirings that are available is given at the end of the output of the command `cora help`

:

```
B, Z, Q, R, C, F2, Z-min-plus, Z-max-plus, R-max-prod, Z/<int>Z
```

The name are explicit. Besides for the last one which is peculiar as it depends from a parameter given by the user, the above writing is the way the semiring is denoted in the `-W`

option.

Boolean automata have been described in the document **GettingStartedWithCora**.
We review here, in this first part, the commands for semirings `Z`

, `Q`

, `R`

and `C`

. In a second part of **Cora Documentation - Weights**, we review the commands for the remaining semirings.

These documents serve the double purpose of the presentation of the available functions in Cora and the systematic test of them.
Hence the redundance and the repetition of the same functions for the various semirings.
Very few commands indeed are specific to certain `WeightSets`

: `determinize`

is valid for Boolean automata, `reduce`

for `Z`

- or `X`

-automata where `X`

is a *field*, `are-equivalent`

for `B`

-, `Z`

- or `X`

-automata.
All other commands are valid for all `WeightSets`

.

Cora is the **command-line interface** of Awali, hence the `!`

prepending each
command below. We use Jupyter notebook as a presentation tool and do not
recommend using Cora through Jupyter in general.
Indeed, some core features of Cora have no real
interface with Python/Jupyter, such as `display`

, `edit`

or autocompletion.

There are several preloaded $\mathbb{Z}$-automata in Awali:
`b1`

, `c1`

, `d1`

, `binary`

.

In [1]:

```
!cora display b1
```

As warned in the Nota Bene, the `display`

command does not draw the figure below the cell in the notebook but opens another window on the screen.

In [2]:

```
!cora display c1
```

It is seen on this figure that weights are written between `< >`

(as in weighted rational expressions), and that the weight is not explicitely written when it is equal to the identity element of the weight semiring (indeed, when this identity element is written $1$).

The latter assertion can be witnessed when using `Z-min-plus`

`WeightSet`

(with some kind of anticipation) in relation with the `support`

and `characteristic`

functions.
A weighted automaton can be "stripped" from its weights and sent to a Boolean automaton by the command `support`

. Conversely, a Boolean automaton can be transformed into a weighted automaton, with any prescribed weight semiring, by the command `characteristic`

with the adequate `-W`

option.

In [3]:

```
!cora support b1 \| -WZ-min-plus characteristic - \| display -
```

The automaton `b1`

"counts" the number of occurences of $b$'s in a word (over $A=\{a,b\}$).
This can be observed with the command `eval`

which associates with every word its coefficient in the series realised by the automaton, or with the command `enumerate`

.

In [4]:

```
!cora eval b1 'bab'
```

In [5]:

```
!cora enumerate b1 3
```

The above line shows that `enumerate`

yields the list of words with a non zero coefficient, in the *radix* order (the same command with `awalipy`

yields the list in the lexicographic order).

The automaton `binary`

is the same as `c1`

but for the fact that label $a$ is replaced by $0$ and label $b$ by $1$. The automaton `binary`

associates with every word over $A_{2}=\{0,1\}$ the value it represents in base $2$.

In [6]:

```
!cora eval binary '101'
!cora eval c1 'abba'
```

The automaton `d1`

" counts" the difference between the number of $a$'s and the number of $b$'s in a words over $A=\{a,b\}$.

In [7]:

```
!cora eval d1 'abaab'
```

**CAVEAT** If the word given to the command `eval`

is not over the alphabet of the automaton, no error is detected (no exception is raised). The word simply does not label any successful computation of the automaton and then the coefficient of the word evaluates to $0$.

In [8]:

```
!cora eval d1 'abacab'
```

In [9]:

```
!cora support c1 \| -WZ characteristic - \| eval - 'bab'
```

The `product`

, and the `power`

, commands yield the *tensor* product, or power, of the automata which realise the *Hadamard product* of the behaviour of the automata.

In [10]:

```
!cora power c1 3 \| eval - 'bab'
```

One can compute the *minimal quotient* or the *minimal co-quotient* of a weighted automaton

In [11]:

```
!cora power c1 3 \| min-quotient - \| display -
```

In [12]:

```
!cora power c1 3 \| min-coquotient - \| display -
```

A $\mathbb{Z}$-automaton can also be *reduced* (because $\mathbb{Z}$ is a *principal ideal domain* -- almost a field).

In [13]:

```
!cora power c1 3 \| reduce - \| display - # (*) #
```

It is not so obvious that this new automaton is equivalent to the two others above. And still they are and this can be checked with Awali (since reduction is computable for $\mathbb{Z}$-automata.

In [14]:

```
!cora power c1 3 \| min-quotient - > c3min.json
!cora power c1 3 \| reduce - > c3Zred.json
!cora are-equivalent c3min.json c3Zred.json
```

A first way to constructing $\mathbb{Z}$-automata is to use the `edit`

or `create`

commands with the `-WZ`

option.
These commands are user-friendly but not presentable in a notebook.
A first alternative way is to input a $\mathbb{Z}$-rational expression.

In [15]:

```
!cora -WZ exp-to-aut '(a+b)*b(<2>a+<2>b)*' > c1Z.json
!cora display c1Z.json
```

This procedure gives the opportunity to study the properties of different methods for computing an automaton from an expression.

In [16]:

```
!cora -WZ -Mstandard exp-to-aut '(a+b)*b(<2>a+<2>b)*' > c1Zstan.json
!cora display c1Zstan.json
```

In [17]:

```
!cora -WZ -Mthompson exp-to-aut '(a+b)*b(<2>a+<2>b)*' > c1Zthom.json
!cora display c1Zthom.json
```

In [18]:

```
!cora proper c1Zthom.json \| are-isomorphic - c1Zstan.json
```

In [19]:

```
!cora min-quotient c1Zstan.json \| are-isomorphic - c1Z.json
```

The last two commands illustrate the statements that the *backward closure* of the Thompson automaton of a rational expression is equal to the standard automaton of that expression and that the minimal quotient of the standard automaton is equal to the derived term automaton (when the latter is minimal).

The next commands show how one can lift at the level of automata the rational operations, when they are applied to *standard automata*.

In [20]:

```
!cora -WZ -Mstandard exp-to-aut 'b' > bZ.json
!cora -Odot display bZ.json
```

In [21]:

```
!cora -WZ -Mstandard exp-to-aut 'a+b' > AlphaZ.json
!cora display AlphaZ.json
```

In [22]:

```
!cora left-mult '2' AlphaZ.json > Alpha2Z.json
!cora display Alpha2Z.json
```

In [23]:

```
!cora star AlphaZ.json > AlphaeZstan.json
!cora display AlphaeZstan.json
```

In [24]:

```
!cora star Alpha2Z.json > Alpha2eZstan.json
!cora display Alpha2eZstan.json
```

In [25]:

```
!cora concatenation AlphaeZstan.json bZ.json \| concatenation - Alpha2eZstan.json > c1Zbuilt.json
!cora are-isomorphic c1Zstan.json c1Zbuilt.json
!cora display c1Zbuilt.json
```

The following variant may be of interest

In [26]:

```
!cora -WZ -Mstandard exp-to-aut 'a+b' \| min-quotient - > AlphaZ-bis.json
!cora left-mult '2' AlphaZ-bis.json > Alpha2Z-bis.json
!cora star AlphaZ-bis.json > AlphaeZ-bis.json
!cora star Alpha2Z-bis.json > Alpha2eZ-bis.json
!cora concatenation AlphaeZ-bis.json bZ.json \| concatenation - Alpha2eZ-bis.json > c1Zbuilt-bis.json
!cora display c1Zbuilt-bis.json
```

To conclude this sequence, let us remark that the construction of the Thompson automaton of a rational expression -- a classic operation in the Boolean case -- may be more than problematic in the case of weighted expressions and automata: the introduction of spontaneous transitions inherent in Thompson construction may produce artefacts that yield non valid automata from valid expressions.

In [27]:

```
!cora -WZ is-validE '(\e+<-1>(b*))*'
!cora -WZ exp-to-aut '(\e+<-1>(b*))*' > Z1.json
!cora is-valid Z1.json
!cora display Z1.json
```

In [28]:

```
!cora -Mthompson -WZ exp-to-aut '(\e+<-1>(b*))*' > Z1thom.json
!cora is-valid Z1thom.json
!cora display Z1thom.json
```

$\mathbb{Z}$-automata are fit to compute combinatorial results. For instance, the (generalised) binomial coefficient $\binom{abaab}{ab}$ is computed by the following sequence of commands (which is easy to write in a shell script if necessary).

In [29]:

```
!cora -WZ exp-to-aut '(a+b)*' > Alphae.json
!cora -WZ exp-to-aut 'ab' > ab.json
!cora shuffle ab.json Alphae.json \| eval - 'abaab'
```

In [30]:

```
!cora display e1
```

The automaton `e1`

associates with every word of $\{a,b\}^{*}$ the value it represents in base $2$ when it is placed *after the radix point*. This figure shows how elements of $\mathbb{Q}$ are represented (and input): `int`

`/`

`int`

.
If the rational number happens to be an integer, it is then represented and input as such: `int`

(see below the automaton `c1Q.json`

).

In [31]:

```
!cora eval e1 'abbab'
```

As $\mathbb{Z}$-automata, $\mathbb{Q}$-automata can be built with the `edit`

or `create`

commands with the `-WQ`

option and which, as above, are not presentable in a notebook.
As for $\mathbb{Z}$-automata again, a possible method is to input a $\mathbb{Q}$-rational expression.

For instance, the next line generates an automaton which "the same" as `c1`

but with weights in $\mathbb{Q}$ rather than in $\mathbb{Z}$:

In [32]:

```
!cora -WQ exp-to-aut '(a+b)*b(<2>a+<2>b)*' > c1Q.json
!cora display c1Q.json
```

The automata `c1`

and `c1Q`

are "equal" but as the weight types are not the same, some functions are realised by distinct algorithms, as shown by the following line of commands.

In [33]:

```
!cora power c1Q.json 3 \| reduce - \| display -
```

This figure, when compared with the one following the instruction `(*)`

, shows that the function `reduce`

calls distinct algorithms for $\mathbb{Z}$ and $\mathbb{Q}$-automata.

Another way of building $\mathbb{Q}$-automata is to use the `characteristic`

function, but of course this concerns characteristic automata only, and those one can built from them.

In [34]:

```
!cora support b1 \| -WQ characteristic - > b1Q.json
!cora display b1Q.json
```

Here again, the difference between the automata `b1`

and `b1Q.json`

can be observed via the behaviour of the `reduce`

function.

In [35]:

```
!cora power b1 3 \| reduce - > b3red.json
!cora display b3red.json
```

In [36]:

```
!cora power b1Q.json 3 \| reduce - \| display -
```

Weights in $\mathbb{Q}$ also allows to deal with situations where the *star of a non proper series* is valid.

In [37]:

```
!cora -WQ exp-to-aut '(<1/6>(a*)+<1/3>(b*))*' > Qaut1.json
!cora display Qaut1.json
```

Another feature of Awali is the **promotion of semirings**.
The semiring $\mathbb{Z}$, for instance, is a sub(semi)ring of $\mathbb{Q}$, its elements can then be considered as elements of $\mathbb{Q}$.
It follows that operations that involve two automata -- such as the *product*, the *union*, or the *shuffle* -- should be allowed between a $\mathbb{Z}$-automaton and a $\mathbb{Q}$-automaton and they are indeed, and the result is a $\mathbb{Q}$-automaton.

As a consequence, any $\mathbb{Z}$-automaton can be transformed into a $\mathbb{Q}$-automaton by making the product with the *characteristic ($\mathbb{Q}$)-series* of the free monoid.

In [38]:

```
!cora -WQ exp-to-aut '(a+b)*' > AlphaeQ.json
!cora display AlphaeQ.json
```

In [39]:

```
!cora product c1 AlphaeQ.json > c1Q-bis.json
!cora display c1Q-bis.json
```

In [40]:

```
!cora power c1Q.json 3 \| reduce - \| display -
```

There is only one preloaded $\mathbb{R}$-automata in Awali: `prob-rabin`

.

In [41]:

```
!cora display prob-rabin
```

In [42]:

```
!cora enumerate prob-rabin 3
```

As for $\mathbb{Q}$-automata, there are several ways for creating $\mathbb{R}$-automata: the commands `create`

and `edit`

commands with the `-WR`

option, the definitions of series with weighted rational expressions with weight in $\mathbb{R}$ and the use of the `exp-to-aut`

command, and since $\mathbb{Q}$ is a subsemiring of $\mathbb{R}$, the *product* with the with the *characteristic ($\mathbb{R}$)-series* of the free monoid.

In [43]:

```
!cora -WR exp-to-aut '(a+b)*' > AlphaeR.json
!cora display AlphaeR.json
```

In [44]:

```
!cora product e1 AlphaeR.json > e1R.json
!cora display e1R.json
```

In [45]:

```
!cora eval e1R.json 'abbab'
```

With these two commands one sees that the two automata `e1`

and `e1R`

are equal but that their weights are in $\mathbb{Q}$ and $\mathbb{R}$ respectively.

Anticipating with the document on transducers, we transform the automaton `prob-rabin`

by replacing `0`

by `a`

and `1`

by `b`

, a task that is performed by the transducer `transcript.json`

.

In [46]:

```
!cora display transcript.json
```

In [47]:

```
!cora eval-tdc prob-rabin transcript.json > prob-rabin-ab.json
!cora display prob-rabin-ab.json
```

The following equivalence, hinted by the command line
`cora enumerate prob-rabin 3`

above, is not so obvious from the automata themselves.

In [48]:

```
!cora transpose prob-rabin-ab.json \| are-equivalent - e1R.json
```

There is only one preloaded $\mathbb{C}$-automaton in Awali: `rotation`

.