安全实例化组件的类型系统

理论计算机科学电子笔记97（2004）197-217www.elsevier.com/locate/entcs一个安全实例化组件的类型系统1Marc Bezem2 和黄长3卑尔根大学信息学院PB.7800，5020 Bergen，Norway摘要组件组合可以导致同一组件的多个实例。某些组件一次只能加载一个实例，例如，当使用唯一的外部资源给出了一种抽象构件语言和一种保证构件安全实例化的类型系统。语言的特点是实例化，组合和一个简单的作用域机制，用于释放实例。关键词：类型理论，构件软件，程序正确性。1介绍想象一个由几个组件组成的计算机程序这些组件可能是从不同的供应商那里购买的，它们可能使用其他组件，而其他组件又使用其他组件，等等。为了分析这个过程，短语newc的语义大致上是指分配资源来运行一个c实例。这不仅意味着为c的数据分配内存空间。1这项研究得到了挪威研究委员会（NFR）的支持。2电子邮件：bezem@ii.uib.no3 电子邮件地址：hoang@ii.uib.no1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.04.037198M.贝泽姆张/理论计算机科学电子笔记97（2004）197-217结构等，但这也意味着创建由C使用的组件的实例。(The创建子组件实例的确切时刻取决于绑定机制，参见[15]。在上面概述的情况下，很容易发生编写者没有预见到的情况，创建了同一组件的不同实例。对于许多组件来说，这根本不是问题。然而，存在不允许多个实例并行运行的组件[4，10]，例如，如果组件使用唯一的外部资源，如打印机或串行输出设备，或者如果组件是集中式功能，如发布序列化ID号[7]。在[10]中，Meijer指出，除了第一个请求之外，对于不能并行存在的组件的多个版本的唯一选择是失败。组件的单实例属性可以由组件实现本身使用单例模式控制[7]。然而，在组件软件中，组件将被使用的上下文不应该被完全预期，因此有些情况下我们需要在更高的级别上控制特定组件的实例数量[5]。本文的目的是开发一个类型系统，它允许一个静态检测，在开发/组合时间，是否多个实例的某些组件并行运行。为此，我们设计了一个基本的组件语言，我们已经抽象出组件的许多方面。我们保留的主要特性是实例化、（顺序）组合和作用域。在这个抽象层次上，组件和类与实例和对象之间几乎没有什么区别。请记住，我们在这里报告正在进行的研究：在不久的将来，将包括更复杂的这里使用的组件的简单绑定机制与ML [11]等函数式语言中的let绑定相似，因此与lambda抽象和应用相似。然而，这里使用的类型完全不同。在某种程度上，我们有可能沿着所谓的纯类型系统（PTS）的路线发展我们的类型理论，见[3]。这增加了我们对所选抽象的信心，可以被视为对PTS通用性的贡献。有几个关于组件类型系统的工作，参见[14，16]。但是，它们没有解决组件的单个实例化的问题。我们的类型背后的直觉与所谓的线性类型有一些相似之处[2，6]。线性类型通常表示一个值将被精确地一次在它的范围内，而不是在我们的情况下最多一次这种差异在我们的削弱和开始规则中得到了体现（见下文）。然而，与线性类型的可能联系仍然必须加以探讨。M.贝泽姆张/理论计算机科学电子笔记97（2004）197-217199本文的组织结构如下。在下一节中，我们将开发组件语言及其术语和操作语义。我们在第3节中定义了类型和类型关系。 然后我们在第四节中证明了类型系统的一些性质。在第5节中，我们概述了一个多项式时间类型的推理算法，最后给出了一些结论和未来研究的方向技术证明委托给附录。2组件语言2.1方面由于我们主要对实例化、组合和作用域感兴趣，因此我们在组件语言中对组件的所有其他方面进行了抽象。在这个抽象层次上，我们没有详细描述组件是如何连接的，就像在许多架构描述语言中一样，比如Wright[1]，Dar- win [9]，SADL [12]和ACME [8]。一个组件可能允许也可能不允许多个实例并行运行。我们通过使用两个不相交的集合S和E来区分这两种成分，用于这种- 是的因此，S中的一个分量可以有任意多个实例，而E中的组件每次最多只能有一个实例我们使用扩展的巴科斯-诺尔形式和以下元符号：|用于选择，用于Kleene闭包（零次或多次迭代）的后固定括号和用于分组的圆括号。花括号{和}是组件语言的一部分，用作作用域分隔符。定义2.1[组件程序]组件程序由下面的抽象语法给出，x的范围是SE。Prog：：=Decl;ExpDecl：：=（x−Exp）Exp：：=|新x Exp|{Exp}Exp上述表达式Exp的语法生成与Exp：：= Exp相同的表达式|新x|ExpExp|{Exp}但是具有非模糊性的技术优势。因此，一个程序由一系列所谓的组件声明组成，后面跟着一个表达式Exp，它会触发执行。对于操作语义的精确定义，读者可以参考下一节。特别是那里的例子将有助于阐明打字规则200M.贝泽姆张/理论计算机科学电子笔记97（2004）197-217这些都是要遵循的。一个复杂的定义x−EXP表示复杂的x是由复杂的x在EXP上的压缩而成的。特别地，x−1表示x是一个本原分量。带有不同变量的声明列表称为基础，如PTS [3]。我们使用Γ，π，.在基地范围内。根据上述语法，组件表达式可以有几种形式。最简单的，空表达式用于声明原始组件。否则，表达式可以是一个新x的将组件放在作用域中的目的是，在它们的生存期内，这些组件需要彼此协作，然后可以解除分配。我们用A，...，E，Exp来对表达式进行范围。一个程序是确定性的，如果每个组件最多只有一个声明。在本文中，我们只研究确定性程序。例如，设S={c，d}，E={a，b}。格式良好的程序我们的语法中的Prog可以如下所示：d−a−newdb−newac−newd{newbnewd}newa;新的c我们将在下面的部分中回到这个例子。2.2操作语义在本节中，我们给出了我们语言的操作语义。我们使用所谓的后置表达式，它是通过删除表达式前缀中的零个或多个连接开头{来定义2.2 [后表达式]后表达式由抽象的yntaxP：：=（Exp}）Exp给出，其中Exp如定义2所示。一曰：我们还给出了两个表达式连接的形式定义定义2.3[表达式连接]的连接表达式M.贝泽姆张/理论计算机科学电子笔记97（2004）197-217201两个表达式A和B，写作A@B，递归定义如下：B=B（ newxA1 ） @B=newx（ A1@B ） （ {A1}A2 ）@B={A1}（A2@B）一个表达式与一个后表达式的连接的定义方式与两个表达式的连接相同，并再次导致一个后表达式。操作语义被建模为一个转换系统，其中的状态是一个堆栈S的多集后面跟着一个后表达式P。堆栈和后表达式由""分隔堆栈的元素由“：”分隔。堆栈在右端被推动和弹出。空栈用y表示。当堆栈的部分是空的时，我们使用M表示堆栈的顶部，使用S表示堆栈的其余部分。当深度堆栈是一个，我们只写多集M，如下面的第二个转换规则。多集表示为[... 。]，其中集合通常表示为{...。}。 M（x）是多重集M中元素x的重数。 操作是多重集的加法并。定义2.4[转换规则]转换规则如下：故障P终止→故障M终止→成功S：M：MJ终止→故障S：M 新的xPx− <$E∈Prg→S：（M[x]） 联系我们S：M {P推→S：M：[ ]CUPS：MPpop→S pop转换规则可以解释如下。当堆栈为空时，转换过程终止并失败。当输入为“0”时，转换过程也终止。在这种情况下，如果堆栈的深度为1，则程序成功，否则程序失败。当输入是newx时，x被添加到堆栈顶部的多集，newx被x的声明替换。最后两条规则是范围。当进入一个新的作用域时，输入的第一个元素是当离开一个作用域时，也就是说，当输入的第一个元素是202M.贝泽姆张/理论计算机科学电子笔记97（2004）197-217堆栈顶部的多集被弹出。这意味着在此范围内创建的所有实例都已被丢弃。第2.1节中的例子再次用来说明我们的运算语义。过渡步骤如下：[ ]newcc−newd{newbnewd}newa→[c]newd{newbnewd}newad−→[c，d]{newbnewd}newapus→h[c，d]：[]newbnewd}newab−newa→[c，d]：[b]newanewd}newaa− newd→[c，d]：[a，b]newdnewd}newad−→[c，d]：[a，b，d]newd}newad−→[c，d]：[a，b，d，d]}新wapo→p[c，d]newa− newd→[a，c，d]newdd−→[a，c，d，d]at→e成功在这个例子中，独占组件a被实例化两次。然而，由于范围的原因，在每个时刻最多有一个a的实例如果d是互斥的，则程序的执行将在[c，d]：[a，b]，newdnewd}newa处失败。继续加载将复制独占组件d。3类型系统3.1类型分量表达式E可以使用若干分量。在后者中，有些实例存在于E的整个生命周期，而另一些实例只存在一段时间，然后被释放。因此，我们使用两个集合来表示组件表达式的类型。第一个集合Xi收集在表达式的生命周期内实例化的所有组件，第二个集合Xo由那些具有在表达式执行后仍存在的实例的组件组成。定义3.1[类型]组件表达式的类型集包括M.贝泽姆张/理论计算机科学电子笔记97（2004）197-217203集合对的X i| X o其中Xo，Xi=SE。 类型由大写和下标大写你... Z.3.2类型关系在定义类型关系之前，我们给出定义域的形式定义，定义域是基中的变量集。定义3.2[基变量]基Γ中声明变量的集合，写作Dom（Γ），归纳定义如下：Dom（）=Dom（x−<$A，Γ）={x} <$Dom（Γ）例如，假设Γ=d−，a−newd ，b−newa ，c−newd{newbnewd}newa然后我们有Dom（r）={a，b，c，d}一个类型三元组ΓA：X i|也简称类型化，表示给定基Γ，分量表达式A具有类型Xi|罗非鱼x 类型关系是一组归纳定义的类型三元组。它以通常的方式定义，通过给出类型规则来构造有效类型的派生树定义3.3[打字规则]公理► ：|∅ΓA：X i|X oStartΓ，x−<$Anewx：Xi<${x}|X o<${x}x∈/Dom（Γ）ΓA：X i|X或Y1：Y i|Y o弱化Γ，x−<$A1<$A：Xi|X ox∈/Dom（Γ）测序r=newx：X i|X或Y i|Y o新xA：Xi<$Yi|XoYoX oEYi=， A范围I：X i|X或Y，A2：Y i|Y oΓ {A1}A2：Xi<$Yi|Y o204M.贝泽姆张/理论计算机科学电子笔记97（2004）197-217让我们简单地解释一下上面的五条打字规则。规则公理不需要前提，用于取零。Rule Start允许我们输入一个新的组件实例。Axiom和Start的组合允许我们键入primiti vecom ponetsx−k的实例。我们使用d来扩展基，这样我们就可以在规则Sequencing和Scope中组合类型，这允许我们使用前缀new x和作用域表达式respectively来键入组件组合。 x∈/Dom（Γ）的恒等式表示了一个简单的圆性。副条件X oEYi=防止独占组件在同一作用域中被多次实例化。继续2.1节的例子，我们展示了{newbnewd}newa的类型派生树。首先，newb的类型可以如下导出：（类型规则的名称被缩短为前三个字母）。StaAXI► ：|∅StaStad−newd：{d}|{d}d−，a−newdnewa：{a，d}|{a，d}d−，a−newd ，b−newanewb：{a，b，d}|{a，b，d}newd的类型可以减弱如下：StaAXI► ：|∅StaAXI► ：|∅韦阿d−newd：{d}|{d}d−newd：{d}|{d}d−，a−newdnewd：{d}|{d}使用这个结果，我们可以通过弱化得到newd的另一种类型......Wead−，a−newdnewd：{d}|{d}d−，a−newdnewa：{a，d}|{a，d}d−，a − newd，b−newanewd：{d}|{d}类似地，我们可以弱化newa的类型：d−，a−newd ，b−newanewa：{a，d}|{a，d}Now，letr=d−nnn，a−nwd ，b−nwa。Based上的所有类型，我们可以如下导出{newbnewd}newaSeq......r= new b：{a，b，d}|{a，b，d}新的d：{d}|{d}...SCOr= new b = new d：{a，b，d}|{a，b，d}r= new a：{a，d}|{a，d}新a {a，b，d}|{a，d}请注意，满足规则Sequencing的边条件XoEYi，d∈/E.M.贝泽姆张/理论计算机科学电子笔记97（2004）197-217205有了定义的类型、术语和类型规则，我们现在可以定义好类型程序的概念。定义3.4[良型程序]一个良型程序P=Decl;Exp是良型的，如果Exp可以在从Decl构建的基中类型化。在这方面，有一项理解是，这些声明可能需要重新排序，以形成法律依据。4类型系统在本节中，我们将陈述类型系统的一些属性。本节末尾的不变定理及其正确性推论将类型系统与操作语义联系起来。为了证明不变性质，需要一些定义和引理引理的一些技术证明被委托给附录A，以提高本节的可读性公式4.1[Bases]Letr=x1−A1， . 。 ，xn−<$Anbeaba s是，且让tA是一个表达式。• 称Γ是合法的，如果Γ ≠A：X i|对于一些A，Xi，和XO。• 定义x−<$A在Γ中，记作x−<$A∈Γ，如果x<$xi且A<$Ai对某个i。• 是Γ的一部分，记作x ik− <$A ik其中1 ≤i1<. 1，则转换步骤为：S1：. . . 。 ：Sn<$}An−1. 。 。}A1po→p学生1：……：Sn−1A n−1}.. 。}A1由于m=n− 1，所有结论都可以立即• 如果An=newx，通过生成引理，我们有x− <$AJ∈Γ。然后，过渡步骤为：史： 。 ：S newx}A. 。 。}Ax−<$AJ∈→Γ学生1：……：（S n[x]）AJ}A n−1.. 。}A1我们有m=n，Bm=AJ，Bj=Aj，其中1≤j≤n− 1。 因此，r ∈B j：X i|X o紧随其后，其中1 ≤j≤m− 1。 Γ B m：Yi|Y ojjmM也可以从引理4.4得出，应用于Γ new x：X i|X O以M mYi=Xi−x和Yo=Xo−x。嗯嗯嗯通过假设，等式（2）对于k≤m−1成立，我们只需证明等式（2）对于k=m。 如果x∈/E，则所述问题是由于（SJ：. 。 ：SJ）|E=1N（SJ：. ：SJ）|E和Y iX i. 否则，由于Yi=X i−x，sox∈/Yi.1m m m嗯嗯通过等式（1），其中hk=n且x∈Xiwhevex∈/（S1：. 。 ：Sn）。因此，我们认为，（SJ：. ：SJ）|EYi当新的独占变量x只出现在1m m交叉操作的左边。结论SJ|E单曲也如下只有一个新的x∈SJ和x∈/（S1：. ：Sn−1）|E=（S，j）：. ：SJ）|E.210M.贝泽姆张/理论计算机科学电子笔记97（2004）197-217m1m−1M.贝泽姆张/理论计算机科学电子笔记97（2004）197-2172111n n−11• 如果An=newxC，其中C/=N，则转换步骤为：史： 。 ：S newxC}A. 。 。}Ax−<$AJ∈→Γ学生1：……：（S n[x]）AJ @ C}A n−1.. 。}A1我们有m=n，Bn=AJ@C，且Bj=Aj，其中1≤j≤n− 1。因此，B j：是的，|对于1 ≤j≤n− 1，Y o紧随其后。ΓAJ @ C：Y i|你也jj nn由引理4.8得出，应用于Γ-newxC：X i|罗非鱼x 其余M m证明与前一种情况类似。• 如果An={C}D，则转换步骤为：S1：. . . 。 ：Sn<${C}D}An−1。 。 。}A1pus→h学生1：……：Sn：[ ]∝C}D}A n−1}.. 。}A1我们有m=n+1，Bm=C，Bn=D和Bj=Aj，其中1≤j≤n−1。 因此，r ∈B j：Y i|Yo对于1 ≤j≤n− 1，则立即出现。J JΓ B m：Y i|Y o和Γ B n：Y i|Yo也可以从引理4.4得出，MM nnΓ{C}D：X i|罗非鱼x 其余的结论都是琐碎的。M mQ推论4.12（正确性）从栈[ ]开始，只包含空的多集和一个类型良好的表达式S|E在每个连续状态下都是单一的，也就是说，每个互斥组件在某个时间最多有一个实例。证据 从n= 1开始迭代前面的定理。Q5类型推断在本节中，我们将简要介绍一个多项式时间类型的推理算法。类型推断问题，或者更准确地说，这个问题的一个例子，是确定，给定基Γ和表达式A，一个类型X i|X o，使得A：X i|罗非鱼x 根据命题4.7，我们知道这样的类型是唯一的，如果它存在.自动推断这些类型使程序员从显式给出类型并检查它们的任务中解脱出来。推断出的类型可以用来指导组件程序的设计。此外，通过正确性结果推论4.12，可以安全地执行良好类型的表达式后者也可以通过根据定义2.4中的规则运行操作语义来测试。然而，运行这些规则可以是指数级的（例如，通过迭代复制），因此多项式时间类型的推理算法是首选的。212M.贝泽姆张/理论计算机科学电子笔记97（2004）197-217让Prog成为一个组件程序。类型推断的一个必要（但不充分）条件是 ， Prog 中 的 声 明 可 以 重 新 排 序 为 abasisΓsuch ， 即 对 于 在 Γ 中 的nydclarationx−A，在A中发生的变量已经在先前的Γ中声明。换句话说：ifr=n，x−nA，nnVar（A）<$Dom（A）（3）这种重新排序的存在可以在多项式时间内通过分析与Prog.从现在开始，我们假设Γ是由Prog中的所有声明组成的基，并且满足（3）。以下考虑因素与使用哪种特定排序无关，只要它满足（3）。类型推理算法背后的基本思想是利用类型规则是语法导向的这一事实，或者换句话说，使用生成引理4.4。通过将该引理的第2和第3条应用于形式newxA与A分别为{ B }和{C}，我们可以将类型推断问题的任何实例分解为表达式的形式是newx。然后我们可以在基Γ中查找x的声明。如果找不到x的声明，则无法推断类型。其他wis er=，x−A，J对于生成引理的some，J和A和clause趋向s，x−A。 这里有一些c是必须要谈的，以确保它是一个pol ynomial。一朴素递归算法可以通过递归地生成相同类型推理问题的重复实例来表现指数行为。然而，通过存储已解决的实例可以避免重复观察所有的实例都是这样的形式：推断A的类型，其中A是原始类型推断问题的基础的初始部分，A是其组成部分之一的子表达式这样的实例有很多，因此类型推断可以在多项式时间内完成这就完成了草图。我们希望最终能够在三次甚至二次时间内推断类型。6结论和未来研究我们设计了一个组件语言和一个类型系统，它允许静态检测某些组件的多个实例是否并行运行。该语言的特点是实例化、（顺序）组合和作用域。在未来，我们计划包括更复杂的语言功能，如显式的处理操作符，连接，并发功能和版本控制。M.贝泽姆张/理论计算机科学电子笔记97（2004）197-217213引用[1] R. Allen和G.加兰形成体系结构连接。第十六届国际软件工程会议论文集，意大利索伦托，1994年5月。[2] H.贝克’Use-Once’ Variables and Linear Objects – Storage Management, Reflection and ACMSIGPLAN Notices 30，January 1995.[3] H. 巴伦德雷Lambda Calculi with Types.In：Abramsky，Gabbay，Maibaum（Eds.），计算机科学中的逻辑，卷。二. 北京：清华大学出版社.一九九二年[4] D. Box和C.卖。Essential .NET，Volume I：The Common Language，Addison- Wesley，ISBN 0201734117，November 2002.[5] J. Cheesman和J.吴晓刚，"UML组件：一个基于UML组件的软件开发的简单过程“，北京：清华大学出版社，2000年.[6] M.Füahndr ichandR.D eL in e. Adop tiondFocus ： PracticaLinearTypesforImpeivProgramming，Proceedings of the SIGPLAN[7] E.伽马河赫尔姆河Johnson，and J. Vlissides. 设计模式-可重用面向对象软件的元素，Addison-Wesley，马萨诸塞州雷丁，ISBN 0201633612，1994年。[8] D.加兰河Monroe和D.怀尔ACME：一种体系结构描述交换语言。在CASCON'97会议记录[9] J. Magee，N. Dulay，S. Eisenbach，and J. Kramer.分布式软件架构。第五届欧洲软件工程会议（ESEC95），巴塞罗那，1995年9月。[10] E.Meijer和C.Szyperski。克服独立可扩展性挑战，《ACM通讯》，第45卷，第10期，第10页。41[11] R.米尔纳等。标准ML的定义（修订版），MIT出版社，ISBN 0262631814，1997。[12] M. Moriconi，X. Qian，和R. A.里门施奈德正确的架构改进。IEEE软件工程学报，1995年4月。[13] B. 皮尔斯类型和编程语言。MIT Press，ISBN 0262162091，February 2002.[14] J. C. Seco和L.蔡文龙，类型化组件的基本模型，计算机科学讲义，第1850卷，2000年。[15] C. Szyperski 。 Component Software ： Beyond Object-Oriented Programming ， 第 2 版 ，Addison-Wesley，ISBN 0201745720，2002。[16] M. Zenger ， Type-Safe Prototype-Based Component Evolution ， Proceedings of theEuropean Conference on Object-Oriented Programming，Malaga，Spain，2002年6月。A附录引理4.3（法律基础属性）如果Γ∈A：X i|X o，则V ar（A）<$X o<$X i <$Dom（Γ），Γ<$<$：|Dom（Γ）中的每个变量在Γ中只声明一次。证据 通过归纳推导。BasecaseAxiom：轴：轴|当Var（λ）=Xo=Xi=Dom（λ）=λ时，λ是三值的。归纳步骤：我们必须考虑与四种类型规则相对应的四种情况。214M.贝泽姆张/理论计算机科学电子笔记97（2004）197-217• 病例开始：ΓA：X i|X oStartr，x−Anewx：Xi+x|xo+xx∈/Dom（Γ）假设引理对于这个规则的前提是正确的，那么V ar（A）<$X o<$Xi<$Dom （Γ） ， Γ <$ ： |每 个变 量在Γ中最 多声明一 次。 则Var（ newx ） ={x}<$X o+x<$X i+x<$Dom （ Γ ） +x=Dom （ Γ ，x−<$A）。 更多关于，Γ，x−A：|通过应用Wea kening，可得出以下结论：中文（简体）| A：X i|X o弱化Γ，x−A：|∅x∈/Dom（Γ）结论是：每一个变量都在Γ中，x−ΣA是递减的常数，遵循边条件x∈/Dm（Γ）.• 病例弱化：弱化ΓA：X i|X或γB：Y i|Y oΓ，x−<$B<$A：X i|X ox∈/Dom（Γ）假设引理对于该规则的两个前提是正确的，则V ar（A）<$X o<$Xi<$Dom（Γ），V ar（B）<$Y o<$Y i<$Dom（Γ），Γ <$：|每个变量在Γ中最多声明一次。我们有V ar（A）<$Xo<$Xi<$Dom（Γ）<$Dom（Γ，x− <$B）。最后两个结论的证明方法与Start情形相同。• 病例排序：r=newx：X i|X或Y i|Y o测序新xA：Xi<$Yi|XoYoX oEYi=， A/=假设引理对于该规则的两个前提成立，则V ar（new x）<$X o<$Xi<$Dom（Γ），V ar（A）<$Y o<$Y i<$Dom（Γ），Γ<$：|每个变量在Γ中最多声明一次。注意，V ar（newx A）={x}V ar（A ）. 我们有V ar （newx A）<$Xo<$Yo <$Xi<$Yi<$Dom（Γ）。剩下的结论是他们自己。• 案例范围：范围I：X i|X或Y，A2：Y i|Y oΓ{A1}A2：Xi<$Yi|Yo假设引理对于该规则的两个前提成立，则V ar（A1）<$X o<$Xi<$Dom（Γ），V ar（A2）<$Y o<$Y i<$Dom（Γ），Γ<$：|每个变量在Γ中最多声明一次。 注意，V ar（{A1}A2）=M.贝泽姆张/理论计算机科学电子笔记97（2004）197-217215Var（A1）→Var（A2）。我们有Var（{A1}A2）<$Yo<$Xi<$Yi<$Dom（Γ）。剩下的结论是他们自己。Q引理4.4（生成）(i) 如果Γ≠newx：X i|X o，则x∈X o且存在<$，<$J，A使得Γ=<$，x−<$A，<$J，annd<$$><$A：Xi−x|X o-x。(ii) 如果r =newxA：Z i|Z o与A，则存在Xi，Xo，Yi，Yo，则Γ ≠newx：X i|X o，Γ A：Y i|Y o，Z i= X i<$Y i，Z o= X o <$Y o，以及X o<$E<$Yi=<$。(iii) 如果Γ ∈ {B}C：Z i|Zo，则存在Xi，Xo，Yi，Yo使得Γ ∈B：X i|X o，Γ C：Y i|Yo，Zi= Xi <$Yi，Zo= Yo.证据所 有 这三个项目都证明了归纳推导。(i) r =newx：X i|X o只能由规则开始或规则弱化导出。 如果它是由规则Start派生的，那么只有一种可能性：A：X i−x|X o−x开始r_nwx：Xi|X ox∈/Dom（n）其中hx∈X o且Γ=<$，x−<$A，sothat<$Jisempty.如果Γ ≠ new x：X i|X o由规则弱化导出：Γ jnewx：X i|X or JB：Y i|Y oW eakeninggrJ，y−Bnewx：Xi|X oy∈/Dom（ΓJ）则 ΓJ≠newx ： Xi|Xo 和 应 用 于 Γ j 的 IH 表 示 新 的 x ： Xi|Xowehavex∈X o，ΓJ=<$1，x−<$AJ，<$2和<$1<$newx：X i−x|X o−x，对于some1，2，andndAJ。 Nowake=1，J=2，y−B，A=AJ我们就有了所有的结论。(ii) 类似地，r =newxA：Z i|只有通过规则排序或规则弱化才能导出A / = 0的Zo。案件的证据测序是即时的。如果r =newxA：Z i|Z o由规则弱化导出：Γ jnewxA：Z i|Z oΓ j B：V i|V o弱化ΓJ，y−<$Bnewx A：Zi|ZOy∈/Dom（ΓJ）nr=rJ，y−nB，且IH适用于rJ∈wx A：Zi|ZoweveΓ jnewx：X i|X o，ΓjA：Y i|Y o，Z i= X i<$Y i，Z o= X o <$Y o，以及X o<$E<$Yi=<$。Noww