转导器等价问题

接受器只需寻找一个被一侧接受、另一侧拒绝的字；转导器还可能在共同定义的输入上写出不同结果。更麻烦的是两台机器可以在不同时间输出同一字：逐边比较会把暂时延迟误当成真正差异。

因此算法通常在状态对之外维护输出残差。每次把两侧新输出接到旧残差后，约去最长公共前缀；若最终共同接受时仍有不相等残差，就找到反例。对非确定关系，还要量化所有输出集合，问题难度会跃迁。

“有限状态”只保证单台机器的配置图有限，不保证两个异步输出关系可以用有限摘要比较。一般 NFT 能用不同运行编码复杂的对应关系，正是等价不可判定的来源。

设两台 sequential 转导器的共同定义域为 $(ab{)}^{\ast }$。$T_1$ 在边 a/a、b/b 上立即原样输出；$T_2$ 读 a 时输出 $\epsilon$ 并进入等待态，随后读 b 一次输出 ab 并回到初态。只有每个完整 ab 块后的状态是终态。

对输入 abab，两侧累计输出如下：

在奇数长度前缀上，$T_2$ 落后一个 a，但这些前缀不在定义域；每个可接受输入结束时延迟都归零，所以两台机器等价。若误按对应边输出检查，会在第一个 a 上给出假反例。

把 $T_2$ 的 b/ab 改为 b/ac 后，最短反例是 ab。若只改变等待态的终态输出，那么差异只在输入结束时出现，算法仍必须比较终态输出。空字也要单独检查初态是否终止及两侧初始/终态输出。

边界方面，一般非确定有限状态转导器的关系等价即使排除空输入边仍不可判定；Griffiths 的结果已覆盖这种强限制。不能先“确定化”绕过，因为许多有理关系根本没有等价确定转导器。

总 Mealy 机可在同步状态对图上局部比较输出；subsequential 机可经输出推动与自动机最小化公理库有限自动机最小化Finite automaton minimization · DFA minimization删除不可达状态并按全部未来后缀的行为划分状态，构造识别同一语言的唯一最小 DFA。式规范化比较，也可直接追踪延迟。标准显式编码下，承诺为函数型的一向 NFT 等价是 PSPACE-complete。上界可拆成两项：先在 PSPACE 内比较两台底层 NFA 的定义域，再取两转导器的不交并；在各自已经函数型的前提下，并机仍函数型当且仅当共同定义域上的输出一致，而功能性本身可在多项式时间判定。下界则把任意 NFA 的每条边都标成输出 $\epsilon$，所得转导器即使高度歧义仍是函数型，其等价恰好就是原 NFA 的语言等价。

这里说的是忘掉输出时机后的普通偏函数等价，不是要求两台运行保留相同 input/output synchronisation 或 origin 的 I-equivalence。后者比较的是更细的同步语言；仅凭相应的 resynchroniser 定理，不能替代上一段对普通函数等价的论证。

确定 2DFT、copyless SST 等 regular function 表示也有可判定等价问题，证明会经过更复杂的模型转换或代数方程。一般 NFT 关系等价则不可判定。模型类别不是实现细节，而是答案从“有算法”变成“无算法”的分界。

编译器重写、转导器优化和格式迁移常用等价检查防止语义漂移。可靠工具应在报告中写出采用的输入编码、偏函数约定、是否已验证函数性，并在不等价时返回具体输入及两侧输出，而不是只给布尔失败。

最短反例也受模型影响。同步 Mealy 机可用宽度优先搜索状态对直接得到；带输出延迟时，搜索节点还含规范残差；一般关系模型则连等价判定都不存在统一终止算法。测试有限长度样例只能发现反例，绝不能把“目前没发现”提升成全体字符串上的等价证明。