Choffrut 孪生性质

确定化要把多个 NFT 状态放入一个集合状态，并为每条候选路径保存“尚未共同输出”的残余。普通子集构造只追踪状态；转导器还必须保证这些残余不会沿循环越积越长，否则会产生无限多个确定化状态。

孪生性质要求同步循环不改变两条候选运行之间的相对输出差。它并不强求两条路径每一步输出相同；有限延迟可以先出现、后抵消。被禁止的是每绕一次共同输入循环，延迟再多积一个无法统一前移的片段。

自由群记号只用于抵消公共前缀后的相对差，不表示输出真的可以删除。实现中可把延迟保存成约去最长公共前缀后的剩余对；判据关注循环前后是否代表同一相对差。

Trim 假设排除了永远不会贡献完整输出的状态。一个不可达坏循环或从循环再也到不了终态的分支，即使输出延迟增长，也不影响所实现函数；先裁剪再检查，才能让图上的反例与真实成功运行对应。反之，漏掉终态输出可能把本来可终止的差异误判为可抵消。

再次考虑定义域 $a^{\ast }\{b,c\}$ 上的函数

一个 functional NFT 在开始时分成状态 $p,q$。$p$ 的 a 环输出 a，只在读 b 时接受；$q$ 的 a 环输出 b，只在读 c 时接受。两状态由同一空输入、同一空输出到达，初始延迟为

同步绕一次输入 a 后，延迟变为 $\mathrm{\Delta }(a,b)=a^{-1}b\ne 1$；绕 $k$ 次会持续增长。孪生性质失败，故不存在等价 subsequential 转导器。直接看前缀也能理解：读完 $a^n$ 尚不知末尾是 b 还是 c，两个候选输出 $a^n,b^n$ 没有公共非空前缀。

一个有固定输出延迟的正例可用下表独立检查。初态为 $s$，唯一终态为 $f$，初始与终态附加输出均为空；未列出的转移不存在。

读完 $a^n$（$n\ge 1$），两支分别输出 $a^n$ 与 $a^{n-1}$，延迟恒为 $a^{-1}$。同步再读任意个 a，延迟仍相同；最后读 b，第二支补出一个 a，两支都输出 $a^n$。所有状态可达且可到终态，机器为 trim、real-time、functional；唯一非平凡的同步循环对 $p,q$ 保持延迟。因此它满足孪生性质，并与“每读 a 就输出 a，读末尾 b 时接受”的确定转导器等价。

该定理不适用于一般多值关系：两个不同输出可能都是规范允许的，此时“把延迟合并成唯一确定输出”本来就没有目标。含输入 $\epsilon$ 边的机器也需先做保持函数语义的正规化；直接把空环当作普通字母循环可能得出错误结论。

判定算法可在状态对的同步积上搜索坏循环，同时用输出差的代数表示避免展开所有输入字。若发现违例，前导路径、循环和各自通往终态的后缀组成可核查证书；若没有违例，带延迟子集构造只产生有限多个规范残余。

孪生性质解释了“函数型”与“可确定化”的缺口。函数性只保证完整成功运行最终一致；孪生性进一步保证在任意长前缀上，候选输出之间的分歧可由有限控制管理。二者不能合并成一句“唯一输出所以能确定化”。

在词典编译和有限状态语言处理中，检查孪生性质可以决定是否值得生成高速 subsequential 机。失败时应保留 functional NFT 或改用 bimachine；为有限训练集强行确定化可能不断产生新延迟状态，无法成为完整算法。

成立时的确定化状态不仅是 NFT 状态集合，还给每个成员附一个规范输出残余；先提出所有残余的最长公共前缀作为当前边输出，再保存余项。孪生性质保证循环不会制造无限多种余项，这正把判定条件转化为实际构造。