Cora Documentation – WeightSets I

(version 19/02/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 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 the commands for other weights semirings.

1. Weights in $\mathbb{Z}$

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

b1, c1, d1, binary
In [2]:
!cora -Odot display c1

c1.svg

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 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'

2
In [5]:
!cora enumerate b1 3

<1> b
<1> ab
<1> ba
<2> bb
<1> aab
<1> aba
<2> abb
<1> baa
<2> bab
<2> bba
<3> bbb

The above line shows that enumerate yields the list of words with a non zero coefficient, in the radix order (the same command with awalipyyields 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 $0$. 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'

5
6

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'

1

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'

0

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 4 \| eval - 'bab'

625

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

In [12]:
!cora power c1 4 \| min-quotient - \| -Odot display -

c4min.svg

In [14]:
!cora power c1 4 \| min-coquotient - \| -Odot display -

c4min-co.svg

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

In [15]:
!cora power c1 4 \| reduce - \| display -

c4Zred.svg

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 [17]:
!cora power c1 4 \| min-quotient - > c4min.json
!cora power c1 4 \| reduce - > c4Zred.json
!cora are-equivalent c4min.json c4Zred.json

true

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 [19]:
!cora support c1 \| -WZ characteristic - \| eval - 'bab'

2

$\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 shel script if necessary).

In [22]:
!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'

4

2. Weights in $\mathbb{Q}$

There is only one preloaded $\mathbb{Q}$-automaton in Awali: e1.

In [24]:
!cora display e1

e1.svg

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.

In [27]:
!cora eval e1 'abbab'

13/32

Alternative ways to constructing $\mathbb{Q}$-automata is to use the edit or create commands with the -WQ option (which are user-friendly but not presentable in a notebook) or 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 [29]:
!cora -WQ exp-to-aut '(a+b)*b(<2>a+<2>b)*' > c1Q.json
!cora display c1Q.json

c1Q.svg

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 command

In [3]:
!cora power c1Q.json 4 \| reduce - \| display -

c4Qred.svg

A third way to create $\mathbb{Q}$-automata is to use another feature of Awali which allows the promotion of semirings.

For instance, $\mathbb{Z}$ is a sub(semi)ring of $\mathbb{Q}$, its elements can be considered as elements of $\mathbb{Q}$. It follows that the product of a $\mathbb{Z}$-automaton by a $\mathbb{Q}$- automaton is allowed and yields 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 [5]:
!cora -WQ exp-to-aut '(a+b)*' > AlphaeQ.json
!cora -Odot display AlphaeQ.json

Alphae.svg

In [6]:
!cora product b1 AlphaeQ.json > b1Q.json
!cora -Odot display b1Q.json

b1Q.svg

In [10]:
!cora power b1 3 \| reduce - > b3red.json
!cora -Odot -Nb3red display b3red.json

b3red.svg

In [9]:
!cora power b1Q.json 3 \| reduce - \| -Odot -Nb3Qred display -

b3Qred.svg

Another example where one sees that the reduce algorithm behaves in a smarter way in fields than in $\mathbb{Z}$.

In [12]:
!cora power b1Q.json 3 \| reduce - \| are-equivalent - b3red.json

true

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

In [18]:
!cora -WQ exp-to-aut '(<1/6>(a*)+<1/3>(b*))*' > Qaut1.json
!cora -Odot -NQaut1 display Qaut1.json

Qaut1.svg

3. Weights in $\mathbb{R}$

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

In [20]:
!cora -Odot display prob-rabin

prob-rabin.svg

In [21]:
!cora enumerate prob-rabin 3

Compiling module "eval" for a new automaton context (lal_char_r)
Linking module "eval" for a new automaton context (lal_char_r)
<0.5> 1
<0.5> 01
<0.25> 10
<0.75> 11
<0.5> 001
<0.25> 010
<0.75> 011
<0.125> 100
<0.625> 101
<0.375> 110
<0.875> 111

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 [29]:
!cora -WR exp-to-aut '(a+b)*' > AlphaeR.json
!cora -Odot display AlphaeR.json

AlphaeR.svg

In [24]:
!cora product e1 AlphaeR.json > e1R.json
!cora -Odot display e1R.json

e1R.svg

In [28]:
!cora eval e1R.json 'abbab'

0.40625

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 [30]:
!cora -Odot display transcript.json

transcript.svg

In [32]:
!cora eval-tdc prob-rabin transcript.json > prob-rabin-ab.json
!cora -Odot display prob-rabin-ab.json

prob-rabin-ab.svg

The following equivalence, hinted by the command line cora enumerate prob-rabin 3 above, is not so obvious from the automata themselves.

In [33]:
!cora transpose prob-rabin-ab.json \| are-equivalent - e1R.json

true

4. Weights in $\mathbb{C}$

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

5. Weights in $\mathbb{F}2$

There is no preloaded $\mathbb{F}2$-automaton in Awali so far.

6. Weights in $\mathbb{Z}\mathsf{-min}\mathsf{-plus}$

There are several preloaded $\mathbb{Z}\mathsf{-min-plus}$-automata in Awali:

minab, minblocka, slowgrow

7. Weights in $\mathbb{Z}\mathsf{-max}\mathsf{-plus}$

There is only one preloaded $\mathbb{Z}\mathsf{-max}\mathsf{-plus}$-automaton in Awali: heapmodel

8. Weights in $\mathbb{R}\mathsf{-max}\mathsf{-prod}$

There is no preloaded $\mathbb{R}\mathsf{-max}\mathsf{-prod}$-automata in Awali.

9. Weights in $\mathbb{Z}/\mathtt{<\!int\!>}\mathbb{Z}$

There is no preloaded $\mathbb{Z}/\mathtt{<\!int\!>}\mathbb{Z}$-automata in Awali.