没有合适的资源?快使用搜索试试~ 我知道了~
可在www.sciencedirect.com在线获取理论计算机科学电子笔记298(2013)325-348www.elsevier.com/locate/entcs具有被动表达式的的自动机理论语义乌代S Reddy1英国伯明翰大学计算机科学学院摘要类Algol语言中的被动表达式表示读取状态但不修改的计算这种只读计算的需要出现在编程逻辑以及并发编程中。这也是Reynolds的Syntactic Control of Interference的核心。 尽管它的重要性和本质上的基本特征,捕捉语义模型中的被动概念已被证明是困难的。在本文中,我们提供了一个新的模型被动表达式使用自动机的理论框架最近提出的作者。 其中心思想是,程序的存储被视为自动机的抽象形式,具有其状态和状态转换的表示。 该框架使我们能够结合传统的基于状态的模型和最近的基于事件的模型的优势来合成新的“基于自动机的”模型。一旦建立了这个基本框架,关系参数性就完成了识别被动计算的工作关键词:理想代数,关系参数性,函子范畴,回归图,代数自动机理论。1介绍我们期望编程语言的指称语义模型为程序推理提供了严格的概念基础。在设计这样的模型时,人们面临的挑战是如何最好地捕捉程序员在理解计算时所拥有的直觉,并将它们纳入严格的理论框架。命令式编程语言的传统模型,可以追溯到Scott和Strachey的模型,是基于状态的。这些模型设想程序在经历状态的存储器上运行。命令被解释为从状态到状态的函数,分解出它们执行因此,这些模型可以被视为是外延的1电子邮件:u.s. bham.ac.uk1571-0661 © 2013 Elsevier B. V.在CC BY-NC-ND许可下开放访问。http://dx.doi.org/10.1016/j.entcs.2013.09.020326美国Reddy/Electronic Notes in Theoretical Computer Science 298(2013)325他们对待商店的态度。这些模型的例子包括Scott和Strachey的原始模型[42],Reynolds发起的函子范畴模型[30,38,45]及其使用关系参数的改进[26,27]。在最近的发展中,一种替代的基于事件的建模计算方法已经脱颖而出。这些模型避开了任何存储或状态的概念。它们将命令视为通过交互事件与各个存储变量交互的进程。基于过程的命令视图公开了所有内部状态操作细节,并使模型具有内涵。然而,总的来说,存储变量的数据抽象和信息隐藏方面在这些模型中被更直接地捕获。他们还能够对计算的内涵方面进行建模,例如“不可逆状态变化”的想法,从而产生强大的完全抽象结果。这种基于事件的模型的例子包括Milner和Hoare的过程演算模型[14,21],Brookes的跟踪模型[ 7 ],作者的基于对象的外延模型和内涵模型之间的差异在关于程序等价的推理中变得明显,例如:gv(x)=<$(x:=x+ 1;x:=x+ 1)<$(x:=x+2)(1)其中gv(x)表示x是通过变量分配获得的“好变量”的条件外延模型满足这样的等价性,因为它们捕捉到命令对状态的净效应,而内涵模型则不然。[2]然而,在可拓模型中,数据抽象(局部变量)和状态变化的不可逆性的处理是有问题的。为了结合基于状态和基于事件的模型的优点,我们最近提出了一种新的方法,使用存储的自动机理论视图[35,36]。存储被看作是一个自动机的状态以及状态转换的显式表示。状态的使用允许对命令进行扩展处理,并且状态转换的使用捕获了基于事件的模型中可用的建模的某些方面我们证明了在纯基于状态的模型中无法验证的三阶类型的几个程序等价物在此设置中是有效的。在本文中,我们根据Reynolds的原始理想化Algol [ 38 ],通过对被动表达式进行建模,进一步发展了自动机理论模型被动表达式读取存储变量以计算值,但它们不改变存储。典型的编程语言出于实际原因允许在表达式中使用副作用,让程序员自行判断使用它们。3然而,被动表达式是程序推理的一个组成部分例如,在霍尔逻辑中,表达式可以嵌入逻辑断言中,[2]人们可能会惊讶地发现,内涵模型,例如,游戏模型,虽然是完全抽象的,但不能“延伸”。解释是,完全抽象只能保证满足无条件等价,这似乎不足以捕捉状态操纵的外延。 等式(1)是有条件的。3表达式的求值顺序通常是未指定或未指定的,因此,不受控制地使用表达式边项在任何情况下都不是一个实际的命题。美国Reddy/Electronic Notes in Theoretical Computer Science 298(2013)325327任何一个侧面的影响都可能导致一个完全不连贯的形式主义。在并发编程中,被动表达式是跨进程共享资源的重要工具各种程序推理系统,所有权类型系统等都包含了对“只读”或“不可变”变量的显式注释特别是,使用“部分每个任务”是一种先进的机制,以捕获存储的被动使用,目前是一个在外延模型中建模被动性是一个重大挑战,因为被动性似乎是一种内涵现象:计算为了产生结果而在内部做的事情。如果我们把建模表达式看作是状态→值类型的扩展函数,我们就无法处理这样的计算可能会做什么。它可能会在内部计算一个新的状态(这意味着计算方面的状态更改),并在新状态中进行进一步的计算以交付结果。新的状态最终会被丢弃,并且表达式会有一个“暂时的副作用”。这种现象可以通过以下形式的“snap back”组合子在语法上doC结果 E这意味着在语义模型中存在这样的快速返回组合子打破了直观的程序等价性。例如,考虑等价性:4if(derefx= 0)thenf(derefx)else 2if(derefx= 0)thenf(0)else2(二)其中f是一个接受表达式参数的函数过程由于f只在x为0的情况下被调用,因此将它作为参数0而不是(derefx)应该会得到等效的结果。然而,在包含快回操作符的语义模型中,有函数f打破了这种推理,例如:f = λe。dox:=x+1结果e利用该函数f,(2)的LHS评估为1,而RHS评估为至0除了Tennent的模型[ 45 ]之外,文献中几乎所有的延伸模型我们通过将商店视为自动机来解决这个困难,它具有其状态QX及其允许的状态变换TX的显式表示。然后表达式类型可以被认为是由自动机的两个组件EXP(QX,TX)=[QX→值]4命令式编程语言通常涉及一种隐式强制,允许存储变量将被视为读取其内容的表达式。为了说明的清晰,我们将这种强制表示为“deref”。还记得理想化的Algol是一个按名称调用的类型化lambda演算。因此,参数在f(deref x)中按名称传递。328美国Reddy/Electronic Notes in Theoretical Computer Science 298(2013)325所有计算都是参数化的[10,27,32,40],即,它们由以下形式的参数多态族解释:QX,TX. F(QX,TX)→ E XP(QX,TX)其中F(QX,TX)表示自由标识符的语义类型。由于结果类型EXP(QX,TX)独立于TX分量,参数性表示无论使用什么类型的T X(受某些约束),族都应该表现为特别地,如果TX被替换为状态变换的平凡集合,例如仅具有恒等变换及其可能的发散近似的集合,则它应该产生相同的结果。因此,表达式计算不能引起任何状态变化,甚至不能引起暂时的变化。这样,被动性就以一种直观上令人满意的形式被捕捉到了。这个模型的定义建立在我们过去工作中的两个技术创新之上(与B. P.Dunphy)。第一个是[10]中提出的关系参数性的范畴公理化。由于整体结构是由Reynolds [38]开创的范畴论可能世界模型的结构,因此需要对参数性进行O’Hearn and Tennent [然而,他们的模型没有必要的公理,并且在他们的模型中存在快速恢复运算符。我们的公理化是基于范畴论[13,16]中研究得很好的纤维化概念,利用它在[10]中得到了强表示结果。它在这里的使用进一步证明了它的力量。第二个创新是在[35,36]中提出的商店的自动机理论建模。回想起来,悬挂物的这种观点已经隐含在雷诺然而,他的模型背后的自动机理论直觉没有得到认可,随后在所有关于函子范畴模型的进一步工作中被忽视。我们的模型似乎是建立在雷诺兹思想基础上的第一个工作。在目前的工作中,我们以一种重要的方式推广了自动机理论模型,这与Tennent在做这样的概括时,很容易走得太远,即,使模型如此内涵化,以致等价性(1)失效。事实上,Tennent(与预期相反,等价性不能在规范逻辑中导出。)本文旨在实现内涵效应和外延效应的微妙平衡。结果本文的主要贡献是提供了一个理想化大陵五的指称模型,令人满意的模型被动,而被扩展。特别是,这意味着被动表达没有副作用,甚至没有临时的。在本文的主体中,我们对一个没有分歧的语言这样做,但以这样一种方式对待它,它推广到分歧。分歧的问题,然后简要地提到在第二节。五、无分歧的治疗也是新颖的,美国Reddy/Electronic Notes in Theoretical Computer Science 298(2013)325329→JΣ→Σ这是第一个被动的模型,能够处理一种没有分歧的语言。所有以前的模型[1,34,45]都依赖于发散的存在来建模无源然而,直觉上,被动性与分歧问题无关。我们的治疗方法能够将这两个问题分开。我们可以用一阶类型获得的准确度来解释这种贡献[25,34]。在没有分歧的情况下:• com com类型的态射应该同构于自然数。 它们都可以用λc形式的闭项表示。其中Cn表示n重顺序组合c;. ; c. [36]的模型具有这种性质。• 类型com→exp[δ]的态射应该是常数函数。它们可以用λc形式的闭项来表示。E表示封闭表达式项E。本模型具有这种性质。2语义框架本文中使用的语义框架是Reynolds [38]倡导的范畴理论可能世界模型。这意味着编程语言的类型被解释为由“store”参数化的类型构造函数形 例如,EXP(X)表示表达式的含义适用于形状为X的存储器,COM(X)表示适用于X形悬挂物等的命令含义的集合。商店形状必须形成一个范畴,其中态射f:X→Y表示存储Y可以被视为X的“未来世界”的方式(通常通过分配额外的事实上,将这样一个态射看作是一个反向的“函数”(f:Y → X)可能会有所帮助,它类型函子自然必须将这种态射映射到函数。 例如,EXP(f:X→Y)表示一个函数,允许我们将X类型存储的表达式转换为Y类型存储,这是可能的,因为X类型存储可以从Y型商店。除了态射,我们考虑商店之间的抽象逻辑关系,用于制定关系参数的一致性条件对于每一对存储器X和XJ,我们有一个逻辑关系R:XParticipateXJ的概念和一个保持这种关系的态射的概念,它被图解地写为FX> Yˆˆ俄.西VVXJf> YJ(三)在文本上是fR SfJ。(本文的注释取决于以下事实:我们在本文中考虑的结构是相关的,即,给定f,FJ,R和S,最多有一个上述形状的正方形因此,R→S可以看作是hom-setsX→Y和XJ→YJ之间的正规集合论关系。的类型330美国Reddy/Electronic Notes in Theoretical Computer Science 298(2013)325ΣΣa,aJ.aR aJ=f(a)S fJ(aJ). 响应图集也满足参数图的附加要求。函子还将存储之间的这种逻辑关系映射到值之间的关系,并且EXP(f)EXP(X)>EXP(Y)ˆEXP(R)vEXP(fJ)ˆEXP(S)vEXP(XJ)>EXP(YJ)形式上,这四个组成部分:商店形状,商店形状之间的态射,商店形状之间的逻辑关系以及它们之间的正方形,形成了一个类别的反射图。此外,它们满足[10]中列出的附加公理以形成参数图。描述该结构的正式定义见附录。除了将在本节的剩余部分中描述的商店形状的自反图之外,我们还使用自反图Set,其对象和态射是集合和函数,Reader幺半群我们选择将商店建模为自动机的抽象形式,类似于代数自动机理论[11,15]中研究的自动机。每个这样的自动机有:5• 一组状态QX,• 允许的状态变换TX<$[QX→ QX]的幺半群(包含单位变换,写作1X,并且在序列复合a·b下闭合),以及• 一个操作read X:(QX→ TX)→ TX,定义为read Xp = λx。p xx。这种形式的结构X=(QX,TX,readX)称为读者幺半群。称它为雷诺兹幺半群也是合适的。读X操作是由Reynolds [38]提出的,他称之为要了解它的动机,请考虑解释形式为ifpthenc1elsec2的命令。该命令读取状态以计算表达式p,并根据结果执行c1或c2,这两者都表示允许的转换。因此,if-then-else运算符将依赖于状态的(QX→ TX)类型的状态变换转换为TX类型的状态变换。它可以使用read X组合子定义为cond Xe a1a2= read X(λx。读作X(es)a1a2)。如果一个给定的自动机(QX,TX)没有读X操作,则可以向TX添加额外的变换以获得读幺半群。我们称之为原始自动机的“读闭包”。[5]为便于阐述,我们将忽略本文正文中的分歧问题但见SEC。5为发散所需的扩展美国Reddy/Electronic Notes in Theoretical Computer Science 298(2013)325331ΣΣΣΣ作为读取器幺半群的示例,考虑具有QZ= IntTZ={a:Int → Int |a(z)≥ z}这个存储包含一个单一的整数变量,并允许它在计算过程中增加(但不能减少)。“被动”存储W具有某个状态集,但只有不做任何事情的对于每个存储X,存在X的对应被动存储,表示为X0,其具有与X的状态集相同的状态集和状态变换的平凡集TX={ 1X}。[35,36,38]中使用的自动机称为Reynolds变换幺半群,具有额外的结构元素:• αX型幺半群作用:TX→(QX→ QX),它代表了一种在状态上“运行”变换的方式在这里,我们放弃这个操作,获得结构以及相应的态射和逻辑关系的一般性。一般化的理由是,命令式程序中的状态是“抽象的”,只能通过其他命令检查,而不能通过外部接口检查通过要求逻辑关系只保留读操作,而不是幺半群作用,我们得到了更多的关系,这给出了一个更强的参数性准则。回想一下在引言中给出的直观论证,其中我们用一个平凡的分量替换TX的一个状态变换分量。请注意,新的转换将在状态上与我们替换的状态不同因此,这种推广对于无源性建模至关重要读者幺半群R:XParticipateXJ的逻辑关系是一对(Rq,Rt),其中• Rq:QXParticipateQX′是集合的正规关系,并且• Rt:TXParticipateTX′是么半群关系(与恒等变换和复合相容),使得读X(Rq→Rt)→Rt读X′。读者么半群X的恒等式逻辑关系为IX=(ΔQX,ΔTX),由状态集和变换的对角关系组成.读者幺半群f:X→Y的态射表示将“当前世界”X扩展到“未来世界”Y的一种方式• fq:QY→ QX是满射函数(注意方向的反转),并且• ft:TX→TY是一个单射幺半群态射,• 满足ft(read X(p))= read Y(ft<$p <$fq)。读的条件也可以用关系符号写为read X<$fq→ft<$$> → <$f t<$read Y,其中符号<$− <$表示函数的图形。 fq和ft的双向信息流类似于内在模型[1,34]中的信息流,可以通过将态射f看作从Y型存储中以相反方向提取X型存储来理解。要进行这种提取,应该可以将所有Y类型的状态解释为X类型的状态,332美国Reddy/Electronic Notes in Theoretical Computer Science 298(2013)325ΣΣ则a ∈ TY,AJ∈ TY′. a Rt aJ=ft(a)ftJ(aJ)S由函数fq完成。另一方面,存储库的转换由存储库所嵌入的计算环境调用。如果环境请求对X类型存储进行转换,则提取必须将其模拟为Y类型存储上的转换ft(a)一个读者幺半群的正方形被定义为一对关系保持正方形(分别用于集合和幺半群):FX> Y东凤企业股份有限公司QY>QXftX>YˆRvfJˆSvˆSQvfqJˆRqvˆ ˆRtStvfJvXJ> YJQY′>QX′TX′>TY′请注意,右侧的方块(在Set和Mon中)具有其标准含义:其中,y∈QY,YJ∈QY′. y<$$>S<$q<$$>yJ=<$fq(y)<$$>R<$q <$fqJ(yJ)这些数据构成了Reynolds么半群的自反图范畴RM参数图所谓的parametricity graph是一个自相关图,它是:• 关系,即,最多有一个给定形状的正方形,• 用精选的卵裂,• 满足同一性条件,即,当fIA→IBg时,我们有f=g。“关系”条件本质上简化了理论。“同一性条件”赋予同一性逻辑关系以语义。The “fibred” condition is a categorical (完整定义见附录nitions.)给定f,fJ和S,如下面左边的正方形所示,必须有一个原像<$f,fJ<$S,它可以以一种通用的方式填充虚线:FA> B.FA> B.J.没关系拉 吉f,f...vSfJvRv. 我操我操RFJAJ> BJAJ> BJ这种形式的正方形称为直角正方形。平方的对偶形式,即余平方,给出了“直接图像”f,f,j。R. 自相关图集具有原像和直接像,由下式给出:不..vSt美国Reddy/Electronic Notes in Theoretical Computer Science 298(2013)325333我操我操! R ={(f(x),f J(xJ))|XxJ}f,fj|f(x)<$S<$$>fJ(<$xJ)}R334美国Reddy/Electronic Notes in Theoretical Computer Science 298(2013)325Jf,f.Q.jCOM(X)=TXEXPδ(X)= [QX→[[δ]]COM(R)=RtEXPδ(R)= [Rq→Δ[[δ]]VARδ(X)=EXPδ(X)×[δ]]→COM(X)]VARδ(R)=EXPδ(R)×[Δ[[δ]]→COM(R)](F×G)(X)=F(X)×G(X)(F×G)(R)=F(R)×G(R)(F<$G)(X)=h: Z<$ X[F(Z)→G(Z)](F<$G)(R)=S<$ R[F(S)→G(S)]Fig. 1. 理想化大陵五类型与O'Hearn和Tennent [ 27 ]所用的图不同,自回归图RM它满足恒等式条件,因为它是通过将满足恒等式条件的Set和Mon放在一起得到的。它是用精选的卵裂来繁殖的:f,fjSq,ft,ftjSt)这特别意味着存在一个“包容映射”,它将每个态射f:X → Y映射到一个逻辑关系f:X Participate Y,由f =(f q ×,f t)给出,这样态图解:东凤企业股份有限公司Q. XQYftT. X>TY.ˆqq!Q..vQX′fJˆSQvQY′.ˆTTT。.vTX′ˆStv>ftJ除了这些事实,我们注意到RM的顶点范畴满足右Ore条件[17],允许我们将其视为原子Grothendieck站点。RM一般不进行协方差计算,但它确实有一些有用的协方差平方,这些平方将在下一节中使用类型函子为了解释理想大陵五的类型,我们使用从RM到Set的适当类型的函子,如图1所示。这形式化的直觉在Introduction中提到的类型被解释为一个自反图-函子(RG-函子)F:G→H在自反图之间映射自反图的所有四个组成部分(对象、态射、逻辑关系和平方),保持它们的结构。PG-函子是一个自反图-函子,它也保留了笛卡尔平方,特别是选择的分裂:F(Ff,fjS)=Ff,FfJS(FS)T′Y美国Reddy/Electronic Notes in Theoretical Computer Science 298(2013)325335我们还坚持认为,函子用于解释理想化大陵保持所有的co-carnival平方存在于RM。这类PG-函子RM→集的范畴记为P(RM),因为“RM上的P(RM)中的态射是保持所有态射(自然性)和所有关系(参数性)的变换。然而,在参数性图的条件下,参数性意味着自然性[10,32]。所以,我们简单地称之为参数变换。接下来,我们限制到RM上的(原子)层[17,19]。 直觉上,层的一个重要特征是,在态射f:X→Y上的函子作用Ff不会丢失任何信息。给定一个元素Ff(a)∈FY,我们可以从它恢复a∈FX定义如下:• 给定一个态射f:X→Y,一对态射(g1,g2):(Y,Y)→(Z,Z)使得f;g1=f;g2称为• 一个元素b∈FY称为f的匹配元素,如果对所有的匹配点(g1,g2),我们有Fg1(b)=Fg2(b).• P(RM)中的一个预层F满足f:X→Y的层公理,如果对于所有匹配元素b∈FY,存在唯一的a∈FX使得Ff(a)=b。• 一个预层F是一个层,如果它满足所有态射的层公理。很容易看出,每个图像Ff(a)∈FY都是匹配元素。层公理说这些是唯一匹配的元素。这是层的标准定义,有一个更基本的特征:引理2.1[17,2.1.11(h)]P(C)中F中的预层是原子层,对于C中的每个f:X→Y,• Ff是一个单射函数。• Ff的像就是f的匹配元素的集合。P(RM)中层的全子范畴记为S(RM)。从预层到层的迁移是由构造有孔虫自同构图的指数所必需的。 它们在国家语义学中的使用是由O'Hearn和Stark [23,43]首先提出的它们也是名词集合[31]框架的基础,可能还有分离逻辑。定理2.2若C是满足右Ore条件的参数图,则C上保持余Carnival平方的原子层范畴S(C)是Carnival闭的。乘积是逐点给出的:(F×G)(X)=F(X)×G(X)和(F×G)(R)=F(R)×G(R)。指数在预层类别中给出: (FG)(X)=h:Z←X[F(Z)→G(Z)],说明,参数极限由以下形式nth∈[F(Z)→G(Z)]nh: X→ Z336美国Reddy/Electronic Notes in Theoretical Computer Science 298(2013)325Σ Σ ΣΣΣΣΣΣFR本身,即, DFRD.在某种意义上,h IX→S hJthF(S)→G(S)th′由于F和G是PG-函子,这样的族自动是自然的[10]。关系(F →G)(R)=<$S <$R[F(S)→G(S)]涉及两个族X→Z,X′→Z′i,对于所有逻辑关系S:ZParticipZ J和适当的类型:h<$R→S<$hJ=<$th<$F(S)→G(S)<$tJh′3建模被动性直观地说,如果计算读取状态但不执行状态更改,则计算是被动的。由于我们的存储X=(QX,TX)具有状态集合分量和状态转换分量,这意味着被动计算应该仅依赖于QX分量并且独立于TX分量。我们使用关系参数化形式化这些概念。称一个逻辑关系R:XParticipXJ为一个Transformer关系,如果它的状态集分量是对角关系:Rq= ΔQX。在逻辑关系的转换组件上没有约束(除了由读者幺半群强加的那些定义3.1给定S(RM)中的PG-函子F和存储X,如果对于所有Transformer关系R:XParticipX,d与这符合我们的直觉。由于Transformer关系保持世界的状态集组件固定,但允许转换组件变化,如果一个值在所有这些变化下都与它自身相关,它必须独立于变换分量。很容易看出,所有的值e∈EXP(X)都是被动的,正如人们所期望的那样。另一方面,在C OM(X)中,值a是被动的,当且仅当Rta表示所有的Transformer关系R。 这仅在a= 1X时才可能,无所事事的状态转换(When我们考虑发散,被动命令值包括1X的所有近似值。)PG-函子本身可以被认为是被动函子,如果它的所有值都是被动的(对于所有存储X)。我们对所有的商店X都要求这一点。定义3.2 PG函子F被称为无源的,如果对于所有的Transformer关系R:XParticipX,FR = Δ FX。注意EXP是被动函子,而COM不是。然而,COM有一个被动子函子,记为X.C.OM,它在每个外挂物形状X处包含1个X。我们研究如何刻画被动子函子。无源性单态回想一下,对于每个存储X,存在对应的被动存储X0,其具有与X相同的状态集,但仅具有平凡状态变换TX0={ 1X}。美国Reddy/Electronic Notes in Theoretical Computer Science 298(2013)32533700由于X0不允许状态变化,我们期望所有d∈FX0的值都是被动的(对于所有PG-函子F)。存在一个被动单态映射pX:X0>X,它由状态集上的恒等式和状态变换的注入TX0<$→TX给出根据引理2.1,S(RM)中的PG-函子将其发送到注入FpX,使F X0成为FX的子对象。在假设F除了保留余平方外还保留余平方的情况下,我们可以证明FX的所有被动值都包含在FX0在FpX下的图像中。引理3.3如果F是S(RM)中的PG-函子且保持余平方,则值d∈FX是被动的当且仅当存在d0∈FX0使得FpX(d0)= d。The有下面左边的正方形:XpX> XFX0FpX>FXˆˆIX0RvpXvˆIFX0 vˆFRF pXvX0> X FX0> FX当PG函子F将其映射到右边的正方形时,图像中F pX:FX0→FX下的所有值都通过FR与自身相关。 因此,所有这些价值观都是被动的。对于“if”方向,我们使用下图左侧所示的co-carbohydrate平方:XpX> X .F X0F pX> FX.- 是的ˆˆI. QI.ˆ. FQX 0。 XF X 0.Xvp.vvFp.vX0X> X外汇0X> FX其中QX:XParticipX是givenbyy(QX)q=ΔQX 且(QX)t={(1X,1X)}。如果F保持协平方,则这意味着FX的所有被动值都包含在Fp X的图像内。无源性回缩关系在Tennent [24,45]所使用的世界范畴中,被动性单态具有收缩rX:X→X0使得pX;rX= idX,使得逆合成αX=rX;pX是幂等元。 定义函子F的被动值为满足FαX(d)=d的值。相反,我们的世界范畴RM没有这样的收缩,因为它们的状态变换分量τrX需要将TX中的所有变换发送到1X∈ TX0,因此不能是单射的。然而,我们可以通过逻辑关系模拟撤回的效果 被动收缩关系<$X:XParticipX由(<$X)q = Δ QX和(<$X)t ={(a,1 X)|a∈ TX}。这个关系满足一个重要的性质:338美国Reddy/Electronic Notes in Theoretical Computer Science 298(2013)325ΣΣ引理3.4对于所有的Algol型函子F,关系F <$X:FXParticipFX有,作为它的域,整个集合FX,和,作为它的范围,FX的被动子集。被动子函子如果F是S(RM)中的PG-函子,则S(RM)中存在被动PG-函子<$F,定义为(F)X=FpX(F)f=Ff对(F)X的限制这个定义基于以下性质。引理3.5若F是S(RM)中的PG-函子且f:X→Y是RM然后Ff:FX → FY将FX中的被动值发 送 到FY中的被动值。使用引理3.4,我们可以证明以下结果,建立被动函子形成可以被称为定理3.6如果F和P是S(RM)中的Algol函子,其中P是被动的,则存在从参数变换F→P到参数变换<$F→ P的自然注入。Par(F,P)>Par(F,P)证据如果t:F→P是一个参数变换,那么对应的t0:<$F→P有分量(t0)X,它只是分量tX对被动值的限制。我们证明了t0唯一地决定t.由于t保留了所有的逻辑关系,特别是Transformer关系<$X:XParticipX,我们有一个关系保持方(在Set中):FXtX 公司简介ˆFX vtXˆPXvFX> PX因为ΔPX是一个Transformer关系,所以P ΔPX= ΔPX。所以,上面的正方形意味着:d0∈FX. DFXd0=tX(d)=tX(d0)由于F <$X的值域仅由被动值组成(根据引理3.4),这意味着tX由它对被动值的作用唯一确定。Q使用这个结果,我们可以对“SCI Revisited”和“ILC Revisited”类型系统中使用的“Passification”或“Co-promotion”规则给出语义解释Π | i:θ,ΓM:φθ,i:θ| ΓM:φ通过在这里,自由标识符的左边“|“在“被动区”,右边的在“主动区”。类型规则说,当在被动类型的术语M中使用时,自由标识符可以从主动区域移动到被动区域这正是自然注入Par(F,P)>Par(F,P)的结果。一美国Reddy/Electronic Notes in Theoretical Computer Science 298(2013)325339[[θ]](X)这样,所有的关系都被保留,即,对于任何关系R:XParticipateXJ,我们需要这样的规则来适应Tennent [ 46 ]提出的定理3.7被动子函子算子S(RM)又是函子S(RM)。它具有以下同构和嵌入:对于被动函子P,COM=1(F×G)F P>F P对于被动函子 P证据如果t:F→G是一个参数变换,那么t:F→G就是作用于被动值的t的约束t0事实上,第一个同构是一个等式P=P,并且从PX的被动子集是整个PX对于COM,1X是COM(X)中唯一的被动值。所以,XAM(X)是一个单例。对于F×G,注意(F×G)pX=F pX×GpX:F X0×GX0→FX×GX。所以,(d,e)在(F×G)pX的范围内,i,d在FpX的范围内,e在GpX的范围内。 最后一个嵌入由定义(FP)(X)得出=[2019 - 04 - 19 00:00:00][2019 - 04 - 19 00:00:00][2019 - 04 - 19 00:00][2019 - 01:00][2019 - 01:00]Q4应用在这一节中,我们将考察在前面几节中发展的理论的结果。理想化大陵五的解释Idealized Algol [38]是一个简单类型的lambda演算(带有按名称调用的参数传递),具有支持命令式计算的基本类型对exp[δ]、com、var[δ]、θ1×θ2和θ1→θ2类型的解释是S(RM)中的PG-函子,如图1所示。为了可读性,我们使用了符号,例如[exp[δ]]的EXPδ等。用typing来解释术语Mx1:θ1,.,xn:θnM:θ是类型为[[M]]:(xi[[θi]])→[[θ]]这意味着,对于每个商店形状X,[[M]]X是类型为(xi[[θi]](X))的函数→有[M]]X(xi[[θi]](R))→[[θ]](R)[[M]]X′。理想化大陵五是340美国Reddy/Electronic Notes in Theoretical Computer Science 298(2013)325XXVXX等式:EXPδ×EXPδ→EXPbool等于X(e1,e2)=λs.e1( s)= e2( s)condE:EXPbool× EXPδ× EXPδ→ EXPδcondE(e,e1,e2)= λs. e( s)→ e1( s); e2( s)跳过:1→COM序列:COM×COM→COM条件C:EXPbool×COM×COM→COM对于:EXPint×COM→COMskipX()= 1XseqX(a,b)= a· bcondC(e,a,b)= readXλs. e( s)→ a; b对于X(e,a)=读作X λs。ae(s)deref:VARδ→EXPδderefX(d,a)= d赋值:VARδ×EXPδ→COMnewvar:(VARδCOM)→COMassignX((d,a),e)= readXλs. a( e( s))new v a rX(p)=(λs. (s,initδ))·p[1](λ var↑XsV)·(λ(s,n). 个)其中V =([δ]],T([[δ]]))mkvar=(λn. n,λk。λn。(k)图二. 理想大代数简单类型的lambda演算,这种解释是标准的[10,27]。[[x]]X(u)=u(x)[[λx:θ。M]] X(u)= Λ h:Z ← X. λd:[[θ]](Z)。[[M]] Z(u↑Z [x <$→ d])[[MN]]X(u)=[[M]]X(u)[idX:X→X]([[N]]X(u))参数u可以被认为是为自由标识符提供值的类型θ→θJ的lambda抽象的意义在([[θ]]<$[[θJ]])(X)中,它由形式为<$th<$h:Z <$X的族组成。在这里,我们使用从多态lambda演算中借用的符号注意抽象的主体λx:θ。M在未来世界Z中被解释,环境u被我们用速记法符号a↑Z对于value[θ]](f)(a),其中f:X→Z是在而θ是a的类型。Z中的参数性对于捕捉[M]]Z不直接访问未来世界的任何信息这一事实至关重要。在函数应用术语的解释中,我们再次使用多态lambda演算符号来传递h参数,即idX:X→X。命令式操作可以定义为一组原始常量,图2中显示了其中的一个示例。他们的解释应该大多是不言自明的。我们使用符号p→v1;v2来表示语义元语言中的条件表达式。注意,Reynolds变量表示为成对的操作:表达式类型的操作取消引用变量,而“接受器”在给定值时将其存储在变量中。The “newvar”prim- itive allocates a new variable in the context of a store 它定义了一个新的存储器V,其状态集[δ]和所有状态变换都在其上,记为T([δ]])。“mkvar”结构在这个存储上提供了解引用-接受器对。为了将商店V添加到现有商店X,我们对商店使用张量积,美国Reddy/Electronic Notes in Theoretical Computer Science 298(2013)325341ΣΣΣΣ.- 是 的Σ* [36]第30段。存储X * Y被定义为读者幺半群:QX Y=Q X× Q YTX Y ={a×b}的读闭包|a∈ TX,b∈ TY}该存储器具有明显的注入11:X→X * Y和12:Y→X * Y。示例首先,让我们注意到,快速返回组合子(doCresultE)被排除了。为了解释它,我们需要一个参数变换的形式:do:COM×EXP→EXPdo X(a,e)= λs. e(a(s))我们可以看到它不是参数化的。例如,保持关系参与者X:X需要C OM(X)×E XP(X)doX> E XP(X)ˆ ˆ ˆCOM(X)vEXP(X)v做XEXP(X)vCOM(X)×EXP(X)>EXP(X)其中,对于a∈COm(X),e∈EXP(X)和状态s∈Q X,ays e(a(s))= e(1 <$X (s ) )。e(a(s))=e(s)。例如,如果X至少有两个状态,比如{0, 1},a可能通过发送0到1来引起状态改变,而e返回当前状态的整数,则违反了该条件考虑引言中所述的等效性:if(derefx= 0)thenf(derefx)else 2如果(derefx= 0)thenf(0)else2这要求,对于所有世界X,值(e,a)∈EXP)(X):VAR(X)和f∈(EXP)λs。 (e s)= 0 −→ f [id X] e s; 2 = λs。 (e s)= 0 −→ f [id X] 0 s; 2考虑由下式给出的关系:Rq={(s,s)|es= 0}Rt={(1 X,1 X)}由于eEXP(R)0,我们必须有,对于所有状态s,使得es= 0,(Note的COM(X)1X和eEXP(X)e.)由于1X(s)=s,我们需要342美国Reddy/Electronic Notes in Theoretical Computer Science 298(2013)325f[idX]es ΔIntf [idX] 0s注意到ΔInt只不过是
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- BSC绩效考核指标汇总 (2).docx
- BSC资料.pdf
- BSC绩效考核指标汇总 (3).pdf
- C5000W常见问题解决方案.docx
- BSC概念 (2).pdf
- ESP8266智能家居.docx
- ESP8266智能家居.pdf
- BSC概念 HR猫猫.docx
- C5000W常见问题解决方案.pdf
- BSC模板:关键绩效指标示例(财务、客户、内部运营、学习成长四个方面).docx
- BSC概念.docx
- BSC模板:关键绩效指标示例(财务、客户、内部运营、学习成长四个方面).pdf
- BSC概念.pdf
- 各种智能算法的总结汇总.docx
- BSC概念 HR猫猫.pdf
- bsc概念hr猫猫.pdf
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功