·586· 北京科技大学学报 1998年第6期 ●变元(x,y,…)是项； ●如果A,B,M和N是项，那么Ix:A.B,1:A.MMN,∑x:A.B,pair∑x:A.BA,M, π1(0和π2(M都是项 用≡表示等同，△表示化简，≌表示变换，如：(ax:A.)N△[N/M. Typei叫类别，也叫类型空间，其中包含的类型形成一种所谓类型累积(ype comulativ-- ity).这种累积在语法上用下面的偏序关系来表示. 定义1类型累积. 定义≤为项上与变换≌有关的最小偏序，有：(1)Prop≤Typei≤Type1≤；(2)如果 A≌A,而且B≤B',那么ΠⅡx:A.B≤Ⅱx:A'.B';(3)如果A≤A,而且B≤B',那么∑x:A. B≤∑x:A'.B',A<B当且仅当A≤B且A≌B. ECC中的上下文是有形式xM的有穷系列.在此x是一个变元，而M是一个项.空上下文 用()表示，断言的形式为is valid或T-MA,在此I是上下文，而M和A是项. 下面是ECC的推理规则，V(T)表示在上下文中的自由变量集. T-A:Typei (Cl)>is valid T,is valid(xEVO方 (C2 I.xA,I'is valid T,xAH M:B （vamT,xAP十xA；T-ixAMⅢEAB Tis valid Tis valid (KIProp:Type0' (K2 Typei:Typei+T° I,x水PPop；I2 Typei IHA;Typei I,x A-B:Typei (I1TPⅡA.P:Prop CeO T Tk∑xAB:Typei T-M:A I-N:[M/x]B I,x.A-B:Typei (pair) T-pair∑xAB(M,M:∑xA.B au'品是arn丽 T-M∑xA.B (conv) I-M:A I-4:Typei 4);(conv) TM:A IHA':Typei (AA). T-M:A' T M:A' 对断言J的推导形式一个有穷的断言序列J,…,Jn有J=J.比如，对于1≤i≤n,J是某 个推理规则某次施用的结果，其前提为J少<)，如果存在J的一个推导，则称断言J是可推 导的.用T上“A表示“如TM:A对某个A是可推导的，那么项M就有上下文中的类型A”. 下面从推理规则来看一下ECC的类型的分层累积特性.在ECC中，空间(universe)是一 个类型，它把许多类型作为其对象.也就是说，这些类型又是把空间作为它们的类型的.规则 (KI)、(K2)就引人了空间类型Prop和Typei(i∈w)可直接看出：Prop∈Type0 ETypel E·, 从而有，类型Prop的任一对象都是类型Type0的一个对象，而类型Typei的任一对象都是 Typei+I的一个对象.也就是说，PeopEType(0 Typel….这种空间之间的类型包含，与≤ 一起构成了前面定义的类型之间的子类型关系.其推理规则表示即是(cum).这一规则隐示，· · 北 京 科 技 大 学 学 报 年 第 期 变元 ， ， … 是 项 如果 ， ， 和 是 项 ， 那 么 ， 又 ， ， 艺 ， 艺 ， 扔 ， 们 哟和 二 娜都是 项 用 三 表示 等 同 ， △表示 化简 ， 望表示 变换 ， 如 认 娜 肥〔 肠 叫类 别 ， 也 叫类 型 空 间 ， 其 中包含 的类 型 形 成 一 种 所 谓 类 型 累 积 这种 累 积在语法 上 用 下 面 的偏 序关系来表示 定义 类 型累积 定 义 ‘ 为 项 上 与 变 换 望 有 关 的 最 小 偏 序 ， 有 ‘ 肠 ‘ ‘ … 如 果 望 才 ， 而 且 ， ， 那 么 才 尸 如 果 ’ ， 而 且 ‘ ， ， 那 么 区 ‘ 艺 才 了 ， ‘ 咬 当且仅 当 ‘ 且 哭 中的上下 文是 有 形 式 戈 的有穷系列 在此 是 一个变元 ， 而 是 一个项 空 上下 文 用 表示 ， 断言 的形 式 为 或厂 卜 胚 ， 在 此 是 上下 文 ， 而 和 是 项 下 面是 的推理规则 表示 在上下 文 中的 自由变量集 卜 厂 ，茉 苗 ， 汇 ， ‘ ，工 ，厂 ’ 卜 羌 ， 尤 卜 触 一又茉 掀 茉 了 训丫 产 ‘ 矛、 、 ，丫佘岩猛 击洗答恙 牛不焉备黑石 卜 次 ， 不 卜 卜 茉 一 触 汇 厂卜 卜 【 名 卜 ， 戈 卜 卜 艺二 厂卜 触月 卜 龙 万 ， 羌 卜 卜 叉 二 从 的 艺二 兀 厂卜 肚 艺二 厂卜 兀 娜 兀 卜 艺二 厂卜 兀 娜 二 娜 卜 触 卜 份 卜 几吏 ， 今 卜 掀 卜 几 卜 人更 ‘ 〕 对断言 的推 导形 式 一个 有穷 的断言序列 去 ， … ， 寿有 大兰 比如 ， 对于 ‘ ‘ 。 ， 是某 个推理规则某 次施 用 的结果 ， 其前提 为 弓以 · 如果存在 的一个推 导 ， 则称断言 是可 推 导的 用 卜 赫 表示 “ 如 卜 胚 对某个 是 可 推导的 ， 那么项 就有上下文 中的类型 ’尸 下 面从推理规则来 看 一下 的类 型 的分层累积特 性 在 中 ， 空 间 是 一 个类型 ， 它 把许多 类 型 作 为其 对象 也 就是 说 ， 这些 类型 又是 把空 间作为它 们 的类 型 的 规则 、 就 引人 了空 间类 型 和 可 直 接看 出 〔 ‘ 。 二 ， 从而有 ， 类 型 的任 一 对 象 都是 类 型 的 一 个 对象 ， 而 类 型 的 任 一 对象 都 是 的一 个 对象 也 就 是 说 ， 二 互 二 · … 这 种 空 间之 间 的类 型 包含 ， 与 一 起 构成 了前 面 定 义 的类 型 之 间 的子类 型 关系 其推理规则表示 即是 这 一规则 隐示