公式化地从有限自动机倒推出正则表达式兴许可以?