构建操作语义：简化与计算

理论计算机科学电子笔记172（2007）479-497www.elsevier.com/locate/entcs构建操作语义：简化与计算莫吉DISIUniv. di Genova热那亚，意大利摘要本文描述了一种由术语和计算规则两层组成的语言，其操作语义是根据两种关系给出的：简化和计算。简化是由项的连续重写计算是由化学反应引起的，就像Join演算中的那些该语言可以作为元语言来定义其他语言的操作语义这可以通过定义几种演算（代表理想化的编程语言）的编码来证明。关键词：操作语义，一致性重写，多集重写。介绍Monad是一种用于构建编程语言的指称语义的工具，它通过选择Monad来识别计算结果的语义（参见[15]）。有没有类似的方法来构造操作语义，也就是将计算结果与其他编程语言特性分开？Plotkin然而，它的普遍性使其难以确定共同的模式和变化点。我们提出了一种更规范的操作语义方法，类似的方法是归约语义[25]和化学抽象机[1]。我们提出的构建操作语义的建议与构建指称语义的一元方法有一些相似之处（实际上，它被认为是一种为一元元语言提供操作语义的方法[16]）。更具体地说，有两层：1电子邮件：moggi@disi.unige.it1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.016480E. Moggi/Electronic Notes in Theoretical Computer Science 172（2007）479• 第一种称为简化，它相当于相应的项重写;• 第二种（模拟计算效应）称为计算，主要基于多集重写。更具体地说，我们的建议也可以被描述为Kahl的模式匹配演算[ 13 ]和Fournet和Gonthier [ 7，8 ]的Join演算的反应性化学抽象机的组合本文件的结构如下：• 第1节回顾了指称语义学的一元方法的本质，主要是为了建立与我们在操作环境中所做的一些类比（见第4节）。• 第2节解释了我们如何在本文的上下文中指定操作语义，即通过转换系统，为这种选择提供了一些理由，并提到了已知的限制。• 第3节（本文的主要技术贡献）描述了我们在两个层面上构建操作语义的方法：简化和计算。• 第4节通过描述几种演算（代表理想化的编程语言）的编码来演示我们方法的通用性。致谢。我要感谢Amr Sabry对提案初稿的讨论，以及Barry Jay对完整草案的评论1简而言之，一元方法程序设计语言的指称语义在于以某种合适的数学结构对语言进行像塔斯基的语义学一样在不失一般性的情况下，我们可以假设用于解释的数学结构形成一个类别（具有适当的属性），并且程序片段由态射解释。通常，相同的类别C用于不同编程语言的指称语义。因此，我们可以引入一个元语言ML，并在C中给出一个解释，然后用ML中PL的翻译（-）PL来替换C中PL的解释[-]]PL。元语言为C提供了一种语言抽象，它隐藏了不相关的细节，同时允许通过将翻译（-）PL与C中ML的解释组合来恢复解释[[-]]PL。在指称语义的背景下，[15]提出了monad作为一种建模计算类型的方法：. . . 为了解释范畴C中的程序设计语言，我们将值的对象A（类型A）与计算的对象MA（类型A）区分开来，并将MA的元素作为程序（类型A）的表示。特别地，我们将类型A与值对象（类型A）标识，并通过将一元类型构造函数M应用于A来获得计算对象（类型A）。我们E. Moggi/Electronic Notes in Theoretical Computer Science 172（2007）479481L称M为计算的概念，因为它抽象了计算可能产生的值的类型。在元语言层面上，这一观察的最重要的结果是ML的扩展，它为计算的概念提供了一个抽象的数据类型构造器。由此产生的一元元语言MLM在C中具有解释，这扩展了ML的解释，并且在选择一元M时被参数化。此外，MLM可以用作翻译编程语言的目标，通常会导致更简单，更容易理解的翻译。2、什么样的操作语义？最广泛接受的描述操作语义的方法是Plotkin在这种方法中，一个操作SE-mantics是由推理规则推导操作判断。 操作判断没有规定的格式（实际上是通过例子来描述的），但它们应该包括一些语法成分（对应于程序片段），推理规则应该包括这些语法成分的一些模式匹配和转换然而，在大多数情况下，人们可以采用更具体的操作判断格式：s==sJLJ或s==s。由此产生的操作语义相当于转移系统（TS）或标记转移系统（LTS）。这些在过程演算的上下文中广泛使用两种格式：• 一个变迁系统（S，=），其中S是一个集合，=S×S，适合描述一个封闭系统的可能演化，即一个不与外部环境相互作用的系统。一个s∈S表示一个状态，在给定的时间，一个封闭的系统，而转移s==sJ说，在状态s的系统可以演变（在一个步骤）到状态sJ。• 标号迁移系统（S，L，=S×L×S，适合于描述开放系统与其环境的潜在相互作用.标号l∈L表示开放系统与其环境之间的相互作用类型，s∈S表示开放系统的状态在给定的时间，和过渡s=sJ说状态S的系统可以与环境相互作用（由l指定）并进化到状态sJ（假设相互作用已经发生）。将开放系统与其所处的环境结合起来，得到封闭系统，这是完全可能的另一方面，给定一个封闭系统，可以有几种方法将其分解为两部分，或者封闭系统可以如此纠缠，以至于没有办法将其分解为两部分。尽管我们已经令人信服地论证了一个有标签的变迁系统（描述一个开放系统）可以被一个变迁系统（对于一个更复杂的封闭系统）所包含，但它们的表达能力是有限的。例如，过渡系统不能描述连续（或混合）系统，其配置482E. Moggi/Electronic Notes in Theoretical Computer Science 172（2007）479随时间连续演化，也不是随机系统，其在转换集合上具有概率也许这些系统可以通过基于[24]提出的函子操作语义的转换系统的推广然而，为了本文的目的，我们把转换系统作为描述操作语义的规范格式TS对LTS。这个讨论是关于LTS和TS之间的权衡的旁白，并为选择TS作为描述操作语义的首选格式提供了进一步的证据一般来说，操作（或指称）语义应该支持对程序的推理。在这方面，一个自然的问题是，当一个程序片段可以被另一个程序片段取代，而不改变系统的可观察行为。在过程演算中，大量的工作致力于确定合适的观测等价性。有许多等价物已经提出，但没有明确的最佳选择。然而，一般的指导方针是，应该寻求开放项的一致性（即程序片段的对应物），并且该一致性应该取决于一组简单的观察。进程演算的工作使用了标记和未标记的转换系统来定义操作语义。LTS适用于描述开放系统与其环境的潜在相互作用组成开放系统的构造可能在LTS级别上有一个语义对应物然而，高阶π演算[20]的工作表明，基于TS的操作语义事实上，封闭系统上的观测（观测可以定义为状态上的半可判定谓词）可以保持相当简单，就像米尔纳和桑吉奥吉我们参考[8]讨论和定义了几个等价（对于Join演算），并详细比较了基于TS和LTS语义的等价3一般方法我们已经把变迁系统作为指定操作语义的规范方法。我们构造操作语义的方法混合了两种成熟的工具：• 并发项重写及其推广，例如组合归约系统[14];• 多集重写，特别是我们借用Berry和Boudol关于化学抽象机[1]和Join演算[7，8]的工作。我们考虑过渡系统，其中状态是项和计算规则的多重集合，我们称这些多重集合为组态（在化学类比中，计算规则是反应规则，组态是化学解）：• 项的多集合对应于给定时间的封闭系统的状态;E. Moggi/Electronic Notes in Theoretical Computer Science 172（2007）47948321• 计算规则描述了系统的潜在演变计算规则捕获编程语言的计算特征。在大多数情况下，它们只涉及多集重写，即。用另一项的多集合替换项的多集合，但是它们也可以生成新的名称并激活新的计算规则。编程语言的非计算性特征被一种关系捕获，这种关系被称为简化，它是连续的和兼容的，即，它可以以任何顺序和在任何上下文中应用。简化体现了引用透明性，并为证明助手定义纯函数语言或类型演算的操作语义简化可以扩展到配置（以一种明显的方式），我们坚持认为“计算步骤对进一步简化不敏感”，即s1）s2∗ ∗V VJ> sJ这个属性是引用透明性的另一个例子，它允许忽略简化何时以及如何完成。特别是，计算规则对简化策略的选择不敏感，因此可以安全地利用纯函数式语言实现中常用的技术[18]，如惰性求值和图归约。在本节的其余部分中，我们描述了一个特定的转换系统，它是根据简化和计算定义的，而在下面的部分中，我们将使用它来描述几个演算的操作语义3.1方面我们假设三个基本句法范畴（即有限集合）用于术语（和相关概念）的定义：• a∈A是FreshML [22]和FM-集理论[10]意义上的原子，即原子可以置换（但不能替换）;• y∈XN是名称变量，可以用原子（和名称变量）替换;• x∈XE是项变量，可以用任意项代替。术语的定义以及名称和模式的辅助概念由以下BNF给出（在续集中，我们将ok和fail视为特殊原子，S484E. Moggi/Electronic Notes in Theoretical Computer Science 172（2007）479名称u∈N：：= a|y模式p∈P：：=？X| up|什么？y p项e∈E：：= x| ue的|奥克埃|费尔|（第1页）|e2）|e 1@e 2|e1：p2|（e1; e2）|设{x i= e i|i ∈ n} in e子句ok e和fail作为u e）的实例：名字u是原子或名字变量。我们将A（u）和FV（u）分别写为u中的原子集和自由变量集模式p比函数式语言和[13]的模式匹配演算（PMC）中的模式更具表达力（例如，PMC中的模式由BNFp：：=？X| ap）。例如，我们可以定义一个项来检验原子的相等性。基本上，我们使用Linda模板的典型特性扩展PMC模式[11]（和相关的结石，如μK权利要求[2]）：• 声明的变量用？标记。 ？x匹配任何项e并将其绑定到x，？y匹配任何名称u并将其绑定到y。• 命名表达式u，也就是命名变量y，在模式中是允许的因此，区分一个自由出现的y的声明是很重要的？y.在μKLAIM对于模式的良构性有一个标准的线性约束，即一个变量在一个模式中最多只能声明一次。原子A（p）、声明变量DV（p）和自由变量FV（p）的集合由p上的结构归纳法定义pA（p）DV（p）FV（p）？X ∅{x}∅u pA（u，p）DV（p）FV（u，p）？yA（p）{y}个DV（p）FV（p）− {y}pp pA（p，p）DV（p，p）FV（p）（FV（p）−DV（p））A、DV和FV的定义通过逐点并合扩展到逗号分隔的句法实体序列，例如A（u，p）= A（u）<$A（p）。FV（p）的定义是说，y出现在？Y是绑定的。我们没有令人信服的例子来利用这个E. Moggi/Electronic Notes in Theoretical Computer Science 172（2007）479485功能。如果要禁止这种绑定，那么FV应该被定义为FV（？y p）= FV（p）和FV（p p）= FV（p，p）。术语e基本上是从[13]的PMC借用的，并且具有以下非正式语义：486E. Moggi/Electronic Notes in Theoretical Computer Science 172（2007）479• u e是应用于术语序列的构造函数（名称）;• ok e表示成功的术语;• fail表示故障（例如，模式匹配）;• （第1页）|e2）表示一个试图将参数与p匹配的函数，如果失败，则将e2应用于参数;•e1@e2为函数应用;• e1：p=e2尝试将e1与p匹配，如果成功，则将匹配替换应用于e2;• （e1;e2）允许故障恢复，即如果e1失败，则返回e2;• 设{x i= e i|i∈n}在e中允许相互递归的定义（声明的变量x i必须是不同的）。原子集合A（e）和自由变量集合FV（e）由e上的归纳法定义。A（e）的子句是直接的，因此我们只给出FV（e）的子句。eFV（e）X{x}ue的FV（u，e）（第1页）|e2）FV（p，e2）<$（FV（e1）−DV（p））e1@e2FV（e1，e2）（e1;e2）FV（e1，e2）设{x i= e i|i∈n} in e n（{FV（e i）|i ∈ n +1}）− {x i|i∈ n}e1：p2FV（e1，p）<$（FV（e2）−DV（p））e eFV（e，e）例子. 我们给出了一些术语的例子，关于它们的运算行为的非正式主张是基于简化的定义（见3.2节）。• 原子相等性的检验定义为等式（？）y1（y1true|？y2alse|fail）|fail），其中true和false是一些给定的原子。该检验具有预期的性质，即对于任何原子a1和a2，如果a1=a2，则eq@a1@a2项简化为真，否则简化为假。更准确地说，eq @ a1简化为eq1（a1true|？y2alse|fail），因为a1匹配？y1. 等式1@a2的简化首先尝试将2与1匹配，如果失败，那么它将2与1匹配。Y2（总是成功）。一般来说，eq可以应用于任何一对项e1和e2，并且eq@e1@e2的简化可能有两个其他结果：· 如果模式匹配失败，则其简单化为失败，例如，a e不匹配？y1;· 它卡住了，因为我们不能确定一个术语是否匹配一个模式。第二种可能性的发E. Moggi/Electronic Notes in Theoretical Computer Science 172（2007）479487生是因为简化是在开放条件488E. Moggi/Electronic Notes in Theoretical Computer Science 172（2007）479(and模式）。例如，我们不能决定变量x是否匹配模式？y1，实际上x的不同替换实例产生不同的结果。类似地，我们不能决定原子a是否匹配模式y，事实上y的不同替换实例会产生不同的结果。• λ-抽象λx.e可以定义为（？X轴|fail），以这种方式，β-约简被分解为（两个）简化步骤。• 数据库的编码。在非类型化语言中，类型可以表示为项的子集或项上的部分等价关系（PER）（模简化）。我们使用原子作为构造函数来形成给定数据类型的术语，而析构函数可以通过模式匹配和递归来定义例如，对于自然数的数据类型N，我们使用两个原子：一个用于零z：N，另一个用于后继s：N→N。 此外，析构函数it：X→（X→X）→N→X可以定义如下le t it=（λx.λxf. （z）x|s？xnit@x@xf@xn|（fail））in. . .人们可以很容易地检查它是否具有方程性质· it@e@ef@zsimplifiestoe· it@e@ef@（sen）simpliestoef@（it@e@ef@en）自然数作为初始代数的特征所暗示的。3.2简化我们定义了一个关于项（模α-转换）的关系e）eJ，称为简化，它是β-约化的类似物简化被定义为图1中给出的左线性和非重叠重写规则的兼容闭包2，它直接受到[13]的PMC的简化的启发，PMC将模式匹配分解为一系列基本步骤。命题3.1简化具有以下特性：• 保持原子和自由变量，即e）eJ蕴含A（eJ）<$A（e）和FV（eJ）<$FV（e）e） eJ• 等方差e[π]）eJ[π]其中π是原子的排列， e[π]是通过排列e中，由πe） eJ• 替代性e[ρ]）eJ[ρ]其中ρ分别将名称/术语变量映射到名称/术语，并且 e[ρ]是paral-2二元关系R在项上的相容闭包是包含R并满足相容性质的项上的最小关系（见命题3.1）。E. Moggi/Electronic Notes in Theoretical Computer Science 172（2007）47948912e（第1页）|e2）@ e）（e：poke1; e 2@e）（ok e;eJ））e（fail; eJ））eJ爱因斯坦：？xeJ）eJ[x：e]u e：？伊佩杰）e：p [y：u]eJ [y：u] when |e|为|p|a e：apeJ）e：peJ当|e|为|p|设{x i= e i|i∈n} in e ）e[x i：let {x i= e i|i∈n} in e i|i∈ n]v@ e）fail when v/（pe1|e2）（v; eJ））failwhen v/ok e|费尔v：？伊佩杰）当与以下项进行交互时失败|e|为|p|v：u2peJ）当与以下项进行交互时失败|e|为|p|a1e：a2peJ）当a1/= a2时失败，并且|e|为|p|其中v：：= u e|（第1页）|e2）不能通过简化或实例化改变顶层结构的术语的范围，并且e：peJ通过归纳定义，|p|为|e|• eJ是eJ• e e：ppeJ是e：p（e：peJ）Fig. 1.简化规则用重命名绑定变量的lel替换来避免变量捕获（因此，使用项模α转换是很方便的）e） eJ• 兼容性C[e]）C[eJ]C[−]term context with one holee）e• consumption，即 ∗∗V V（J）J1 2∗e490E. Moggi/Electronic Notes in Theoretical Computer Science 172（2007）479简化可以模拟纯函数式语言的大多数特征，包括记录和变体，但它不能模拟数据库的生成性（这需要生成新的名称）。E. Moggi/Electronic Notes in Theoretical Computer Science 172（2007）479491连接模式J：：={（u i pi|i∈ n）}计算规则r：：=J > νy.R E多组模式，与R E规则和术语的多集3.3计算规则在定义配置上的计算关系之前，我们介绍了连接模式和计算规则的另一层语法，它建立在模式和术语之上。连接模式指定触发条件，即具有连接模式J的计算规则只能由作为J的实例的多重集E激活。Join-calculus [7]有更简单的join模式，由u？y1.. . ？yn（或u？简称Y）具有一定的线性约束。在Kell演算[3，21]和KLAIM[6，2]中可以找到触发器的类似复杂性。原子A（J）、声明变量DV（J）和自由（名称）变量FV（J）的集合的J 由逐点联合定义， 例如 DV（{（u i p i|i∈n）}）=n∈nDV（ui pi）. 我们对格式良好性连接模式：术语变量x在J中最多只能声明一次。 一般来说，一个名称变量y可以在J的多个模式中声明，但是一个多项集E是J的实例，只有当J中所有出现的y都被同一个原子替换时。 例如，{（SendTo a e1，GetFrom a e2）}是{（SendTo？y？x1，GetFrom？y？x2）}，但{（SendTo a1e1，GetFrom a2e2）}不是。计算规则J > v y. RE指定了系统的以下潜在演化：J的一个实例被消耗，名称变量y被新原子替换，RE的一个合适的替换实例被释放。Join演算的反应规则J > e看起来更简单，但这是可判定的。事实上，Join演算的术语表示具有并行组合的术语的多集合，并且允许反应规则和新鲜名称的局部声明因此，计算规则可以被改写为Join-calculus反应规则（除了我们的join模式，它本质上更具表达性）。我们认为强度具有分层，其中项的定义独立于计算规则，同样，简化的定义独立于计算。原子A（r）和r的自由变量FV（r）的集合定义如下（其中A（-）和FV（-）通过逐点并集扩展为多集• A（J > νy.R|E）= A（J，R，E）• FV（J > νy.R|E）= FV（J）<$（FV（R，E）−y− DV（J）），即在J中声明的变量和新名称y在RE中绑定。注3.2Join演算具有局部性质，便于演算的分布式实现。也就是说，可以以这样的方式划分原子集合：每个反应规则位于划分的给定元素处492E. Moggi/Electronic Notes in Theoretical Computer Science 172（2007）479并且消息（即a e形式的项）必须移动到划分的特定元素（由a唯一确定），以便参与反应。我们可以对计算规则的良构性施加约束，以确保类似的局部属性。为了简单起见，我们避免这样做。然而，我们考虑的所有计算规则的例子都满足这些约束。简化的定义以明显的方式扩展到计算规则和多集RE。此外，命题3.1继续保持，如果一个一贯取代与多集，例如兼容性成为兼容性R E）RJEJC[R E]）C[RJEJ]C[−]有一个洞例子. 我们展示了如何使用计算规则来定义对引用进行操作的解释器。首先，我们固定一些原子（类型注释被用作非正式的解释），例如。• prg：MY标记程序（计算类型MY），即prg e表示e是一个程序;• str：RX，X标签存储单元格，即str y v表示引用y（RX类型）存储值v（X类型）;• new：X→（RX→MY）→MY是一个操作，它接受一个值v，创建一个用v初始化的新引用y，然后将y传递给程序的其余部分;• get：RX→（X→MY）→MY是一个操作，它接受一个引用y，取出存储在y中的值v，然后将v传递给程序的其余部分下面的计算规则指定了new和get的解释• prg（新？x？k）> νy.prg（k@y），str y x（其中，是多集并）;• prg（get？y？k），str？y？x > prg（k@x），str y x.为了证明规则诱导了预期的行为，我们需要建立一个合适的配置（见3.4和4.1节），包括规则、几个程序和一个共享存储（即prg e和str a e形式的项的多集合）。3.4计算我们取闭多集RE作为配置，即FV（R，E）=E。配置上的计算关系s）J由以下重写规则定义SJρJ> νy.RE）s （R）E）[y：a][ρ] J> v y.R E其中• p是一个封闭的置换，即它将名称/术语变量映射到原子/封闭术语;• a是新原子的序列，即不在A（s）中JρJ > νy.RE）;E. Moggi/Electronic Notes in Theoretical Computer Science 172（2007）4794932• Jρ是J与ρ的实例化，其中−ρ在模式和连接模式上的定义如下（−ρ总是闭合的，当替换ρ闭合时）−−ρ？X其中e∈ρ（x）u pu[ρ]pρ？y pa pρ，其中a<$ρ（y）p ppρ pρ{（u ipi|i ∈n）}{（u ipi）ρ|i ∈ n）}注3.3关于配置的计算只使用实例化−ρ和用封闭ρ替换−[ρ]，因此它们不需要重命名绑定变量。这意味着计算不必考虑配置模α转换。相反，简化使用了用任意ρ替换−[ρ]，因此它需要重命名绑定变量。这意味着简化必须考虑配置模α转换，但一些简化策略可以更严格地使用替换。命题3.4计算具有以下性质：s） sJ• 等方差• 延伸s[π]）sJ[π]s1）s2A（s）与A（s2）-A（s1）s s1 ）s s2s1）s2• 通过简化（模拟）保留计算，即 ∗vJ1∗v> sJ一般情况下，计算关系是不连续的。此外，计算步骤不能对涉及任意大的多项集的集体操作（诸如广播）进行建模。过渡系统至此，我们已经介绍了在构形集Sc上定义一个转移系统的所有成分定义3.5TSc=（Sc，=C=ε）是跃迁系统，其中关系式= C ⇒ 由下式给出）），即s=CsJ假设一个人可以从s到SJ，简化步骤的有限序列，然后是一个计算步骤。S∗494E. Moggi/Electronic Notes in Theoretical Computer Science 172（2007）479一些简化对于实现计算步骤是必不可少的。事实上，通过简化，多项集E可以成为触发计算规则的连接模式J的实例。请注意，在绑定器的作用域下，不需要进行简化以使E成为J的实例。∗命题3.6关系）是TSc上的互模拟关系，即jJJ(i) 若s1）s2且s1= C = εs1，则存在s2s.t. s2=C=s2和s1）s2jJJ(ii) 如果s1 ）s2且s2= C = εs2，则存在s1s.t. s1=C=s1和s1 ）s2证据容易的后果是，）和模拟特性。Q因此，我们可以用一个等价的转移系统来代替TSc，其中状态是模简化配置的等价类，并取S1=C=S2<$Δs1作为转移关系 对于s1∈ S1和s2∈S2，支持3. [7] Rπ中的关系式，定义为s1Rπs2<$Δs1[π]=s2，是TS c上的一个模拟关系，对原子上的任意置换π都是如此。证据 简单的等方差推论）和 ）的。Q因此，我们可以用一个等价的跃迁系统来代替TSc，其中的态是组态模原子排列的等价类，即[s]={s [π] |π置换}。通常有一组具有特殊意义的原子，例如，用于定义对组态的基本观察在这种情况下，应该只考虑在这组原子上是同一性的排列4编码我们表现出的过渡系统TSC的表现力编码在它的抽象机器（即小步操作语义）为现有的演算表示理想化的编程语言。在每个编码示例中，我们指定• 演算的语法PL• 描述抽象机的转移系统TSPL=（SPL，=P L=N），PL（SPL中的状态涉及PL中的程序，通常还有其他一些学习）;然后，我们定义• 从PL到项集合E的合成翻译（−）（在一元中方法这对应于从PL到元语言MLM的翻译• 从SPL到配置集Sc的转换[-]]，它扩展了合成转换（-）（在单子方法中，这对应于选择一个单子来解释MLM，更确切地说是选择计算规则对应于选择单子）;最后，我们证明了翻译[-]]是一个很好的编码。在理想情况下，可以定义TSPL和TSc之间的锁步互模拟R，即E. Moggi/Electronic Notes in Theoretical Computer Science 172（2007）479495一(i) 若s1Rs2且s1=PL=SSJ，则存在SJs. t.s2=C=sJ和sJRsJ1 2 2 1 2(ii) 若s1Rs2且s2=C=SSJ，则存在SJs. t.s1=P L=PsJ和sJRsJ2 1 1 1 2[1]，故每一个人，都有一个自己的故事。 在其他情况下，当TSPL中的跃迁被TSc中的几个跃迁模拟时，必须使用具有较弱性质的关系（例如弱互模拟）。4.1带指称的我们提出了一个带有参考文献的一元元语言的编码，首先在[16]中描述。编码特别简单，因为一元元语言的操作语义是根据简化和计算来定义的其他具有不同计算效应的一元语言在[17]中描述，并且应该具有类似的编码。• 一元元语言的项M∈PL由以下BNF给出（其中a的范围超过表示引用的原子）M：：= x |λx.M |M1@M2|ret M|做M1M2|新的M|得到M|集合M1M2|一• 转移系统TS PL的状态是三重态（μ|M，S），其中· M∈PL0是一个闭项芬· μ： →PL0是一个商店，即从引用到封闭项的有限映射· S：：=无|pushM S是控制栈，即闭项M∈ PL0的栈。∗转换关系=P L=P是），其中（简化）β-还原和）（计算）由以下规则定义· （μ|do M1M2，S））（μ|M1，推M2S）· （μ|ret M1，push M2S））（μ|M 2@M 1，S）· （μ|新的M、S））（μ，a：M |ret a，S）with a ∈ A fresh· （μ|得到a，S））（μ|ret M，S），如果μ（a）= M· （μ，a：M J|设置一个M，S））（μ，a：M |ret a，S）如果我们将λx.e与（？）X轴|（1）考虑术语构造函数ret，do，。. .是原子。[（μ|M，S）]是配置{（str a M）}|μ（a）= M）}prg M<$S<$R，其中str和prg是原子（用于表示存储和程序线程），R是包含以下计算规则的集合（与上述规则一一对应）• prg（do？x1？x2）？xS> prg x1（push x2xS）• prg（ret？x1）（推？x2？xS）> prg（x2@x1）（push xS）• prg（新？x）？xS> νy.prg（ret y）xS，str y x（其中，是多集并）• prg（get？y）？xS，str？y？x> prg（ret x）xS，str y x• prg（set？y？x）？xS，str？y？xJ> prg（ret y）xS，str y x最后，我们对关系（μ）进行了一个lock-stepbilation|M，S）RsΔs等于[（μ|M，S）]]模化简496E. Moggi/Electronic Notes in Theoretical Computer Science 172（2007）479Pyyyi连接模式J：：=y？y|（J1）|J2）过程P：：= y y|def D in P|（P1）|P2）|0定义D：：= J > P|（D1至D2）|不4.2联演算我们给出了一个编码的Join演算，它涉及TSc的反应性化学抽象机的Join演算。这种编码的关键特征是它不使用简化（并且所涉及的项非常简单，即u u形式的项）。我们回顾Join演算的（异步核心）语法，并参考[8]以获得Join演算和响应式化学抽象机的更多细节。变量有一个基本的语法类别，我们可以用变量y来识别它;其他的语法类别是反应性化学抽象机定义为一个过渡系统TSJC，其状态（称为化学溶液）是定义D和过程P的多组，过渡关系由加热、冷却和反应定义。我们定义一个具有以下性质的合成翻译（-）• 10.J2EE是一个连接模式（|对应于多集并集）;• D是规则的多集（D对应于多集并，T对应于空集）;•翻译是术语和规则的多集合，在这种情况下，翻译取决于额外的参数，即不应该出现在P中的名称变量y。翻译中有趣的句子是：• （def D in P） （y > v y，yJ.DP），其中y是声明变量的集合yDV（D）和YJ/∈FV（D，P，y）;• （P1）|P2）y= y（y > v y1，y2.（P1）yJ（P2）∈FV（P1，P2，y），其中y1，y2/∈FV（P1，P2，y）;年一年二• （J > P）n=Jn> νy.Pn，其中y/∈FV（J，P）.第一个子句使用了额外的参数y。如果事实上，我们不能采取（defDinP）），否则规则将总是有效的（由于y y到空连接模式），我们将有D和P的多个副本。 上另一方面，只有当y恰好出现一次时，翻译才正确，因此这两个子句被设计为保持该属性。我们现在定义化学溶液（即TSJC的状态）和组态之间的关系RSJC×Sc，如下：• 存在不同名称变量yi的选择，一个变量用于多集合P，s. t中的每个元素Pi。对于D和P，yi是新鲜的;• s=D<$[ρ]（iP i<$[ρ]）对于从变量名到原子的单射映射ρ。显然，对于每一种化学溶液，至少有一种构型与之相关，因此，通过选择，我们可以定义从SJC到Sc的转换。E. Moggi/Electronic Notes in Theoretical Computer Science 172（2007）4794971 2 1212关系R是TSJC和TSc之间的弱互模拟，更准确地说，（D P）Rs意味着(i) s不能被简化，并且s的任何计算步骤都可以通过D的一个反应或一个加热步骤来模拟;(ii) D_（10）P的任一反应步骤用一个s的计算步骤来模拟，任一加热步骤用至多一个s的计算步骤来模拟。我们忽略冷却步骤，因为它们的唯一目的是将化学溶液与过程P联系起来（更确切地说，是形式为PNP的化学溶液）。4.3移动环境：集中实施我们给出了移动环境（MA）的编码[5，4]，对应于MA的集中式实现，在这个意义上，用于解释MA的计算规则位于一个地方（见备注3.2）。我们还没有沿着[9]的路线研究与MA的分布式实现对应的替代编码。然而，这是不可能的，一个可以避免的技术复杂性（如使用耦合弱模拟）证明的正确性，MA的分布式实现的联合演算。为了使编码的性质更容易公式化，我们对MA的语法和操作语义的原始定义进行了一些调整。 对于语法，我们将原子a和名称变量y（并使用名称u：：= a）作为基本语法类别|y）。对于操作语义，我们使用一个过渡系统TSMA类似于反应性化学抽象机（以避免使用结构一致性）。• MA的过程P∈PL由以下BNF给出P：：= 0|（P1）|P2）|！P| Vy.P|u [P] |M.P，其中M表示能力M：：= in u|外出使用|打开使用• TSMA的状态是闭过程的多重集合P的嵌套，SMA是域方程SMA=μ（MA0+A×SMA）的最小解，其中μ（X）是元素在X中的有限多重集合的集合。• 过渡关系MA 是以下重写规则·0~、P1|P2~P1、P2、！P~ P，！P· n[P]~n [{（P）}]（lhs是MA 0中的元素，即过程n [P]，而rhs是A × S MA中的元素，即过程n [ P]）。n与单例多重集{（P）}）新· 具有n个新原子的νy.P~ P[ y：n ]（严格地说，这不是重写规则，因为边条件是全局的，并且n是非确定性地选择的· n[inm. P，P]，m[P]in）m[n[P，P]，P]· m[ n]n[outm. P，P]，P]o）tn[P，P1]，m[P2]· OPENM。P，m[P]ope）nP，P加热规则（用~表示）与结构一致性有关，反应规则（用））对应于归约规则。498E. Moggi/Electronic Notes in Theoretical Computer Science 172（2007）479MA的合成翻译（-）是直接的，对于过程（和能力）的BNF中的每个子句，我们都有一个对应的原子•0=零， （P1|P2）= parPP， （！P）=repP1 2• （νy. P）n=new（？y⇒P∗|（fail）• （u[P]）=box uP• （in u.P）=in uP，其他能力P∈SMAintoconfigurationsis[P]]=RMA[[P]]ar，其中RMA是一组计算规则，原子ar是根环境的唯一标识符（UId），[−]]a是通过嵌套多集上的归纳定义的项的多集（特别是它与多集并交换）。[P]]a中的项具有以下形式：• prg a e是在环境a中执行进程e的线程（更准确地说，具有UIda），具体地，[P]]a=prg aP;• amb a n a p表示ambient a具有名称n和父ambient a p;这些项编码嵌套多重集的树结构，因此对于每个UId a（除了根UId a r），应该正好有这些项中的一个，特别是[n [P]] a=（amb aJna）[[P]]aJ，其中reaJ是一个freshUI d。RMA中的一些规则引入了形式为opn a ap的项，表示环境a已被父环境ap打开。当这种情况发生时，amb a n ap将被删除，但a中的线程和子环境必须迁移到ap。RMA的规则是：• 采暖计算规则· prg？y nil>prg？y（par？x1？x2）> prg y x1，prg y x2prg？y（rep？x）> prg y x，prg y（rep x）· prg？y（new？x）> vn. prg y（x @ n）· prg？y（box？n？x）> v yJ.amb yJn y，prg yJx（yJ是名称为n的新环境的UId）• 能力计算规则· amb？yJ？m？是JJ，prg？y（in？m？x），amb？y？n？yJJ> prg y x，amb y nyJUP意味着匹配项被读取，但不被移除。换句话说，（up，J >. . ）是计算规则（up，J >.、|u p|），其中|p|这个词是通过擦除的方式获得的吗？在图案P中。· amb？yJ？m？是JJ，prg？y（out？m？x），amb？y？n？yJ> prg y x，amb y nyJJ· prg？y（打开？m？x），amb？yJ？m？y > prg y x，opn yJy•