反应语义学：过程代数和通信系统演算的结合方法

理论计算机科学电子笔记175（2007）57-70www.elsevier.com/locate/entcs反应语义学的主动评估上下文亨里克·皮勒加德·弗莱明·尼尔森{hepi，nielson，riis} @ imm.dtu.dk信息学与数学建模丹麦技术大学摘要在过程代数的上下文中，习惯上以由结构同余关系支持的反应关系的形式定义语义。最近，过程代数变得更具表现力，以满足业务建模和系统生物学等领域的建模需求。这导致了各种特征的结合，例如之前单独研究的一般选择和并行性，并且定义反应语义通常变得困难。我们提出了一个通用的方法，基于积极的评价上下文，可以很容易地构建反应语义。关键词：结构操作语义学，反应语义学，进程代数，一般选择，通信系统演算，生物环境。1介绍自从他们提出[7，11，1]以来，进程演算已经成为研究并发计算范式的主要工具.在过去的三十年里，出现了两种类型的语义学结构化操作语义[15]描述了进程如何与其直接环境交互。与通常的结构操作语义一样，复合过程的直接行为是根据其组成过程的直接行为在结构上定义的。行为通常使用标记的转换系统来表示。标签语言具有相当大的潜力，这确保了结构操作语义方法也适用于更具表达性的演算。然而，随着演算变得更具表达性，所需的标签语言往往变得复杂，并且在某种程度上模糊了并发性的直觉化学抽象机（CHAM）风格的反应语义[2]清楚地表达了对并发性的直观（化学）理解。每1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.09.01458H. Pilegaard等人理论计算机科学电子笔记175（2007）57过程术语被认为是（语法）反应实体的解决方案的描述。通常的结构一致性是一种神奇的搅拌机制，允许句法实体根据需要进行混合和混合。然后，反应关系虽然非常直观，但这种类型的语义具有结构一致性受制于冲突要求的一方面，我们要求全等性严格区分语义不同的过程表达式。另一方面，我们要求它能够移动潜在的redex成分，这些成分在句法上相距任意远，足够接近，以便反应规则识别它们。除了通常的可判定性问题之外，这两个要求似乎随着微积分表达能力的增长而发生冲突。由于它们不同的优势，微积分通常具有两种类型的语义。然而，对于更复杂的演算，这通常是困难的，除非施加句法限制。米尔纳的通信系统演算（CCS）就是一个很好的例子。最近的版本[13]，我们在第2节中简要描述，将选择限制为保护和。这有利于这两种类型的语义，因为范式Σαj.Pj（1）J总是可以假设为赎回权的组成部分。这可能与原始微积分[11]形成对比，原始微积分具有不受限制的选择。由于这个原因，（...） （α.P + P J）|P JJ）+P JJJ）|P JJJJ.. . （2）需要为赎回权的组成部分假设。这种范式很难在句法上匹配，结构一致性也没有什么帮助，因为允许选择和平行词自由地分布在彼此之上在语义上是没有意义的。因此，传统上，只有结构操作语义被定义为这个演算的衍生物。在本文中，我们将展示如何反应语义可以定义，即使是非常富有表现力的演算。人们可能会问，为什么能够处理二元无限制选择而不是索引保护和（在某些任意有限索引集上）是有趣的。在这样做时，我们遵循Gordon Plotkin在设计结构操作语义学时使用的设计原则之一[15]：应该始终努力使用一元或二元语法构造器而不是一般的n元构造器，因为前一种选择有助于机器可读的形式语义，并且还可以对手头的编程构造进行更深入的语义理解[16]。所提出的方法是基于一个新的概念，积极的评价背景。当人们允许标准评价语境（最初由Felleisen [5]提出）在反应发生时演变时，这些语境自然会出现。在第3节中，我们开发了主动求值上下文，并使用它们为CCS的无递归片段定义了一个反应语义，该片段具有不受限制的选择。主要理论-H. Pilegaard等人理论计算机科学电子笔记175（2007）5759P：：= 0| α。P|Σi∈Iαi。Pi|PP|（νa）Pα：：= τ|一|一图1.一、有限核CCS与保护和（CCSg）的关系本文的一个重要结果是，所得到的反应语义与Milner在更复杂的演算的情况下，主动求值上下文和结构一致性的概念很我们在第4节中对此进行了说明，其中我们定义了扩展为无限制选择的完整BioAmbients演算的反应语义2CCS与保护总和为了设置场景，我们首先考虑具有Milner定义的保护和的CCS [13]。为了更清楚地展示我们在第3节中的贡献，我们将集中讨论语言的有限片段，从而省略递归。这并不意味着我们的框架有局限性--正如我们将在后面的第4节中演示的那样，递归可以很容易地使用结构一致性来合并现在，让N，由a，b，···，是一个可数的通道名称集，让特殊符号τ表示内部动作。动作前缀的句法类α∈Act则包含所有名称a∈ N、所有对应的共同名称a∈ N和特殊符号τ。在这种情况下，具有保护和的有限核CCS过程类（表示为CCSg）由文法描述：Σ在图1中，我们假设i中的I∈Iαi。Pi是有限的，写0，当|= 0和α.P，当|我|= 1。|= 1.因为选择结构Σi∈Iαi. Pi是有保护的，可以定义a传统（CHAM风格）反应语义。 一如既往，由于语法由于反应语义的本质，该定义依赖于结构一致关系。 如果我们让α表示普通的α-等价，则结构同余，是满足图2中公理和规则的最小关系。利用同余关系，反应关系，−→gs，由图1的公理和规则定义3 指定CCSg的完整反应语义。注意这个定义是如何依赖于前面描述的类型（1）的正规形式的存在的。接下来，我们定义了一个结构化的操作语义，指定过程是在标记的转换系统。我们假设与前面相同的动作前缀类α，但使用缩写λ来表示非内部的动作前缀（即λ∈Act\{τ}）;我们将写n（α）来表示一个新的一个ctionprefix。结构关系−α→uc定义结构优化语义则是满足图4的公理和规则的最小关系。虽然CCSgs语义的这两个公式通常用于不同的目的，但它们旨在表达封闭进程表达式的相同行为。因此，下面的结果[13]是至关重要的：60H. Pilegaard等人理论计算机科学电子笔记175（2007）57P−→gsPJPQ−→ gs PJQP P−→gsP′τQ′λλααα并行进程的重新排序：名称限制的作用域规则P0gP（νa）0g0PQgsQ P（νa）（νb）P gs（νb）（νa）PP（QR）<$gs（PQ）R（νa）（PQ）<$gsP（νa）Qifa∈fn（P）Alpha等价：求和中项的重新排序PαQPgQSummands可以自由重新排序。等同性：一致性：PgsPPgsQα.P+Mgsα.Q+MPgQQgPgQ（νa）Pg（ν a）QPgQQgRPgRPgQP RgQ RPgsQRPgsR Q图二. CCSG的结构一致性P−→gsPJTAU：τ。P + M −→gs PRES：（νa）P−→gs（νa）PJPAR：PQQ−→gsQJQjPJ反应：（a. P +M）（a. Q + N）−→gs P问：P−→gsPJ图三. CCSg的反应关系P−→gsP′Q−→gsQ′总和试验α： M + α。 P + N−→gsP反应t：L-部分：P−→gsP′P−→gsP′R-部分：Q−→gsQ′P Q−→gsPαQ′保留时间：α（νa）P−→gs（νa）P′如果n（α）/=a见图4。 CCSG的结构操作语义定理2.1（对于CCSg反应与τ-跃迁一致）对任何CC-Sgppp，如果p−→gsPj，则存在P− τ →gsPj.证据参见米尔纳[13]定理5.6Q3CCS的主动评估环境当微积分被推广到有限核CCS与无限制选择（CCSuc）时，如图5所示，情况发生了变化。Milner和其他贡献者都没有为这种语言的衍生物定义过经典（CHAM风格）的反应语义-并且有很好的技术原因。我们认为，处理类型（2）的正规形式的技术手段一直缺乏，因此，从CCSuc派生的演算传统上只给出一个结构运算。P Q−→gsP′QαH. Pilegaard等人理论计算机科学电子笔记175（2007）5761C −→C′PC −→PC′ααατP：：= 0| α。P|P + P|PP|（νa）P图五. 无限选择的有限核心CCS（CCSuc）。Pα′a′−→ucPP−→ucPPREtα： α。P−→ucPL-PARt：Q′L-SUMt：一P+Q−→ucP′′R-PARt：−→ucQR-SUMt：Q−→ucQP+Q−→ucQ′αPλ′λ′′P−→ucP若n（α）a−→ucP Q−→ucQ结果：α（νa）P−→uc（νa）P′反应t：P Q−→ucP′Q′见图6。 FcCSSuc的结构操作语义C：：= [ ]|（νa）C|CP|PC|C+ P|P+ C见图7。 协调委员会的积极评价背景EMPc：[ ] −→[]NEWc：C −→C′（νa）C−→（νa）C′L-PARc：C −→C′C −→C′CP−→C′PC −→C′R-PARc：L-SUMc：C+P−→C′R-SUMc：P+C−→C′见图8。 CCSuc中活动评估上下文的上下文缩减语义类似于图6中所示的语义[12]。我们现在将为CCSuc提出一个语义，它保留了反应语义的直观性为此，我们将引入图7中定义的活动评估上下文的概念。与通常的过程/求值上下文一样，活动求值上下文是只有一个洞的过程表达式[5，13，8]。然而，与普通上下文相反，我们将允许活跃上下文在占据其空穴的反应子过程参与反应时演化。为了便于实现这一点，我们定义了图8中描述的上下文约简关系。它具体说明了当反应子过程参与反应时，上下文会发生什么。 上下文的约简能力使得反应关系式− →的定义，如图9所示。在这里，我们使用辅助函数masked（C）来确定受上下文C. 该函数由下式给出：P Q−→ucP′QαP Q−→ucPαQ′62H. Pilegaard等人理论计算机科学电子笔记175（2007）57masked（C）={λ|一些（νλ）CJ出现在C}特别地，masked（（νa）C）={a}masked（C）。H. Pilegaard等人理论计算机科学电子笔记175（2007）576312案例RC、R+C和C+R：TAU：τ。P−→ucPC1−→C′C2−→C′反应：CONT：如果n（λ）/∈（masked（C1）≠masked（C2））C−→ C′P−→ucP′C[P]−→ucC′[P′]见图9。 CCSuc的反应关系3.1语义对应很明显，上下文归约关系非常类似于将递归下降编码为过程项的结构操作语义的那些规则因此，结构一致性被证明是不必要的，就像结构操作语义学一样。在这个有利的上下文中，封闭进程表达式的反应语义和结构操作语义的等价性可以简单地表示为：定理3.1（反应对应于τ跃迁）P−→ucPJ当且仅当P−τ→ucPJ。证明有两个部分，但首先我们建立了以下有用的结果，它显示了活动上下文的概念如何与结构操作语义学相关引理3.2（上下文尊重行为）如果Pn（α）∈/masked（C）则nC[P]−α→ucCJ[PJ].−α→ucPJ，C−→CJ，annd证据证明过程通过C：Base case []：trivial上的结构归纳进行。案例C和R：从前提我们有P掩蔽（C）。−α→ucPJ，CR−→（CR）J，andn（α）∈/根据−→的推论的形式，我们有（CR）J=CJR和C−→CJ作为必要前提。 从归纳假设中可以清楚地看到，C [P] −α→ucCJ [PJ]。现在，只需应用L-PARt规则即可建立所需的结果：C[P]R−α→ucCJ[PJ]R都差不多情况（νa）C：C1 [λ. P] C2 [λ. Q] −→ucC′[P] C′[Q]12H. Pilegaard等人理论计算机科学电子笔记175（2007）57631从前提我们有Pmasked（（νa）C）.−α→ucPJ，（νa）C−→（（νa）C）J，anndn（α）∈/根据−→的推论的形式，我们有（（νa）C）J=（νa）CJ，C−→CJa neces是一个非常简单的概念，并且我们知道，如果n（α）∈/masked（C）。从这一点的影响来看，这一点是新的，即C[P]−α→ucCJ[PJ]。若有atn（α）∈/maskd（（νa）C），则有atn（α）/=a和askd，且REStrulen的一个简单的应用是：（νa）C[P]-α→uc（νa）CJ[PJ].Q有了这个引理，现在就很容易建立Lemma3. 3如果P−→ucPJ，则nP−τ→ucPJ。证据我们通过归纳法继续进行−→uc的推论：情形TAU：给定过程项τ.P，规则PREt简单地实例化为：τ.P−τ→ucP，正如所希望的那样。案例反应：规则PREt给我们一个。P1 −a→ucP1andda . P2−a→ucP2，并从e开始当n（a）∈/（masked（C1）∈（mask e d（C1）时，n（a）∈（masked（C1）1 2掩蔽（C2））。使用引理3.2，我们可以建立C1 [a. P1]−a→ucCJ[P1]andC2[a . P2]−a→ucCJ[P2]. 通过一个简单的程序，可以对规则进行更新2τJ J现在总结C1 [a. P1] C2 [a. P2] −→ucC1 [P1] C2 [P2]，根据需要。病例继续：从前提出发，我们有C−→CJ和P−→ucPJ。 使用感应hypothessobtainP−τ→ucPJ，其中viouslyn（τ）∈/掩蔽（C）。引理3.2现在告诉我们C[P]−τ→ucCJ[PJ]，这是必要的。Q我们现在转向Lemma3. 4如果P−τ→ucQ，则nP−→ucQ，如果P−λ→ucQthenn，对于所有的c∈xtsC，Cj都满足C −→Cj且n（λ）∈/maskedd（C），则有C[P] λ。 R −→ucCJ [Q] R和λ。 R C [P] −→ucR CJ [Q].我的律师。通过不依赖于f−α→uc的内部关系来执行预处理：基本情况PREt：如果α是τ，则P是τ.PJ，Q是PJ，并且从TAU得出跃迁P−→ucQ。否则，P是λ.PJ，Q是PJ，所需的转换都遵循REACT（将C1和C2中的一个取为C，另一个取为[]）。案例L-PARt：64H. Pilegaard等人理论计算机科学电子笔记175（2007）57深深如果α是τ，则P是PJQ是P，QJ和跃迁P−→ucQ由归纳假设和CONT得出，其中C取为[ ]QJ。否则，P和Q具有类似的形式，但是过渡必须从RR EACT开始。从PJ−λ→ucPJJ的形式可以看出，归纳假设告诉我们，C[PJ] λ。R−→ucCJ [PJJ] R，对于所有连 续 的 C ，CJ（即， C −→CJw ithn（λ）∈/masked（C））。显然，C[[ ]QJ]、CJ[[ ]QJ]也是合适的，然后所需的转换都遵循REACT。情况R-PARt、LSUMt和R-SUMt：均相似。病例结果：如果α是τ，则P是（ν a）PJ，Q是（νa）PJJ，跃迁P−→ucQ由归纳假设和CONT得出，其中C取为（νa）[]。否则，P和Q具有类似的形式，但是转换必须从R_E_A_C_T向下。从这个假设可知，PJ−λ→ucPJJ，归纳假设告诉我们，C [P J] λ。R −→ucCJ[PJJ] R对于所有可替换的C，CJ（即， C −→CJw ithn（λ）∈/masked（C））。显然C[（νa）[]]， CJ[（ν a）[]]也是合适的，因为我们知道，如果n（λ）∈/masked（C）∈{a}，则从n（λ）/=a的分解系数中，我们可以得到n（λ）//masked（C）∈ {a}。然后，所需的转换都遵循REACT。案例反应：这里α是τ，P是PJQJ，Q是PJQJ。 根据前提和归纳假设，我们有C [PJ] λ。R−→ucCJ [PJJ] R和λ。 R C [P J] −→ucR CJ [P JJ]。 由于这些反应只能通过使用R EAC来发生，因此C[P]可能是C[Cdep[λ ]的替代物。Pdeep]]，其中Cdeep−→CJandn（λ）∈/masked（Cdeep）。对于QJ，类似的论点允许我们假设C[QJ]具有以下形式：C[Cdeep[λ . Qdeep]]，其中Cdeep−→CJandn（λ）∈/掩蔽（C深）。由此，我们通过一次应用REACT得到所需的反应。Q4BioAmbients的主动评估环境使用过程演算作为真实世界领域的建模语言，如业务建模和系统生物学，似乎是基于语言的技术的当前趋势。这一趋势结合了许多以前未研究或仅孤立研究的语言特征这必然会导致越来越多的表达性结石，它们在定义适当的反应语义方面与CCSuc一样困难。Regev等人[18，17，3]的BioAmbients演算就是一个很好的例子。该语言是Mobile Ambients（Cardelli和Gordon [4]）的兄弟，旨在H. Pilegaard等人理论计算机科学电子笔记175（2007）5765模拟生物系统。它保留了环境作为活动的有界移动场所的概念;然而，与移动环境相反，生物环境被视为无名实体。环境被用于以直观的方式模拟由生物屏障（膜）约束的化学活性子系统（隔室）。就建模原语而言，微积分是相当广泛的。 设计了适当的能力和协同能力集，用于模拟可能发生在子系统之间的各种生物反应，例如运动和通信。通信和移动都是通过能力/协同能力对彼此反应来促进的，如[10，14]中所示。因此，所有的反应都是同步的，在这个意义上，暴露能力的过程和暴露相应的协同能力的过程必须同时同意一个反应才能发生。只有双方达成一致，实体共享相同的（信道）名称。过程的控制结构的集合比针对Mobile Ambients所研究的trans-mandatory略大。除了环境构造，它还包括非确定性（外部）选择以及CCS方式的一般递归构造[12]，以便于描述更忠实的生物系统模型。遵循环境结石的传统，Regev赋予BioAmbients（CHAM风格）反应语义[18，17]。可以说，这是一个自然的选择，因为它确保了固有的生物化学建模领域和语言的操作模型之间的高度一致性。至于CCSG，外部选择仅限于保护和，我们再次认为，这是因为在定义时缺乏在下文中，我们提出了一个BioAmbients变体，其中选择是不受限制的。我们相信这是一个保守的扩展的原始演算，但正式的证明是除了本文件的点。相反，我们将专注于使用我们的主动评估上下文来定义反应语义。4.1语法BioAmbients的完整语法定义见图10。请注意，我们使用粗括号[和]表示环境边界;普通括号[和]保留用于替换和上下文漏洞我们使用a，b，···∈ N来表示通道名称，M∈Cap用于（协同）能力的概念，其基于名称并概括了动作的概念按照BioAmbients的惯例，我们省略了内部τ作用的概念此外，由于反应基于（共同）能力，我们不需要共同名称。在下文中，我们将写作P[a/b]来表示与P相同的过程，只是名称b的所有自由出现都被a取代。 类似地，我们将使用P[Q/X]来标识作为P的过程，除了过程标识符X的所有自由出现都被过程表达式Q替换。 在这两种情况下，我们都小心地执行必要的α重命名，以避免捕获自由名称和进程标识符。最后，我们将使用fn（P）来挑选一个66H. Pilegaard等人理论计算机科学电子笔记175（2007）57P：：=0一个终端（卡住）进程|（νa）P将a的作用域限制到过程表达式P|[P]被周围边界包围的过程P||PP′P+P′进程P与进程P′并行P和P′之间的非确定性外部选择|M. P能力预定过程|rec X. P递归过程定义（X=P）|X进程标识符M：：=输入a|接受入场动作|驱逐出境|expel aexit movement| 合并+合并运动|merge+ a merge movement| a! {二} |是吗？{c}约束可伸缩性的有限共同体| a! {二} |一个女的？{c} 用于绑定值c的隐藏共同体的p aren| aˆ! {二} |是吗？{c}childtoparentcomion绑定variablec| a#! {二} |a#？{c}绑定值c的兄弟共同体见图10。 BioAmbients公司C：：= [ ] |CP|PC|C+ P|P+ C见图11。 BioAmbients的活动评估环境EMPc：[ ] −→[]L-PARc：C −→C′C −→C′CP−→C′PR-PARc：C −→C′L-SUMc：C+P−→C′R-SUMc：P+C−→C′见图12。减少BioAmbients主动评估上下文。进程P和写P<$αQ来说明两个进程P和Q在名称的α-重命名之前是相同的4.2语义图11和图12所示的BioAmbients的主动评估上下文比CCSuc的要简单。它们的定义体现了三个关键的选择，我们将在下面进一步证实：(i) 活动上下文不受名称限制。(ii) 活动上下文是无环境边界。(iii) 活动上下文是无递归。选择（i）是必要的，因为π样式的名称传递和环境样式的移动都当受限制的名称被传递给收件人或移动到其原始边界之外的位置时，就会盒子将活动上下文定义为无名称限制允许我们处理C −→C′PC −→PC′H. Pilegaard等人理论计算机科学电子笔记175（2007）5767名称绑定的作用域规则（νa）0<$0（νa）（PP′）<$（（νa）P）|P′ 如果a∈/fn（P′）（νa1）（νa2）P<$（νa2）（νa1）P（νa）（P+P′）<$（（νa）P）+P′如果a∈/fn（P′）（νa）（[P]）[（νa）P]递归的展开recX. P P [rec X. P/X]α-重命名：同余要求：PαQPQPPPQPPQQRPRPQC[P]C[Q]PQPQ（νa）P（νa）Q图十三. BioAmbients的结构一致性PQ以通常的方式显式地处理所有与范围相关的问题，即使用结构一致性，如图13所示，根据需要将名称限制迁移到赎回中或从赎回中迁移出来。与通常的做法相反，我们允许常数引入（νa）迁移非确定性外部选择构造的进出方式与并行组合的习惯方式大致相同。这是必要的，因为我们的反应语义规则将隐式地采用范式（...）（（（[... （（M. Pi+ P ′）P ′′）+P ′′）P′。. ）]+ P ′）P ′′）+P ′ ′）P′。.（三）I I I I O O O对于运动行为的赎回权的组成部分，以及（...）（（（[... （（M.Pi+P ′）P′′）+P′′）P".. . ）]+P′）P′′）+P′′）P".. . ）（4）I I I I OO O（其中灰色符号表示可能存在或可能不存在的语法）。在每一种情况下，一致性必须足够强，以在适当的情况下迁移阻碍的名称限制。选择（ii）是为了确保图14所示的反应语义规则正确识别和更改赎回。所有的Redex都有两个组成部分，一个暴露一个功能前缀，另一个暴露相应共同能力预设。如前所述，这些成分总是可以假定为形式（3）或（4）之一，这意味着在某些情况下需要恰好一个边界来包围暴露的前缀，而在其他情况下不允许边界。将活动评估上下文定义为无环境边界允许我们以以下方式轻松匹配这些情况中的每一个(I) 如果不允许环境边界，则构成要素只是一个包含在活动评估上下文中的能力前缀过程表达式，我们通过C [M]匹配。 P]。(II) 如果只需要一个环境边界，则成分是封闭在环境边界构造和进一步的活动求值上下文中的形式（I）的表达式，我们通过C1 [C2 [M]匹配。P]]。[P][Q]68H. Pilegaard等人理论计算机科学电子笔记175（2007）5712341232134121231232134环境的移动C1−→CJC2−→C3C3−→CJC4−→CJC1 [C2[输入a。 接受，接受。 Q]] −→ CJ[0] CJ[[CJ[P]] CJ[Q]]1 324C1−→CJC2−→C3C3−→CJ[C1[C2[退出a.P]]C3[排出a.Q]]−→[CJ[P]] [CJ[0]CJ[Q]]21 3C1−→CJC2−→C3C3−→CJC4−→CJC1 [C2[merge- a. P]] C3 [C4[merge+ a.Q]]−→CJ[0] CJ[CJ[P] [Q]]1 3 24环境之间的沟通C1−→CJC2−→CJC1[a！{b}。 P]C2[a？{c}。 Q]−→CJ[P]CJ[Q[m/p]]12C1−→CJC2−→C3C3−→CJC1[a！{b}。 P]C2[C3[a]？{c}。 Q]]−→CJ[P]CJ[CJ[Q[m/p]]12 3C1−→CJC2−→C3C3−→CJC1[C2[a！{b}。 P]]C3[a？{c}。 Q]−→CJ[CJ[P]]CJ[Q[m/p]]1 23C1−→CJC2−→C3C3−→CJC4−→CJC1[C2[a#！{b}。 P]]C3[C4[a#？{c}。 Q]]−→CJ[CJ[P]]CJ[CJ[Q[m/p]]1 23 4在上下文中执行：结构一致性：C−→ CJP−→QC[P]−→CJ[Q]P−→Q（νa）P−→（νa）QP−→QP<$Q Q−→QJQJ<$PJP−→PJ见图14。BioAmbients的反应关系如图14所示，活跃的上下文被淡化了，系统地应用这些模式可以让我们完全专注于redex和contractum的高级结构，而上下文则方便地隐藏了redex成分和反应的细节最后，选择（iii）完全将递归的概念与活动求值上下文的概念分开。因此，递归很容易以通常的方式处理，即使用结构同余来展开递归过程，必需的.5相关工作使用求值上下文来表达进程演算的语义并不是一个新的想法。Berry和Boudol [2]使用程序上下文来表示构成CHAM中语义等价基础的任意测试实例。后来的作者，如米尔纳[13]，使用了类似的（派生的）过程上下文的概念，主要是为了将等价扩展到同余。一些作者，如Godskesen，Hildebrandt和Sasone [6]的移动资源演算，也使用类似的派生概念（路径上下文，评估上下文，资源上下文等）。以确定结石的实际反应关系。然而，在所有情况下，所涉及的语境概念都是（标准的）静态概念，没有一位作者讨论语境的概念。[P]−→[Q]H. Pilegaard等人理论计算机科学电子笔记175（2007）5769一般选择与平行性相结合的问题休厄尔[20]对语境的使用截然不同。他展示了如何自动地从各种重写语义中导出标记的转换系统，只要在反应发生时简单地使用合适的上下文作为转换标签。这允许操作等价物，如反应语义所提供的，在（大概）更好的标记设置中进行研究。所涉及的上下文概念与我们的上下文概念无关，并且根本不考虑具有选择的演算。Larsen [8]使用配备了结构化操作语义的上下文来定义上下文相关等价的概念。Larsen和Xinxin [9]将其扩展为组合性的概念，该概念允许将组合系统的Hennesy-Milner属性分解为子组件的联合属性。这种对活动上下文的使用随后被Sands重新应用到函数式语言领域[19]。在所有情况下，在某种意义上，上下文都是主动的，但相关的语义是使用反应语义学努力避免的复杂标签语言来定义的，而且，在目的上，这种方法与我们的方法无关。6结论我们已经发展了主动求值上下文的概念，它允许化学抽象机[2]风格的反应语义被定义为比以前考虑的更大的一类过程代数根据之前关于CCS反应语义的工作[13]，我们将我们的方法与更经典的结构操作语义方法[11]进行了比较，并证明了当考虑封闭进程表达式时，这两种类型的语义是一致的这一结果表明，积极的评价语境的概念构成了一个健全的反应语义学的方法为了说明我们在更具表达力的演算上的方法，例如那些为了满足复杂领域领域特定建模的需求而出现的演算，我们为Regev和Cardelli的全面BioAmbients演算[ 18 ]的扩展提供了完整的反应语义由此产生的语义有两个属性，我们发现非常令人鼓舞。首先，实际定义它的过程是高度系统化的，因此很容易。其次，我们发现，它是可比的优雅Regev的原始语义。这表明，积极的评估上下文的概念也构成了一个明智的反应语义学的方法因此，我们认为，主动评价语境构成了一个合理和明智的方法来定义反应语义一般。然而，我们只能通过将其他以新方式结合各种特征的高级微积分应用于该方法来充分证实这一主张。70H. Pilegaard等人理论计算机科学电子笔记175（2007）57引用[1] 伯格斯特拉，J. A.和J. W. Klop，通信过程的代数，在：CWI研讨会，数学和计算机科学（1986年），pp.89比138[2] Berry，G.和G. Boudol，The chemical abstractmachine，POPL81-94.[3] 卡尔代利湖，Bioware语言，在：A.赫伯特和K. S. Jones，editors，Computer Systems：Theory，Technology，and Applications - A Tribute to Roger Needham，Monographs in Computer Science，Springer，2004 pp. 59比65[4] 卡尔代利湖和A. D. Gordon，Mobile Ambients，Theoretical Computer Science240（2000），pp.177- 213[5] Felleisen，M. 和D. P. Friedman，Control operators，the SECD-machine，and the λ-calculus，in：M. Wirsing，编辑，Formal Descriptions of Programming Concepts III，North-Holland，1986年。193-219[6] Godskesen，J.C.，T. Hildebrandt和V.Sassone，移动资源的演算，在：L。Brim，P. Jancar，M. ir Kretinsky和A.在Kucera，editors，CONCUR 13272-287。URLciteseer.ist.psu.edu/article/godskesen02calculus.html[7] 霍尔角A. R.，通信顺序进程，Commun。ACM21（1978），pp.666-677。[8] Larsen，K.G.，一个上下文相关的等价过程，理论。Comput. Sci. 49（1987），pp. 185-215[9] Larsen，K.G. 和L.Xinxin，Compositionality through an operational semantics of context，Journal of Logic and Computation1（1991），pp.761-795。[10] Levi，F.和D. Sangiorgi，控制环境中的干扰，在：Proc. of POPL352-364.[11]米尔纳河，“A Calculus of Communicating Systems,” Lecture Notes in Computer Science Vol. 92,Springer-Verlag,[12] 米尔纳河，“Communication and Concurrency”，Prentice-Hall，Inc.，上鞍河，新泽西州，美国，1989。[13] 米尔纳河，[14] Nielson，H. R.，F. Nielson和M. Buchholtz，Security for mobility，in：FOSAD 2001/2002，LNCS2946， Springer，2004 pp. 207-265[15] Plotkin，G. D、A Structural Approach to Operational Semantics，Technical Report DAIMI FN-19，University of Aarhus（1981）.URLciteseer.csail.mit.edu/plotkin81structural.html[16] Plotkin，G.D、个人通信给尼尔森，奥胡斯（1981年）。[17] Regev，A.，“计算系统生物学：生物分子知识的微积分”，博士。论文，特拉维夫大学（2003年）。[18] Regev，A.，E. M，Pamina，W.西尔弗曼湖Cardelli和E.Shapiro，BioAmbients：An abstractionfor biological compartments，Theoretical Computer Science325（2004），pp.141-167.[19] Sands，D.，Towards operational semantics of context in functional languages，in：Proceedings of the6th Nordic Workshop on Programming Theory，1994，pp. 378-385.网址citeseer.ist.psu.edu/68354.html[20] Sewell，P.，从重写规则到互模拟同余，理论计算机科学274（2002），pp。183-230URLciteseer.ist.psu.edu/sewell98from.html