重写时态逻辑入门

### 重写时态逻辑入门 #### 1. 可计算重写理论基础 在可计算重写理论中，对于给定的重写规则 \(l : q \to r\)，若存在基础 \(A\) - 等价类 \([t]_A\) 满足 \([t]_A \xrightarrow{1}_{RR/A} [t']_A\)，总能找到对应的重写 \([can_{E/A}(t)]_A \xrightarrow{1}_{RR/A} [t'']_A\)，使得 \([can_{E/A}(t')]_A = [can_{E/A}(t'')]_A\)。 基于条件 (1) - (3) 可知，对于 \(\Sigma\) 中的每个类别 \(s\)，\((\to^1_{R,s})\) 是 \(T_{\Sigma/E \cup A,s}\) 上的可计算二元关系。判定 \([t]_{E \cup A} \to^1_R [u]_{E \cup A}\) 的步骤如下： 1. 生成 \(can_{E/A}(t)\) 模 \(A\) 的所有单步 \(R\) - 重写的有限集合。 2. 检查其中是否有与 \([can_{E/A}(u)]_A\) 具有相同的模 \(A\) 的 \(E\) - 规范形式。 满足以下条件的重写理论 \(R\) 属于 \(RWTh_0\) 类： - \(R\) 是可计算的，且有一个名为 \(State\) 的类别对应系统的状态。 - 若 \(R\) 有一个名为 \(Prop\) 的类别，则必须有一个名为 \(Bool\) 的类别，包含常量 \(true\) 和 \(false\)，以及一个运算符 \(\vDash : State \times Prop \to Bool\)。\(Prop\) 是原子状态谓词的指定类别，\(\vDash\) 用于定义给定状态是否满足给定状态谓词。 - \(R\) 是无死锁的，即不存在有限序列 \([t_1]_A \xrightarrow{1}_R [t_2]_A \cdots [t_n]_A \xrightarrow{1}_R [t_{n + 1}]_A\) 使得 \([t_{n + 1}]_A\) 无法进一步重写。 #### 2. 证明项 重写逻辑的推理规则可推断出重写理论 \(R\) 所指定系统中的所有并发计算。给定两个状态 \([u], [v] \in T_{\Sigma/E \cup A}\)，能从 \([u]\) 经过可能复杂的并发计算到达 \([v]\) 当且仅当能证明 \(R \vdash [u] \to [v]\)。这种复杂计算由证明项见证，例如在客户端 - 服务器协议中，从状态 \([u]\) 到状态 \([v]\) 的并发计算可由证明项 \(\lambda = req(b, a, 7) \ reply(a, b, 7)\) 表示。 证明项之间存在等价关系，任何证明项 \(\lambda\) 都有（可能多个）等价的交错描述，可表示为单步证明项 \(\gamma_i\) 的顺序组合 \(\gamma_1; \cdots ; \gamma_k\)。单步证明项形式为 \(\gamma = t[l(u_1, \cdots, u_n)]_p\)，其中 \(t, u_1, \cdots, u_n\) 是 \(\Sigma\) - 项，\(l\) 是规则标签。 为了在可计算重写理论中规范处理单步证明项，引入规范单步证明项的概念。对于可计算重写理论 \(R = (\Sigma, E \cup A, R)\) 和状态 \([u]_{E \cup A}\)，由于证明项之间的等价关系包含模 \(E \cup A\) 的等价性，通常会有无限多个单步证明项。而规范单步证明项能确保从给定状态出发的单步重写只有有限个规范表示。 #### 3. 计算 若 \(R = (\Sigma, E \cup A, R) \in RWTh_0\)，可定义两个有用的集合： - \((Can_{\Sigma/E,A})_{State}\)：所有形式为 \([can_{E/A}(t)]_A\) 的 \(A\) - 等价类的集合，其中 \(t\) 是类别为 \(State\) 的基础 \(\Sigma\) - 项，描述了系统所有状态的规范形式。 - \(CanPTerms_1(R)\)：\(R\) 中所有单步规范证明项的集合。 \(R\) 中的无限计算是一对函数 \((\pi, \gamma)\)，其中 \(\pi : \mathbb{N} \to Can_{\Sigma/E,A}^{State}\)，\(\gamma : \mathbb{N} \to CanPTerms_1(R)\)，且对于所有 \(n \in \mathbb{N}\)，\(\pi(n) \xrightarrow{\gamma(n)}_1 \pi(n + 1)\) 是 \(R\) 中的规范单步重写证明。 以下是无限计算的图形表示： ```mermaid graph LR classDef startend fill:#F5EBFF,stroke:#BE8FED,stroke-width:2px; classDef process fill:#E5F6FF,stroke:#73A6FF,stroke-width:2px; A([π(0)]):::startend -->|γ(0)| B([π(1)]):::process B -->|γ(1)| C([π(2)]):::process C -->|...| D([π(n)]):::process D -->| ```