跳到主要内容

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

标签：

Author​

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

Description​

Let VV be a finite set of symbols denoting variables, F0F_0 a finite set of constant symbols, F2F_2 a finite set of binary function symbols, and TT the set of terms constructed from symbols in VV, F0F_0 and F2F_2. Let GG be a finite set of rewrite rules of the form x→cx\to c or of the form x→f(y,z)x\to f(y,z), where x,y,z∈Vx,y,z\in V, c∈F0c\in F_0 and f∈F2f\in F_2, and each x∈Vx\in V appears in the left-hand side of exactly one rewrite rule in GG. For α,β∈T\alpha,\beta\in T, the relation α⇒β\alpha\Rightarrow\beta is defined as follows:

β\beta is obtained by applying a rule x→γx\to\gamma (γ\gamma is cc or f(y,z)f(y,z)) in GG to one occurrence of x∈Vx\in V in α\alpha and replacing the occurrence with γ\gamma.

The relation ⇒∗\Rightarrow^* is defined as the reflexive and transitive closure of ⇒\Rightarrow, and the relation ⇔∗\Leftrightarrow^* is defined as the reflexive, transitive and symmetric closure of ⇒\Rightarrow.

Answer the following questions.

(1) Show that if α,β∈T\alpha,\beta\in T and α⇔∗β\alpha\Leftrightarrow^*\beta, then there exists δ∈T\delta\in T such that α⇒∗δ\alpha\Rightarrow^*\delta and β⇒∗δ\beta\Rightarrow^*\delta.

(2) Give an algorithm that judges α⇔∗β\alpha\Leftrightarrow^*\beta for α,β∈T\alpha,\beta\in T, and explain its correctness.

For α∈T\alpha\in T and w∈{L,R}∗w\in\{L,R\}^*, the operation α.w∈T\alpha.w\in T that extracts a subterm of α\alpha is inductively defined as follows:

α.ϵ=α,α.Lw={α1.wif α=f(α1,α2),undefinedotherwise,α.Rw={α2.wif α=f(α1,α2),undefinedotherwise.\begin{aligned} \alpha.\epsilon&=\alpha,\\ \alpha.Lw&= \begin{cases} \alpha_1.w&\text{if }\alpha=f(\alpha_1,\alpha_2),\\ \text{undefined}&\text{otherwise}, \end{cases}\\ \alpha.Rw&= \begin{cases} \alpha_2.w&\text{if }\alpha=f(\alpha_1,\alpha_2),\\ \text{undefined}&\text{otherwise}. \end{cases} \end{aligned}

Here ϵ\epsilon is an empty word. For α,β∈T\alpha,\beta\in T, the relation α≈β\alpha\approx\beta is then defined as follows:

for any α′,β′∈T\alpha',\beta'\in T and w∈{L,R}∗w\in\{L,R\}^*, if α⇔∗α′\alpha\Leftrightarrow^*\alpha' and β⇔∗β′\beta\Leftrightarrow^*\beta', and α′.w\alpha'.w and β′.w\beta'.w are both defined and their first symbols belong to F0∪F2F_0\cup F_2, then those symbols are identical.

Answer the following question.

(3) Give an algorithm that judges α≈β\alpha\approx\beta for α,β∈T\alpha,\beta\in T, and explain its correctness.

题目描述​

设 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,y,z∈Vx,y,z\in V、c∈F0c\in F_0、f∈F2f\in F_2，且每个 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.\varepsilon=\alpha；若 α=f(α1,α2)\alpha=f(\alpha_1,\alpha_2)，则 α.Lw=α1.w\alpha.Lw=\alpha_1.w、α.Rw=α2.w\alpha.Rw=\alpha_2.w，否则这两种操作未定义。这里 ε\varepsilon 是空串。定义 α≈β\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,y)x\to f(x,y)、y→cy\to c（x,y∈Vx,y\in V、c∈F0c\in F_0）是合法的，并给出 x⇒f(x,y)⇒f(x,c)x\Rightarrow f(x,y)\Rightarrow f(x,c)。

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

本页目录