依赖对的终止分析

### 依赖对的终止分析 #### 1. 归约对与DP问题处理 归约对 `(≿, ≻)` 由一个稳定单调拟序 `≿` 和一个稳定良基序 `≻` 组成，且 `≿` 和 `≻` 是兼容的（即 `≿◦≻◦≿ ⊆≻`）。对于DP问题 `(P, R)`，存在一个处理器，它要求 `P` 中的所有依赖对（DPs）严格或弱递减，`R` 中的所有规则弱递减，然后可以删除所有严格递减的DPs。 归约对处理器定义如下： 设 `(≿, ≻)` 是一个归约对，DP处理器 `Proc` 定义为： ```plaintext Proc( (P, R) ) = { (P \≻, R) }, if P ⊆≿∪≻ and R ⊆≿ { (P, R) }, otherwise ``` 其中，`P \≻` 表示 `{s →t ∈P | s ̸≻t}`。 例如，对于问题 `({(11)}, R′sort)`，我们寻找一个归约对，使得 `(11)` 严格递减（相对于 `≻`），`R′sort` 中的规则弱递减（相对于 `≿`），但当前终止工具中的序无法满足此条件，因为该DP问题的终止本质上依赖于“每个非空列表都包含其最大值”这一论点。 #### 2. 多类重写 我们的目标是证明不存在无限最内层 `(P, R)` - 链。每个这样的链对应于如下形式的归约： ```plaintext s1σ →P t1σ i→!R s2σ →P t2σ i→!R s3σ →P t3σ i→!R ... ``` 其中 `si →ti` 是 `P` 中变量重命名后的DPs，`i→!R` 表示零个或多个到范式的归约步骤。归约对处理器确保： ```plaintext s1σ (≿) t1σ ≿ s2σ (≿) t2σ ≿ s3σ (≿) t3σ ≿ ... ``` 因此，严格递减的DPs（即 `siσ ≻ tiσ`）不能在最内层链中无限次出现，从而可以从DP问题中移除。 我们还可以放宽条件，若从DP的右侧 `tiσ` 到下一个左侧 `si+1σ` 严格递减，即对于每个 `tiσ` 到范式的归约都使项相对于 `≻` 严格变小（`tiσ ≻ si+1σ`），则该DP `si →ti` 也不能无限次出现，可从DP问题中移除。 本质上，如果对于每个正规替换 `σ`，`tσ i→!R q` 意味着 `tσ ≻ q`，则可以从DP问题中移除DP `s →t`： ```plaintext (14) 对于每个正规替换 σ，tσ i→!R q 意味着 tσ ≻ q ``` 其中，替换 `σ` 是正规的当且仅当对于所有变量 `x`，`σ(x)` 相对于 `R` 是范式。 为了移除 `({(11)}, R′sort)` 中的 `(11)`，我们需要使用满足 `(14)` 的归约对。这里 `t` 是 `(11)` 的右侧，即 `t = SORT(del(max(co(x, xs)), co(x, xs)))`。 当前的条件 `(14)` 过于严格，我们可以逐步放宽它，只考虑“类型良好”的替换。下面我们来明确“类型良好”的定义。 #### 3. 类型定义 设 `F` 是一个（无类型）签名，多类签名 `F′` 是 `F` 的类型化变体，如果它包含与 `F` 相同的函数符号，且具有相同的元数。即 `f` 是 `F` 中具有元数 `n` 的符号，当且仅当 `f` 是 `F′` 中具有类型 `τ1 × ... × τn →τ` 的符号。类似地，变量集 `V` 的类型化变体 `V′` 包含与 `V` 相同的变量，但每个变量都有一个类型 `τ`。对于每个类型 `τ`，`V′` 包含无限多个类型为 `τ` 的变量。 一个关于 `F` 和 `V` 的项 `t` 相对于 `F′` 和 `V′` 类型良好，当且仅当： - `t` 是一个变量（`V′` 中某个类型 `τ` 的变量）； - `t = f(t1, ..., tn)`（`n ≥ 0`），其中所有 `ti` 类型良好且具有类型 `τi`，`f` 在 `F′` 中具有类型 `τ1 × ... × τn →τ`，则 `t` 具有类型 `τ`。 一个TRS `R` 相对于 `F′` 和 `V′` 类型良好，当且仅当对于所有 `ℓ→r ∈R`，`ℓ` 和 `r` 类型良好且具有相同的类型。 对于任何签名 `F` 上的TRS `R`，可以使用标准类型推断算法自动计算 `F` 的类型化变体 `F′`，使得 `R` 类型良好。为了使我们的方法更强大，最好使用 `R` 类型良好的最一般类型化变体，这样可以减少被认为“类型良好”的项的数量，从而减少需要考虑的替换 `σ` 的数量。 例如，设 `F = {0, s, true, false, nil, co, ge, eq, max, if1, del, if2, SORT}`，为了使 `{(11)} ∪R′sort` 类型良好，我们得到 `F` 的类型化变体 `F′`，其类型包括 `nat`、`bool`、`list` 和 `tuple`，函数符号的类型如下表所示： | 函数符号 | 类型 | | ---- | ---- | | `0` | `nat` | | `ge, eq` | `nat × nat →bool` | | `s` | `nat →nat` | | `max` | `list →nat` | | `true, false` | `bool` | | `if1, if2` | `bool × nat × nat × list →list` | | `nil` | `list` | | `SORT` | `list →tuple` | | `co, del` | `nat × list →list` | #### 4. 最内层终止的持久性 最内层终止是一个持久属性，即一个TRS最内层终止当且仅当它在类型良好的项上最内层终止。 定理：设 `R` 是关于 `F` 和 `V` 的TRS，且 `R` 相对于类型化变体 `F′` 和 `V′` 类型良好，则 `R` 对于所有相对于 `F′` 和 `V′` 类型良好的项最内层终止当且仅当 `R` （对于所有项）最内层终止。 证明思路： - 组件封闭性：最内层归约中出现的所有项都来自同一个等价类，所以最内层终止显然是组件封闭的。 - 分类模块化： - `(d) ⇒ (c)` 是显然的。 - 为了证明 `(c) ⇒ (d)`，假设存在一个类型良好的项 `t` 具有无限最内层 `R1∪R2` - 归约，找到一个最小的这样的项，分析其归约过程，将其转化为 `R1` 上的无限最内层归约。 利用这个定理，我们可以放宽移除DP的条件，现在只需要对于每个类型良好的正规替换 `σ`，`tσ i→!R q` 意味着 `tσ ≻ q` 即可： ```plaintext (15) 对于每个类型良好的正规替换 σ，tσ i→!R q 意味着 tσ ≻ q ``` #### 5. 进一步放宽条件 条件 `(15)` 仍然较难满足，对于满足适当非重叠性要求且 `R` 已经最内层终止的DP问题 `(P, R)`，我们可以将条件放宽到只考虑基替换 `σ`。即如果对于每个类型良好的基项 `tσ` 的正规替换 `σ`，`tσ i→!R q` 意味着 `tσ ≻ q`，则可以从 `P` 中移除 `s →t`： ```plaintext (16) 对于每个类型良好的基项 tσ 的正规替换 σ，tσ i→!R q 意味着 tσ ≻ q ``` 例如，考虑DP问题 `(P, R)`，其中 `P = {F(x) →F(x)}`，`R = {a →a}`，使用类型化变体 `F′` 使得 `F : τ1 →τ2`，`a : τ1`。对于DP的右侧 `t = F(x)`，唯一类型良好的基实例是 `F(a)`，由于该项没有范式 `q`，条件 `(16)` 成立，但移除 `P` 中的唯一DP是不合理的，因为存在无限最内层 `(P, R)` - 链。这说明 `R` 的最内层终止对于将 `(15)` 替换为 `(16)` 是必要的。 为了证明条件 `(16)`，我们将其替换为更易于检查的条件 `(17)`： `