区域和位置在计算机科学中的应用及安全内存管理探讨

理论计算机科学电子笔记158（2006）171-197www.elsevier.com/locate/entcs区域和位置Matthew Collinson马修·柯林森1，2巴斯大学计算机科学系英国贝辛斯托克David Pym大卫·皮姆1，3Hewlett-Packard Laboratories英国布里斯托尔摘要有许多应用的类演算，其中术语和类型用表示机器存储器中的位置或位置的参数来注释。这样的演算在设计时考虑了安全的内存管理操作。很难为现有的这类结石直接建立指称模型。我们的做法不同的问题，从一类数学模型，描述了一些基本的语义属性，在这些演算。特别是，区域（或位置）之间的不相交条件隐含在许多内存管理操作中。集束多态性提供了自然的类型理论机制，用于捕获此类模型中的不相交条件。我们通过在αλ的基本不相交性模型中添加区域来说明这一点，α λ是与集束蕴涵逻辑相关的代数演算。 我们展示了加性和乘性多态量化器如何在我们的模型中自然出现。位置模型是一个特例。为了将此企业与以前的内存管理工作联系起来，我们提供了一个示例，其中模型被细化并用于为具有明确的区域分配和处理的语言。关键词：指称语义，类型，多态性，集束蕴涵逻辑，区域，位置，指称。1这项研究得到了英国EPSRC资助“Bunched ML”的部分支持2电子邮件地址：cssmc@cs.bath.ac.uk3 电子邮件：david. hp.com1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.04.010172M. Collinson，D.Pym/Electronic Notes in Theoretical Computer Science 158（2006）1711引言近年来，在类型、语义和编程语言社区中，对区域的使用兴趣激增。这种兴趣可以追溯到Lucassen和Gi Joreord的论文[12][14][15][16][17][18][19][[12]的系统被设计为提供对结合函数式和命令式编程的语言中的副作用的分析。副作用涉及到对包含引用的表达式求值所引起的机器状态的改变.引入区域来描述表达式的侧效应发生的存储区域。这就控制了某个较大表达式的各种子表达式的副作用如何相互作用。区域被认为是无限的，并且可以分配、读取和更新引用。特别是，引用总是由程序员在特定的命名区域内分配。目前关于区域的大部分工作是关于用于内存管理的类型系统.这样的类型系统旨在成为一种比垃圾收集器更早地回收未使用的内存的方法，并且可以很容易地看到内存何时被分配和释放。最近对基于区域的内存管理的调查可以在[10]中找到。与那里描述的语言一样，我们的类型系统享有所谓的区域安全属性;也就是说，在运行时不会发生对未分配或释放区域的访问。在[25]中，ML类语言的（几乎）所有值都放在区域中。这是通过翻译到一种语言来完成的，在这种语言中，表达式用区域变量进行注释。这些区域变量的作用域然后由某种let表达式限定。在运行时，这些区域变量被映射到实际区域。例如，一个创造价值的程序M（大致）是翻译成注释程序letregρinMJatρend，其中MJ是通过适当地翻译M的子表达式而形成。当这个被执行时，首先分配一个内存区域（对应于ρ），计算MJ（存储和检索ρ中的值），然后释放ρ由于letreg是分配和释放区域的唯一构造，因此区域的堆栈规则被强制执行。这个系统的一个重要组成部分是在区域变量中多态的函数后来，别名类型语言家族被开发出来-参见Walker和Morrisett [28] -也考虑到了内存管理的安全操作。这些系统中的类型通常包含位置参数。本文中的一个关键概念是位置。对于我们目前的目的，我们需要捕获的主要属性是位置是M. Collinson，D.Pym/Electronic Notes in Theoretical Computer Science 158（2006）171173机器存储器的不可分割的部分，并且任意大小的值可以存储在一个位置。因此，我们的位置概念是一个（有限的）抽象，例如，公式中的大值存储使用多个链接的内存地址。区域只是机器内存中的一组位置。区域可以重叠。例如，在[12]之后，引用是指指定区域内的位置。因此，我们对位置和区域的表征是在一个类似于BI语义中资源的抽象层次上获得的[18，17]，其数学结构捕获了这样一种观点，即在该抽象层次上资源的基本属性是它们的可组合性和可比性。区域和位置系统通常与详细的操作语义一起呈现。这些通常是相当复杂的，但各种安全性能仍然可以验证。另一方面，区域和位置语言的指称模型几乎从未提出过-例外是Banerjee ，Heintze和Riecke [1]。最近Morrisett，Ahmed和Fluet [13]也朝着这个方向采取了一些措施。我们相信数学模型对于这些语言的重要性并不亚于其他语言。指称语义在概念清晰性、抽象正确性标准和证明程序等价性的方法（可能在不同的实现甚至语言中）方面的通常论点都在这一集合中成立;参见Scott和Strachey[21]。在本文中，我们从指称的角度来处理内存管理。我们提出的技术，建立模型的类型系统中，区域和位置参数存在于类型。两个关键技术是使用聚束多态性和在区域基础上构建索引类别的模型。聚束多态性的要点是在一个单一的代数演算中提供多态量化的加法和乘法变体。Collinson、Pym和Robinson [3]对理论方面进行了研究。本文给出了范畴模型的定义。这些由多态性的超理论的变体[22]以及解释乘法的额外结构组成。因此，底层索引范畴的纤维由双闭范畴组成，而基有一个额外的monoidal结构来解释类型变量的乘法组合。幺半群也支持一种弱投影，这使得我们可以定义一个函子，该函子将乘法量化器建模为导出代换的右伴随。给出了可靠性和完备性定理。给出了一个基于部分等价关系的模型：被索引范畴的纤维中有pers对.我们在这里关注的是一个更简单的情况，其中我们有区域174M. Collinson，D.Pym/Electronic Notes in Theoretical Computer Science 158（2006）171而不是类型变量。这使我们能够为聚束多态量化器提供更具体的资源读取。从逻辑的角度来看，这构成了从二阶命题到二阶谓词量化的一个步骤。在我们提出的模型中，加法量化器是普通的二阶量化：它表示模型中的“所有谓词”。这给出了处理区域多态性功能的机制。乘法量化器也具有吸引人和有用的特性。它可以被理解为“对于所有新谓词”，其中“新”意味着与用于解释quantifier范围的谓词不相交。我们很好地利用了这个乘法量化器。不相交性对于区域的分配和释放至关重要。当分配区域时，假设其与所有先前分配的区域不相交。在一个区域被释放后，不应该使用它的任何位置，因此它必须与其余计算所使用的所有区域不相交。区域变量之间的隐式不相交条件可以使用聚束多态的语法来捕获。类似的评论适用于具有位置变量的演算我们提出了一种构造模型的方法（在一定的范畴上建立索引），这是相当普遍的。我们作为例子使用的特定模型是从O'Hearn [ 14 ]的基本不相交模型（BDM）构建的，BDM是Reynolds-Oles函子范畴语义[16，19]和分离逻辑的堆语义的相对，参见Reynolds [20]。在BDM中，类型由变量集（preheave）表示。这些是由机器位置集合参数化的集合。使用位置的方式使其成为尝试区域化的明显设置。 事实上，它支持αλ有助于开发一种用于参考的语言。由于这是第一次尝试构建简单的区域指称模型，我们不希望保留现有区域和位置语言的所有有用属性。我们首先介绍了Collinson，Pym和Robinson [3]引入我们回顾了BDM及其状态概念。我们定义了区域和领域的类别（区域变量束），这是我们方法的基础。作为语义的一个例子，我们展示了如何构建一个基于BDM和领域索引的纤维索引类别。我们描述了加法和乘法量化器的解释。我们展示了如何专门针对位置变量的情况。我们对BDM态的概念作了适当的修正。我们通过给出一种具有区域分配和释放的编程语言来更深入地在这种语言中，基于M. Collinson，D.Pym/Electronic Notes in Theoretical Computer Science 158（2006）171175T→−−∗∀在Berdine和O'Hearn [ 2 ]中我们用区域来细化BDM，以给出语义，并展示它如何支持区域的分配和释放我们感谢Josh Berdine和Peter O'Hearn的讨论和帮助。特别是，他们在[2]中的语言和模型是我们在区域中参考的语言和模型的起点。我们的模型也是我们与Edmund Robinson早期联合工作的聚束多态性PER模型的后代[3]。最后，我们感谢匿名推荐人对本工作的初步版本提供了有益的评论2聚束区多态性我们希望在本文中处理的结石类型包含区域变量和上下文包含这样的变量束。这些演算的设置遵循我们早期对类型（而不是区域）变量的聚束多态性[3]的处理。这些情况之间的主要语法差异在多态应用中：区域变量必须用区域实例化，而类型变量可以用更一般的类型实例化。这一节介绍了聚束多态类演算，它构成了我们将在本文中使用的所有类型系统的基本功能核心。该演算基于对应于BI的αλ-演算，参见[15，18]。回想一下，这个特征是某些树的上下文，称为束，叶子上有普通的变量。我们将αλ推广到一个新的微积分，类型变量的上下文区域，也包含束。该扩展是正交的，在这个意义上，聚束在两个层次的变量是完全独立的。在每一个（但不是两个）上下文区域中都有完全合理的结石我们选择了一阶聚束的微积分，以帮助我们开发第4节中的语言。假设一个区域变量的可数集合，写为ρ，可能带有下标、上标、素数和一个（普通）变量的可数集合，写为x、y、z。类型由语法τ：= T|我|ρref|τ∧τ|τ∗τ|τ→τ|τ−−∗τ|我的天τ|你好τ，其中ρ是区域变量。 经营者、得双曲正弦值.是添加剂单位，产品，功能空间和多态抽象（通用量化器）分别。单位I、乘积I、函数空间都有乘法算子和多态抽象- 是的 我们允许字母σ、τ在类型上变化一个区域变量ρ在τ中是自由的，如果它不受（在176M. Collinson，D.Pym/Electronic Notes in Theoretical Computer Science 158（2006）171►范围）一个量化器的范围或范围。类型ρref将区域变量引入类型系统。 这个想法是，具有这种类型的值将是对由ρ确定的区域中的某个位置l的引用（在合适的环境中）。对于第一种语言，我们并不假设位置具有某种价值。因此，对于引用（取消引用、更新、分配、处置）或区域（分配、处置），我们没有任何标准操作。当我们在第4节详细阐述模型时，将添加这些内容。我们最初的目标是研究区域变量的加性和乘性量化，并建立一个简单的集合论模型。一个领域是一堆区域变量。它们的生成方式如下B：==|ρ| B，B|B; B，受到任何区域变量在一串中最多出现一次的限制。设B（以及带有素数、下标和上标的变体）在域上变化。我们写B τ，并说当τ中的每个自由区域变量都存在于B中时，类型τ在（区域）B是良构的。特别地，这意味着一阶形式f或types（T，n，→，I，n，−−n）takeplaceov固定域。上下文是一堆类型化的普通变量。 这些由Γ：= π生成|∅∗|x：τ|Γ，Γ |r;r，其中x是一个变量，τ是一个类型，因此任何变量最多出现一次。我们在上下文中使用字母Γ和Δ。 单位和与服务器的单位不同写B<$r，并说上下文r在B上是良构的，当B<$τ对于r中的每个变量x：τ。我们的背景只是在领域上的αλ束可以被看作是带有标记节点的树束总是服从一对等价关系，参见[18]，这适用于我们的领域和我们的上下文。第一个等价子串用于构建结构规则，允许我们在领域或上下文中排列变量。它是由交换幺半群规则为“;"，为“，“和一个同余，以确保幺半群规则可以应用在任意深度的第二个关系式是使用d个连续的牵引规则。TheequivalenceB=onrealms是对ype变量s的隐式重命名：B=BJ，如果BJ可以通过用区域变量双射重命名从B获得。当Δ可以由已知的公式得到时，以类型保持的方式对Γ的叶的变量进行：Γ的任何叶x：τ必须M. Collinson，D.Pym/Electronic Notes in Theoretical Computer Science 158（2006）171177∀T→−对应于一个节点y：Δ的τ束B的子束是子树BJ，使得BJ的所有叶子都是B的叶子。设B（B1|......这是什么？| B n) be the notation for a bunch(realmor context) B withdistinct, distinguished sub-bunches B1,...，B n.一群B [B1]/B1， . . BnJ/Bn]是通过用B i j替换B中的每个ChBi来形成的。我们重申，变量只能在上下文中出现一次，类型变量只能在领域中出现一次该语言的术语由以下语法给出M：= x|不|我|让我成为M中的M| M，M|π1M|MM|设（x，y）是M中的M| λ x：τ. M|λx : τ.M|λmax：τ. M|应用程序（M，M）|Λρ. M|Λ ρ.M|Λρ. M |App（M，ρ），|App ∗ (M, ρ) ,其中ρ是区域变量，τ是类型，B是领域，x是变量。我们用字母M和N来表示术语。我们现在试图传达我们语言背后的预期含义-当我们给出外延时，这些含义将变得精确。本文的一个基本思想是使用领域的聚束结构来跟踪区域变量解释之间的假定分离。如果两个区域变量以乘法分隔（用逗号），则它们表示不重叠的区域。另一方面，相加分离的区域变量可能重叠。在这个特殊的设置中，区域变量的参数化通过类型ρref进入语言。这是对ρ中位置的引用类型。一阶类型，有它们的标准不相交性读数，例如参见[14]。项M：ρ.τ可以用任何区域实例化以给出项App（M，ρ）：τ。 因此我们有区域多态性的一种明确形式。相比之下，项M：ρ.τ可以用与所有其他看起来自由的区域不相交的任何区域来实例化。在M和τ中。这将使我们能够在第4节中为区域分配和处理输入常量。令FV（−）是在上下文（−）中或在项（−）中自由（不受lambda抽象约束）的变量的集合。我们使用FRV（−）表示区域变量的集合，它们分别在领域（−）、类型（−）、上下文中变量的类型（−）或项的类型（−）中自由出现。 在项App（M，ρ）中，类型变量ρ是自由的。 各期限M，设μ（M）是自由的区域变量的集合，并且出现在这个区域中。在M中，也就是说，用于在M的子项中实例化乘法量化器。178M. Collinson，D.Pym/Electronic Notes in Theoretical Computer Science 158（2006）171∧ ∗→微积分产生（术语形成）如下形式B|Γ M：τ，给定一堆区域变量B和一堆（普通）变量Γ，项M是具有τ的良好类型这些判断依赖于领域上的类型和上下文的良构性.这些判断是根据一套规则得出的，下面列出了在图1中除了所示规则外，还有加法（T）和乘法（I）单位规则的引入和消除规则，加法（）和乘法（）合取、加法函数（）、收缩（C）和等价（E）。这些可以在[3]中找到。除了量化规则和领域结构之外，所有规则都使用固定的领域B。也就是说，它们本质上是αλ的熟悉规则，但通过该规则参数化d。在（？）n（？）n（？）n d（？）n（？）n（？）n（？）nd（？）n（？）n（？）ρ∈/FRV（Γ）. 消除规则（E）、（E）、（→E）和（−E）是一个子对象到边条件（†）μ（N）FRV（M）=这需要分离存在的某些自由区域变量。这个副条件使得用项M替换项N中的变量x成为固定域上的可接受规则。然而，这要求M所使用的区域都不被用于实例化N的形成中的乘法量化器。这是有意义的，因为用于形成这种实例化的见证的区域可能需要与x所需的区域不相交，因此也与M不相交。因为主语归约需要代入，所以排除规则上相应的副条件这个系统的约化由αλ的约化和固定域上的明显βη-规则组成，详见[3]。关键的元理论属性（即，，容许的替代（切割），规范化，主题减少）的系统都持有：证明是简化那些从类型变量的情况。3区域不相交模型αλ的模型由Carnival双闭范畴（CDCC）组成。[14]中给出了一个重要的模型，称为αλ的基本不相交模型（BDM）。这个模型是基于集合的范畴和机器位置的集合的范畴（称为世界）。它是αλ的一系列模型中最简单的一个，解释了以机器内存为资源的计算中αλM. Collinson，D.Pym/Electronic Notes in Theoretical Computer Science 158（2006）171179−−∗†−−∗1∗⎨11111111（Ax）BτB|x：τ x：τ（ 一）B |Γ，x：σ <$M：τB|Γλx：σ。M：σ−−τB| Γ（Δ）<$M：τ B <$ΔJ（W）B| Γ（Δ; ΔJ）M：τ（）B|Γ<$N：σ−−<$τB|ΔΣM：σ（E）B |Γ，Δ app（N，M）：τ（一）B;ρ|τM：τ（††）B|ΓM：τρ.τ（τE）B|Γ π Λρ.M：π ρ.τB;ρJ|ΓApp（M，ρJ）：τ [ρJ/ρ]（一）B，ρ |τM：τ（††）B|ΓM：ρ.τ（E）CIBB|我的天玛：好的。τB，ρJ|Γ<$App<$（M，ρJ）：τ[ρJ/ρ]<$（FW）BJ|r M：τ（BBJ）B1|τM：τ（FE）B（BJ）|τB1J|rM：τ（FC）B（B1; B1J）|r M：τB（B）|Γ[B/BJ]<$M [B/BJ]：τ [B/BJ]（B1=B1J）图1.一、术语构成在本节中，我们开发BDM，使其支持聚束区域多态性。我们称之为基本区域不相交模型（BRDM）。这是一个索引类别，其中基对象是领域。它是[3]中一般范畴模型的一个实例（简化）。在大多数情况下，可以理解BRDM，而不需要索引类别的知识，因为大多数结构实际上只是关于集合和函数的族。3.1基本不相交模型[14]中的构造从给定的无限集合Loc开始。世界是一组有限的地点。设W=Pf（Loc）是所有世界的集合。这也被视为同一名称下的一个独立类别BDM基于函子范畴SetW，其中Set是集合和函数的范畴。对象用来表示αλ的项的类型和态射。本文逐点给出了可加乘积和函数类型的闭包结构，并利用它来解释可加乘积和函数类型。另一个monoidal封闭结构（用于解释乘法乘积和函数类型）稍微复杂一些。W上的部分二进制运算定义为：如果VW=，则VW =VW否则将无法确定180M. Collinson，D.Pym/Electronic Notes in Theoretical Computer Science 158（2006）171∈ W{}×∈{}∈ W∈ W对V，W∈ W。对于任何世界W，设W#是与W不相交的世界的族。在[4，5]之后，这导致了集合W上的张量。对于A，B∈集合W，这由下式给出：（A <$B）W ={<$U，V，a，b<$|a ∈ AU，b ∈ BV，U <$V = W}在W∈ W。 相应的指数有（A−−B）V=W∈V#（A（W）=B（VW））在任何世界V，其中=是集合论函数空间这产生了乘法的共享解释：乘法对来自不相交的世界;乘法函数从与函数使用的世界不相交的世界中获取参数在[14]中通过使用一种类型的存储器产生了使用乘法的分离性质的有趣例子。 为了做到这一点，我们让L：W −→Set成为包含函子，这样LW=W就被认为是一个位置的设N：W −→Set是自然数的常数函子。使用显逐点运算定义函子S=L−→（1<$（N<$L））。 对于某个单例a和任意W，我们有SW = W =（a+（NW））。然后我们可以把s SW看作世界W上的store部分的表示：元素a表示空指针，每隔一个位置包含一个整数和一个位置。现在我们引入一些额外的符号。设WJ是W的任意子族，t是函子族，对任意U∈ WJ，t（U）∈SetW.让U∈WJ是乘积的逐点提升。 也就是说，（U∈WJt（U））V=U∈WJt（U）V对于任何VJ。 记πU为U∈WJ的第U个投影， 逐点提升3.2位置、区域和领域回想一下，位置是内存不可分割的一部分-对于本节，我们不存储值-而区域是位置集合的一个-对于本节，有限-子集。 在这个特定的模型中，一个区域就像一个世界。情况并非总是如此，区分区域和世界是有用的，因为它们扮演着不同的角色。M. Collinson，D.Pym/Electronic Notes in Theoretical Computer Science 158（2006）171181∩我⎩∩∅对于任意函数R：FRV（B）−→ W，设R [Bi] ={R（ρ）|ρ∈FRV（B）}Loc对于任何Bi，它是B的子束。域B的（区域）环境是函数R：FRV（B）−→ W，使得如果（B1，B2）是B的子束，则nR[B1]<$R[B2]=n。注意，如果例如（B1;B2）是B的子块，则R [B1] R [B2]不一定为空。令LocR=R[B]，对于B的任何区域环境R。设REnv（B）是B的区域环境的集合。我们现在构造一个范畴Realms，对象由Realms组成。设A和B为零，并且设FRV（B）={p，1， . . ，ρJn}。代入（−）[ρ1/ρJ1， . . ，ρn/ρJn]由ρ1，. ..其中ρ i在A i中，ρ j在A j中。 注意n = 0时的特殊情况。中的箭头从A到B的领域就是用A的变量替换B的变量。验证这是一个类别是例行的。此外，这个范畴有有限积和一个额外的幺半群结构。这个幺半群实际上是一个伪积，如[3]中所描述的。设s：A−→B是一个置换。对任意R∈REnv（A），我们可以定义函数Rs：FRV（B）−→W。 Ifs=（−）[ρ1/ρJ1， . . ，ρn/ρJn]表示Rs（ρJi）= R（ρ i），其中1 ≤i≤n.这给出了一个函数（−）s：REnv（A）−→REnv（B）在不同领域的区域环境之间。我们可以将B的任意区域环境R扩展，使得对于某个新的区域变量ρ∈/F，RU：FRV（B）<${ρ}−→ W给出RU（ρ）=R（ρi）ifρi∈FRV（B）U，如果ρi=ρ对于任何选定的区域U。设R是B的区域环境。则RU是B;ρ的环境。如果LocR U=，则RU也是B，ρ的环境。182M. Collinson，D.Pym/Electronic Notes in Theoretical Computer Science 158（2006）171−→−→−→−→拉吉−→3.3索引类别一个域B上的语义类型就是一个函数τ：REnv（B）SetW。也就是说，它是一个函子族，由区域环境索引。语义类型之间的morphismf：τ τJ是一族箭头（自然变换）（fR：τR−→τJR）R∈REnv（B）按区域环境索引B.也就是说，它是由区域环境和世界索引的函数族。从集合W逐点提升合成和恒等式给出了B上的语义类型范畴P（B）。对于每个领域B，范畴P（B）是一个CDCC，其操作是从集合W逐点提升的。给定替换s：A B，定义函子P（s）=s：P（B）P（A）如下。设τ是B上的语义类型。然后sτ（R）=τ（Rs）其中R∈REnv（A）. G ivenf：τ−→τJoverBwehaves（f）：s（τ）−→s（τ）由一族自然变换s<$（f）R=fRs：τ（Rs）−→τJ（Rs）其中R∈REnv（A）。s的赋值使它成为一个保持CDCC结构的函子。这些事实的证明是简单的验证，从定义-选项。特别是，第二个原因来自定义的逐点性质。进一步的计算表明，P给出一个函子P：RealmsCDCC是CDCC类和严格CDCC类的函子。对于投影π：B;α−→B和π：B，α−→B，通过用αi替换B中的任何αi，可以得到替换。函子π：P（B）−→P（B; α）将对象τ∈P（B）映射到族π（τ）（R）=τ（RTFRV（B）），其下标为R∈ REnv（B;α）。P（B）的一 个 函数f：τ−→τJ是 由 R ∈ REnv （ B ; α ） 表 示 的 函 数 π（f） ：π（τ）−→π（τJ）inP（B;α）given由 一 个 函 数 π（f）R=fTFRV（B ）：τ（RTFRV（B））−→τJ（RTFRV（B））.函子ππ的描述：P（B）−→P（B，α）与π的描述相同，只是族的索引为R∈REnv（B，α）。M. Collinson，D.Pym/Electronic Notes in Theoretical Computer Science 158（2006）171183−→∈J3.4泛量化器定义一个函子：P（B;ρ）−→P（B），用于加法量化器如下。将对象τ发送到τ（τ），τ（R）=τ（RU）（1）U∈W其中R是B的环境。 给定f：τ−→τJ，指定<$（f）R：<$（τ）（R）<$（τ）（R）由R索引REenv（B），带组件投影在每个U∈ W处。n（f）R，U=fRU<$πU：τ（RU）−→τJ（RU）U∈W对于乘法量化器，我们使用函子：P（B，ρ）−→P（B）。这将一个对象τ发送到τ（τ），（τ）（R）=U∈LocR#τ（RU）（2）其中R是B的环境。箭头的作用是通过对与LocR不相交的区域的索引的类似限制。定理3.1有两个算符π<$E <$和π <$E <$。该定理的证明是通过解开P（B）、P（B;ρ）和P（B，ρ）中箭头的定义对于加法，这表明箭头π<$（τ）−→τJ所对应的族可以归结为与箭头π<$（τ）−→ τj所对应的族相同的东西。箭头τ−→τJ。一个类似的证明给出了乘法的情况。Beck-Chevalley条件是普通（可加）量化器的指数分类模型所需的标准属性。它必须被检验，因为为量化器建模所需的函子的存在并不一定证明它成立。从逻辑的角度来看，贝克-谢瓦利条件说，量化与替换是互换的：如果我们在对ρ进行量化之后进行替换，这与对ρ进行量化然后进行替换是一样的。关于Beck-Chevalley条件的更多信息可以在[11]中找到。命题3.2 Beck-Chevalley条件。也就是说，对于任何s：A−→B，我们有P（s×1）=P（s）184M. Collinson，D.Pym/Electronic Notes in Theoretical Computer Science 158（2006）171∈））<$B∈Wτ（RU）=U∈Wτ（RU）保持。一个弱版本的贝克-Chevalley条件对λ成立。任何s：A−→B，有一束BJ和一个箭头sJ：A−→BJ，使得wsJ=sP（sJ1）=P（sJ）两者都成立，其中w：BJ−→ B是弱的。完整的贝克-谢瓦利条件不适用于乘法量化，因为索引上的不相交条件定义了函子的作用。直观地说，如果我们通过弱-在对ρ进行量化之前，则ρJ必须与ρ不相交。这不是如果我们在ρ上量化，然后在ρJ上减弱，那么必然是这种情况。弱Beck-Chevalley条件进行了适当的修改以处理这些问题。分离的问题。3.5模型结构总结事实上，我们有一个模型的演算立即遵循上述分类的结果关于这一点的一些评论是适当的。多态类型使用<$B<$ρ.τ）（R）=U∈Locτ（RU）R（三）其中RREnv（B），τ = B; ρτ和τ= B，ρτ。 的解释加法量化器的值使得量化变量在所有区域范围内变化。相比之下，对于乘法，它只在所有新的区域上变化，也就是说，那些与解释该类型时使用的所有其他区域不相交的区域。这暗示了多态性与（区域）分配和处置之间的联系-这是过去几位作者提出的。要弄清楚这种联系的确切性质，需要对模型进行一些改进，并对微积分进行仔细但相对较小的修改。这在第4节中完成。术语使用P的hyperdoctrine结构来解释;见[3]。纤维P（B）的CDCC结构被认为是第2节的一阶规则中的域的固定。在这种语言中，区域变量通过类型进入语言ρref. 在这个阶段，我们不直接使用这些类型开发示例。#M. Collinson，D.Pym/Electronic Notes in Theoretical Computer Science 158（2006）171185否则，（Ⅲ）（2）⊆不W −→然而，为了被定义解释，如果{l}=W<$R（ρ），则<$B<$ρref）RW=<$W{l}对于任何区域环境R和世界W。类似的选择在第4节中做出并解释。通过对[3]中给出的项M的解释，我们得到以下可靠性性质：定理3.3如果B |r M：τ是可证明的，则有一个箭头M：在B上的纤维中B<$r −→B <$τ。另一种模型是世界依赖于领域。 设R是区域环境。一个世界，W，是环境友好的，如果W LocR。语义类型的定义和以前一样，除了现在，在被赋予区域环境之后，它们只接受环境友好的世界。这个模型提供了函子来模拟两个通用量化器。乘法比加法简单.加性不再满足贝克-谢瓦利条件，所以不是很普通的多态性。出于这个原因，我们宁愿不坚持世界是环境友好的。在BRDM和第4节中，世界和领域之间的兼容性约束是在引用的解释中，而不是在结构中。3.6带区域的BDM的状态我们可以简单地采用BDM状态来给出一个在每个领域都是恒定的状态概念然而，我们可以重新定义国家的概念，以便充分利用区域结构。如 果 B=B1;B2 或 B=B1 ， B2 ， 则 n 写 为 Ri=RTBi=RTFRV （ Bi ） 且Wi=W<$LocRi，对于W∈W且i=1，2. 从定义域W的任意函数出发，定义si= sWi作为Wi的限制条件.设R：FRV（B）−→ W是域B的区域环境。德费恩在R处的状态函子，SR：Set，递归地在底层领域B的结构上：• 如果B=，则SR W={：={a}}• 如果B=ρ则SR W=（W<$R（ρ））=<${a}+（N×（W<$R（ρ））• 若B=B1，B2或B1，B2，则ns∈SRWi∈SRiWi，其中bi=1，2，其中{a}是任何固定的单元素集合。集合SR W总是包含在函数空间（W<$LocR）= N{a}+（N×（W<$LocR））中。186M. Collinson，D.Pym/Electronic Notes in Theoretical Computer Science 158（2006）171−−→用于ρ的子句强制了这样一个条件，即任何与R（ρ）相交的链接位置 系 统 必 须 完 全 包 含 在 R （ ρ ） 内 。 注 意 ， 条 件 si ： Wi−→ {a}+（N×Wi）在三个定义子句的最后得到保证，因此存储si完全包含在区域Wi内。重要的是要理解第三个条款的最后两个部分之间的区别在B=B1;B2的情况下，世界W1和W2可以重叠;因此，对于i j，Wi中的位置可以指向Wj中的位置。 的情况B=B1，B2，世界W1和W2不重叠，因此Wi中的指针不能看到Wj中的位置。一个带有状态参数s的过程，如果在域B1，B2上键入，可以保证产生一个完全包含在R[B1]中的输出，因此不与R[B2]相交。如果B2上的参数不再使用，那么我们可以处理R[B2]。在[24]中给出了一个这样的例子，涉及两个列表，存储在不同的区域中，并连接到其中一个区域中。3.7带单例区域的BDM区域模型很容易专门化为位置模型：一个带有位置变量而不是区域变量的微积分模型。位置变量旨在在位置而不是区域范围内变化。语言和以前一样，只是解释发生了变化。 参考x：ρref旨在居住在ρ指定的位置。这种类型在一些更高级的内存管理演算中广泛存在-例如[13，28]。我们继续使用FRV（），即使我们现在有位置而不是区域变量。我们将区域环境的概念修改为位置环境，这是一个映射R：FRV（B）Loc，以便每个位置变量与环境中的唯一位置相关联。在一个位置evnirrR中，R（ρ）=l，一个参考x：ρref位于位置l。请注意，当两个位置变量相乘组合时，它们必须通过位置环境映射到不同的位置。利用上述方法构造了语义类型、基范畴和由替换引起的函子。如果ρ i ∈ FRV（B），则Rl（ρ i）= R（ρ i），否则Rl（ρ i）= l，则B的环境R可以通过位置l扩展到B ; ρ的环境Rl. 这也是对B的一个不确定性，当nl∈/LocR时。用于解释量化器作用于适当对象τ的函子<$：P（B;ρ）−→P（B）和<$：P（B，ρ）−→P（B）为：（τ）（R）=τ（R l） τ（τ）（R）=l∈Locτ（R1）l∈/LocRM. Collinson，D.Pym/Electronic Notes in Theoretical Computer Science 158（2006）171187（2）否则，其中R是B的任何位置环境。 即<$B∈Locτ（R）=l∈Locτ（Rl）（四）我的天啊τ）（R）=l∈/LocRτ（R）L其中R∈REnv（B），τ = B; ρ<$τ和τ= B，ρ<$τ。加法只是对个体的普通量化，而乘法是一种新的量化：量化的变量在未使用的位置上变化。引用类型的解释修改为：如果W={R（ρ）}，则<$B <$ρref）RW=<$<$W对于任何位置环境R和世界W。在下一节中，我们将开发一种语言，通过区域变量中的乘法多态性进行区域分配和对于在位置变量中使用乘法多态来分配单个引用，应该可以做类似的事情，但是我们还没有完成这种方法的所有结果。4区域分配和处置在本节中，我们对BRDM和集束区域演算进行了改进，以展示如何使用它来支持区域分配和处置。我们引入了一种带引用的聚束多态区域语言，基于Berdine和O'Hearn[ 2 ]给出的一阶语言这是[2]中给出的用于分配、强更新和处置一阶引用的语言的变体。它是建立在一阶聚束微积分αλ上的，但由于技术原因（与处理的合理性有关），它是用连续传递式（CPS）来表示的。他们的语言在BDM的一个版本上具有指称语义，因此可以将其巧妙地集成到我们的方法中。我们不要求我们地区语言的实际意义。我们的主要目的是表明，指称模型，捕捉一些最基本的属性区域语言可以使用我们的方法构建。对Berdine和O'Hearn语言的基本扩展188M. Collinson，D.Pym/Electronic Notes in Theoretical Computer Science 158（2006）171≡►⊆重要的是，我们的语言不需要新的证明规则或约简关系，因此对第2节的元理论的修改是最小的。4.1该区域语言类型τ由可存储类型σ：= T生成|int，如下所示：τ：= σ|我|τ∧τ|τ→τ|τ∗τ|τ−−∗τ|我的天τ|你好τ|一|H（B，τ）|（ρ，σ）ref这里我们使用了一个新的类型常量a，以及类型构造函数H和ref。包含类型为σ的值并且位于区域ρ中的引用将是类型（ρ，σ）ref。H（B，τ）的居民是一个连续，它取堆和B中的区域来产生τ型值。因此，H（B，τ）中的领域B与Tofte-Talpin系统的类型判断中被称为结果的句法实体有相似之处类型a在延续类型H（B，a）中用于描述通过分配、释放和引用的强更新对堆的改变。[2]中的一个基本思想是加法类型H（B，a）→H（B，a）描述不改变堆的命令。相比之下，命令H（B，a）−H（B，a）可以进行这样的更改。这跟踪了一个分离逻辑中逻辑连接词的类似概念。和前面一样，良构类型B τ就是那些具有FRV（τ）FRV（B）的类型。域B上的上下文像以前一样生成，服从这些新类型。使用第2节中的规则生成格式良好的项，并与图2所示的常数族一起生成。常量上的下标表示索引族。这些通常会被忽略。newregion和freegion常量在任何包含B. 新的，免费的，！，：=和：numb常量在域B上是类型良好的，不要把它放出来。零和后继常量具有其通常的含义。有常量new和free用于分配和释放单个引用。常数！是解引用，而：=是类型保持（弱）引用更新。我们还有：用于类型更改（强）更新引用。最后，我们有常量newregion和freegion来分配和处理整个区域。获取这些常量句柄的方法是查看相关的派生规则，以