规范逻辑与非原子细化：原理、问题与解决方案

# 规范逻辑与非原子细化：原理、问题与解决方案 ## 1. 规范逻辑基础 ### 1.1 ZC 逻辑与模式 在逻辑分析中，采用了 Henson 和 Reeves 提出的“Church 风格”的 Z 逻辑版本，即 ZC。ZC 是一种类型化理论，它在高阶逻辑的类型基础上扩展了模式类型。模式类型的值是无序的、由标签索引的元组，称为绑定。 例如，如果 $T_i$ 是类型，$z_i$ 是标签（常量），那么 $[··· z_i : T_i ···]$ 就是一个（模式）类型。该类型的值是形式为 $\langle| ··· z_i⇛t_i ··· |⟩$ 的绑定，其中项 $t_i$ 的类型为 $T_i$。 ### 1.2 模式操作与符号 模式操作包括模式子类型关系（$\preceq$）、模式类型交集（$\land$）、（兼容的）模式类型并集（$\lor$）和模式类型减法（$-$）。用 $U$ 表示操作模式表达式，其类型可写为 $P(T_{in} \lor T_{out}')$，其中 $T_{in}$ 是输入子绑定的类型，$T_{out}'$ 是输出子绑定的类型。 同时，允许绑定连接操作，写作 $t_0 \star t_1$，前提是 $t_0$ 和 $t_1$ 的字母表不相交。该操作可提升到集合：$C_0 \star C_1 =_{df} \{z_0 \star z_1 | z_0 \in C_0 \land z_1 \in C_1\}$。 为避免在成员关系和相等命题中重复使用过滤操作，引入了以下符号约定： - 定义 3：$t_{T_0} \in_C P T_1 =_{df} t \restriction T_1 \in C$（$T_1 \preceq T_0$） - 定义 4：$t_{T_0}^0 = t_{T_1}^1 =_{df} t_0 \restriction (T_0 \land T_1) = t_1 \restriction (T_0 \land T_1)$（$T_1 \preceq T_0$ 或 $T_0 \preceq T_1$） - 定义 5：$t_{T_0}^0 =_T t_{T_1}^1 =_{df} t_0 \restriction T = t_1 \restriction T$（$T \preceq T_0$ 且 $T \preceq T_1$） 此外，还定义了原子模式、模式析取和模式合取： - $[S | P] =_{df} \{z_T | z \in S \land z.P\}$ - $S_{P_{T_0}}^0 \lor S_{P_{T_1}}^1 =_{df} \{z_{T_0 \lor T_1} | z \in S_0 \lor z \in S_1\}$ - $S_{P_{T_0}}^0 \land S_{P_{T_1}}^1 =_{df} \{z_{T_0 \lor T_1} | z \in S_0 \land z \in S_1\}$ ### 1.3 前置条件 操作模式的前置条件用于表达其部分性，即操作在某些状态下可能无法执行。定义如下： - 定义 6：$Pre U x V =_{df} \exists z \in U \cdot x =_{T_{in}} z$（$T_{in} \preceq V$） 同时，有以下关于前置条件的引入和消除规则： - 命题 12：设 $y$ 是一个新变量，则有 - $t_0 \in U$，$t_0 =_{T_{in}} t_1$ $\Rightarrow$ $Pre U t_1$ - $Pre U t$，$y \in U$，$y =_{T_{in}} t \vdash P$ $\Rightarrow$ $P$ ## 2. 复合操作的前置条件 ### 2.1 合取操作的前置条件 一般来说，操作合取的前置条件不是各个组成部分前置条件的合取。通常的合取引入规则不成立，但消除规则成立。 命题 13：设 $i \in 2$，则有 $Pre (U_0 \land U_1) t$ $\Rightarrow$ $Pre U_i t$（$Pre - \land i$） ### 2.2 析取操作的前置条件 析取操作前置条件的分析相对简单，因为存在量词在析取上是完全分配的。 命题 14：设 $i \in 2$，则有 - $Pre U_i t$ $\Rightarrow$ $Pre (U_0 \lor U_1) t$（$Pre + \lor i$） - $Pre (U_0 \lor U_1) t$，$Pre U_0 t \vdash P$，$Pre U_1 t \vdash P$ $\Rightarrow$ $P$（$Pre - \lor$） 定理 1：$Pre (U_0 \lor U_1) t \Leftrightarrow Pre U_0 t \lor Pre U_1 t$ ### 2.3 存在量化操作的前置条件 对于存在量化操作模式的前置条件，首先定义了一个模式类型 $T_z$，其字母表包含要从操作中隐藏的观察结果。 定义 7： - $T_z =_{df} T_{in}^z \lor T_{out}'^z$ - $T_{in}^z =_{df} [z : T_z]$ - $T_{out}'^z =_{df} [z' : T_z]$ 然后有以下关于存在量化的引入和消除规则： - 命题 15：设 $T_z \pr