12《理论计算机科学电子札记》68卷第1期（2002）网址：http://www.elsevier.nl/locate/entcs/volume68.html20页马可踢1爱丁堡大学信息学系，爱丁堡EH9 3JZ，苏格兰，英国电子邮件地址：mk@dcs.ed.ac.uk定时进程摘要在前人工作的基础上，本文描述了两种为时间进程定义“行为良好”操作语义的句法方法。在这两种情况下，语义规则是从行为comonads的抽象操作规则，从而确保一致的结果。 的首先，一个轻量级的尝试，在示意性规则中，被示出是合理的，即，如[8]中所介绍的那样，确实可以归纳出抽象的规则。然后 ， 第 二 种 格 式 ， 基 于 一 种 新 的 和 非 常 普 遍 的 抽 象 规 则 ， 共 同 的 SOS（CSOS），提出了使用Meta规则，也是完整的，即，它描述了定时过程的所有可能的CSOS规则1引言在他们的论文[15]中，Turi和Plotkin提出了Plotkin的结构操作语义学（SOS）[12]的数学理论，使用了单子在单子上的分配律[13]和这种律的双代数为了对抽象操作规则建模，他们考虑了类型(1)（IdB））BT对于函子概念和B的签名和（一步）行为，分别，和T的单子自由生成的（对应的术语超过签名）。结果表明，抽象规则（1）诱导一个分布-T对B上的余自由共单原子的定律（定义见，例如，[14]）。利用这个定律的双代数，他们能够获得共代数B-互模拟的抽象同余结果[1]（在B保持弱拉回的技术假设下）。对于行为函子的特定选择，他们还表明，由此产生的抽象规则（1）精确地对应于研究充分的GSOS格式中的具体规则[4]。因此他们的方法提供了一种概念上的解释1 这项工作得到了EPSRC资助GR/M56333的在CC BY-NC-ND许可下开放访问。踢13为什么互模拟是GSOS语言的一致性。这表明，在有利的情况下，通过仔细分析（1）中表达的约束，可以从抽象规则中推导出句法格式，这些约束源于所选择的行为和规则的自然性。最近，这导致了概率转移系统的GSOS风格格式的发现[3]。以类似的格式作为最终目标，[8]展示了如何调整[15]的方法以适应时间过程和时间过程演算的时间规则，以时间CCS（TeCCS）[10]为主要示例。这是通过从文献中提取时间和时间过程的抽象描述作为时域（特殊类型的幺半群，例如，N或R0）和定时跃迁系统（TTS，具有适当限制的跃迁关系以说明时间流逝的特定性质的标记跃迁系统）。一个重要的结果是，对于一个新的演化共单子E，TTS与（Eilenberg-Moore）余代数是相同的. 更抽象地说，需要在[15]的双代数框架内容纳演化comonad的余代数， 发送一般行为comonads的抽象规则，对应于“全局”行为，或“大步”语义，与“局部”行为相对，或“小步”语义，由行为函子描述。[8]中提出的解决方案采用了类型为(2)E）E（Id+）关于共聚单体E的结构，即，证明了规则（2）分别与E的数和余乘有关的两个图。这些要求成为必要的，因为E不是cofrely产生的，一次给出一个完整的帐户的所有时间转换的过程，不像cofree的情况下，原子步骤迭代，而不产生额外的约束。在具体规则一级，这些新的约束条件对应于规则集的全局条件，而不是对局部条件起作用的GSOS条件，即，规则，基础。满足这些条件的抽象规则（2）则确实导出了E上自由单子的分配律。作为一个应用，它表明，（时间）规则的TeCCS可以用这种方式表示，因此，E-互模拟（由时间互模拟，一个非常自然的概念等价的TTSs）的同余结果得到。此外，在[8]中表明，对于离散时间的特殊情况（具有时域N），演化余单子实际上是从函子余自由生成的。因此，应用[15]的机制，至少获得了这种情况下的语法格式，留下了用于任意时域的格式的推导本文的目的是通过提出两种不同的方法来缩小这一差距，在一般情况下，语法上指定行为良好的操作语义的定时进程。 在这样做时，假设（如[8]）时间规则和动作规则之间没有干扰，因此再次仅讨论时间规则，因为动作规则踢14通常只是GSOS规则已经在[15]的框架中设定，因此无需在此考虑。该文件的组织如下。在x2之后，它包含了对[8]中必要背景的简要介绍，x3引入了具有时间变量的示意性规则形状，允许通过实例化具有具体时间值的变量来均匀地导出时间转换（如所做的，例如，在操作语义的TeCCS），和容许运营商组成的speci c组合，这样的形状。这些构成了描述定时过程行为的一种合理方式，即， 容许算子确实导出了类型（2）的抽象规则，这些规则另外考虑了E的结构。因此，时间bisimulation是自动建立作为一个同余，这些运营商，这是足够强大的，以涵盖TeCCS的时间规则。因此，这就给出了文[8]（以及原文[10]）中的同余结果的一个新的证明。然而，它们是不完整的，因为有抽象规则的简单例子，如（2）中关于E的结构，但不是由允许的算子诱导的。即便如此，该方法提供了一种易于使用的，系统的方式来描述行为良好的规则，定时过程，表达能力足以包括最有趣的运营商从文献。接下来，x4为任意行为comonadD提供了非常强大的抽象操作规则，(3)D）DT这种共同的SOS（CSOS）结合了（1）和（2）的元素，但严格来说为了保证CSOS规则像以前一样导出T在D上的分配律，规则再次必须尊重D的结构，由于表达能力的增加，这导致抽象规则上的更复杂的全局条件（3）。CSOS的一般性然后通过表明CSOS规则尊重D的结构已经等价于给出完整的分配律TD）DT来证明，TD）DT是自由生成的单子T的最一般的抽象规则，从而扩展了[13，9]的结果。最后，x5给出了一个完善的格式，用于从用演化comonad实例化的CSOS规则派生的定时过程，以使用nite集的nitaryMeta规则为代价，在具体和抽象规则之间建立一对一的对应关系。这基本上是由于演化comonad描述定时过程的演化，一般来说，在夜间域。为了给这样的过程一个完整的表征（与行为comonads的“全局行为”解释相结合），需要在nite许多前提，和nite许多可能的域需要在nite许多规则。来自x3的容许算子包含在更一般的格式中，从而为大多数（如果不是全部）重要情况提供了successently具体的描述。踢15转变关系P不P满足以下公理，其中2赋时过程本节简要回顾了[8]中的一些定义和结果定义2.1（i）时域是一个交换幺半群T =（T;+;0），对所有s; t; u2T，满足消去规则s+t= s+ u）t= u，其诱导前序定义为tu，（9s）： t+s=u是一种线性秩序。(ii) 时间转换系统（TTS）是标记转换系统（LTS）（P;T;），其中P是一组过程，T是时域，并且pt0 0p表示（p; t; p）2：（确定性）p不 p0^ptp00 ）p0 =p00（零延迟）（连续性）0pppt+u p0，（9p00）：p不p00上p0(iii) GivenTTS（Pi;T;i），i2f1;2g，关系RP1P2是T上的（长）时间互模拟，如果（p1;p2）2R对所有t2T蕴涵pt00t0 0 011p1）（9p2）：p22p2^（p1; p2）2Rpt00t0 0 022p2）（9p1）：p11p1^（p1; p2）2R为了获得由TTS表示的定时过程的共代数描述，引入了以下进化概念定义2.2设T是一个时域，X是一个集合. X上的T-演化是满足两个公理的部分函数e：T * X，对于t; u 2 T：(4)e（0）#(5)e（t+u）#）e（t）#其中（：）#表示部分表达式（：）被定义（并且，双重地，（：）”表示表达式的不必要性X上所有T-演化的集合记为EX=ETX.给定一个函数f：X！ Y，de ne the map Ef：EX！E7！好的。这最后一个定义使E=ET成为集合上的一个内函子，集合和全函数的范畴，但更多的是真的：踢168>e+t （一）：X命题2.3函子E是集合上的一个余单子，其计数和余乘由下式给出：“X：EX！X; e 7！ 中文（简体）DF前 ：EX！E2 X;E 7！测试：undefife（t）“而E的（Eilenberg-Moore）余代数恰好是TTS。此外，余代数E-互模拟[1]（推广到余代数的情形）是时间互模拟，并且E保持拉回.定理2.4设是集合上的闭函子，使得集合上的自由单子T存在.此外，假设：E）E（Id+）是关于E的结构的自然变换，即，满足“-和”-图（6）EzE（Id+）EzE（Id+）““ID+密码公司简介公司简介czINRzId+E2zE（E+E）ZE2（Id+）对于fDF=E[ Einl; ]. 然后归纳出一个分配律：TE）ETmonadT over the comonadE.定理2.5TeCCS的时间规则可以用一个自然变换来描述，如Thm.2.4，它尊重E.由于E特别保持弱拉回，[15]中的`-双代数理论适用于TeCCS-情况，允许自动获得以下良好建立的结果：推论2.6时间互模拟是TeCCS的同余3定时过程本节介绍了一种简单的方法，使用示意性规则在任意时间域上指定定时进程的行为良好的操作语义：规则仅包含由时间变量标记的时间转换，而不是具体的时间值。然后，为了导出具体的时间转换，这种规则中的时间变量必须根据规则的适用性用实际值为此，引入了用于确定时间转换的某些示意性规则形状，并且仅允许这些规则的某些组合作为用于描述具体操作符的容许操作符。因此，不是一种“格式”，E=F踢17不不（x）xK不这种方法实际上只是产生了一系列“运营商蓝图”。为了描述时间过程，容许算子必须包括时间参数化算子，即，除了通常的过程参数之外，还具有时间作为参数的算子。为了简单起见，容许算子的集合仅考虑至多一个时间参数的情况在推导原理性规则时，TeCCS的时间规则作为指导性示例，特别是TeCCS的time prexing（t）：p，对于时间t6= 0和过程p，是时间参数化算子的原型。因此，容许算子包含TeCCS的时间规则，但也包含[11]中的附加规则合理的容许运营商的建立表明，容许运营商确实引起自然的转变，在Thm。2.4，而完备性的失败则通过给出一个抽象规则不能用容许算子表示的简单例子来证明.最后，一种方法，使示意图的形状有点更宽容的讨论，考虑他们相对于时域。在本节的其余部分中，设V是可数变量集，并且DF设T为任意时域，记为T> = T n f0 g。注意，时间以下规则形状中的变量仅允许在T>范围内变化。 是0因此无法推导出 - 过渡。 这种限制的原因是（6）中的“-图”已经确定了这种跃迁的目标（见Prop.3.4的证明）。请注意，潜在的时间参数也不能具有值0。此外，规则中出现的所有变量必须是不同的，因此每个规则形状都应该是GSOS规则的限制：定义3.1设是一个签名，2是一个函数符号;对于不同的xi2V和适当的ari n2N，s;t时间变量，记为x =（x 1 ;：; x n），其中If 1;：; ng，1jn，使得j62I。那么，可能的规则形式是以下类型的GSOS规则：(i) 由形状规则定义的标准运算符（一）（十）（十）xt0t0（B）1X1xnxnxt0（十）（x0）不（Cj）Jxj;（81Kn）：k6=j）x k6的t0J(ii) 由形状规则定义的时间参数化算子x0的fxx0 ji2Ig;（81kn）：y=如果k2i我我（tAI）Kxkif k62 I不（x;t+s）（y;s）（踢18J不我我不Sfx x0 ji2Ig（tBI;j）t（x;t）xjfx x0 ji2Ig;xx0(tCI;j）iijjt+s（x;t） x0的注意，对于常数c，即，一个函数符号c为0，两个形状（A）和（B）变得相等，并且不可能有形状（C j）的规则。定义3.2设是一个签名，设2是一个元数为n2N的函数符号.然后，除了完全没有规则的情况外，可容许算子如下所示。对于标准操作员：(i) 对于arityn= 1一种形状规则（A），或一种形状规则（B），或一个形状规则（C j），其中j =1(ii) 对于arityn6= 1一种形状规则（A），或一种形状规则（B），或一个形状规则（B），对于每个1Jn一个形状规则（Cj）对于任意元的时间参数化算子，下列算子是可容许的：对于某个If1;：;ng，有一个形状为e（tA I）的规则，或每个形状（tA I）、（tB I;j）和（tC I;j）都有一条规则，匹配If1;：;ng和1jn，使得j62I再次对于常数c的情况，注意，唯一的非平凡（即，由至少一个规则形状组成）容许算子由一个规则形状（A）或等价地（B）的情况给出，参见前一句话。例3.3 TeCCS的所有运算符都可以用上述容许运算符建模，例如：(i) 无进程0和操作前x *没有规则;(ii) 延迟前x_n：一个形状规则（A）的一元情形(iii) 强选择+和平行合成j：一个形状规则的二元情况（B）(iv) 弱选择：一个形状规则（B）和两个形状规则（Cj）的二元情况j= 1和 j=2各一个;(v) Time-prexing（t）：对于t2 T>：形状（tA I）、（tB I;j）和（tC I;j）中的每一个的一元情况，其中I=;且j =1。本节的主要结果表明，定义3.2中的容许算子为时间过程提供了一个合理的操作语义：踢192>：（22undefife1（t）“_e2（t）“！2 ！12命题3.4让成为一个签名，2n元函数符号。如果的时间规则可以由上述容许算子的任意一个来描述，则它们导出一个映射[[ ]]：（EV）n！E（V+ V）在V中的自然性，它尊重E的结构。证明（草图）证明是TeCCS的强选择+的情况下的例子。 如前所述。3.3，它的语义是由一个二元规则定义的 （B）转换为[[e +e]]=t2 T：（e1（t）+e2（t） ife1（t）#^e2（t）#对于两个演化e1;e22E V。再次注意，该映射不是针对t= 0，因为规则形状不能用该值实例化。然而，（6）的“-图”表示方程的有效性[[e1+e2]]（0）=e1（0）+e2（0）因此，简单地把这个作为[[e1+e2]]（0）的定义，自动地使“-图交换。综合起来，这产生了良好的地图[[+]]：（EV）2！E（V+ V）;[[e1+e]]=t：（e1（t）+e2（t） ife1（t）#^e2（t）#undefife1（t）“_e2（t）“此外， [ [+ ] ] 的（6）式的判别式，如以 下 计 算 所 示。首先， 映射<$X+X<$[[+]的结果，即围绕图的右下路径[[e+e]]=t：（e1（t）+e2（t）如果e1（t）#^e2（t）#^X+X8>u：（e1（t+u）+e2（t+u）如果e1（t+u）#^e2（t+u）#12如果e（t）#^e（t）#t：undefife（t+u）“_e（t+u）“1 2undefife1（t）“_e2（t）“映射E[Einl;[[+]][[+]]EX（+），c或依赖于图周围的另一路径，使用以下事实得到以下映射：[[e +e]]+[[e+e]]=t：（e1（t）+e2（t）ife1（t）#^e2（t）#=t：（e1+t）+（e2+t）ife1（t）#^e2（t）#undefife1（t）“_e2（t）“E[Einl;[[+]！undefife1（t）“_e2（t）“1>undefife1（t）“_e2（t）“11undefif_测试：u：（e1（t+u）+e2（t+u）ife1（t+u）#^e2（t+u）#ife（t）#^e（t）#>12图中的路径）导致与应用规则两次相同的过程=t：undefife（t+u）“_e（t+u）“1 2>undefife1（t）“_e2（t）“因此，这两张地图是相等的，而且图是互换的。最后，所有的规则形状都服从GSOS变量条件，这一事实自然地得出参见。在证明[15，Thm。1.1]。2注意，在这个证明中说明了图的直观含义+应用规则一次，- 过渡（以右下角t u首先导出到中间状态的过渡，然后导出-另一条路（另一条路）换句话说，该图表示时间连续性的基于规则或基于推导的版本。现在，通过组合所有操作符2的映射[[]]来实现合理性：定理3.5如果一种语言的时间规则只使用上述允许的算子，则它们引起关于E的结构的自然变换E）E（Id +）。除了TeCCS的时间规则之外，在文献中还有其他可以使用容许算子描述的算子。例如，在一个示例中，不考虑超时操作符P。q来自[11]，具有时间规则t0t t0pp0;t0 <不pp0pp0;qq0tt0tt0tttt+t0p. qp0 . Qp. Q Qp.Qq0不Intueland，p. q在时间t之前的行为严格类似于p;那么在时间t，切换到Q，简单地丢弃P：如果P等待太久，即，如果在t个时间单位内没有执行其预期的任务，则它会被“超时处理程序”q抢占。然而，请注意，p确实必须等到抢占点才能使超时生效：如果p由于某种原因不能空闲至少t个时间单位，q永远不会被激活。事实上， 0或者，作为血液时间规则（同样，t仅在T>范围内）：不（十）0（x）检查[[ ]]是自然的并且尊重E的结构是很简单的，但是，对于6 =0，规则不测试任何规则形状，因为最上面的运算符在规则的结论中被改变（从到0）。对容许算子进行这种限制的原因是图。直觉上要求规则满足连续性，在最上面的操作符中的变化将导致问题，特别是在操作符之间的循环依赖例如，假设有一个时间转换，从一个以作为其最高运算符的项到一个以0为最高运算符的项，反之亦然;一旦包括这样的情况，似乎几乎不可能保证语法此外，所有相关的运营商从文献t踢22（不格式，所以它看起来足够一般。此外，经过反复尝试，似乎更宽松的规则形状或运算符格式总是使良好的定义或图无效。3.1重新制定规则尽管可以说表达得足够好，但可容许算子并不像它们所能达到的那样普遍。作为一个说明性的例子，考虑以下“速度减半”运算符，如一位匿名裁判所建议的：（七）不p p0（p）t+t（p0）这个操作符可以用函数[[ ]]来描述：EX！E（X+X）e7！t： （e（t）） if 9 u：u + u =t ^e（u）# undef否则一般来说，这不是很好的定义：对于T =N，[[ ]]可能允许导出2-转换（在e（1）#的情况下），但永远不会导出1-转换（在那里，不存在u 2 N使得u + u = 1），因此演化公理（5）对[[]（e）不成立。然而，当在时域R 0上考虑时，[[]]是自然的，它属于类型（2），并且它尊重E的结构。因此，对于时域R 0和特定时间变换t7！t+t，（7）会产生一个行为良好的算子。 这可以概括为在下面的试探性发展，允许规则形状参数化的时域T和“良好的”转换T！T.令f：T！T是么半群同态。 f的像是集合dff[T]=fs2 T j 9t 2 T：s=f（t）g;它必然是T的子幺半群，因此非空，始终包含0。T上的一个序理想是T的一个向下闭子集I（关于T上的诱导预序，参见。Def. 2.1），即，t 2 I和u t隐含u 2 I。现在假设f：T！ T是一个单射幺半群同态，其象是一个序理想。 第二个条件是，如果存在st2 T使得f（st）= t和ut，那么也存在su2 T使得f（su）= u。给定这样一个f，下面的规则形状就构成了关于T的容许算子：Xx0的（x）f（t）（ x0）利用f的内射性，得到了它的反函数f1：f[T]！T存在，并且通过附加的性质，也是一个单射同态，因此上述规则踢23F、、.得双曲余切值.不undefiff1（t）“_e（f1（t））“可以转化为精心设计的地图（（e（f1（t）iff1（t）#^e（f1（t））#这也尊重E.对于N，只有这样的f是单位函数，而对于R 0，我们猜想，只有功能的形式t 7！ 对于r 6 = 0的r t（包括对于r = 1的恒等式，以及对于r = 2的等式（7））满足所有条件，即， 仅允许以恒定因子加速/减速。 它仍然有待调查，在多大程度上，这样的功能f可以使用在以前提出的规则形状，包括必要的推广到n元的情况下。4Comonadic SOS从更抽象的角度来看，本节现在给出了任意beh的抽象规则的一般描述，该beh是基于类型（3）的自然变换的vourcomonadD=（D;“;n）和自由生成的语法2，因此具有比（2）更大的表达性，这反过来形成了前一节的示意格式的基础。（3）的表达能力的增加需要对规则进行更强的假设，以便它们尊重comonadD的操作。定义4.1让;F是内函子，自由生成具有自由代数结构的单子T =（T;;）：T）T.给定一个自然变换：F）FT，de ne `：TF）FT作为唯一的映射，使得下面的图可交换（通过T的自由度获得）：(8)FZTF，sTF、、、 ."“F，.zczFTFFT2，sczFT我们称之为 由 。命题4.2令; F; T和`be如定义4.1所示。 则：TF）FT是单子T在函子F上的分配律。使用`，现在可以制定条件，在这些条件下，如（3）中的规则尊重D的结构：2通过使用任意（语法）单子T来对偶这种方法，例如，在[15]中，B是一个单步行为的内函子，但它与[5]密切相关，在[5]中，利用T-代数范畴上的B-余代数，考虑了所谓的结构化转移系统（其中状态集被赋予Te 7！测试：F踢24z定义4.3设T为定义中的T。4.1，和de ne自然transforma-dfTby=0. 此外，设D=（D;“;n）是一个commonad，D）DT是具有诱导分配律的自然变换（D）T的DT（被视为闭函子）。如果下面的两个图（再次分别称为“-图”和“-图”）互换，那么就说它尊重了comonad D的结构：（九）DzDTD DT““TT公司简介zTD2ZDTDD` zD2T然后通过一个自然变换给出D的抽象共单元SOS（CSOS）规则：D）DT关于D的结构。定理4.4假设：D）DT考虑了comonadD=（D;“;”）的结构。 则诱导分配律：TD）DT是单子T在共单子D上的分配律。Thm. 4.4指出，抽象的CSOS规则诱导分配律的自由语法（任意）行为comonadD。因此，它在闭函子F是comonadD的情况下推广了Prop. 4.2的结果，使得规则尊重comonad结构。这也是一个比Thm更一般的结果。2.4，因为类型（2）的每个自然变换都可以扩展到类型（3）的一个变换，但反之亦然。[15]的主要结果，即抽象的GSOS规则（1）在cofree行为上导出自由句法的分配律，也被Thm所覆盖。4.4当在cofree comonad打开的情况下实例化D行为函子B，例如，对于离散时间上的定时过程，其中DF如果演化余单子是由BN=1 +(see[8]）。在下面，抽象的CSOS规则的一般性变得更加精确：这样的规则实际上已经等价于自由单子在comonad上的分配律，提供了Thm的逆四点四引理4.5设F和T如上。 则F）FT型自然变换与分配律一一对应：TF）FT的单子T上的endofunctor F。证明（草图）对应关系定义如下，留给读者证明两个映射是相互逆的。 给定，使用诱导分配律`：TF）FT;Prop. 4.2然后表明`尊重单子T的运算。 在相反的方向上，给定`：TF）FT，考虑“="F： F）FT。2用D代替F，并添加尊重D的结构的要求，引理4.5中的一一对应扩展到在余单子上分布自由单子：D踢25我i=1i=1我定理4.6设T和D如上。 然后，在抽象的CSOS规则：D）DT和分配律之间存在一一对应关系自由生成的单子T在共单子D上的：TD）DT。证明（草图）假设（9）允许推导出导出的分配律是单子在余单子上的分配律（不仅仅是内函子），而在另一个方向上，如果将单子分配给余单子，则满足（9）中的两个图。因此，来自Prop的通信。4.5扩展到自由生成的monads和comonads的情况 2直觉，Thm。4.6指出，在T是自由生成的情况下，（9）中的条件恰好是D）DT型抽象规则的必要和充分条件，允许应用[15]的双代数方法;换句话说：在T是自由生成的情况下，没有办法使用严格更具表达性的抽象规则并仍然获得分配律TD）DT请注意，如[8]中所述，抽象CSOS规则（3）和[8]中的规则（2）形成抽象规则的类型层次的极端情况，在全局约束（如（9）或（6））下，确保获得T在D上的分配律。5定时进程作为CSOS规则的一个应用，本节给出了演化共同名词E的CSOS规则的句法特征。该格式基于Meta规则的概念，元规则将作为innite sets of innitaryrules的方便缩写。即便如此，该格式仍将包含许多这样的Meta规则，以完全捕获所有可能的抽象规则。在下文中，x是非平凡时域T，因此T具有无穷基数，参见[8]。此外，设V是一组变量，其中jVj = jT j，并且对于每个n，1x是V的n元枚举，没有重复：对于每个1 i n，不相交子集Vi =f x tjt2T g V。 对于一个集合X和一个演化e2EX，e的定义域和值域是dom（e）=ft2Tje（t）#gT和rng（e）=e（T）X，分别对e进行扩展 =（e1;：;en）2（EX）nbydom（e）=（dom（e1）;：;dom（en））和rng（e）=Snrng（ei）。 如果e2ETX是项的演化e的变量vars（e）都是在rng（e）中出现的变量TX. 对于元组e2（ETX）n，de nevar s（e）=Sn var s（e）。一个元组e 2（EX）n是泛型的，如果所有的e我我是单射的，并且具有成对不相交的值域。对于n2N和某个n元整环，该整环的n元标准元组由n个演化给出.i这样，i有所需的域，它们的值如下所示：i（t）=x t2 V i V。在下文中，规范元组由表示。由于V上的n元枚举都不包含重复，规范元组是具有规范名称的通用元组.注意，对于e2（EX）n，存在具有相同域的唯一对应的规范元组2（E V）n。踢26n直观地说，通用元组在新格式中的作用与在GSOS规则中使用不同变量的作用相同，即，确保规则“匿名地”处理变元过程：尽管在不同的变元位置用相同的过程实例化规则当然是可能的，但是规则不能要求这样的标识，例如，只有当两个端点相等时才定义转换。 作为一般元组e的这种“anoi nymi ty”的结果，rn g（e）中的每个元素n t可以唯一地“追溯到”某个ei，并且规范元组是真正规范的：它们可以被转换为同一域的所有其他元组。引理5.1（i）如果e2（EX）n 是一个通用的元组和x2rn g（e），那么re存在唯一的1in和t2T，使得x=ei（t）。（ii）每个元组e2（EX）n，其中c或r是对应于一个anonial元组，导致一个唯一的映射e ：rn g（）！rng（e）使得E'e（i）='e i=ei.后来，'e 将被扩展到一个函数ty peV！ 通过将值任意赋给不包含在范围内的变量。定义5.2让成为一个标志，2是n元函数符号，e2（EX）和#2ETX.然后是形式的表达式（10）（e1;：;en）=）#是的Meta规则。在下文中，将t=#（t）2 TX写为t 2dom（#）。Meta规则 （ 10 ） 的 域 与 do m （ e ） 相 同 ， 并 且 它 是 通 用 的 （ 分 别 为canonical），如果e是演化的通用（canonical）元组。每个Meta规则（10）都是（innite）一组初始时间规则的缩写，范围在t2dom（#）上，格式为（十一）TTTIfei（0）ei（ti）jti2T^ei（ti）#g1in 中国（0）不jti2T^ei（ti）“g1in（e1（0）;：; en（0））t不有时缩写为（e）t，模糊了规则之间的区别规则的结论。请注意，每个Meta规则都包含参数行为的完整（或全局）描述，而不仅仅是对特定时间转换的存在或不存在的本地测试（如示意图格式）。 这与对行为comonads建模全球行为的解释是一致的。下面的开发将完全基于Meta规则，以使其更加简洁;所有这些都可以通过通信（11）使用标准时间规则来执行。定义5.3如果Meta规则（）=）#是规范的并且如果vars（#）rng（），则它是GSOS元规则。签名上的一组Meta规则是完整的（相应地，确定性）如果对于每个n元函数符号2和每个n元域，存在至少（至多）一个Meta规则。 一组确定性的、完整的GSOS Meta规则被称为可接受的。踢27紧接着，一个可接受的Meta规则集精确地包含使用术语“GSOSMeta规则”是因为每个诱导时间规则（11）是一个（抽象的）GSOS规则：所有i都有不相交的范围，因此在前提中发生的变量是不同的，特别是i（0）;更重要的是，由于vars（#）rng（），在某个t中发生的每个变量必须在前提中发生。请注意，此属性不依赖于规范，它也适用于var s（#）rn g（e）的泛型元组e su c h。 然而，正典名称用于保证精确的一一对应。 下列结果表明，Meta规则的容许集是自然变换E）ET的正确刻画.命题5.4Meta规则的每一个容许集合R都导出一个自然变换[[R]]：E）ET。（Sketch）De neamap[[R]]V ：EV！ ETV在所有的非线性元组上（可能是因为R是可容许的）由[[R]]V（（））=#iR包含Meta规则（）=）#. 这是我们定义的，并扩展到自然变换[[R]]，因为R中的所有Meta规则都是GSOS，然后使用引理5.1（ii）。 2命题5.5设：E）ET是一个自然变换。 然后归纳出Meta规则的容许集hh ii。证明（草图）通过（（）=）#）2hhiiiV（（））=#从V的值导出hh ii中的Meta规则。 单ce是自然的，hhii是可接受的。2下面的定理来自于使用规范元组来描述允许的Meta规则集。定理5.6两个结构R 7！[7][8][10] HH和II是相互逆的。因此，在Meta规则的容许集合和E）ET型自然变换之间存在一一对应。注意，在相应的条件下，对于Meta规则的容许集R和自然变换E）ET，分别有（（）=）#）2Ri[[R]]V（（））=#，V（（））=#i（（）=） # ） 2hhii. 该 格 式 的 下 一 个 目 标 是 （ 9 ） 中 的 “- 图 ” 的 基 于（Meta）规则的表征定义5.7Meta规则（e）=）#如果满足以下0=#（0）=（e1（0）;：;en（0））如果R中的每个元规则都是，则将Meta规则的集合R称为共点的简单的检查结果：定理5.8 Meta规则的可容许共点集与自然变换一一对应：E）ET还满足（9）中的“-图”.踢28我我最后的任务是给出（9）中的图的一个类似的特征，其中使用了映射E和`，后者是根据T来定义的。在下文中，对于特定参数，这些映射的值以V表示。因为规则的最后一个组成部分是在Thm中建立的对应关系的核心5.6，获得图和Meta规则（上的条件）之间的匹配定义5.9设是一个签名，2TX是某个集合X上的一个项。设f：X*Y是满足vars（）dom（f）的部分函数.则表示f （ xi ）在by[f]或[f（xi）=xi]中对xi 2 var（）的同时替换。 将此概念扩 展到e解#2ETX，写作#[f]或#[f（xi）=xi]来表示T Y上的e解，其在eact2dom（#）处的值是项t[f]，服从条件var s（#）do m（f）。引理5.10假设：是一个典型的n元元组，并且#2（ET V） n具有与;'E：V！ EV和'#：V！TV是从引理5.1（ii）得到的函数的（扩展），分别映射到λ和 λ;：E）ET是Meta规则的导出容许集R = hh i i的自然变换; i是签名，2是n元函数符号。然后，利用的自然性，人们得到以下特征：（i）EV（（t））=#[t]=#[i+t=xt]当且仅当V（（t））=#.（ii）T（（#））=#['#]=#[#i（t）=xt]当且仅当V（（））=#.定义5.11给定一个规范Meta规则集R，将R-派生的概念定义如下。F或2TEX和#2ETX ，写R`=）#如果有一个只使用以下两个规则的nite证明（其中，为了简单起见，省略了对T的单位和乘法的任何引用(i) 如果对于某个e2EX= e，则R`e=）e(ii) 如果2是n元函数symbol并且1;：;n2TEX，则fR`i=）#i;dom（#i）=dom（i）g1in （（）=）#）2RR`（）=）#['#]特别地，如果（（）=）#）2R，则R`（）=）#，因此可以将表达式R`（）=）#称为公理。注意，对于R-导子来说，R是可容许的并不一定引理5.12设R是Meta规则的一个容许集，=[[R]]是它对应的具有诱导分配律的自然变换。那么以下等价性对于2 TEX和#2 ET X成立：（`）X（）=#，R`=）#证明（草图）通过归纳的结构。出现了两种情况，如在`的定义中，它们由R-导子的两个相应规则来处理2踢29不不t+uuu直观地说，R-导子（或等价地，对于可容许的R来说，[[R]]）从一组规则中捕获可证明性的概念Meta规则只适用于只有一个函数符号的“简单”术语。由R-导子给出的归纳延拓决定了规则在复数项上的作用，迭代规则的应用（服从必要的替换）。对于容许R，R-导子描述自然变换。因此，当verR`=）#（或equivalently，`（）=#）时，必须保持vars（）vars（），其中vars（）是来自X的所有变量的适当定义的集合，这些变量出现在2TEX中。否则，“不可能是自然的”，其理由与表明全球SOS（Meta）规则引起自然转变的理由相同。定义5.13设R是一组规范Meta规则，一个签名，2是一 个 n元函数，（）=）#R中的一个元规则，且t;u2T. 则R称为连续的，如果以下两个陈述是等价的：（一）（）下一页t+u，以及（二）（）下一页t^R`t[]=）#0^#0
我的内容管理
展开
