第10章子定型

第10章子定型内容摘要：

(n) = M (n)  : l1:1, …, ln:n (重新定序公理 ) 其中 是 {1, …, n}的任意置换 记 录 • 例 b=true, a=3, c=“Hello”=a=3, b=true, c=“Hello”: b : bool, a : int, c : string a =3, b = true, c = “Hello” = a =3, b = true: a : int, b : bool 子定型的语义模型 概述 • :最一般的转换语义 – 每个类型解释 为一个集合 – 每当 A:B， 则有从 A到 B的“转换”函数 若 A是 B的子集，可用恒等函数完成从 A到 B的转换  子定型的语义模型 子定型的转换解释 – 如果 b1 : b2直接由基调给出，相应的转换函数必须作为解释的一部分给出 – 如果  :是使用某个证明规则从基调可证明的，那么从该基调给出的“基本”转换函数可以定义相应的转换函数 – 有了转换函数，那就可以给类型化的项以含义 – 定义类型化项的含义的自然方式是在项的定型推导上归纳 子定型的语义模型 • 定义类型化项的含义的自然方式是在项的定型推导上归纳 • 如果   M:可由 推导，那么该项的含义将是把 到 的转换函数应用到与   M:的定型推导有关的含义上 • 对于 :， 所需要的转换函数是恒等函数、基本转换和由函数合成定义的转换  M :    :   M :   子定型的语义模型 • 任何 的语义模型可以作为 :的语义模型 – 只要对基本转换函数能找到适当的解释 – 其它转换函数都是 可定义的 – 从 的等式可靠性和完备性定理中可导出 :的对应定理   子定型的语义模型 • 从 :基调  = B, Sub, C开始，将 上的每个:项翻译成基调 B, CSub上的 项 – 让 CSub是 C和一组写成 c 形式的不同常量符号的并集 – 对每个子定型 b1:b2,有符号 c :b1b2 – 转换函数上的协调限制 c  …  ca = c  …  ca : a  b – 所有这样 的等式集合称为    b2 b2 b ak a1 al b a1 b1 b1 子定型的语义模型 转换函数 • c的定义是在  :证明上的归纳 (ref :)  : c  x:.x (trans :) c  x: . c (c x) ( :) c  f: 1 2. x: (f (c x)) 通过一系列不改变相关转换函数的证明变换，可 以证明这些转换函数是唯一的  :   :   :  1:1 2:2 12:12     12 12 2 2 1 1  子定型的语义模型 项的翻译 对基调  = B, Sub, C上的任何 :项 M:,定义 它到基调 B, CSub上的 项的翻译 Trans(M:), 由 :项的定型规则上的归纳， Trans的 定义如下 (cst) Trans (  c:) = c (var) Trans (x:  x:) = x ( Intro) Trans (  x:.M: ) = x:.Trans(, x:  M:) ( Elim) Trans (MN:) = Trans(M: ) Trans (N:)   子定型的语义模型 (add var) Trans (, x:  M:) = Trans (  M:) (subsumption) 若 M:是可用   :从 M: 推导的 ， 则 Trans (  M: ) ＝ cTrans (  M: ) • 引理 如果  M:是基调 B, Sub, C上一个可推导的 :定型断言 ， 则 Trans(M:):是基调 B, CSub上可推导的 定型断言   子定型的语义模型 • 命题 令  = B, Sub, C是一个 :基调 ， 并且令 M: 是 上的一个 :项 若对于 M:有两个定型推导 ， 并且令 M1,M2=Trans(M:) 是按这两个定型推导得到的 M的两个翻译 则使用 的证明规则可得   M1 = M2:    递归类型和对象的记录模型 本节研究带函数成员的记录 – 用 “ 方法结果 ” 的记录来表示对象 : 选择一个记录的成员同发送相应的消息到一个对象返回同样的值 – 对于带参数的方法 ， 记录选择将返回一个函数 – 这个模型简单 、 易理解 、 提供了面向对象的概念可以用类型化 演算来研究的某种感觉 递归类型和对象的记录模型 • 在面向对象的程序设计中 ， 对象类型经常可以递归地定义 – 点类型 point type point = x:int, y:int, move:int  int  point – 如果 有带 x和 y坐标和一个方向的 “ 有向 ” 点 ， 那么每个有向点可以。