范畴pCpo中的一阶对象演算模型及其在面向对象编程中的应用

理论计算机科学电子笔记138（2005）79-94www.elsevier.com/locate/entcs对象演算Johan Glimming1斯德哥尔摩大学瑞典尼尔·加尼2莱斯特大学数学与计算机科学系联合王国摘要本文给出范畴pCpo中Abadi和Cardelli的一阶对象演算FOb 1+× μ（无子类型）的指称模型. 我们模型的关键新颖性在于它广泛使用递归定义的类型，支持自应用，以建模对象。在技术层面上，这需要使用一些复杂的技术，如Freyd论文的最后一节证明了我们的语义中固有的规范递归运算符在面向对象编程中是潜在有用的。这是证明了给一个简单的翻译代数datashees到所谓的包装类。关键词：范畴理论，面向对象程序设计1介绍对象的语义本质上是复杂的。首先，对象是递归的，因为它们包含对对象本身进行操作的方法这个参照物被称为自我1电子邮件地址：glimming@kth.se2 电子邮件地址：ng13@mcs.le.ac.uk1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.09.01280J. Glimming，N.Ghani/Electronic Notes in Theoretical Computer Science 138（2005）79<：<：方法的参数。其次，对象类型通常与子类型的概念相结合，这可能会在操作语义中引入异常。第三，方法更新（包括继承）对模型来说是困难的第四，对象通常带有类的概念，这导致了寻找类编码的问题（已经研究了预方法[1]，新函数[23]等）以及从类创建新对象实例的相关机制可以说，所有这些列出的问题都是由对象的递归性质引起的（参见[3]）。对于如何找到处理对象中固有的递归的好方法，已经有很多研究。自应用语义学[16，10]认为对象应该被建模为复杂的递归类型。 还有其他涉及高阶多态性的方法[17，18]，它们将所有递归隐藏在存在量化器下。 递归记录语义[5，6，23]可以被看作是一种妥协，其中（协变）递归类型用于自返回方法，并且需要项级别的定点运算符来处理对对象实例变量的引用。不幸的是，直接编码到Fω中的自应用程序不支持子类型，而其他两种列出的方法不支持方法更新（注意，然而，[4]给出了一种支持方法更新的递归和有界存在的编码Abadi和Cardelli [1]提出了各种支持方法更新的不同对象演算，并给出了基于约简规则的原语语义我们的出发点是，方法更新确实是面向对象范式中的一个重要因素，我们相信递归类型应该用于对象建模由于[1]中解释的原因，我们因此认为对象的概念是基本的，因此更喜欢流线型的理论方法，而不是通过Fω编码。我们的工作的一个目的确实是提供一个数学基础的逻辑对象演算，特别是逻辑程序转换。对象演算的直接指称模型本文介绍了该程序的第我们发展了一个对象演算的范畴模型[1]中提出的FOb1+×μ（略有修改）基于通过混合方差函子将对象类型解释为递归类型的对象类型的编码具有自应用语义的特性。该模型的主要新颖之处在于它广泛使用递归定义的类型来建模对象类型。我们的数学设定是pCpo范畴，我们的模型是一个self=self→Fself的解，其中F是一个常数表示方法类型的functor最简单的物体到一个常数函子F，而充分的普遍性允许我们定义我们所谓的代数数据集的包装类我们相信，这个模型可以扩展到支持子类型的自然转换下，J. Glimming，N.Ghani/Electronic Notes in Theoretical Computer Science 138（2005）7981说谎函子F，并通过将F视为模式函子，开辟了面向对象编程的多型风格的道路。本文的结构如下：在建立Freyd代数数学框架后，在第二节中，我们给出了紧范畴的演算FOb1+×μ，3. 在第4节中，我们给出了pCpo中演算的语义。在第5节中，我们讨论包装器类，即 将我们的对象语义与代数和共代数的编程风格联系起来，包括给出自然数对象的例子。最后，第6节总结了我们的贡献，并与相关工作进行了比较。最后，由于这项工作仍处于早期阶段，我们非常乐意收到有关方向和扩展的评论和反馈。2数学范畴我们假设读者熟悉初等范畴论，特别是范畴论的基本概念，如乘积和指数- 参见Mac Lane [13]了解详细信息。正如在引言中提到的，我们提出了一个类型化对象演算的指称模型，其主要新颖之处在于使用了递归定义的类型。一个简单的例子，例如，找到一个对象D，D=[D，D]，表明存在一个可重复定义的类型不是一个测试所有的Bious，E。G. 因此，如果D=[D，D]，则显然不存在D。的这个例子的关键特征是对象D到对象[D，D]的映射不是函子，因为D在表达式[D，D]中的左出现是逆变的，而右出现是协变的。 这种映射称为双函子。定义2.1[双函子]如果C是范畴，则双函子是函子F：Cop×C）C。这样一个双函子的不动点是一个对象X，使得X≠FXX有很多关于寻找双函子的不动点的研究。经典论文[21]定义了一类嵌入和投影对，其中函子F作用协变，并且可以从中导出F最近，[12，11，8，9]使用了代数紧范畴的更公理化的设置。即范畴，其中所有（在适当的等价意义上）协变函子都有一个初始代数，其结构映射的逆是最终的协代数。相关的，但较弱的，代数完备性的性质仅仅要求所有的（同样，在适当限定的意义上）协变函子有一个初始代数。公理化方法可能更容易应用于非领域理论模型，如可实现性82J. Glimming，N.Ghani/Electronic Notes in Theoretical Computer Science 138（2005）79模型和包含内涵特征的模型由于我们不希望在这个阶段将自己过度地投入到特定的语义设置中，因此我们在提升单子的Kleisli范畴中工作时隐式地遵循[8，9然而，四的目的，具体和简单的介绍，我们选择工作与规范模型的范畴pCpo的w-完全偏序和部分连续函数。我们用Cpo表示pCpo的子范畴，它由所有的Cpo和全连续函数组成。关于范畴pCpo和Cpo的显著事实可以在[19]中找到。Cpo的标准结构是由有限个余积构成的闭壳结构。我们给出pCpo的结构的简要概述：• Zero对象：空的cpo是pCpo中的零对象。也就是说，它既是初始对象又是终端对象。• 余积：如果A和B是cpo，则它们的不相交并是A和B在pCpo中的余积。• 部分积：如果A和B是cpos，则基础集合的卡方积是它们的部分积。它不是一个产品，因为对（f，g）的定义域是f和g，因此fst（f，g）/=f等。 我们将部分乘积表示为：一个提醒自己它不是产品的广告牌• Kleisli/偏指数：如果A和B是cpos，那么从A到B的部分连续函数的集合像往常一样形成cpo我们记为cpo [A，B]或A~B。正如所料，部分指数是右伴随的部分产品。−AE[A，−]：Cpo）pCpo. 注意这个附加函数中涉及的函子的定义域和上定义域• 紧性：pCpo是代数紧的，因为所有局部连续函子都有重合的初始代数和最终余代数[11]。这里值得注意的是，除了紧性之外，我们希望我们的环境范畴是carnival闭的，并且有有限的上积，这样我们就可以操纵多项式函子和它们的（上））代数使用的标准技术。事实上，满足于部分乘积和克莱斯利指数似乎是一个糟糕的选择。然而，任何紧范畴都有一个零对象（作为单位函子的不动点导出），而具有零对象的CCC是不一致的，因为A=A×1=A×0=0因此，我们无法摆脱在非封闭环境中工作J. Glimming，N.Ghani/Electronic Notes in Theoretical Computer Science 138（2005）7983尽管如此，子范畴Cpo（其中值取其指示）当然仍然是那么，给定一个像pCpo这样的范畴，如何找到双函子的不动点呢回想一下，在协变的简单情况下，内函子F：C ）C，则找到一个对象A =FA作为初始F-算法B，或finalF-余代数。定义2.2[代数，余代数]给定一个函子F，我们说一个箭头α：FA→A是一个带有载体A的F-代数。这样的F-代数是范畴Alg（F）中对每个函子F的对象.对偶概念是F-余代数，即反向箭头α：A→FA。（余）代数之间的箭头是F-同态，即箭头h使得，对于F-代数，下面的左图交换，对于F-余代数，下面的右图交换：FAF h）FB Ah）BαAlg（F）βVVαCoalg（F）βV VA）BHFA）FBF h当处理双函子时，代数和余代数推广到对偶代数。注意，双函子中的协变性和逆变变性的存在术语双代数在文献中有几个定义，因此我们在这里给出我们的定义定义2.3[双代数]双函子G：Cop×C → C的G-双代数是一对对象A，B以及一对相关联的箭头f：GAB→B和g：A→GB A。对偶代数范畴具有如下给出的对偶代数之间的映射定义2.4[双代数映射]给定G-双代数（A，B，φ，）和（AJ，BJ，φJ，J），G-同态是一对箭头（g：B→BJ，h：AJ→A）使得以下图可交换：GA Bφ）BA<$）GBAGG Hvˆ ˆggg gvGAJBJ）BJφJAJ）GBJAJ拉吉84J. Glimming，N.Ghani/Electronic Notes in Theoretical Computer Science 138（2005）79公理域理论的一个关键思想是使用代数紧性来找到双函子的不动点。以下是建筑草图：引理2.5设G：Cop×C）C是代数紧范畴C上的双函子。G有一个固定点。证据按照Freyd提出的加倍技巧形成函子GJ：Cop×C → Cop×CGJX Y（G（Y，X），G（X，Y））由于C是代数完备的，所以Cop×C也是代数完备的，因此GJ有一个初始代数，比如说GJ（X，Y）→（X，Y），它由内映射G：X→G（Y，X）和外映射G：G（X，Y）→Y给出。根据Lambek其次，对（outG，innG）：（Y，X）→GJ（Y，X）很容易被看作是最终的GJ-余代数。由于C是代数紧的，所以Cop×C也是代数紧的，因此初始GJ-代数和最终GJ-余代数重合。因此，X=Y，我们有一个G固定点。Q当然，虽然上面的证明看起来很简单，但大部分工作都隐藏在证明i）代数完备性和紧性是通过乘积和相反的范畴来保持的; ii）形式化要考虑的双函子的类; iii）证明某些范畴是代数完备和紧的。更微妙的技术问题出现了，例如。这些固定点应该适当地参数化等，但对于这个演示，我们决定忽略细节。详情见[8]话虽如此，固定点构造的模块化非常优雅。也请注意，比我们声称的更多的是真实的。特别地，我们构造了具有泛性质的双函子的一个特定点，即初始双代数。我们将在以后应用这个普遍性质3对象演算我们现在将给出一阶对象演算的语法和操作语义，以下简称为FOb，它本质上是Abadi和Cardelli因此，FOb有方法更新，但没有子类型或更高类型。在微积分中没有真正的惊喜，它的包含仅仅是为了论文的完整性。我们假设可数集L（方法标签），V（类型J. Glimming，N.Ghani/Electronic Notes in Theoretical Computer Science 138（2005）7985变量）和U（术语变量），并将使用希腊字母表示类型变量，小写字母表示术语变量，以及索引i∈N的li表示方法标签。定义3.1[FOb-类型]集合TFOb由归纳法定义，τ：=v类型变量|1终端类型|τ1× τ2产品类型|τ1+τ2和型|τ1 →τ2函数类型|μv.τ递归类型|[11：τ1，. ，ln：τn]对象类型其中v∈V，且对于每个i，li∈L。请注意，在递归类型中，类型变量的出现没有限制，这意味着这种演算在包括各种复杂类型（如Lam = μX）时是有表现力的。N+（X →X），其中N =μX。1+X。像往常一样，接下来定义FOB的前置项。定义3.2[FOb-preterms]集合NFOb由UNFOb的归纳法定义。归纳地说，如果m，MJ，b∈NFOb，τi∈TFOb，li∈L且xi∈U（其中i∈N）theNn∈，[l1=<$ （x1：τ1）b1，.， ln= n（xn：τn）bn]，m. l，mmJ，λ（x：τ）b，m. l7-π（x：τ）mJ，inlm，inrm，case（b，x. m，y。mJ）、fstm、snd m、（m，mJ）、inn（τ，m）和out（m）在NFOb中。对于表示项的元变量，我们将采用以下约定：symbolo是形式[l1=l（x1：τ1）b1，.，ln=<$（xn：τn）bn]，其中n∈N.有时我们也写[li=<$（xi：τi）bi]i∈I，因为I是N的有限子集。这两种等价形式的术语称为对象。为了方便起见，我们将识别任何两个项（类型），它们等于方法标签的顺序，例如[l1 =...，l2 =.... [l2 =...，l1 =.... ]，我们假设方法标签出现在相同的封闭括号[. ]是不同的。我们使用Abadi和Cardelli此外，m（x）意味着x在m中是自由的（因此甚至可能不在m中出现），然后m（a）<$m[a/x]。定义3.3 [FOb-环境]一个环境E是一个形式为x1：τ1，. ，xn：τn，没有变量在序列中出现两次。86J. Glimming，N.Ghani/Electronic Notes in Theoretical Computer Science 138（2005）79nj/类型判断的形式是Ea：σ，其中E是环境，a是前项，σ是类型。我们还令E<$σ表示<$a∈ NFOb使得E<$a：σ，即σ是良构居住型的陈述。定义3.4[FOb-分型判断]FOb的分型判断是E，xi：σb1：τ1，.，bn：τnσ= [l1：τ1，...，ln：τn]E[l1=（x1：σ）b1，.， Ln =（xn：σ）b ]：σ（object intro）Ea：σ，E，x：σb：τjσ= [l1：τ1，.，ln：τn]是的l-Σ（x：σ）b：σ（对象更新）埃琳娜：[l1：τ1，.，ln：τn]0in +1是的Li ：τi（object elim）Ec：σ1+σ2E，xi：σimi：τ（i= 1，2）E=（c，x1. m1，x2. m2）：τ（case）Em：τ1→τ2，n：τ1Ea：τEmn：τ2（λ-elim）Einla：τ+σ（inl）Eb：σE，x：τ1b：τ2E<$λ（x：τ1）b：τ1→τ2（λ-介绍）Einrb：τ+σ（inr）E单位：K（unit-unit）Ea：τ×σEfsta：τ（第一个项目）Ea：τ×σEsnda：σ（snd proj）Ea：τEb：σE（a，b）：τ×σ（对形式）Eb：σ[μ α.σ（α）]E_n（τ，b）：μα.σ（α）（μ-in）Eb：μ α.σ（α）E输出（b）：σ[μ α.σ（α）]（μ-输出）我们说一个预项m∈NFOb是良型的，如果存在一个类型τ∈TFOb和一个环境E使得E<$m：τ。我们让MFOb表示良好类型项的集合，直到由项绑定器λ、λ和case诱导的明显的α等价概念。4双函语义学在本节中，我们使用范畴pCpo给出FOb的指称模型。这种语义的关键特征是，它反映了我们的直觉，即FOb的对象类型是递归类型方程的不动点。更具体地说，递归是在自参数上发生的。这种直觉在σ = [l1：τ1，. ，ln：τn]，这表明第i种方法将消耗具有类型σ的自参数，以产生类型τ i的东西。因此，直观地，σ的解释应该满足[[σ]]=[[σ]]~[[τ1]]×· · ·×[[τn]]J. Glimming，N.Ghani/Electronic Notes in Theoretical Computer Science 138（2005）7987所以σ的表示应该是μ X的不动点。X~[[τ1]] ×···×[[τn].重要的是，下面的引理表明，这样的解释支持自应用[10]，这是我们的语义学所要求和支持的。我们专门为pCpo陈述引理，以明确我们在证明中没有使用carnival闭包。引理4.1设F：pCpo）pCpo是一个协变函子，O满足O∈[O，FO]. 这是一个自适应映射：O→FO。证据所有的同构都是全的，因此这个同构可以给出一个映射O→O→FO。现在预组成的对角线，其中部分的产品。Q注意这与递归记录语义[1]的区别，其中递归位于输出或协变位置，而self的逆变出现被替换为具有单独的状态类型和项级别的定点运算符。我们的语义也不同于其他编码，例如存在的各种编码[18，4]，其中逆变发生是存在的，但隐藏在存在量化器下。在我们的FOb模型中，我们解释了逆变的自参数，并将所有对象类型解释为更精细的递归类型，正如我们所看到的，超级端口自我应用。如果C是一个cat egory，则由C指定该cat egoryCop×C，并注意到（C）n=（Cn）。用于获得双函子不动点的加倍技巧为每个双函子F：Cop×C）D分配一个函子F：Cop× CDop×D。我们可以看到所有的函数，在他的算法中-见[8]的完整定义。每个对称函子F通过后合成诱导两个函子F1和F2，其中投影F1和F2产生于因为我是CAT。如果映射F<$→F是双函子和对称函子的逆函数F到F2。 这一事实将被用于下面通过给出双函子来定义对称函子。最后，设P是范畴pCpoop×pCpo。有了这个符号，我们可以给类型一个语义，如下所示。如果类型τ有n个自由类型变量3，则它的解释是对称函子[[τ]]：Pn ）P利用上面提到的双射，我们通过给出[τ]] 2来定义对称函子[τ]]。这条规则的例外是对递归[3]在这一点上，我们为不使用自由类型变量索引判断付出了一点非正式的代价。然而，我们以前通过减少符号上的繁琐判断而获得了好处我们让读者来决定这是否是一个合适的选择。88J. Glimming，N.Ghani/Electronic Notes in Theoretical Computer Science 138（2005）79类型和对象类型。[[1]]2X= 1[[τ1+τ2]]2X=[τ1]]2X+[[τ2]]2X[[τ1× τ2]]2X=[τ1]]2X<$[[τ2]]2X[[τ1→τ2]]2X =[τ1]]1X~[[τ2]]2X[[μv.τ]]X=（[τ]]X）†其中（[τ]] X）†是[τ]] X：P）P的固定点。最后，对于对象类型σ =[11：τ1，. ，lm：τm]，我们有[[[l1：τ1，. ，lm：τm]=[μv. v → τ1×···× τm]]在定义上，我们有[[σ]]2X<$=[[σ]]2X~[[τ1]]2X<$· ·<$[[τm]]2X注 意 ， 在 这 种 情 况 下 ， 引 理 4.1 适 用 ， 因 为 我 们 可 以 取 F 为 返 回[τ1]]2X<$··<$[[τm]]2X的常数函子。就像我们给类型一个解释一样，我们也给环境一个解释如果E是一个有n个自由类型变量的环境，那么[[E]]：Pn ）P是对称函子，定义为[[x1：τ1，. ，xm：τm]] 2X =[[τ1]] 2X···[[τm]] 2X最后，我们来解释为长期判断。如果E_e：τ是一个使用n型变量的判断，那么它的解释是一个有指标的态射[[Ee：τ]]A：[[E]]2A）[[τ]]2A对于每个对称函子A： Pn，即对于某个X：pCpon，函子A的形式为A =（（X1，X1），.，（Xn，Xn））。由于与基本类型1、+、×、→相关联的术语构造的语义子句如所预期的，我们把它们作为练习，而把重点放在对对象引入、更新和消除的判断上，我们从定义3.4中逐字引用这些判断。J. Glimming，N.Ghani/Electronic Notes in Theoretical Computer Science 138（2005）7989• 对象介绍：通过假设我们给出映射[[E，x：σ <$bi：τi]]A：[[E，x：σ]]2A）[[τi]]2A在pCpo中。利用[E，x：σ]]2的定义和附加在部分乘积和和部分指数之间，这些对应于到以下类别Cpo中的地图：[[E]]2A）（[[σ]]2A~[[τi]]2A）因此对于每个A，我们得到一个映射[[E]]2A）（[[σ]]2A~[[τ1×·· × τn]]2A）但是，由于[σ]]2A ~[[τ1× · ·×τn]]2A与[σ]]2A同构，我们又作了修正。• 对象消除：我们给出了一个家庭的地图[[Ea：σ]]A：[[E]]2A）[[σ]]2A想要一张地图[[Ea：σ]]A：[[E]]2A）[[τj]]2A这可以通过自应用映射[[σ]]2A）[[τ1]]2A×···[[τn]]2A和第j个投影的后合成来构造• 对象更新：从地图[[Ea：σ]]A：[[E]]2A）[[σ]]2A解出定义[σ]]2A的同构。将元组的第j个[[E，x：σb：τj]]A：[[E，x：σ]]2A ）[[τj]]2A然后将同构重新折叠以得到所需的映射。5包装类在前一节中，我们看到了如何通过求解以下形式的递归方程来为对象类型和相关的项判断赋予语义：O→O→K，其中K表示90J. Glimming，N.Ghani/Electronic Notes in Theoretical Computer Science 138（2005）79对象类型。因此，存在不对称性，因为自参数可以是J. Glimming，N.Ghani/Electronic Notes in Theoretical Computer Science 138（2005）7991被方法消耗，但方法更一般地，人们希望方法能够消费和返回self参数-这在函数式和命令式对象演算中都有意义这样做意味着求解以下形式O=[O，FO]其中F是某个协变函子。这样的广义对象显然是支持的语义，我们已经开发。另请注意，然后利用该函数建立了判别方程D_n=[D，D]。我们把通过问下面的问题来使用这个想法鉴于这两个非-最终代数和最终余代数风格的编程已经被证明在函数世界中非常流行，我们可以将它们融入到函数世界中吗？物品？更确切地说，如果F是一个具有初始代数μF和最终余代数νF的协变函子，我们能否找到一个对象O，它支持μF和νF所享有的那种编程。当然，由于我们在代数紧范畴μF=νF中工作。 我们通过将O设为方程O=[O，FO]的固定点，给出了这个问题的部分肯定答案. 注意我们的分析是语义的，因为我们处理所有的协变函子，而不是退回到一些受限制的函子语法类，如多项式。对于本节的其余部分，固定一个协变函子F并定义双函子G（X，Y）=X→FY。对于结构图我们也写了inn和out内：[O，FO]）O外：O）[O，FO]初始G-双代数我们的第一个结果是，对象可以被引理5.1 O是F-余代数，因此存在F-余代数同态O）νF。证据 由引理4.1，自应用给出一个余代数O）FO。Q不仅存在从O到最终F-余代数的映射，而且存在从初始代数到O引理5.2O是F-代数，因此存在F-代数同态μF）O.证据 我们想要O的构造函数，也就是说O是F-代数。92J. Glimming，N.Ghani/Electronic Notes in Theoretical Computer Science 138（2005）79使用定义O的同构，结构映射FO）O可以由映射FO）[O，FO]给出，我们将其作为解卷积后的第一个投影。现在O是一个F-代数，初始代数的折叠运算定义了一个F-代数同态μF ）O.Q复合μF）O）νF是由μF的初性和/或νF的终性诱导的正则映射依赖于O的正则性。因此，在这种情况下，O是μF的收缩，表明它包含μF的元素，但也包含更多的元素接下来，我们要考虑递归原理。初始代数带有一个标准递归算子fold，从初始代数到另一个代数的唯一映射类似地，有一个递归算子展开，它是从某个余代数到最终余代数的唯一映射如前所述，O具有作为初始双代数的普适性质，因此有自己的递归原理来定义从O到任何其他双代数的映射。解开双代数等的定义，这给出了方向性原理。定义5.3 [方向]设（φ，φ）是一个双代数，其类型如下图所示。定义（[φ]）：O）B和[（φ）]：A）O是唯一的双代数同态，使得下面的图交换：[O，FO]innG）O OoutG）[O，FO]G[（φ）]（[φ]）v（[φ]）vˆ[（）]ˆG（[φ]）[（φ）][A，F，B]）BφA）[B，FA]ψ通过简单地追踪上图，可以将方向性原理提取为两个相互递归的组合子：定义5.4[方向-组合子]（[φ，]）oφ（（F（[φ，]））<$（outGo）<$[（φ，）]）[（φ，）]oinnG（（F[（φ，）]）<$（o）<$（[φ，]））这种递归方案已被开发为一种编程工具，由[7，15]，也开辟了道路，为潜在的优化的基础上融合，砍伐森林等，并给予法律面向对象的程序一个代数J. Glimming，N.Ghani/Electronic Notes in Theoretical Computer Science 138（2005）7993编程学校。在未来的工作中，我们计划测试论文是否是实际可行的。在这里，我们使用direcursion来证明O可以用来模拟最终F-余代数的展开运算。给定任何F-余代数α：A→FA，我们定义一个从A到O的映射。这可以通过将B作为一个元素cpo来实例化方向性原理来完成。映射φ必须是唯一的全映射，而映射A→[1，FA]将a发送给返回α（a）的全函数总之，我们定义了一个将初始代数和最终余代数编程的一些关键特性转换到对象世界中。也就是说，我们定义了一个对象类型，它包含初始代数的元素，具有用于模式匹配的构造函数，可以被求值到最终余代数中，支持互模拟的概念，并支持展开运算符。这些构造非常简单，这向我们表明这些包装器对象是自然的，并给我们带来了希望，可以将更多的概念合并到模型中，而不会变得难以处理。但这当然是未来研究的主题。6结论和进一步工作本文的方法不同于文献[1]中给出的指称语义。首先，也是最基本的，他们使用理想/度量方法[14]，而我们的方法基于Fiore其次，Abadi和Cardelli将类型解释为泛域上的部分等价关系（pers），而我们通过在pCpo中求解递归类型方程来解释对象类型。因此，我们得到了一个更直观的对象模型，以及相关的递归原理我们认为将归纳类型转换为包装器显示了该模型的简单性和自然性然而，子类型与递归类型结合存在已知的问题，需要进一步的研究，以便将子类型与方向原则一起Reus和Streicher [20]最近在域理论环境中处理了无类型对象演算。他们使用归纳原理来推理这些对象。然而，在他们的工作中只有一个归纳原则，而在我们的类型化设置中，每个对象类型都有一个实例化。引用[1] 我不知道你是谁. AOb e c t s的Teory。 Sprin ger-Verlag，1996年。94J. Glimming，N.Ghani/Electronic Notes in Theoretical Computer Science 138（2005）79[2] Mart'enaba d iandGord onD. 我是PLOTK I N。 一种新的聚合物形态是一种新的聚合物。在J. Mitchell，编辑，Proceedings，Fifth Annual IEEE Symposium on Logic in ComputerScience，pages 355IEEE计算机学会出版社.[3] 金 湾 布 鲁 斯 范 例 面 向 对 象 编 程 语 言 ： 设 计 ， 静 态 类 型 和 语 义 。 Journal of FunctionalProgramming，4（2）：127[4] 金湾 布鲁斯， 卢卡·卡德利 和本杰明C.皮尔斯比较对象编码。信息与计算，155（1-2）：108[5] 卢卡·卡德利多重继承的语义。Information and Computation，76（2/3）：138[6] 卢卡·卡德利子类型的纯演算中的可扩展记录。In C. A.冈特和J.C. Mitchell，editors，TheoreticalAspects of Object-Oriented Programming：Types，Semantics，and Language Design，pages 373麻省理工学院出版社，马萨诸塞州剑桥，1994年。[7] 列奥尼达·费加拉斯和蒂姆·谢尔德。重新审视带有嵌入函数的数据库（或者来自外太空的程序）的变形。在会议记录23rd ACM SIGPLAN/SIGACT Symp.程序设计语言原理，POPL 1996，第284-294页。ACM Press，New York，1996.[8] M.菲奥雷部分映射范畴中的公理化Domain理论。计算机科学杰出论文。剑桥大学出版社，1996年。[9] Marcelo P. Fiore和Gordon D.普洛特金 公理域理论模型到综合域理论模型CSL，第129-149页，1996年[10] Kathleen Fisher，Furio Honsell，and John C.米切尔对象和方法专门化的lambda演算。NordicJournal of Computing，1（1）：3[11] P. 佛瑞德代数上完全的范畴。 在proc 1990年科莫范畴理论会议，第1488卷的讲义在数学，第95-104页。Springer-Verlag，1990.[12] 彼得·J·弗洛伊德。递归类型被简化为归纳类型。在第五届IEEE年度研讨会上。计算机科学中的逻辑，LICS'90，第498-507页。IEEE计算机协会出版社，1990年6月[13] S.麦克·莱恩数学家的工作类别，数学研究生教材第5卷。Springer-Verlag，1971.[14] 大卫·麦奎因戈登·普洛特金和拉维·塞西递归多态类型的理想模型。第11届ACM SIGACT-SIGPLAN编程语言原理研讨会论文集，第165-174页。ACM Press，1984.[15] E. Meijer和G.赫顿 空间中的香蕉：将折叠和展开扩展到指数类型。在proc 第七次会议函数式编程语言和计算机体系结构，1995年。[16] John C.米切尔为方法专门化和继承奠定类型化基础。在第17届ACM SIGPLAN-SIGACT专题讨论会上，编程语言的原则，第109-124页。ACM Press，1990.[17] 本杰明·C Pierce和David N.特纳没有递归类型的面向对象编程。在第20届ACM SIGPLAN-SIGACT专题讨论会上，编程语言的原则，第299-312页。ACM Press，1993.[18] 本杰明·C Pierce和David N.特纳面向对象编程的简单类型理论基础。Journal of FunctionalProgramming，4（2）：207[19] 戈登·普洛特金Pisa笔记（论域理论）。购自http://homepages.inf.ed.ac.uk/gdp/publications网站。[20] Bernhard Reus和Thomas Streicher。对象演算的语义和逻辑。 在Gordon Plotkin，编辑，第十七届IEEE年度会议论文集。计算机科学中的逻辑，LICS 2002。IEEE计算机协会出版社，2002年7月。J. Glimming，N.Ghani/Electronic Notes in Theoretical Computer Science 138（2005）7995[21] M. Smyth和G. 普洛特金递归域方程的范畴论解SIAM Journal of Computing，11（4）：761[22] 迈克尔·史密斯和戈登·普洛特金递归域方程的范畴理论解。SIAM Journal of Computing，11（4）：761[23] 米切尔·万德具有实例变量和继承的对象的类型推断。In C. A.冈特和J.C. Mitchell，编辑，面向对象编程的理论方面，第97-120页。MIT Press，London，1994.