跳到主要内容

東京大学 情報理工学系研究科 コンピュータ科学専攻 2017年8月実施 専門科目II 問題2

标签：

Author​

祭音Myyura (co-authored with GPT 5.6 SOL)

Description​

设 VV 是有限变量符号集，F0F_0 是有限常量符号集，F2F_2 是有限二元函数符号集，TT 是由它们构成的项集。有限重写规则集 GG 中每条规则形如

x→c或x→f(y,z),x\to c\quad\text{或}\quad x\to f(y,z),

且每个 x∈Vx\in V 恰在一条规则的左侧出现。若在项 α\alpha 的某个 xx 处应用其规则得到 β\beta，记 α⇒β\alpha\Rightarrow\beta；其自反传递闭包记为 ⇒∗\Rightarrow^*，其自反、对称、传递闭包记为 ⇔∗\Leftrightarrow^*。

（1）证明：若 α⇔∗β\alpha\Leftrightarrow^*\beta，则存在 δ∈T\delta\in T，使 α⇒∗δ\alpha\Rightarrow^*\delta 且 β⇒∗δ\beta\Rightarrow^*\delta。

（2）给出判定 α⇔∗β\alpha\Leftrightarrow^*\beta 的算法并说明正确性。

对 w∈{L,R}∗w\in\{L,R\}^*，以 α.w\alpha.w 表示沿 ww 指定的左右孩子路径取得的子项。定义 α≈β\alpha\approx\beta：对任意 α⇔∗α′\alpha\Leftrightarrow^*\alpha'、β⇔∗β′\beta\Leftrightarrow^*\beta' 及任意路径 ww，只要 α′.w,β′.w\alpha'.w,\beta'.w 均存在且其根符号属于 F0∪F2F_0\cup F_2，两个根符号就相同。

（3）给出判定 α≈β\alpha\approx\beta 的算法并说明正确性。

Kai​

（1）​

一个变量本身是叶结点，所以两个不同的可重写位置必不相交；在两个位置分别重写时，先后次序可以交换。若两次选择同一位置，由于每个变量恰有一条规则，两次结果相同。因此 ⇒\Rightarrow 满足菱形性质：

由菱形性质归纳可得 ⇒∗\Rightarrow^* 的合流性；再对 α⇔∗β\alpha\Leftrightarrow^*\beta 的有限正向、反向步骤数归纳，即得共同后继 δ\delta。

（2）​

把 VV 中的变量也暂看成零元符号。建立一个 DAG，包含 α,β\alpha,\beta、所有规则右端以及它们的全部子项，然后作基项合同闭包：

  1. 用并查集合并每个 xx 与其唯一规则右端；
  2. 反复执行：若已有结点 f(s1,s2)f(s_1,s_2) 与 f(t1,t2)f(t_1,t_2) 的对应孩子已经分别同类，则合并这两个父结点；
  3. 闭包稳定后，当且仅当 α,β\alpha,\beta 的根结点同类时回答“是”。

⇔∗\Leftrightarrow^* 正是包含各等式“x=x= 规则右端”的最小合同关系。上述算法计算的正是有限基项等式的合同闭包，故判定正确且必然终止。

（3）​

在（2）的有限项图上做不带 occurs-check 的有理树合一：先加入所有等式“x=x= 规则右端”，再加入待检验等式 α=β\alpha=\beta，并用工作队列反复执行：

  • 若同一等价类中出现不同常量、不同函数符号，或一个常量与一个函数符号，则报告冲突；
  • 若同类中有 f(s1,s2)f(s_1,s_2) 与 f(t1,t2)f(t_1,t_2)，则继续合并 s1,t1s_1,t_1 以及 s2,t2s_2,t_2。

队列稳定且没有冲突时回答“是”，否则回答“否”。允许循环而不作 occurs-check 是必要的，例如规则 x→f(x,c)x\to f(x,c) 本身是合法的。

沿路径分解同根函数，恰好把 α\alpha 与 β\beta 在该路径上能够暴露的构造符号放入同一类。因此出现冲突当且仅当题目定义中的某条路径能观察到两个不同的 F0∪F2F_0\cup F_2 符号。有限图上的每次操作只合并等价类，故算法终止并且判定恰为 α≈β\alpha\approx\beta。

本页目录