捆绑类型化中的强更新和处理

理论计算机科学电子札记158（2006）81-98www.elsevier.com/locate/entcs捆绑类型化中的强更新、处置和乔什·伯丁微软研究院1Peter W.伦敦大学玛丽皇后摘要我们提出了一种用于强（类型更改）更新和处理一阶引用的捆绑中间语言。与其他子结构类型系统相比，捆绑类型的附加构造允许封装由过程集合共享的状态关键词：成束类型，分离逻辑，强更新，处理，封装，连续传递风格1引言子结构类型系统提供了一种控制程序中资源使用的方法。 这种资源控制的第一个例子是干扰的语法控制（SCI）[17]，它使用了一个a-contrast类型的系统（禁止收缩但不削弱）来控制一阶引用的别名。这促进了集束类型和逻辑的发展[13，15，12]，其中子结构特征与intu处于相同的基础上独立式打字。“同一立足点”的意义一个单一的范畴，既承认carbohydrate封闭，1在伦敦大学玛丽皇后学院EPSRC支持下完成的工作1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.04.00682J. Berdine，P.W.−∗→对称幺半群闭合结构集束类型的完整直觉连接词被用来定义SCI的扩展版本，该版本处理原始版本中与递归和连续性有关的问题[12]。在平行的发展路线中，受线性逻辑启发的类型系统[7]允许在纯函数设置中进行破坏性更新和安全处理内存[23，24，25]。这些语言反过来又是强制执行的强制类型化中间语言，允许安全处理和强更新，其中引用的类型允许随时间变化[10，26，4]。本文的部分灵感来自[9]中报道的最近的工作，它以一种令人愉快的精简形式呈现了类型化中间语言的一些想法，并通过定义一种空间可能世界模型向集束逻辑或类型理论迈出了一些步伐。 （特别是那些新的主题，鼓励阅读[9]。 这有助于我们更好地理解所涉及的一些问题，把我们的手指放在一些困难上，现在我们在相反的方向上采取了一些我们自己的步骤（从集束类型理论到类型化中间语言）。我们参考[9]进一步讨论线性类型如何支持强更新和处置，以及它们在中间语言中的使用，参考[25，1]了解子结构类型系统的一般背景和对进一步文学关键的一点是，这些平行的发展路线已经以不同的方式应用。在使用SCI和集束类型的行中，别名是受控制的，并且允许全强度附加连接词。但所研究的语言不允许强更新或处置。在线性类型行中，允许强更新和处置，但在特别是线性逻辑的加法积，不是。那么，一个自然的问题是，捆绑类型是否也可以包含安全处理和强更新。答案并不是立即的，因为[12]中的例子表明，使用次数读数提供了为什么强更新和处置在线性类型中是合理的直观理由，与集束类型不兼容。第二个问题是，允许使用添加剂是否会带来任何好处，就像聚束打字一样。本文旨在探讨这些问题。我们提出了一种基于束类型的语言，它确实支持处置和强更新。该语言以CPS（continuation- passing style）形式呈现。处置作业的类型为：自由基：a→（nref − na）在这里，a是答案的类型，是直觉函数类型，乘法类型ref a被赋予一种空间解读：如果你给我一个与我所拥有的不同的存储空间，我就能产生一个答案。J. Berdine，P.W.83−∗→对自由内存的理解是，如果你给我一个引用某个存储的延续，然后给我一个完全独立的存储中的引用，我可以处理这个引用，然后安全地运行延续。请注意，这篇文章没有提到使用次数;处置的安全性源于对分离的直觉（镜像分离逻辑[16]和别名类型[26]）。这里的答案类型a表示Reynolds [18]意义上的命令延续：命令延续接受一个状态，然后运行。常规命令是类型a的加法函数 a. 我们也有使用类型A的“乘法命令”的可能性因为我们的语言是CPS，所以它应该被看作是一种中间语言而不是源语言。事实上，定义一种支持处置的直接风格语言并非易事。其原因可以从两个预期的附加类型规则中看出：rM：σrN：τr（M，N）：σ×τΓM：σ→τΓN：σΓM N：τ如果我们从按值调用计算的角度考虑，如果M和N在产生值之前都处理了一个公共引用，那么（M，N）将导致错误，即同一个引用被处理了两次。类似的评论也适用于M N。解决这个问题的一个可能的方法是使用一种形式的Hoare类型，也就是说，一个既有前置条件又有后置条件的类型系统。一个技术含量较低的方法是使用CPS。例如，CPS类型规则ΔK：arM;K：a可以被认为是相对于前置和后置条件Γ和Δ的M类型化。前置/后置类比可以在某些类型化中间语言中清楚地看到，如 [21]。最终的目标是获得一个直接风格的源语言，所有的束类型，支持更新和处置。 然而，一个首要的问题是，集束类型是否可以表达这些功能。从科学上讲，作为第一步，从现有的类型系统（[15，12]）的角度来研究这个问题，而不是假设的，还不存在的，使用束的高阶前/后类型系统，这是更明智的。这样一个系统的公式化是未来研究的一个主题，与分离逻辑的联系也是如此（考虑到分离逻辑和聚束逻辑之间的联系，这可能是希望的）。考虑到我们有了集束类型的全部添加剂，下一个问题是这是否增加了可扩展性。总之，我们能够将Reynolds在其关于SCI的工作中强调的一个特征：由过程集合共享的状态的封装转移到具有处置和强更新的语言。84J. Berdine，P.W.→∧−∗−∗→−∗基本思想可以通过生成计数器对象的过程的例子来解释方法的类型为μ=（（int→a）→a）<$（a→a）（一个a），一个方法的类型的加法乘积，用于获取计数器的值，递增，并在完成时销毁它。前两种方法使用additive函数类型。它们保留了背景堆的类型和形状destroy方法是一个乘法命令，其中输入continuation操作的堆比命令小。乘法命令不能与其他两个方法中的任何一个进行后组合，因为不会有堆形状（语义上）或上下文（理论上的类型）的匹配。这种对象的客户端类型是（μa）、a，在捕获客户端不知道方法共享的状态在第3节中，我们将推导出一个术语（目前不太可能有意义）。真λ k。新λ_x。x：0 $λx。k（mb）：（μ − a）→ a用于生成计数器，其中mb是用于方法主体的代码。据我们所知，这种封装行为不能像[23，25]那样使用线性类型语言的单态片段来表示，因为加法类型A B的值不能包含任何表示线性对象的标识符。引用是典型的线性对象。因此，不可能构造共享对隐藏状态的访问的加法函数的集合。在继续之前，我们应该说，我们在这一节中所做的评论不应该被解释为支持捆绑类型的最终论点。例如，共享状态可以通过向线性语言添加类型量化来表示。这就是为什么我们包括了“单态”这个限定词。我们的评论只是为了指出与以前的工作相比，我们的一些差异是什么，我们这样做只是为了给子结构分型的图片增加信息，而不是为了争辩最终的优势。此外，我们的玩具语言是故意削减，以便让我们调查的问题，在这篇文章中处理的最低限度的分心。出于这个原因，我们不包括高阶引用或多态性，即使这些对于具有表达性中间语言是必要的，例如，[10];这是未来工作的方向[6]，[5]给出了这里提出的语言的语义，扩展了多态位置和区域类型。2型系统我们通过指定几个基类型和常数来专门化[15]的单态聚束类型理论。(We省略联产品类型，因为它们J. Berdine，P.W.85≡S将不需要，尽管它们将出现在稍后介绍的模型中。） 基类型是integers的int类型，这是要使用 作为延续传递样式中的答案类型，而原始类型则是包含可存储类型的值的引用，可以是int或true。我们认为这是两个可存储的类型，只是为了让我们能够研究变化的类型（强更新）。系统的类型和上下文由语法给出φ，φ：：=int|真可存储类型σ，τ：：= a|ψ|τ∧τ|τ→τ|EMP|阿夫雷夫|τ∗τ|τ−∗τ类型Σ、Δ、Γ：：= x：τ|真正|Γ; Γ |EMP| Γ，Γ簇其中x在某个标识符集上的范围。“每个人都有自己的单位。符号Γ（Δ）指示束Δ表现为Γ的子束。我们用来表示满足交换幺半群律的丛上的最小同余关系separatel y，for“，“and d emp. Γπ=Δ表示Γ和Δ同构作为树;即，一个可以通过标识符的适当重命名从另一个获得。出现在一串中的标识符的集合记为i（Γ）。类型规则如表1所示，其中是一个尚未指定的常量与类型的关联。 最后两个结构规则是捆绑版本第一个概念通过引用连贯的等价（交换的）来包含交换。语言的术语在类型规则的结论中显示，常量（我们现在指定S）如下：z：intZ∈ Z+ ：intint →intswap，φ：（φref−a）→（refφ−a）new：（true ref−a）→a自由基：a→（nref− na）！：（：=：a→（（reftrue）→a）框架：（a→a）→（（−a）→（−a））hoistσ，，τ：（σ（τ））→（（σ）τ）我们使用连续变压器类型（例如，形式（σ→a）→（τ→a）），而不是连续第二类型（例如，形式τ→（σ→a）→a），因为，尽管有一些句法复杂性（例如，$语法），我们发现它们更容易理解，遵循M：（σ−a）→（τ−a）和Hoare三元组{τ}M{σ}之间的粗略类比。常量交换交换了引用中的类型和没有引用的类型（遵循[9]）。然后我们有分配和交易位置的常数。接下来，有查找和弱（类型保持）86J. Berdine，P.W.（2）表1打字规则x：τx：τI标识符和常量S（c）=τ真实温度：τ结构规则ΓM：τΔM：τΓ（Δ）M：τΓ（Δ ;ΔJ）M：τ添加剂Γ（Δ ;ΔJ）M：τΓ（Δ）<$M[i（Δ）/i（ΔJ）]：τΔ=ΔJ真实的，真实的：真实的rM：σΔN：τr;Δ（M;N）：στΓ;x：σ<$M：τΓλx：σ。M：σ→ τ电子邮件：emprM：σΔN：τr，Δ（M，N）：στΓ，x：σ<$M：τΓλx：σ。M：σ − τr（true）M：τΔN：truer（Δ）lettrue=NinM：τΓ（x：σ;y：τ）<$M：<$ Δ<$N：σ<$τ在M：π中， Γ（Δ）的双曲方程（x：σ;y：τ）=NΓM：σ→τΔN：σΓ;ΔM N：τ乘法Γ（emp）<$M：τ Δ<$N：empΓ（Δ）令emp=NinM：τΓ（x：σ，y：τ）<$M：<$ Δ<$N：σ<$τM中的Γ（Δ）Elementlet（x：σ，y：τ）=N：ΓM：σ−τΔN：σΓ，ΔM N：τ更新，这是更多的添加剂的字符。然后有一个常数用于添加遵循分离逻辑的框架规则的不变量最后一个常量的作用是告诉类型系统，可存储类型是纯的，这意味着它们对堆不敏感，因此可以在堆和堆中移入和移出。在分离逻辑中，这些事实是通过这两个连词的逻辑含义，和，对于纯类型一致。对于类型论，我们将展示一个模型，其中σ <$（σ<$τ）=（σ <$$>）<$τ，因此hoist是恒等函数。我们可以包含一个递归常数，具有通常的类型，没有困难;它只需要我们使用域来代替稍后定义的模型中的集合。下一节将包括这些常量如何工作的示例和直观解释。符号我们在乘法和加法乘积的项形成规则中玩了一个小游戏，在表示对的符号中使用这Γ≡ΔJ. Berdine，P.W.87表2允许和可导出的类型规则Γ（π）πM：τΔ πN：π在M中，Γ（Δ）小峰Σ=N：τΓ;ΔμM：τΓλΔ.M：Δ→τΓ，ΔM：τΓλΔ.M：Δ−τ联系我们ΔK：φref−aΓ，ΔswapM$K：a中文（简体）ΔK：ref−aI，Δ！！马来西亚$K：aΓK：true ref−a中文（简体）联系我们ΔK：φref−adefΓ-新K：aΓ，ΔM：，φN$K=：，φK（M;N）：a中文（简体）ΔK：aΓM：ref（r，Δ）;n=K：n→a无Γ、ΔτM$K：a（r，Δ）;def$true）： a中文（简体）（r，Δ）; N：（Γ，Δ）;ΔK：adef（r， Δ）;M：=，φN$K=：=，φK（（M，true）;N）：aΓπC：a→aΓK：−aΔF：r，ΔframeCK F：aΓ（（Δ ;x：τ），τ）M：τdefr（Δ，（x：;））hoistM=let（Δ;x：），=hoistΔ，（x：;）inM：τ允许我们引入一些语法糖，以减轻束（上下文）和类型之间的区别的不便，这并没有出现在语义中。首先，我们把“类型”的“类型”写成“类型”，也就是说，没有任何标识符的“类型”的“类型”，用“，“替换为”类型“，用”;”替换为“类型”。类似地，我们为没有任何类型的Γ写Γ然后，对于任何Γ，我们得到：联系我们此外，我们将使用letn =N在M中销毁任意束。当这个句法糖通过对Σ的归纳来定义时，我们得到了表2中第一个规则的可容许性（Σ具有形式x的情况：σ是割）。此外，我们引入了明显的句法糖抽象，然后破坏任意束，产生的第二和第三规则的受理。在示例中，我们将（MK）N写成MN$K，将（MK）N写成MN$K才能从头到尾写程序特别要注意的是，$绑定比应用程序更紧密。为了方便起见，表2包含了常量的派生类型规则（我们在一些结论中引入了语法糖）。ψ！CIMMK =！K（M，88J. Berdine，P.W.≡−∗→ ∧−∗∧−∗→−∗defdef≡在继续之前，我们用几个介绍性示例来说明该系统：双处理为了说明显式释放是安全的，我们从最基本的病态类型术语开始，尝试双重释放：？empx：true refk：ak：ax：truerefx：true refk：a无错误x$k：ak：a，x：truerefx$freex$k：ak：一个新的λ_x。 free x $free x $k：a我们指出，这是univable与前提。强大的更新和更新定义查找的乘法形式，！！：（a）、（参考文献a）和强更新：，φ：（φrefa）、（参考文献φa），（注意类型的改变）在swap和hoist方面提供了一个强更新的例子：当在整数引用上调用时，对参数进行两次类型改变赋值。！！：（=λk。λ x。swap（x; true）$λ（v; x）. （swap（x; v）$λ（u; x）. 提升k（v; x））：，φ：（φref−a）→（refφ−a）=λk。15.swapxv $λ（i; x）.K x我们将在示例中使用这些操作，表2包括它们的派生类型规则。查找操作接受一个continuation，k，和一个独立于k的引用，x，并将x和x本身的内容返回给k。强更新本质上只是交换操作，除了：不返回被覆盖的值。的推导过程中有趣的部分！！（k;v：），（vJ：;x：true ref）swap（x;vJ）$λ（u;x）. 提升器k（v;x）：ak，（v：; vJ：; x：true ref）hoist（swap（x; vJ）$λ（u; x）. 提升器k（v; x））：ak，（v：k; x：true ref）hoist（swap（x; vJ）$λ（u; x）. 提升器k（v; x））[v/vJ]：a说明了收缩（将v复制到vJ）和使用hoist来重新排列束的组合，这使得v可以在第一次调用swap的参数和继续中使用。J. Berdine，P.W.89→−∗3封装我们现在给出一系列与更新和封装有关的示例将内部资源使用保持在内部作为一个热身来展示一个命令的内部资源使用如何不影响程序其余部分的类型，考虑组合new和free：x：truerefx：true refk：ak：ak：a，x：trueref无x$k：atrue无λk。新λ_x。freex$k：a→a因为我们有一个类型为a的命令在加法空上下文中，内部资源使用在类型中没有表现。该命令的表示是CPS标识功能，这意味着后续的分配可以自由选择在此分配和释放的相同位置无封装我们可以通过使用期望引用的延续（continuation）来对确实改变状态的命令建模，其中在延续类型中使用禁止别名。下面是一个简单的递增整数引用的例子：..v;xx：int refv;xv+1：intk：int ref−ak：int ref−ak：int ref − a，（v：int; x：int ref）x：v+1 $k：ax：int refx：int refk：int ref − a λ（v; x）. $k：intn+1 $k：int n +1k：int ref − a，x：int ref！！ x $λ（v; x）. x：pw+1 $k：ax：int ref λ k. 我的天！ x $λ（v; x）. x：k+1 $k：（int ref − k a）− k a这个例子存在于线性逻辑和BI的公共片段中，并且是建立在线性逻辑上的系统的类型，例如[20，9]，处理得很好。此示例显示工作中的更新，但不提供任何解释。代替这个例子中使用的 类 型 ， 我 们 希 望 有 一 个 递 增 命 令 ， 它 不 必 将 引 用 传 递 给 它 的contination，这样它就满足了判断x：int ref_inc：a→a。我们在这里使用一个加法箭头，直观地说，因为由con表示的计算，tinuation也应该访问引用，例如，再次inc它我们依赖于对BI 也就是说，90J. Berdine，P.W.→≡►→→a中的附加箭头必须表示函数（命令）和它的参数（延续）共享相同的资源，因为意图是两者都访问int ref。第5节将给出一个支持这种直觉的模型。物体生成使用加性弱更新和查找操作，上面寻求的整数引用上的增量操作可以由下式给出：..x：int ref=x：int ref（emp，x）; k; v=v +1：int（emp，x）;k;vk：a（emp，x：int ref）;k：a;v：intnx：=v+1$k：ax：intrefx：int refx：int ref;k：a;v：intx：=v+1$k：ax：int ref; k：a！ x $λv. x：= v+1 $k：a → adefx：int ref_inc = λk。 ！ x $λv. x：= v+1 $k：a → a(Note我们省略了一些在推导中已经出现的较低的类型。这里的要点是，我们可以在加法函数类型的项中有一个自由引用。这样，引用可以改变，而不会在术语的整体类型中提及。然而，我们不能做的是改变幕后引用的类型，因为，如果我们没有像在状态传递中那样在接口中显示引用类型（a→a），那么类型的变化将不会被跟踪。 对于这个例子，注意k：a;v：int是如何在对：=的调用中被保留的，即使它与x：int ref并不分离，x：int ref对：=进行操作。 规则：不允许对上下文的附加组合部分进行类似的保留（因为它不应该）。返回引用x的值的操作：int ref get：（intA.简单明了。最后，我们还定义了一个析构函数：x：intrefx：int refk：ak：ax：int ref，k：a无约束x$k：adefx：intreffree =λk. freex$k：a−a就像inc和get代码一样，这里面有一个整数引用。但是它的类型使用-而不是→;在捆绑类型中，当涉及到可以自由使用的标识符时，这两个都不比 另 一 个 更 特 殊 。 然 而 ， 因 为 我 们 这 里 有 一 个 乘 法 命 令 ， 所 以continuation操作的堆比命令本身小这里的区别是J. Berdine，P.W.91x：int ref，所以continuation将不能访问x。使用乘法命令，我们有机会处理自由引用，而在加法命令中，我们不能。加法命令和乘法命令之间的本质区别在于前者是顺序可组合的;例如，两次：（a → a）→（a → a）= λc。λk。 c（c k），而后者不是，因为以下不进行类型检查：两次：（a − a）→（a − a）= λc。λk。c（c k）乘法命令对于释放共享资源很有用，但它们不能与使用同一资源的其他命令后合成使用这三个操作，我们可以定义一个对象构造函数，其中μ=（（int→a）→a）<$（a→a）<$（a− <$a）是方法的类型，通过：.k：μ−ak：μ−ax：intref（get;inc;free）：μk，x：intrefk（get;inc;free）：a.x：true ref x：true refx = 0：intk <$λ<$x。k（get; inc; free）：int ref − int ak，x：true ref x：0 $λx. k（get; inc; free）：adef真新计数器=λk。新λ_x。x：0$λx。k（get;inc;free）：（μ−a）→ a我们要提醒读者的是，这个子是用于加法乘积的元组形成（使第2节末尾提到的博弈成为可能），而不是用于顺序合成。注意new counter和new类型之间的相似性：它们具有相同的形式，但new将引用单元传递给其客户端延续，而new counter传递命令元组。这里的一个关键点是方法的类型，这是一个加法结合。这意味着所有方法都可以共享它们之间的整数引用。然而，尽管有这种程度的共享，请注意，x和k在类型上下文中是这是很重要的，因为如果我们要处理x使用free，然后k访问x，将导致不可靠性。为了比较，与Ahmed的讨论表明，基于线性逻辑的系统的非递归，单态片段，如[2]，允许共享如上所述的一些资源的函数的类型元组，但没有自由方法。另外，可以构造inc和free对，但其类型不允许多次调用inc，然后调用free。92J. Berdine，P.W.−∗∗→ → →−∗4成帧在程序逻辑中，框架公理描述了不被计算改变的状态部分的不变量。在资源类型化中也会出现类似的问题，本节将研究语言支持的框架程度Framing Multiplicative Commands（免费）对于乘法命令，例如true ref a类型的free K，分帧很简单。请考虑：y：truerefy：true refΓK：ax：truerefx：true refΓ，y：truereffreeK y：aΓ，x：true ref，y：truereffree（freeK y）x：aΓ新λx。新λ_y。自由（自由K y）x：a对于callfree（free K y）x，上下文由Γ，x：true ref，y：true ref组成，而命令只对x：true ref进行操作，这使得上下文的其余部分，Γ，y：trueref，成为框架公理。正如上面的推导所证明的，乘法应用规则的形式允许这样的框架公理只被发送到推导的命令框架线程对于加法命令，事情就不那么容易了：考虑用λk调用计数器的方法。新计数器0 $λ（g; i; f）.i（i（f k））。要对此进行类型检查，我们需要导出：？k：a，Γi：a→a···k：a，Γi（i（fk））：a其中r=g：（int a）a; i：a a;f：a a. 但给定的前提是不可类型化的，因为实际上，对iif的调用不会干扰k，所以我们需要的是在调用方法时将k保留在一边，然后在最后将其传递给f。要实现这一点，可以给出一个inctype（a−a）→（a−a），它可以将a型（框架公理）的延拓贯穿于计算之中。这将是复杂和迂回的。此外，当解释-仅仅是线程框架，在不同的调用点上用不同类型的框架调用函数的类型示例可能需要为每个函数提供与调用点一样多的类型这将是非常不幸的。J. Berdine，P.W.93JavaScript 类 型 使 用 帧 线 程 ， 但 使 用 存 储 多 态 减 轻 了 负 担 [26] 。Thielecke [22]采用了这种框架线程方法，但他通过使用多态答案类型和省略涉及− k的类型规则的术语注释来避免复杂性。框架常数通过允许不变量直接添加到（添加）命令，保持单形语言，遵循分离逻辑成帧加法命令（使用帧）使用frame，可以在调用方法时保留continuation..Γ标架ai：（a−a）→（a−a）Γf：a −aΓ-标架aif：a−ak：afk：arfframeai（frame aif）：a − fak：a，r_f_framea_i（framea_if）k：atrue_f_λk。新计数器0 $λ（g; i; f）。framea i（framea if）k：a → a这个例子说明了框架的作用是如何实现（附加）命令的顺序组合的版本，其中命令不需要运行的上下文的单独部分（在这种情况下为k：a）被不变地传递到后续命令。这个推导还演示了树结构上下文（即束）的实用性。上下文k：a，（g：（int→a）→a;i：a→a;f：a−a）的集束结构表示所有方法都可以共享对公共引用的访问，而continuation被禁止共享它。这些成帧方法之间的语义差异在于，使用帧线程，基本上发生的是通过赋予命令存储多态或参数化类型，命令不会与参数交互的事实是手动内置的。另一方面，框架常数表明，命令的含义已经得到保证，不会干扰任何可能的单独参数。Recap总结一下前面的例子：只使用乘法类型和操作以及状态传递不允许封装状态，但是加法类型和操作允许封装的表达式然而，虽然框架是容易的，只有乘数，添加剂是更困难的。框架线程是一种方法，但是94J. Berdine，P.W.芬def∈（Ⅲ）（1）def（1）w=（1）（σJτJJ（Ⅲ）def否则，w=def否则，（w'，w"）|w=w'w''（Ⅱ）w）×（Ⅱ）w）w=w=瓦胡岛它包含了一些不必要的复杂性。另一种方法是借鉴分离逻辑(Here我们只包括一阶框架，也可以研究高阶框架规则[14，3]5模型在[12]之后，我们描述了一个空间可能世界模型。世界是一个部分函数，它为每个分配的位置分配一个类型。当这样一个功能被定义时，我们认为位置没有被分配。 集合 可能世界的值和部分交换幺半群定义为：defdef翅片Val={true} Z和Wld=（Loc~，，−−）其中w∈wJ取具有不相交域的部分函数的并集，当w和wJ的域重叠时定义。我们写wwJ是指这是我定义的。这里，洛克芬表示所有有限函数芬从位置到句法类型，都证明了：∈ Loc~，− −是Loc ~上的部分二元运算。可存储类型V表示值的集合，V（V）：def defV（true）= {true} V（int）= Z对于每个世界w∈Wld，H（w）=l∈dom（w）V（w（l））是与w兼容的堆的集合。类型表示将各个世界映射到值集合的函数，因此因此，τindexedw是每个世界wLoc集合元组的 集 合 。一个类型代表一个世界-w=H（w）2（1）w=V（V）EMPdefw=στdefσw）×（<$τ）w）（{emp}ifw=0（<$στ）defP（<$σ→τ）w=（<$σ）w）（<$τ）w）（参考文献）def{l}ifw={[l：]}<$σ−<$τ）defQ（<$σ）wJ）（<$τ）w<$wJ）集合论函数空间记为2，2是两点集。答案类型的含义 在一个特定的世界中，w由以下部分组成：函数接受该世界的堆并返回答案。它们是命令的延续。可存储类型的含义是与世界无关的，也就是说它们是常量元组. 引用类型的解释是值得注意的：只有当世界~）一¢芬J. Berdine，P.W.95（2）（1）∗→）（Ⅲ）|L不ϕ w=λc.λf是一个单体。这与分离逻辑中的“精确”指向关系有关对聚束类型理论中的其他联结词给出了标准的解释。加法乘积的乘积允许存在于同一世界的值对，而乘法乘积的乘积则从不同的世界中选取值对。这个结果可以在int ref int refw和int ref int refw中看到。在前一个世界w只能是一个单元素，如果外延是非空的，所以元组的两个元素必须是一个和相同的。在后者中，w的大小必须正好为2，并且不同的引用被发送到. 加法函数类型的语义要求它将给定世界的参数转换为同一世界的结果，而乘法类型则要求来自单独或新世界的参数类型为τ的常数c可以通过为每个w指定一个元素来解释cw∈τw也就是说，常量是一个类型正确的、世界索引的元素族。下面我们在给出常数的表示之前，先回忆一下每个常数的类型交换率，φ ：（φref−a）→（refφ−a）交换（φ，φ）defw=λkQwl'w<$φref）wl'<$a）wwl'. 鲁鲁鲁. λ（l（参考）wl，v<$φ））的。 λhwwl.k[l：φ]（h（l），l）[h |l：v]new：（true ref−a）→a（新）defw=λkQwlw<$trueref）wla）wwl. λ hw.Vl∈/dom（w）k[l：t ru e]l[h|l：t ru e]自由基：a→（nref − na）（免费）defw=λk （a）w . 鲁鲁鲁 .λl（参考）wl. λhwwl .k H|Whoistσ，，τ：（σ（τ））→（（σ）τ）升降机defσ，τ，τ w = λx。X！：（！）defw=λk <$→a）w. λx<$ref（真）wL不. λ hw.casexofi（w，w）（l<$ref）wl，t<$true）wt）ek（hl）h：=：a→（（reftrue）→a）：=defw=λk（a）w . λ（x（参考文献）w，v<$））的。λ hw.casexofi（w，w）（l<$ref）wl，t <$true））e<$k[h|l：v]框架结构 ：（a→a）→（（−a）→（−a））（图1）defa→a）wQwfw<$）wfa）wwfw<$）wfJwwfc（λ hw. kwff（hJ|（h））hJ|W这里，hw表示将h的定义域限制在世界w的定义域中得到的h的子堆。通过几个例子的语义值得一谈。 让它期望在世界w中的延续k和来自a¢.λk. wf.λh.96J. Berdine，P.W.（1）（2）∧ →∗−∗完全独立于k的由于引用的单例语义，这个单独的世界只能是一个单例，由单个位置l组成。然后我们取一个堆h，它给w和l中的位置赋值，因为整个命令continuation要求我们这样做，我们必须产生一个元素2。我们通过将h限制为w来做到这一点，从而有效地释放l，并将修剪后的堆提供给我们的输入延续k。最棘手的例子是新的。我们首先取一个期望引用的连续k，其中该连续期望一个与当前世界w分离的引用变元。因此，如果我们要使用k，那么类型的语义迫使我们找到一个新的位置。然而，有一个问题：有很多这样的新鲜地点。所以我们选择其中的任何一个，但是要求总体结果对我们所做的任何选择都满意，通过取结果的合取，在定义中， aw=H（w）2我们把集合2看作是由真和假组成的布尔值这是一个我们使用2是什么的知识。为了理解这里连词的使用，它有助于回忆一种对两个命令的非确定性选择（c1choose c2）进行连续语义的方法，即，a→a型连续变压器。我们可以这样做，如果我们知道2用于最终答案，λk。λs。（c 1） wksC2 wk s）。 从操作上讲，我们不希望两种选择都被采纳。特定运行，但它允许我们记录，在外延上，对于命令来说，它必须满足于任何不确定性的选择，进行了(This在应答类型中使用从状态到真值的映射使得连续变换器类似于断言变换器）。 语义ofnew使用了这一思想，调整以考虑期望引用的连续性而不是作为参数的普通命令连续性，并考虑对应于较大的不确定性选择的较大的合取。同样，这并不要求在操作上采取所有的选择，但捕捉到k必须满足于所做出的任何选择。在这里，我们将不试图给出与谓词变换或操作语义学的正式联系，而只是把这些评论作为我们自己发现有帮助的直观帮助。我们给出的信息足以指定整个语言的模型。我们所描述的是产品类别SetWld中的语义的类型和常量的语义，其中双闭结构（，）与[12]的基本分离模型相同。 为了填充语义，我们只需要遵循[15，12]中规定的范畴方案。我们不会在这里重复细节，但会简单地说明定理5.1（可靠性）类型判断Γ<$M的每个推导：J. Berdine，P.W.97<$r）w−→<$τ）wτ决定一族语义型函数由worlds w.(Note：在[12]的一般函子范畴模型中，这个族会带有自然性约束。然而，对于这个特定的模型，这些约束是微不足道的，因为Wld是一个离散的类别。这是一个显式类型语义（“Church模型”）所期望的结果。 而不是引入一种错误，然后证明，打字避免了错误，我们建立了自己的意义，根本不提错误，并观察到我们的语言停留在它的话语语言中。这种可能的语义世界形式需要一些时间来适应，特别是术语的赋值。然而，类型的语义相对来说是直接的，并且在确定语言中可以做什么和不可以做什么方面除了作为一个有用的设计辅助工具之外，这样的模型还有助于理解语言之间的基本差异。例如，我们对封装的评论是从观察到几种线性语言可以在像这里这样的可能世界模型中建模而来的，其中非线性函数类型本质上解释为（A− <$B）emp。然后，立即不能使用这些函数来访问共享的隐藏状态，并且同样明显的是，可以使用存在于模型中的Carbohydrate封闭结构（加法）来完成这种共享。一般来说，首先建立模型的方法-引用[1] A. 艾哈迈德，M。Fluet和G.莫里塞特L3：一种带有位置的线性语言技术报告TR-24-04，哈佛大学，2004年。[2] A.艾哈迈德，M。Fluet和G.莫里塞特子结构状态的阶跃指数模型。载于ICFP，2005年。[3] L. Birkedal，N. Torp-Smith和H.杨分离逻辑类型和高阶框架规则的语义。第20次LICS，第260-269页[4] J. Cheney和G.莫里塞特一种线性类型的汇编语言。技术报告2003-1900，计算机科学系，康奈尔大学，2003年。[5] M. Collinson和D.皮姆 区域和位置语义的集束方法。在SPACE，2006.[6] M. Collinson，D. J. Pym和E. P.罗宾逊。关于集束多态性。CSL，第36-50页，2005年98J. Berdine，P.W.[7] J. - Y.吉拉德线性逻辑。Theoretical Computer Science，50（1）：1[8] S. S. Ishtiaq和P.W.奥赫恩BI作为可变数据结构的断言语言。在第28届POPL，第14-26页[9] G. Morrisett，A.J. Ahmed和M.弗拉特L3：一种带有位置的线性语言在p.Urzyczyn，编辑，TLCA，LNCS第3461卷，第293[10] G. Morrisett，D.沃克，K. Crary和N. Glew.从System F到类型化汇编语言。ACM TOPLAS，21（3）：527[11] P. O'Hearn，J. Reynolds，and H.杨关于改变数据结构的程序的局部推理。在CSL，LNCS的第2142卷，第1-19页[12] P. W.奥赫恩关于集束打字。J. Functional Programming，13（4），2003.[13] P. W. O'Hearn和D. J. Pym。一堆暗示的逻辑。Bulletin of Symbolic Logic，5（2）：215[14] P. W.奥赫恩，H。Yang和J.C.雷诺兹分离和信息隐藏。在第31期POPL，第268-280页[15] D. J. 皮姆The Semantics and Proof Theory of the Logic of Bunched Implications，第26卷，应用逻辑系列。Kluwer，2002年。[16] J. 雷诺兹分离逻辑：共享可变数据结构的逻辑第17次LICS，第55-74页[17] J. C.雷诺兹 干扰的句法控制。 1978年，第五届人民解放军[18] J. C. 雷诺兹 大陵五的精华 在j.W. de Bakker和J.C. van Vliet，编辑，《明史》卷345-372。 1981年北荷兰[19] D. S. Scott和C.斯特雷奇 计算机语言的数学语义学。 在计算机与自动机研讨会论文集，1971年。[20] F.史密斯，D. Walker和J. G.莫里塞特你这是什么人。In G. Smolka，editor，ESOP，volume1782 ofLNCS，pages 366-381.斯普林格，2000年。[21] K. N. Swadi和A. W.阿佩尔类型化机器语言及其语义。Mandarin pt，2001.[22] H. Thielecke。 从代码指针的答案类型中构造规则。在POPL，2006年。[23] P. 瓦德勒线性类型可以改变世界！In M.Broy