Skip to content

函数型传导

Functional transduction · Functional rational transduction · Functional finite-state transduction

每个输入至多对应一个输出的有理关系,也称由函数型一向转导器实现的有理函数。

条目类型
定义

形式陈述 ​

本页在有限状态的一向语境中使用“函数型传导”:若有理关系 R⊆Σ∗×Γ∗ 满足

(x,y1)∈R ∧ (x,y2)∈R⟹y1=y2,

就称 R 函数型,并把它写成偏函数 f:Σ∗⇀Γ∗。定义域是存在成功运行的输入;“偏”表示定义域不必等于 Σ∗,不是说某个已定义输入可以有半个答案。此类函数也称 rational functions。

转导器 T 函数型,是指其实现关系 RT 函数型。它仍可有多条成功运行,只要所有运行输出相同;这与无歧义转导器“每个输入至多一条成功运行”不同。经典表示定理说明,函数型有理传导与双自动机传导在表达能力上等价,但两者的运行组织方式并不相同。

直觉

函数性是外部可观察语义,不是转移表长相。用户给定一个输入,只看最终结果是否唯一;机器内部为同一结果尝试多少条路径并不重要。把路径唯一性当成函数性,会错误排除许多可合法合并的分析器。

另一方面,“程序最后任选一条路径”不会使关系变成函数。除非选择规则也进入模型且对所有执行固定,否则两个不同输出仍同时属于关系。函数性证明要比较任意一对同输入成功运行,并说明它们累积的输出延迟最终归零。

一向函数型转导器可以先猜未来,再由输入末尾验证。这个能力使 rational functions 严格超过确定的逐步输出函数;唯一结果不等于能够在单次左到右扫描中及时确定结果。

函数性还是一种全局一致性条件。只检查每个状态的出边输出是否唯一远远不够:两条路径可能先读不同的空边,经过长循环后才在共同终态留下差异。反过来,局部看似不同的输出块也可能在后续连接后成为同一个完整字;正确判据必须覆盖整条成功运行。

例子与边界

先看“有歧义但函数型”的最小例子。初态经两条 ε/ε 边分别进入 p,r;两条支路都按

p→a/xp→b/yp,r→a/xr→b/yr

读取输入,且相应状态都可终止。输入 ab 有两条成功运行,二者输出均为 xy,所以纤维是单元素集合 {xy}。若把第二支路的 b/y 改成 b/z,同一输入立即得到 xy 与 xz,函数性失效;路径数在修改前后都是二。

更有内容的例子定义域为 a∗{b,c}:

f(anb)=an,f(anc)=bn.

NFT 可在开始时猜末字符:一支每读 a 输出 a 并只在末尾 b 接受,另一支每读 a 输出 b 并只在末尾 c 接受。每个合法输入恰有一支成功,故函数唯一。它却不能由确定左到右机器以有界延迟实现:读前缀 an 时,两个可能结果没有非空公共前缀,机器必须等待最后一字母,而有限终态输出无法一次补出任意长的 an 或 bn。

以 n=3 为例,读前缀 aaa 时两支分别已输出 aaa、bbb;末字符 b 使后一支失败,末字符 c 则使前一支失败。失败支路的输出不属于实现关系,因为只有读完整个输入并成功终止的路径才计入语义。猜测之所以不会造成多值,靠的是互斥的成功条件,不是最后随意丢弃一个输出。

函数型也不等于全函数。上述 f 在 aa、d 上未定义;强行补一个错误串会得到另一个总函数,并可能改变闭包、等价与最小化问题。定义域是语义的一部分。

推论与应用

函数性可判定;在标准显式编码的一向 NFT 上已有多项式时间算法,但方法不是普通 NFA 的子集构造。典型算法同步两条同输入运行,逐步约去输出的最长公共前缀;若能到达共同接受而残余输出不同,就给出反例。空输入输出环和终态输出必须一并进入比较,否则会漏掉只在结束时分歧的运行。

这里应区别“某台转导器无歧义”与“该函数存在无歧义表示”。函数型机器可以像上例那样含重复运行;但经典有理统一化结果保证,每个函数型有理关系都能换成一台无歧义转导器。换表示会消去多余成功路径,却仍未保证能换成确定的一向逐步输出机器。

函数型有理传导对复合封闭。它们可用确定的 bimachine 表示,也可以保留非确定 NFT 以获得更紧凑的图。是否还能确定化为 subsequential 转导器,要由输出延迟的孪生性质判断;不是每个 rational function 都可以普通子集构造确定化。

在词形规范化、发音生成和编码转换中,函数性证明提供稳定接口:实现可以有内部猜测,调用者仍得到唯一结果。若业务上允许多个候选,则应该保留有理关系语义,不要用任意优先级伪装成数学函数。

参考资料
  • Jean Berstel, Transductions and Context-Free Languages, Teubner, 1979, Chapter IV, §§1–2, “Rational Functions” and “Sequential Transductions.”
  • Marie-Pierre Béal, Olivier Carton, Christophe Prieur, and Jacques Sakarovitch, “Squaring Transducers: An Efficient Procedure for Deciding Functionality and Sequentiality,” Theoretical Computer Science 292(1), 2003, pp. 45–63, §§4–5.
  • Emmanuel Filiot and Pierre-Alain Reynier, “Transducers, Logic and Algebra for Functions of Finite Words,” ACM SIGLOG News 3(3), 2016, §§2–4.
  • Emmanuel Filiot, Olivier Gauwin, and Nathan Lhote, “Logical and Algebraic Characterizations of Rational Transductions,” Logical Methods in Computer Science 15(4), 2019, §§2–3.
关系图谱9 个相邻概念 · 5 类关系

拖动节点调整位置。

显示关系

显示:依赖

  1. 前置三跳
  2. 前置二跳
  3. 前置一跳
  4. 当前条目
  5. 后续一跳
  6. 后续二跳
  7. 后续三跳
文字版关系按与当前条目的最短距离分组
分类位置

上位 / 更一般

下位 / 直接特例

暂未标注直接特例。

类型化关系

使用的工具

限定层次等价

并列辨析