双自动机传导

顺序转导器在位置 $i$ 只知道左侧历史，bimachine 额外拿到一个有限的右侧摘要。它并未在运行时猜测未来：右自动机先从末端计算每个后缀状态，左自动机再正向输出；也可离线预计算右状态数组后一次正扫。

右摘要只能表达正则性质，例如“后面是否还有 b”“到末尾的长度模 3 是多少”。它不能保存整个后缀或给出无界计数。有限右状态足以把 NFT 中由未来验证的非确定选择变成确定局部输出。

初始输出依赖 $r_0$，因此可以根据整个输入所属的有限右同余类先写固定前缀；终态输出依赖 ${\ell }_n$。删掉两端函数会缩小具体语法，虽然常能借端标记重新编码。比较文献时必须说明端标记或端输出采用哪一种。

定义函数：每个 a 若其右侧还出现 b 就改写成 x，否则保留为 a；其他字符原样输出。右自动机只有状态 $N$（后缀无 b）和 $B$（后缀有 b），从右向左读到 b 后进入并保持 $B$。

输入 aaba 的右侧摘要依位置为

因此四个局部输出依次为 x、x、b、a，结果 xxba。左自动机在这个例子中可只有一个状态；$\lambda$ 与 $\rho$ 都输出 $\epsilon$。

同一函数可由 NFT 在读开头的 a 时猜测未来有无 b，再由后缀验证；bimachine 把猜测换成确定右状态。它通常不是 subsequential：对输入族 $a^n$ 与 $a^{n}b$，前 $n$ 个输出分别应为 $a^n$ 与 $x^n$，正向确定机在看到末字符前没有可安全写出的非空公共前缀。

在至少含两个符号的字母表上，bimachine 不能实现无界反转。右自动机虽从右读，却只把有限状态交给输出函数，并不把读到的后缀逐字保存；每个位置的输出仍按原位置从左到右连接。单字母表上的反转退化为恒等函数；把“有一台反向自动机”误解为“可以倒序吐出全部输入”，才会把 rational 与 regular functions 混为一谈。

每个 rational function 都有确定 bimachine 表示，即使没有等价 subsequential 转导器。这把“语义唯一”与“可在线单向确定输出”彻底分开：前者保证 bimachine 存在，后者还要满足孪生性质。

Bimachine 也支持规范化与最小化研究。左、右自动机分别对应输入前缀和后缀的有限同余；不同表示可以在两侧之间交换状态复杂度，因此一般不存在像最小 DFA 那样只按一个状态数排序的朴素唯一最小机，需固定一侧同余或采用规范构造。

在带正则 lookahead 的重写、词形消歧和逻辑刻画中，bimachine 是有用中介：NFT 给紧凑关系式描述，bimachine 给确定执行，代数同余则给可判定性质。若转换含反转或跨位置重排，应转向 regular function 模型，而不是继续扩大右自动机。