一个纯微积分的命令式语言的简单演算及其应用性

可在www.sciencedirect.com在线获取理论计算机科学电子笔记322（2016）87-102www.elsevier.com/locate/entcs一个势在必行的纯微积分1安德烈·卡普里乔利DIBRIS意大利Genov大学Marco Servetto2新西兰惠灵顿维多利亚大学埃琳娜祖卡3DIBRIS意大利Genov大学摘要我们提出了一个简单的演算，其中的命令式功能建模重写源代码条款，而不是通过修改一个辅助结构，模仿物理内存。从形式上讲，这是通过块构造来实现的，它引入了局部变量声明，当这些声明被评估时，它也扮演了存储的角色 通过这种方式，我们获得了一种语言语义，这是更抽象的，并直接表示在句法层面上的约束别名，允许更简单的推理相关属性。我们通过标准类型系统的一个简单扩展来说明这种可能性，该扩展将胶囊标签分配给表达式，这些表达式将减少到（表示）商店的隔离部分。保留字：操作语义，命令演算，别名1引言命令式语言的传统执行模型使用一种称为内存或存储的辅助结构，它是物理内存的数学抽象，通常是从位置（建模内存地址）到可存储值的映射。位置是一个运行时概念，它们的名称是全局可用的，1这项工作得到了MIUR CINA的部分支持-未来ICT社会的2电子邮件：marco. ecs.vuw.ac.nz3电子邮件：elena. unige.ithttp://dx.doi.org/10.1016/j.entcs.2016.03.0071571-0661/© 2016作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。88A. Capriccioli et al. /Electronic Notes in Theoretical Computer Science 322（2016）87内存是抽象的，而变量是一个语言概念，它们的名字遵循作用域规则（阴影）和α转换。在本文中，我们提出了一种替代的，更抽象的，执行模型，这是一个纯演算。也就是说，执行是通过重写源代码项来建模的，就像lambda演算建模函数式语言一样下面是微积分中的一个归约序列的例子，我们在每一步都强调被归约的redexDz=newD（0）Cx=newC（z，z）Dw=新D（y. f1.f+1）x. f2 =wx −→（1）C=C（0）C=C（0）C（0） C = C（ 0）C =C（0）C（0 ）C= C（0）C（0.f+1）x. f2=w x −→+1）x. f2=wx−→C=C（0）Dz=newD（0）Cx=newC（z，z）Dw= newD（1））x. f2=wx−→x−→Dz=newD（0）Cx=newC（z，w）Dw= newD（1）x其主要思想是使用局部变量声明，如let构造，直接表示内存。也就是说，声明的变量不会像标准let那样被其值替换，但会保留关联并在必要时使用。4微积分是用面向对象的Java语言设计的，它的灵感来自于轻量级Java [14]。也就是说，假设一个程序（类表），其中类C有两个D类型的字段f1和f2，类D有一个整数字段f，在初始项中，前两个声明可以被看作是一个存储，它将z关联到一个字段包含0的D类对象，并将x关联到一个C类对象，其两个字段包含（引用）前一个对象。第一个归约步骤通过将y的出现替换为x来消除别名。接下来的三个约简步骤通过执行两次场访问和一次求和来计算x.f1.f+1最后一步执行字段分配。计算的最终结果是一个C类的对象，其域包含两个D类的对象，其域分别包含0和1。通常，存储中的引用可以是相互递归的，如下面的例子所示，我们假设一个类B具有一个类型为B的字段。Bx= new B（y）By= new B（x）y在到目前为止的例子中，内存是可扩展的，因为它通常发生在命令式语言的模型中。然而，在我们的微积分中，我们也能够表示一个层次记忆，如下面的例子所示，我们假设一个类A分别有两个类型为B和D的场Dz=新D（0）Aw =（Bx=newB（y）By=newB（x）Au=newA（x，z）u）w在这里，存储关联到w一个引入局部声明的块，也就是说，[4]由于循环lambda演算[4，3]的目的和技术问题不同，更多评论请参见结论。5这只是一个陈述的选择：论文的所有想法和结果都可以很容易地重新措辞，例如，在类似ML的语法中使用数据类型构造函数和引用类型。x.f2=wZ.F0+1C y=xx.f1A. Capriccioli et al. /Electronic Notes in Theoretical Computer Science 322（2016）8789−→一家商店。6这种表示的优点是，它以一种简单而自然的方式对对象之间的锯齿约束进行建模，特别是：• 一个对象不能从某个封闭对象的外部被引用的事实直接由块构造建模：例如，由y表示的对象只能通过w到达• 相反，对象不引用外部的事实由相应块是封闭的（即，没有自由变量）的事实来建模：例如，由w表示的对象不是封闭的，因为它引用外部对象z。请注意，这两个信息也保存在以下术语中Dz=newD（0）Bx=newB（y）By=ne wB（x）Au=newA（x，z） u而是应该通过计算变量之间的依赖关系来重构。换句话说，我们的演算平滑地集成了记忆表示与阴影和α转换。然而，有一个问题需要处理以保持这种表示的正确性：读取（或对称地更新）字段可能会导致范围挤压。例如，项C y=（D z= new D（0）C x= newD（z，z）x）y.f将简化为C y=（D z= new D（0）C x= newD（z，z）x）z。为了避免这个问题，禁止上述还原步骤然而，约简并不卡住，因为我们可以将上述项转换为内部块已被删除的等价项，并获得以下正确的约简序列：Dz=newD（0）Cx=newD（z，z） Cy=xy.fD z=新D（0）C x= new D（z，z） x.fD z=新D（0）z也就是说，我们认为表达式是等价的模移动一个声明序列从一个块到直接封闭的块，反之亦然，这种等价的使用方式与lambda演算中使用α-等价的方式完全相同还要注意，在最后一项中，x的声明已经被删除（更确切地说，我们通过等价再次得到这个简化的项），因为它是无用的。在[17]中已经提出了一个没有存储的命令式演算，然而，归约规则需要一个局部声明序列的堆栈作为辅助结构。在本文中，我们通过纯演算来形式化相同的想法，其中仅减少语言术语，为命令式语言提供简单而自然的基础模型，类似于如上所述的函数式语言的lambda演算。除了优雅和简单之外，这种语言执行模型不受机器实现的驱动，也不依赖于源程序中不存在的运行时结构更重要的是，它可以构成许多重要研究方向的基础，因为，如上所述，对象图拓扑结构直接以语法方式形式化，因此它们的属性可以更自然和更容易地表达和形式化验证尽管目前的焦点[6]在例子中，为了可读性，我们省略了最外面方框的括号。−→90A. Capriccioli et al. /Electronic Notes in Theoretical Computer Science 322（2016）87e **=x|e. F|e. m（es）|e. f=eJ|新C（es）|（dse）表达式D* *=Cx=e声明dv：：=Cx=rv求值声明rv：：=newC（xs）|（dvsv）钻机ht值v* *= x |rv值（对象）E：：=[] |E. F|E. m（es）|X. m（xs，E，es）|E. f= e J|X. f=E评估上下文| （dvs Cx = E ds e）|（dvsE）|(dvsE)Fig. 1.表达式、值和求值上下文本文是在演算本身，为了说明这些可能性，我们提供了一个简单的扩展的标准类型系统的语言，它可以分配给一个表达式的胶囊标签，这意味着表达式将减少到一个可达的对象子图，不能从外面别名。这个概念在有关别名的文献中有许多变体（外部唯一[5]，气球[2，19]，岛屿[13，8]，孤立[12]）。本文的其余部分组织如下：在第2节中，我们提供了微积分的形式定义，在第3节中，类型系统，在第4节中的结果，在第5节中，一些结论和进一步工作的指针。附录提供了辅助定义。因篇幅有限而省略的证明将在本文件即将出版的扩充本2微积分语法如图1所示。我们假设变量x，y，z，...，类名C，字段名f，方法名m。我们采用这样的约定，即以s结尾的元变量被隐式地定义为一个（可能是空的）序列，例如，ds被定义为ds：：= s| dds，其中，* 表示空字符串。一个表达式可以是一个变量（包括在方法体中表示接收者的特殊变量this一个声明指定了一个类型，一个变量和一个初始化表达式。我们假设在格式良好的块中，同一个变量没有多个声明，也就是说，ds可以看作是从变量到表达式的映射，我们使用符号dom（ds）和ds（x）。此外，为了简单起见，我们只允许在评估的声明7之间相互递归，例如，（Cx= newC（x）x）是允许的，而（Cx=x.fx）是不允许的。允许一般递归需要一个复杂的类型系统8，如[18]，但这不是本文的重点在示例中，我们可以自由地使用基本类型的表达式，例如int，[7]由第三生产定义，下面非正式地解释8.避免像示例中那样访问尚未初始化的对象A. Capriccioli et al. /Electronic Notes in Theoretical Computer Science 322（2016）8791但为了简单起见，在正式定义中将其此外，我们通常省略块的最外方括号，当x在eJ中不自由出现时，将（Cx=e eJ）替换为e eJ。在命令式语言的传统模型中，求值声明的序列dv扮演着存储的角色，也就是说，每个dv可以被视为右值与变量的关联右值可以是对象状态，形状为newC（xs），也可以是块值，即所有声明都已评估的块，并且主体是（递归地）值。后一种情况允许存储是分层的。对象状态newC（xs）表示基本分配单元，并且可以被认为是块的较短形式（Cx=newC（xs）x），如通过图2中的同余规则（NEW）形式化的。因此，块值具有形状（dv s1（. . （dv snx）.. . ）），对于n≥0。 我们称x为值的根，并假定在well-formed block值中，它约束在某些dvsi中。值是表达式归约的最终结果，它可以是变量（对对象的引用），也可以是对象状态，或者是块值。一个封闭的表达式应该减少到一个封闭的值。求值上下文表示标准的从左到右求值。请注意，当字段访问、方法调用和字段赋值子项是变量（引用对象）时，它们被认为是求值的我们将FV（e）和FV（ds）分别写为表达式和声明序列的自由变量，在附录中正式定义语义由一个全等关系和一个归约关系定义，全等关系捕获结构等价性，归约关系模拟实际计算，类似于发生的情况，例如，在π-演算中[15]。同余关系，记为y=，定义为满足图2中给出的公理的最小同余。规则（ALPHA）是通常的α-转换。通过以下两个规则，我们可以操作块中的声明。规则（REORDER）指出我们可以首先移动求值声明，在任意的或- der中。非正式地说，这是安全的，因为它们不再有副作用。规则（垃圾）指出，我们可以删除（或相反，添加）一个无用的评估decla序列一个街区的口粮请注意，只有安全地删除/添加被评估的声明才是可能的，因为否则，它们的评估可能会有副作用。通过以下两个规则，我们可以消除和引入块。规则（ELIM）声明了一个明显的事实，即没有声明的块等价于它的主体。 在rule（NEW）中，构造函数调用可以被视为一个基本块， 分配新对象。通过其余的规则，我们可以从一个块中移动一个声明序列， 到直接封闭的块，或者相反，因为它发生在π演算[15]中的范围扩展在前两个规则（BODY）和（DEc-RIGHT）中，内部块分别是封闭块的主体或声明的右侧的92A. Capriccioli et al. /Electronic Notes in Theoretical Computer Science 322（2016）87∼（ALPHA）（重新排序）（垃圾）（dsCx=eds′e′）=（dsCy=eds′e′）[y/x]（dsCx=rvds′e）n=（C x=rvdsds′e）、（dvsdse）=（dse）FV（（dse））（dvs）=（ELIM）（正文）（e）= e（新）新C（es）n=（C x=新C（es）x）FV（ds1）随机数（ds2）=随机数（ds（ds1ds2e））=（dsds1（ds2e））FV（ds）dom（ds1）=dom（DEc-RIGHT）FV（ds1）随机数（ds2）=随机数（dsCx=（ds1ds2e）ds′e′）n=（dsds1Cx=（ds2e）ds′e′）（字段-AccESS-Rcv）（dse）。f=（dse. f）的（甲基全反式） （dse）。m（es）=（dse. m（es））FV（es）dom（ds）=FV（dsds′）dom（ds1）=dom（meth-cALL-ARG）（FIELD-ASSIGN-LEFT）e. m（es，（dvse ′），es′）=（dvse. m（es，e′，es′））FV（e，es，es′）随机数（dvs）=（dse）。f=e′n=（dse. f=e′）FV（e′）dom（ds）=（FIELD-ASSIGN-RIGHT）e. f=（dvse ′）f=（dvse. f=e′）FV（e）dom（dvs）=（NEW-ARG）newC（es，（dvse），es′）=（dvsnewC（es，e，es′））FV（es，es′）dom（dvs）=图二. 同余规则附带条件确保声明可以安全地移动。更准确地说：前者防止移动到依赖于内部块的局部变量的声明相反，后者防止在由封闭块的其他声明使用的声明中移动。注意，这两个条件都不能通过α转换得到此外，请注意，条件dom（ds1）dom（ds2）=dom和dom（ds1）dom（ds）=dom（在第二条规则中，dom（ds1）dom（dsdsJ）=dom）是从块的良构性中隐含其他规则处理内部块是字段访问、方法调用、字段赋值或构造函数调用。在所有这些情况下，要执行的操作都将在声明的范围因此，我们必须避免捕获自由变量，如规则的副条件所指定的，这总是可以通过α重命名获得。 此外，正如上面的规则（重新排序）和（垃圾）一样，我们必须保持计算顺序，因此在某些情况下，声明需要也就是说，不再有副作用。约简规则如图3所示。Werite[y/x]表示通过将e中所有（自由）出现的x替换为y而获得的表达式，HB（E）表示E的洞绑定器，即在包围上下文洞的块中声明的变量，两者在附录中正式定义。我们假设一个固定的类表，由以下函数抽象建模：A. Capriccioli et al. /Electronic Notes in Theoretical Computer Science 322（2016）8793.（cTX）e −→e ′E[e]−→E[e′]（同意）e1−→e2e′1−→e′2e1=e′1e2=e′2dvs（x）=Cx=rv（FIELD-AccESS）（dvsE [x. f]）−→（dvsE[y]）x/∈HB（E），y/∈HB（E）场（C）= C1f1. Cn fn和f = figet（rv，i）=y且y∈FV（rv）x/∈HB（E）（meth-cALL）xiHB（E）<$i∈1.. n（FIELD-ASSIGN）（dvsE[x. m（x1， . ，xn）]）−→（dvsE[e[x/this][x1/y1]. . . [xn/yn]]）dvs（x）=Cx=rvx/∈HB（E），y/∈HB（E）dvs（x）=Cx=rvmbody（C，m）= 10y1.yn，e（DEc）（dvsE[x. f=y]）−→（dvs[x=rv′]E[y]）（dvse）−→（dvs′ e′）（dvsCx=edse′′）−→（dvs′C x= e′dse′′）场（C）= C1f1. Cn fn和f = fiset（rv，i，y）=rv′（化名）（dvsCx=ydse）−→（dvsds e）[y/x]图三. 减小规则• fields（C）为每个声明的类C给出其fields声明的序列C1F1... Cnfn• mbody（C，m）给出了，对于类C中声明的每个方法m，对x1. xn，e由它的参数序列和它的主体组成最有趣的归约规则是用于读取/分配字段的规则，因此我们首先详细说明这些规则，并提供示例，然后解释其他规则。字段访问在rule（FIELD-A cc ESS）中，给定一个形状为x的域访问。f，找到x的第一个封闭声明（侧条件x/∈HB（E）确保它是第一个），并从类表中检索x的类C的字段如果f实际上是C的一个场的名字，比如说，第i个，那么场的访问被减少到存储在这个场中的引用y返回右值的i-th字段的函数get定义如下（辅助函数auxGet也返回值的根• get（newC（x1， . ，xn），i）=xi• get（（dvsv），i）=yifauxGet（（dvsv），i）=x，y• auxGet（x，i）=x，i•auxGet（（dvsv），i）=x，y如果auxGet（v，i）=x，y，则auxGet（（dvsv），i）=yauxGet（v，i）否则副条件y/∈HB（E）确保y没有内部声明（否则y将被错误地绑定），并且总是可以通过α-重命名获得。例如，假设一个类表，其中类A有一个int字段，类B有一个A字94A. Capriccioli et al. /Electronic Notes in Theoretical Computer Science 322（2016）87段，则项A. Capriccioli et al. /Electronic Notes in Theoretical Computer Science 322（2016）8795⎪⎩如果auxSet（v，i，y）={x，i，y}，则将{x，i，y}转换为{x，i，y}，• auxSet（（dvsv），i，y）=dvs（x）=rvAa=newA（0）Bb=newB（a）（Aa=newA（1）b. f）的降低到Aa=newA（0）Bb=newB（a）（Aa1=newA（1）a）边条件y∈FV（rv）要求引用y不在rv中局部声明，防止作用域挤压，并且总是可以通过同余来保证，即通过应用规则（cONGR）。例如，如果没有这个附加条件，Dx=（Cy=newC（）Dz=newD（y）z）x。F将减少到Dx=（Cy=newC（）Dz=newD（y）z）y其中最后一次出现的y将是未绑定的。相反，我们可以取等价项C y=新C（） D X=（D） z=新D（y）z）x.f正确地简化为C y=新C（）D X= （D） z=new D（y）z）y外地任务在规则（FIELD-ASSIGN）中，给定形状为x的场赋值。f = y，找到x的第一个封闭声明（侧条件x/∈ HB（E）确保它是第一个），并从类表中检索x的类C的字段。如果f实际上是C的一个场的名字，比如说，第i个，那么x的右值的第i个场被更新为y。 我们将dvs [x = rvJ]写为从dvs获得的求值声明序列，将x声明的右侧替换为rvJ（省略了明显的形式定义）。下面定义了一个函数集，它返回一个右值，其中一个字段已经被更新（辅助函数auxSet也返回一个值的根• set（newC（x1， . ，xn），i，y）=新C（xi，. ，xi−1，y，xi+1， . ，xn）• set（（dvsv），i，y）=rvifauxSet（（dvsv），i，y）=x，rvx• auxSet（x，i，y）=x，yauxSet（v，i，y）否则边条件y/∈HB（E）要求引用y没有内部声明，防止作用域挤压，并且总是可以通过同余来保证，也就是说，通过应用规则（cONGR）。例如，如果没有这个附加条件，D x=新D（.）（C）y=新C（）x.f=y）将减少到D x=新D（y）（C）y=新C（）y）96A. Capriccioli et al. /Electronic Notes in Theoretical Computer Science 322（2016）87T：：=μC型μ：：=胶囊|可读|新型改性剂：：=x1：T1，.， xn：Tn类型上下文见图4。 类型和类型上下文其他规则Rule（cTX）是常见的上下文闭包。规则（cONGR）指出，同余是通过归约来保持的，并且可以用来，如上所示，减少一个否则会被卡住的项，就像lambda演算中的α-规则一样在规则（METH-c ALL）中，给定一个形状为x的方法调用。m（x1，. xn），找到x的第一个封闭声明（侧条件x/∈HB（E）确保它是第一个），并且从类表中检索x的类C的方法m在这种情况下，调用被减少到方法体，在那里它被接收者对象（引用）和参数所已经被年轻人取代了 边条件xiHB（E）i=1. n确保对于某些参数没有内部声明（否则，将被错误地绑定），并且总是可以通过α重命名获得规则（DEc）避免重复上述字段访问、方法调用和字段赋值的规则在rule（ALIAS）中，一个引用x，它被初始化为另一个引用通过替换其所有出现来消除y3类型系统图4中给出了类型和类型上下文。一个类型存在于一个类名中，它可能被一个类型修饰符修饰，这个类型修饰符可以是封装的，也可以是可读的。一个capsule表达式被期望简化为一个capsule对象，也就是说，一个没有来自/到外部的引用的对象（形式上，一个封闭的块值），而一个可读的表达式表示一个不能被修改或别名的对象。9类型上下文被假设为集合（也就是说，顺序和重复是固定的），我们对空集使用“空”而且，像往常一样，它们是从变量到类型的部分最后，我们假设这些类型要么是类名，从源代码中的类型注释中获得，参见规则（T-BLOcK），要么是可读类型，通过规则（T-CAPLOGS）削弱当前类型获得也就是说，虽然胶囊类型可以分配给表达式，但它们不允许作为变量类型。109更准确地说，可以暂时别名，例如，当作为方法的参数传递时，但不能存储在其他对象中。也就是说，这里的混叠是指[13]意义上的静态混叠。正如上面所讨论的，静态别名可能会在执行过程中的任意远处引起令人不快的意外，而动态别名在其发生的范围之外没有任何影响10原因是，为了保持capsule属性，capsule变量应该只使用一次。 在A. Capriccioli et al. /Electronic Notes in Theoretical Computer Science 322（2016）8797（T-c表）toReadable（Γ）e：CΓe：胶囊C（T-SUB）Γe：TΓe：TJT≤TJ（T-vAR）rx：TΓ（x）=T（T-字段-AccESS）温度：μC你好f：μCi场（C）= C1f1. Cnfnf=fi（T-甲基-cALL）（T-字段-赋值）Γe i：Tii∈ 0.. n我是0。m（e 1，...，en）：Tre：CreJ：Ci你好f=eJ：CJT0=μCmtype（C，m）= μT，μ，T1. Tn场（C）= C1f1. Cnfnf=fi（T-新）Γe i：Cii∈ 1.. nr =newC（e 1，.，en）：C场（C）=C1f1... Cnfn（T-BLOcK）Γ[Γ J]e i：Cii∈1.. n Γ[Γ J]e：TΓπ（C1x1= e 1... Cnxn= e ne）：T图五. 类型规则ΓJ =x1：C1... Xn：Cn类型判断具有形状Γe：T，意味着表达式e具有类型类型上下文中的T。子类型关系是关于诱导类型的自反传递关系通过胶囊C≤C≤可读C类表提供了关于方法的类型信息，由以下函数抽象建模：m型（C，m） 给予，为 每个 方法 M宣布 在 类 C，三重μT，μ0，μ1C1. 由它的返回类型、this的类型修饰符和参数类型组成。类型修改器μ0，.，μn是可读的或不可读的。当然，我们假设一个良好类型的类表，也就是说，方法体应该是良好类型的。对应的方法类型。形式上，如果mtype（C，m）=μ0，T1... 那就应该是mbody（C，m）=10x1. xn，e，和re：T，其中r = this：μ0C，x1：T1，.， xn：Tn.图5中给出了类型规则。规则（T-c APPLICATIONS）指出，如果表达式的所有自由变量都被用作可读变量，则表达式可以被类型化为胶囊。我们通过将所有类型修饰符设置为可读，为从Γ获得的类型上下文编写toReadable（Γ）。 规则（t-sub）是通常的98A. Capriccioli et al. /Electronic Notes in Theoretical Computer Science 322（2016）87包含. 其他规则大多是标准的，除了它们对预期的本文为了简单起见，我们倾向于省略这种特殊的语义。A. Capriccioli et al. /Electronic Notes in Theoretical Computer Science 322（2016）8799类型修改器的行为。 值得注意的是，在rule（T-FIELD -AccESS）中，类型修饰符它传播到田野。例如，可读对象的字段也是可读的。在规则（T-FIELD-ASSIGN）中，接收者和右边的表达式都不可读。类似地，在rule（T-NEW）中，赋值给field的值是不可读的，因为将引用保存为对象的field会引入别名。在规则（T-BLOcK）中，我们将Γ和ΓJ的级联写成Γ[ΓJ]，其中，对于在两个域中出现的变量，ΓJ优先。应该清楚如何扩展形式定义来处理在前面和下面的例子中使用的基本类型。简单地说，修饰符对这些类型没有意义，它们只是以标准的方式使用。例如，在规则（T-NEW）的前提中，构造函数参数的类型也可以是原始类型，而在规则（T-METH -cALL）中，方法接收者的类型不能是原始类型。现在我们举例说明规则（T-CAPPROXIMATE）是如何工作的. 考虑以下术语：Dz=新D（0）C X=（D） y= new D（z.f+1）new C（y，y））x内部块（x声明的右侧）可以是capsule类型的，因为自由变量z只作为可读变量使用（既没有修改也没有别名）。从形式上讲，我们可以应用规则（T-CAPPROXIMATION）。的确，块简化为（Dy = new D（1）Cx = newC（y，y）x），这是一个胶囊。作为反例，考虑以下项：D z=新D（0）Cx=（Dy=znewC（y，y））x在这里，内部块不能被类型化为capsule，因为z是内部别名。形式上，我们不能在块上应用（T-CAPTITUDE），因为我们应该用Γ =z：readableD来检查块的类型，而（T-BLOcK）需要D作为z的类型。实际上，块简化为（newC（z，z）），其不是胶囊。4结果我们使用缩写e−→fore−→eJ for someeJ，e：Tfore：T，► e代表some，T代表some。可靠性定理指出，良好类型的封闭表达式的约简不会卡住。定理4.1（无音）如果εe，且e −→εeJ，则要么eJ是一个值，要么e J−→。像往常一样，作为进步和主体归约定理的结果，得到了可靠性。请注意，由于我们的操作模型是一个纯演算，在证明中，我们不需要辅助结构（如内存）上的不变量定理4.2（进步）如果e是一个值，那么e是一个值，或者e −→。进展定理是作为扩展进展的直接推论而得到的100A. Capriccioli et al. /Electronic Notes in Theoretical Computer Science 322（2016）87►定理4.3（扩展的进展）如果Γe：T，则下列情况之一(i) e是一个值，其中FV（e）是随机数（r）(ii) e−→(iii) e= E [x. f]，x ∈HB（E），且x∈dom（Γ）(iv) e= E [x. m（xs）]，x ∈HB（E），且x∈dom（Γ）(v) e= E [x. f= y]，x ∈ HB（E），x ∈ dom（Γ）.定理4.4（主语归约）若Γe：T，且e−→e J，则Γ e J：T。除了稳健性，我们声明胶囊改性剂实际上确保了预期的行为。我们的非标准操作模型的一个很好的结果是，这可以很容易地形式化表达和证明，如下所示。非正式地说，胶囊是一个可到达的对象子图，其中节点不能从外部到达。在我们的模型中，可达对象子图直接由语言值表示，胶囊只是一个封闭的值。因此，胶囊类型的表达式实际上简化为胶囊的事实可以在下面的定理4.6中陈述令typectx（E）是从上下文E中提取的类型上下文，其平凡定义在附录中给出此外，为了在上下文中追踪表达式的归约，让我们假设在填充上下文的洞的结果E[e]中，我们仍然可以恢复子项e（例如，我们可以用[e]替换洞，方括号对于归约规则来说是无关紧要的引理4.5如果E[e]，typectx（E）e：T，且E[e]−→ EJ[eJ]，则EJ[eJ]，typectx（EJ）e J：T.定理4.6（Capsule）如果E[e]，typectx（E）e：capsuleC，且E[e]−→EJ [v]，则v是闭合的。证据 我们通过引理4.5知道typectx（EJ）v：capsuleC。 设ΓJ =typectx（EJ）. 通过对V的结构归纳。x空箱子。实际上，我们只能通过规则（t-c APPLIES）或（t-v AR）将胶囊类型分配给变量。然而，要应用规则（t-c APPLICABLE），我们应该导出toReadable（Γ J）x：C，这是不可能的，要应用规则（t-v AR），我们应该有Γ J（x）=capsule C，而类型上下文不分配capsule类型。（dvsv）我们只能通过规则（t-c APTITUDE）或（t-blo c K）将胶囊类型分配给块。如果我们应用了规则（T-CAPPROXIMATION），那么所有的自由变量都必须是可读的.块值中的自由变量只作为字段的值出现（根变量必须是绑定的），这是不可读的，因此块没有自由变量。如果我们已经应用了规则（t-blocK），则v也有一个胶囊，因此归纳命题是封闭的。 因此，（dvsv）等于v的同余规则（垃圾）。QA. Capriccioli et al. /Electronic Notes in Theoretical Computer Science 322（2016）871015结论我们已经提出了一个命令式演算，其中块构造，引入局部变量声明，也发挥了存储的作用时，这样的声明已被评估。通过这种方式，我们能够定义一个没有辅助数据结构的纯语义，其中别名属性可以直接在语法级别表达，从而允许更简单的推理。为了说明这一优点，让我们考虑图5中的类型规则（T-CAPPROACH）.这里我们想表达一个表达式e，一个程序的子项，如果它只能修改它的局部对象，那么它可以是类型化的胶囊相反，从程序的其他部分可以访问的对象只能作为可读对象使用。在我们的模型中，从程序的其他部分可到达的对象仅仅是由e中的自由变量表示的对象，其类型在规则的前提下确实需要可读，而局部对象是由e中声明的局部变量表示的对象。换句话说，只能从e访问的内存部分被编码在e本身中。在具有全局内存的传统模型中，为了表示同样的属性，我们应该首先输入内存位置，并在内存中添加不变量来证明主题归约。然后，我们应该要求只使用可读的位置，这些位置可以从程序的其他部分访问。 然而，某些位置只能从e在全球记忆中消失了。 具体来说，考虑以下示例：一 a= new A（...）B b=（C c= new C（）C. foo（））在传统的模型中，这个程序是通过首先在内存中添加两个新的位置来减少的，比如说ιa和ιc，然后分别用于替换变量a和c然后我们开始执行ic.foo（）。要键入这个表达式，我们将使用以下判断：;ιa：A，ιc：C ι c.foo（）：B。 正如你所看到的，没有关于如何在程序的其余部分使用ιc的信息。例如，IC可以在IA的可达图中。在我们的方法中，C c=new C（）保持不变，我们使用以下判断：a：A（Cc=newC（）c.foo（））：B。在这里，c只在块中使用的信息是从块作用域中隐含的。 我们的目标是以一种简单而抽象的方式形式化我们所考虑的执行模型为此，我们定义了一个项的同余，它可以用来减少一个否则会卡住的项。当然，实现应该检测何时以及如何应用同余规则，这与lambda演算的实现在必要时必须应用α转换的方式非常相似。别名属性可以在语法级别上表达，这一事实应该更容易允许将微积分的解释器实现为定理证明器。实际上，例如，Key theorem prover [1]使用了一种称为抽象对象创建的方法，其中并行更新（一种运行时表达式）被添加到语言中，并用于表示代码中的存储：所有对象创建和字段更新都被保存并由字段访问进行咨询Racket stepper [7]是一个程序执行可视化工具，它模拟了一个纯演算的语言，该语言具有以传统方式定义的可变绑定，依赖于专门伪造的运行时表达式。步进器精确地模拟了102A. Capriccioli et al. /Electronic Notes in Theoretical Computer Science 322（2016）87球拍的功能设置。在stepper中，绑定被提升到顶层;虽然它目前没有遍历可变绑定，但作者认为可以通过这种方式轻松扩展它。最近的发展，PLT Redex [9]，可以应用于像我们这样的纯微积分语言值是具有相互递归声明的块这一事实让人想起循环lambda演算，参见，例如，[4，3]。事实上，在这两种情况下，声明的变量都不会被它的值替换，就像标准的let一样，但是关联会被保留并在必要时使用。然而，在循环lambda演算中，有一个不同的目标（主要是提供一个有效的归约策略），并且，在技术方面，没有等同于读取/分配字段可能导致范围挤压的问题。Felleisen在未来的工作中，我们计划使用本文中提出的演算（的变体）作为基础来表达和正式验证对象图的不同属性，其中包括在关于所有权的广泛文献中提出的属性，例如，[6]的文件。一个更雄心勃勃的目标将是在这个模型之上研究霍尔逻辑的（一种形式）。我们相信，我们记忆表征的层次结构应该有助于局部推理，允许规范和证明只提到相关部分，类似于分离逻辑所实现的。我们还计划正式的状态和证明与传统的命令式模型的演算的等价性。确认我们衷心感谢匿名推荐人提供的非常有用的意见。特别是，一位裁判指出了与π演算中的范围挤压的类比，从而导致了同余和归约规则的更好表述。我们还要感谢Lindsay Groves，这项工作的初步版本的共同作者[17]，专注于教学应用。引用[1] 放大图片作者：Wolfgang Ahrendt，Frank S.de Boer和Immo Grabe。动态逻辑中的抽象对象创建在FM 2009：正式方法，第612[2] 保罗·塞尔吉奥· 阿尔梅达。 Ball oonty pes：控制数 据 类 型 中 的状态共享。 在MehmetAksit和SatoshiMatsuoka的编辑，ECOOP'97 -面 向对 象 编程 ， 计 算机 科 学 讲义 第 1241 卷 ， 第32-59页 。Springer，1997年。[3] Z. M. Ariola和Stefan Blom用letrec实现斜同余和lambda演算。Ann. Pure Appl. Logic，117（1-3）：95[4] 泽纳M. Ariola和Matthias Felleisen。按需调用lambda演算。你好，7（3）：265 -301，1997。[5] 大卫·克拉克和托拜厄斯·里格斯塔德外部的独特性是独一无二的。在ECOOPSpringer，2003年。A. Capriccioli et al. /Electronic Notes in Theoretical Computer Science 322（2016）87103[6] David G.克拉克约翰·波特和詹姆斯·诺布尔 用于灵活别名保护的所有权类型。 在ACM Symp