基于共归纳类型理论的命令式面向对象演算及同余闭包算法

### 基于共归纳类型理论的命令式面向对象演算及同余闭包算法 #### 1. 命令式面向对象演算中的类型系统与证明 在命令式面向对象演算（如 impς）的研究中，利用共归纳类型理论（如 CC(Co)Ind）的特性对其语法和语义进行编码有着重要意义。 ##### 1.1 结果类型系统 通过两个相互共归纳的谓词，可以在 Coq 中轻松实现图 8 中的共归纳结果类型系统。在核心编码时，需要像对象类型那样携带完整的（结果）类型。以下是相关代码： ```coq CoInductive cotype_body : Store->Body->TType->Prop := t_ground: (s:Store) (b:Term) (A:TType) (type b A)->(cotype_body s (ground b) A) | t_bind : (s:Store) (b:Var->Body) (A,B:TType) (v:Res) (cores A s v A)-> ((x:Var)(typenv x) = (A)->(cotype_body s (b x) B))-> (cotype_body s (bind v b) B) with cores : TType->Store->Res->TType->Prop := t_void : (A:TType) (s:Store) (cores A s (nil (Lab*Loc)) (mk (nil (Lab*TType)))) | t_step: (A,B,C:TType) (s:Store) (v:Res) (i:Loc) (c:Closure) (l:Lab) (pl:(list (Lab*TType))) (cores C s v A)->(store_nth i s) = (c)-> ... ((x:Var) (typenv x) = (C)->(cotype_body s (c x) B))-> (cores C s (cons (l,i) v) (mk (cons (l,B) pl))). ``` ##### 1.2 元理论证明 形式化的一个主要目标是对 impς 的重要属性进行形式化开发，其中主题归约属性至关重要但证明较为复杂。该属性在 Coq 中形式化为以下定理： ```coq Theorem SR : (s,t:Store) (a:Term) (v:Res) (eval s a t v)->(A:TType) (type a A)-> ((x:Var; w:Res; C:TType)(stack x)=(w)/\(typenv x)=C-> (cores s w C))-> (EX B:TType|(cores t v B)/\(sub B A)). ``` 为证明该定理，需要处理存储、对象、对象类型、结果等具体结构的各个方面，为此已经形式化证明了许多关于操作语义、项和结果类型的技术引理。这些引理相对紧凑且易于证明，特别是通过 Cofix 策略对 cores 谓词进行了共归纳证明。 与完整的 impς 相比，这里的共归纳编码在处理存储类型时更加简单。虽然完整 impς 中存储类型和结果类型是归纳编码的，但共归纳编码的证明具有一定的可重用性，尤其是那些不需要显式检查存储类型结构的证明。同时，将栈和类型环境委托给证明上下文，以及使用共归纳处理存储循环，大大减少了证明的长度和复杂度。 ##### 1.3 高阶抽象语法与上下文理论 形式化的另一个关键方面是使用（弱）高阶抽象语法。CC(Co)Ind 的表达能力在某些情况下不足，因此引入了上下文理论（ToC）。ToC 通过假设一组捕获（变量）名称和项上下文基本自然属性的公理，实现了高阶抽象语法中模式的平滑处理，数学和逻辑开销非常低。 上下文理论允许通过不饱和公理创建“新鲜”变量。在本文中，采用了两种形式的不饱和公理： ```coq Axiom unsat : (A:TType; xl:Varlist) (EX x|(fresh x xl)/\(dummy x)/\(typenv x)=A). Axiom unsat_cores : (s:Store) (v:Res) (A:TType) (cores s v A)-> (xl:Varlist)(EX x| ```