552这个题其实是我搞研究的时候遇到的小问题，比较简单&比较有趣就拿来主义给大家练个手了。背后的理论体系其实蛮大的，而且OI里面没引入，抛砖引玉介绍一下，你们懂的。

Weighted Automata：

形式上而言，对于一个半环$S$与一个字符集$\mathrm{\Sigma }$，我们可以定义一个带权自动机$\mathcal{A}$，由以下部分组成：

1. 状态集合$Q$.
2. 带权初始状态与结束状态$I,T:Q\to S$.
3. 转移矩阵$E:\mathrm{\Sigma }\times Q\times Q\to S$.

那么对于输入串 $w=a_1{a}_2...a_l$, $\mathcal{A}$输出$I{E}_{w}T=I(\prod _{i=1}^{l}E(a_i))T$.

直观而言，带权自动机是非确定性自动机的一个小扩展，每条边有边权（对于输入边与输出边也成立），对于给定串的输出是每一条可能接收串的路径的边权乘积的总和。如果$S=\mathbb{N}$，则可以理解为是可被接收的路径数量。取$S=\mathrm{Bool}$，则该定义退化成非确定性自动机。

Weighted Language/Formal Power Series:

类比于自动机与语言的关系，带权自动机实际上接受带权语言，现代的术语也称它为形式幂级数。形式化定义就是一个函数 ${\mathrm{\Sigma }}^{\ast }\to S$。

同样，类比于正则语言，也可以找到一类形式幂级数精确刻画可以被带权自动机接受，被称为有理形式幂级数。

关于有理形式幂级数有一大堆理论，具体可以参考Jean Berstel写的《Non-commutative Rational Series with Applications》，不过这本书比较晦涩，但是囊括了很多结果。

等价性判定

Samuel Eilenberg在1974年的书《Automata, Languages and Machines》里证明了，对于$S=\mathbb{N}$的情况，两个自动机等价仅当：对于长度不超过两个自动机状态总量的串，他们输出相等。

这变相提供了一个PSPACE的等价性判定算法（当字符集是有限的），只需要枚举有多项式上界长度的串即可。

同时，我们可以构造多项式$P_n[(x_{i,a}{)}_{i\in [n],a\in \mathrm{\Sigma }}]=\sum _{w\in {\mathrm{\Sigma }}^{\ast },|w|\le n}I{E}_{w}T{x}_w$，其中 $x_w=x_{1,a_1}{x}_{2,a_2}\cdots x_{l,a_l}$.

注意到这个多项式分别列举了所有长度不超过$n$的串，自动机的等价性可以转化为两个多项式等价性的判定，其中所有系数都是自然数。这个问题是一个经典的问题，只需要给每一个变量均匀随机生成一个在$[d/ϵ]$里的元素并带入多项式检测，其中$d$是多项式次数，那么检测失败概率不超过$ϵ$。

在程序等价性判定中的应用

经典的程序的控制流图可以使用自动机来描绘，所以自动机等价性有着其独特的意义。

对于更加复杂的程序，比如带有概率的程序，或者量子计算机中的程序，它们的控制流图实际上是一个带权自动机，因为不同的道路都可能有概率/振幅经过。所以我们可以把两个程序的控制流图用带权自动机描述出来，然后套用带权自动机来验证一些情况下的程序等价性。

这种方法在编译器规则验证中有广泛应用环境，可以在控制流图层面对优化规则进行正确性证明。

理论上的更多问题

留一些可以思考的问题（虽然大都有人解决过了）给大家思考：

1. 如何引入ε-转移？如何消去ε-转移？
2. 如何判定一个带权自动机的输出是否一定小于等于另一个带权自动机的对应输出？
3. 如何最小化带权自动机（最小化状态数）？
4. 带权自动机的输出大小是否可以被界住？
5. 哪些形式幂级数是有理的？什么样的构造可以得到有理形式幂级数？
6. 单字符的带权自动机是否有更好的性质？

这里面有很多问题都是不可判定的，所以总的而言这个事情还挺难的。

总结

自动机理论里还有很多很有趣的问题、技术并不广为人知，它们在实际生产中有举足轻重的地位，大家感兴趣可以稍微学习一些。

以上。