基于共归纳类型理论的命令式基于对象的演算

### 基于共归纳类型理论的命令式基于对象的演算 #### 1. 基本定义 首先给出一些基本定义，设 $\Gamma$ 为上下文，$S$ 为栈，$E$ 为类型环境，$s$ 和 $\sigma$ 为存储，定义如下： - $\Gamma \subseteq S \triangleq \forall x \mapsto v \in \Gamma. x \mapsto v \in S$ - $\Gamma \subseteq E \triangleq \forall x:A \in \Gamma. x:A \in E$ - $S \subseteq \Gamma \triangleq \forall x \mapsto v \in S. x \mapsto v \in \Gamma$ - $E \subseteq \Gamma \triangleq \forall x:A \in E. x:A \in \Gamma$ - $\gamma(S) \triangleq \{x \mapsto S(x) | x \in Dom(S)\}$ - $s \preceq \sigma \triangleq \forall \iota_i \in Dom(s). \gamma(S_i), closed(x_i) \vdash wrap(b_i, s(\iota_i)(x_i))$，且 $\sigma(\iota_i) = \langle \varsigma(x_i)b_i, S_i \rangle$ - $\sigma \preceq s \triangleq \forall \iota_i \in Dom(\sigma). \gamma(S_i), closed(x_i) \vdash wrap(b_i, s(\iota_i)(x_i))$，且 $\sigma(\iota_i) = \langle \varsigma(x_i)b_i, S_i \rangle$ 对于闭包体 $\overline{b}$，定义 $stack(\overline{b})$ 为包含 $\overline{b}$ 中绑定的栈，$body(\overline{b})$ 为最内层的体，递归定义如下： - $stack(ground(b)) = \varnothing$ - $stack(bind(v, \lambda x.\overline{b})) = stack(\overline{b}) \cup \{x \mapsto v\}$ - $body(ground(b)) = b$ - $body(bind(v, \lambda x.\overline{b})) = body(\overline{b})$ #### 2. 动态语义的充分性 **定理 2（动态语义的充分性）**：设 $\Gamma$ 是良构的，且 $\sigma \cdot S \vdash \diamond$。 1. 若 $\Gamma \subseteq S$，且 $s \preceq \sigma$： - (a) 若 $\Gamma \vdash eval(s, a, s', v)$，则存在 $\sigma'$ 使得 $\sigma \cdot S \vdash a ; v \cdot \sigma'$，且 $s' \preceq \sigma'$； - (b) 若 $\Gamma \vdash evalb(s, \overline{b}, s', v)$，则存在 $\sigma'$ 使得 $\sigma \cdot stack(\overline{b}) \vdash body(\overline{b}) ; v \cdot \sigma'$，且 $s' \preceq \sigma'$。 2. 若 $S \subseteq \Gamma$ 且 $\sigma \preceq s$，若 $\sigma \cdot S \vdash a ; v \cdot \sigma'$，则存在 $s'$ 使得 $\Gamma \vdash eval(s, a, s', v)$，且 $\sigma' \preceq s'$。 **证明**： 1. 通过对推导 $\Gamma \vdash eval(s, a, s', v)$ 和 $\Gamma \vdash evalb(s, \overline{b}, s', v)$ 的结构进行互归纳证明。 2. 通过对 $\sigma \cdot S \vdash a ; v \cdot \sigma'$ 的结构进行归纳证明。 #### 3. 静态语义 术语的类型系统可以很容易地用自然演绎系统（NDS）表示。术语类型判断 $E \vdash a : A$ 转换为 $\Gamma \vdash type(a, A)$，其中 $type \subseteq Term \times TType$。类型的良构性和子类型关系也在这个设置中恢复，分别表示为 $wt \subseteq TType$ 和 $sub \subseteq TType \times TType$。对于栈，（分布式）类型环境的良构性由局部量化变量的新鲜性保证。 栈 $S$ 从归约判断中消失，类型环境 $E$ 从类型判断中消失，从而简化了判断本身和关于它的形式证明。全局上下文 $\Gamma$ 包含（自由）变量和对象类型之间的绑定等断言。NDS 中术语类型和相关判断的规则如下表所示： | 规则 | 条件 | | --- | --- | | $(wt\ obj)$ | $wt(B_i), \forall i \in I \Rightarrow wt([l_i : B_i]_{i \in I})$ | | $(sub\ refl)$ | $wt(A) \Rightarrow sub(A, A)$ | | $(sub\ trans)$ | $sub(A, B), sub(B, C) \Rightarrow sub(A, C)$ | | $(sub\ obj)$ | $wt(B_i), \forall i \in I \cup J \Rightarrow sub([l_i : B_i]_{i \in I \cup J}, [l_i : B_i]_{i \in I})$ | | $(t\ sub)$ | $type(a, A), sub(A, B) \Rightarrow type(a, B)$ | | $(t\ call)$ | $type(a, [l_i : B_i]_{i \in I}), j \in I \Rightarrow type(a.l_j, B_j)$ | | $(t\ var)$ | $wt(A), x \mapsto A \Rightarrow type(x, A)$ | | $(t\ clone)$ | $type(a, [l_i : B_i]_{i \in I}) \Rightarrow type(clone(a), [l_i : B_i]_{i \in I})$ | | $(t\ obj)$ | $(x_i \mapsto [l_i : B_i]_