正则字符串传导

正则函数允许用有限状态决定“输出哪些输入位置、按什么有限规则排列，以及在附近插入哪些常量”。2DFT 用多次访问输入实现次序，SST 用少量字符串片段实现次序，MSO 则直接描述输出位置图；三者提供操作、流式和逻辑三种视角。

模型能重排任意长字符串，却不能无限复制历史。固定 2DFT 的停机运行至多访问线性多个配置；固定 copyless SST 中每个旧片段不分叉；MSO 解释只有固定份输入位置副本。因此输出长度总被 $c|w|+d$ 这样的线性式控制。

线性大小不是充分条件。函数还必须由有限状态/有限逻辑描述其选择与排列；需要比较两个任意长计数、解析无界嵌套或根据素数长度选择输出，都不会仅因输出短就自动正则。

正则函数的定义域必为正则语言：在 2DFT 视角中，只保留成功停机的输入得到一个双向有限自动机，而双向有限自动机不超过普通正则语言。于是只在 $\{a^n{b}^n:n\ge 0\}$ 上输出空字的偏函数就不是正则传导，尽管每个已定义输出长度都是零。

考虑

Copyless SST 用两个寄存器 $X,Y$，每读当前字符 $a$ 更新 $X:=Xa$、$Y:=aY$，最后输出 $X\mathrm{\#}Y$。输入 cab 时，三个时刻的估值为

故结果是 cab#bac。每个旧变量在更新中只出现一次。

2DFT 的对应算法先向右扫描并原样输出 cab，在右端输出 #，再向左回扫输出 bac。两种轨迹不同，却得到同一函数。MSO 解释则取输入位置的两份副本：第一份保持顺序，第二份反序，中间插入常量位置。

函数 $g(w)=w^{|w|}$ 不是正则字符串传导，因为长度 $n$ 的输入产生 $n^2$ 个字符，违反固定模型的线性输出界。一般 copyful SST 可通过复制寄存器产生更快增长，这正说明 copyless 条件不能从等价定理中删去。允许非确定 2-way transducer 后得到的也可能是多值关系，不再属于本页函数类。

正则函数对复合封闭，也对在正则定义域上的分段选择稳定。闭包可从 MSO 解释的复合得到，也可通过模型构造实现；但连续翻译和复合可能造成指数状态增长，因此实际工具会采用惰性状态生成或保持原始表示。

该统一类覆盖反转、固定次数复制、正则前后文重写、字段重排与有限格式转换。它为程序验证提供明确边界：copyless SST 像单遍程序，2DFT 像多遍只读程序，逻辑刻画则便于证明闭包和可定义性。

判断某个转换是否“正则”时，应给出模型或逻辑见证，而不是只观察若干样例。尤其要核对定义域、端标记、终态输出和空字；这些接口差一个固定字符，也会定义不同函数，尽管宏观算法看似相同。

逻辑刻画还提供反证路线：若一个候选函数需要无限多份位置副本、非正则定义域或超线性输出，就不可能来自固定 MSO 解释。这样的结构性障碍比“没有想到 SST 写法”更可靠，也能指出究竟是哪项能力越界。