分布式系统的定时器扩展：定时分布式π演算的类型系统和操作语义

理论计算机科学电子笔记164（2006）81-99www.elsevier.com/locate/entcs分布式系统的定时器1加布里埃尔Ciobanu和克里斯蒂安Prisacariu2计算机科学研究所，罗马尼亚学院大道。Carol 8，700505 Iai，Romania摘要我们处理分布式系统的时间方面，介绍和研究一个新的模型，称为定时分布式π演算。该模型对分布式π演算进行了定时器扩展，将通信信道转化为临时资源。分布式π演算描述了进程之间的相互作用，并限制了对资源的访问。我们通过考虑通道的超时计时器来引入时间约束。结合这些定时器的类型和位置，我们提供了一个正式的框架，能够描述复杂的系统与时间和资源访问的限制。给出了它的类型系统和操作语义。事实证明，时间的流逝不会干扰打字系统。 通过使用基于主题约简的方法，证明了新模型的合理性保留字：计时器、位置、打字系统、主题缩减1引言在本文中，我们使用定时器和研究它们的作用，在复杂的系统建模的分布式和移动过程。我们选择π演算[10]作为基础平台;这种形式主义非常适合基于通信过程的系统建模。 为了强调分布式系统中的空间方面，我们使用明确的位置概念。 进程之间的交互可以通过使用各种排序来控制。排序允许限制分布式资源的使用即定位的通信信道。π 演算的 位置和排序的 组合已经在[6]中给出; 得到的 演算称为分布式 π（Dπ）。在Dπ中，作者使用“类型”（而不是“排序”）来表达交互通道的某些功能。排序在π演算中用于定义交互模式;交互通道的排序定义了沿着该通道发送或接收的消息的类型。通过“过程之间的交互”，我们理解为“过程之间的通信”。通信信道被认为是固定资源CEEX项目47/20052电子邮件：gabriel@iit.tuiasi.ro和cprisacariu@iit.tuiasi.ro1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.07.01382G. 乔巴努角Prisacariu/理论计算机科学电子笔记164（2006）81在某个地方。通信是本地的，代码迁移用于将进程移动到相同的位置，以便沿着它们具有适当能力的公共本地通道进行通信。类型化系统允许通过用类型环境标记进程来限制对资源的访问，并限制可以沿着通道传输的消息。我们采用Dπ，通过减少连接到通信信道和信道类型的定时器来扩展它。新的形式主义被称为时间分布π-演算（tDπ），它是描述具有时间和资源约束的分布式系统的严格框架。通道上的计时器定义通信超时，通道类型上的计时器限制通道空房的每当信道或信道类型的定时器期满时，相应的信道被丢弃，并且相应地信道类型丢失。tDπ将时间约束与类型和位置相结合，以给出对具有时间受限资源访问的分布式进程之间的定位和定时交互进行建模的可能性。按照[4]中介绍的方法，我们证明了tDπ的类型系统在π-演算的等价和约化关系方面是可靠的.此外，时间不会干扰打字系统2tDπ的结构和语义通过在通信信道中添加定时器，沿着信道的通信在无限时间内不再可用（如在Dπ中）。如果在由计时器值确定的预定义时间间隔内没有发生交互，则过程进入另一状态。每个渠道都有两个选择：一个是当沟通完成时，另一个是当我们没有沟通时。通道计时器使用通道创建一次，但仅在通道变为活动状态（可用于通信）时启动。2.1tDππDπ通道a的语法通过用定时器Δt标记它而扩展;这意味着通道aΔt仅在一段时间内等待通信由定时器值t（即t个时间单位，因为我们使用离散时域）确定。输入和输出通信的语法使用一对进程（P，Q）。例如，输入表达式aΔt？（X：T）。当在Δt给定的时间间隔内在信道a上建立通信时，（P，Q）演变为P，否则演变为Q。在这个表达式中，考虑T类型的变量X只在P中有界我们考虑输入和输出通道的定时器。选择在输出中添加计时器的原因是，在分布式系统中，我们有多个客户端和多个服务器。这意味着输出进程（客户端）可以根据等待时间从一个服务器切换到另一个服务器。一般来说，一个输入过程等待一个资源，G. 乔巴努角Prisacariu/理论计算机科学电子笔记164（2006）8183X一个输出过程在一段时间内对资源进行操作，而一个输出过程在一段时间内对表1：tDπ的λu：：=x| a Δt l ::= x| Kv：：=bv| u | l| u@l|（v1，..，vn）X：：=x|X@l变量名称定时通道变量名称位置名称基值名称已定位的名称值元组变量定位变量P，Q：：=停止| P|Q| （ν u：A）P| 去L.P| u！你好（P，Q）| 你呢？（X：T）。（P，Q）|CUPM，N：：= M |N| （ν u@l：T）N终端合成通道限制移动输出输入复制组合定位限制| （X1，..，Xn）变量| l[[P]]r定位过程上表按顺序定义了tDπ的通道名称和位置名称、值、变量、进程和标记的已定位进程。对于输入表达式的变量X，Δt？（X：T）。（P，Q）我们还应该提供它的类型T，并且对于CableRestriction表达式中的通道名称u，我们必须提供它的通道A型（类型见第2.2节）。请注意，我们可以用变量x来代替通道名称（在Input 、 Output 或 LocatedRestriction 中 ） 和 位 置 （ 在 LocatedP 进 程 中 ，LocatedNames或Movement）。在输出通道上，进程可以发送通道名称（连同其计时器）、位置名称、变量名称、位于某个位置的通道（或变量）名称或值的元组注意，利用定位限制（ν a@k：T）N，我们指定新的私有信道a及其位置k。例如，在这个过程中，（ν a @ k：T）（l [[P]] |k [[Q]]）|k [[QJ]]信道a对于P和Q是私有的，并且位于Q.此外，QJ不具有关于信道a的任何知识，即使它也在位置k处运行。这意味着进程P在私有信道a上通信之前必须移动到位置k。还要注意，通道限制的语法只指定了专用通道的名称，而不是相关的计时器;这是因为限制只引用通道的名称进程之间的交互是通过输入和输出进程表达式给出的，这些表达式必须具有相同的通道名称;通道计时器在这样的交互中扮演次要角色。例2.1下面两个并行运行的进程可以沿着公共通道a进行交互。aΔt！你好（P，Q）|aΔtJ？（X：T）。（P J，QJ）−→ P |P J{v/}直觉上，在这样的交互之后，左边的过程演变为右边的过程输出进程（并行复合操作符左边的进程）在名为a的通道上发送值v，然后表现为P。当接收到值v时，在输入过程（并行复合运算符右边的过程）中，所有出现的绑定变量X都被PJ中的v替换。84G. 乔巴努角Prisacariu/理论计算机科学电子笔记164（2006）81通过将Δ t视为∞，允许在通道a上无限等待。输出过程表达式a∞！你好（P，Q）永远等待发送值v，模拟无时同步π演算中输出过程2.2分型系统每个被定位的进程被标记有类型环境T，类型环境T是由表2中的K表示的位置类型的集合。形式上，类型环境是从自由位置名称k到位置类型K的映射。位置类型K可以包含由κ表示的定位能力;这些能力可以表示使用信道名称的能力，其具有它们的相应信道类型Ak（k：A k），或者移动能力，或者信道限制能力（即，允许创建私人频道）newch.通道类型A可以包含以下通道能力一般由α表示：读取类型T的消息的能力rT，写入类型T的消息的能力wT，以及仅读取类型T的消息的能力rT。t型 可以包含元组（T1，.，T n）的类型对应于名称的元组和通道类型A1，.，A n@K对应频道名称a1，.，n位于类型K的位置。 B表示基本类型的集合。表2：类型系统和子类型关系类型：子类型：K：：=loc{κε}A：：=res{α}ΔtE：：= A| K|BT：：= E|（T1，...，Tn）|A1，.，A n@Kκ<：κa：A<：a：B 如果A<：BK：L如果<$λ ∈L：<$κ∈K：κ<：λ A：B 如果<$β ∈B：<$α∈A：α<：βA@K：B@LifK：LandA<：B功能：S：T如果I：Si<：Tiκ：：=a：A| 去|纽奇α：：= rT|关于我们|罗TrT<：rTjifT<：TJwS ： wSjifSJ ： SroT：roTJifT<：TJ在位置类型K中，我们可能只有go和newch能力的一个实例;它们分别表示进程移动到该位置的能力，以及在该位置创建私有通道名称的能力为了证明这一点，让我们考虑一个进程，它在其类型环境Γ中有一个通道名a，通道类型为res{rT，wTj，roTJ}。这意味着沿着这个通道a，进程可以接收类型T的消息，并发送类型TJ的消息。RO能力类似于R能力，区别在于接收到的消息的类型不被添加到进程的类型环境中。当沿着输入通道接收到名称时，G. 乔巴努角Prisacariu/理论计算机科学电子笔记164（2006）8185有能力恢复。有了可重写能力，我们可以描述这样的过程，它可以使用通过具有可重写能力的输入通道在消息中接收到的数据，只要在它们的类型环境中存在新数据的适当类型更准确地说，让我们考虑在位置k处的进程P，其接收所定位的信道名称b@k在输入通道a上的类型res{roT}。 所定位的过程k[[P]]r可以使用只有当新信道名b的类型环境Γ在位置k处包含b的相应类型时，才能在不产生错误的情况下进行通信，即，（k，b）的定义。 在第2.3节的末尾列出了误差，其中表9包含错误系统的规则。在Dπ中，资源被积累，但它们永远不会被丢弃。我们用Δt形式的定时器扩展了Dπ的通道类型。这些计时器定义了类型环境中通道类型的存在。计时器会随着宇宙时钟的每一个“滴答”（我们假设我们有一个宇宙时钟）。通信操作可以沿着通道执行，直到其类型上的计时器到期。过期后，通道功能将被丢弃，任何通信都将生成运行时错误。计时器与通道类型一起创建一次，当功能添加到类型环境中时，计时器被激活。在我们的方法中，一个进程可以移动到某个位置，并等待一段时间在特定的通道（固定的本地资源）上与一个互补进程建立通信为了限制进程执行的操作，有必要位置的能力和来自类型环境的通道的能力类型环境的一个示例是：r ={l：loc{a：A，b：B}，k：loc{a：AJ}}其中，我们用Γ（k）表示位置k的类型loc{a：AJ}，并且用Γ（l，b）表示位于l处的信道b的信道类型B。通过使用环境扩展明确了能力积累的过程。我们用Γ{k：K}表示用K型的新位置k扩展的环境Γ。此外，考虑到如上所述的Γ，我们可以通过以下方式扩展具有位于k处的新通道c的类型环境：r {c@k：BJ}={l：loc{a：A，b：B}，k：loc{a：AJ，c：BJ}}当一个进程接收到新的通道名称及其关联的类型时，新名称的功能就变得可用（被添加到进程的类型环境中）。作为示例，让我们假设一个进程通过具有读取能力的输入通道接收具有通道类型Bj的所定位的通道的名称c@k新通道的类型将添加到对应的位置类型k：loc{.. . }。这意味着现在流程知道了新的通道，并获得了通过积累的通道进行通信的能力c根据类型BJ。引入子类型关系（：）来比较类型环境。如果我们考虑一个新的整数形式，即r ={l：loc{a：A，b：B}}和rJ={l：loc{a：A}}，则根据表2第二列中的定义，我们有r<：rJ86G. 乔巴努角Prisacariu/理论计算机科学电子笔记164（2006）812. 比较类型环境Γ和ΓJ，我们可以看到具有更多能力的环境（Γ）是具有更少能力的环境（ΓJ）的子类型这样解释子类型关系的原因是，ΓJ比Γ更具限制性。子类型关系表示集合论中的子集关系的逆;如果我们将类型环境视为位置类型的集合，则上述关系变为ΓΓJ。我们推广了Dπ的部分交H算子和部分并H算子，新的渠道能力将持续增长。直觉上，部分交算子表现为集合论的并算子，而部分连接算子表现为交算子。 我们用a：−/∈K表示在位置类型K对于信道a，不存在信道类型A，使得a：A∈K。我们用γ表示任何定位能力的一部分。位置类型KHKJ的部分交算子是未定义的，当且仅当存在一个通道名a使得a：A∈K，a：AJ∈KJ和AHAJ是未定义的（参见表4中的通道类型H的定义）。表4：通道类型的部分满足运算符通道类型的部分满足算子HAJ）定义为：rT∈A andrT ∈AJandT HTJunifined roT ∈A androT∈AJandTHTJunifinedwS∈AandwSJ∈AJandSHSJunifinedrT ∈ A和w ∈ AJ和SJ：Tw <$S <$∈ A，r ∈ AJ和S/<：TJroT ∈ A和w ∈ AJ和SJw<$S <$∈A andro <$TJ <$∈AJanddS ∈AJ，r<$− <$/∈AJ和THTJ=不确定或不确定}{r|r∈AJ且T JJ= TH T J或r∈A和ro ∈AJ和r ∈AJ和TJJ=THTJ且THS=未定义或未定义}{r|r<$T<$<$∈ A且ro<$T J<$$>∈ AJ且r<$<$− <$/∈ AJ且T JJ= T\ΔT J或r<$T <$<$∈A和ro <$TJ<$$> ∈AJ和r <$S <$∈AJ和TJJ=T\ΔTJ和THS=λ或unfined}加上所有其他自然情况下，从交换A与AJ去除能力的方法是形式化的二进制减法运算，表3：位置的部分满足运算符K H KJ={γ|γ ∈ K或γ ∈ KJ}{a：A| a : A ∈ K and a : − /∈ KJ}{a：AJ|a：−/∈K且a：AJ∈ KJ}{a：AJJ|a：A ∈ K和a：AJ∈ KJ和AJJ=A H AJ}G. 乔巴努角Prisacariu/理论计算机科学电子笔记164（2006）8187使用连接运算符H（见表5）定义的算子\Δ，以及类似于集合论中定义的对称差分运算符\我们写\Δ来表示从第一个类型环境中删除第二个类型环境中包含的所有类型的操作。我们用E表示类型环境的集合。上面描述的减法运算符\Δ被定义为\Δ：E × E → E，其中Γ\ΔΓJ=ΓH（Γ\ ΓJ）。如果我们考虑两种环境r ={loc{a：A，b：B}}和rJ={loc{b：B，c：C}}，每个由一个位置类型和两个通道类型组成，然后通过应用减法运算符\Δ，我们得到r\ΔrJ=loc{a：A，b：B} H（loc{a：A，b：B}\loc{b：B，c：C}）=loc{a：A}一个进程如果其通道类型的能力为rouT，则只能接收T类型（或T的任何子类型）的消息而不会产生错误。当信道的类型被扩展为具有能力ro_T_J_j时，则该过程能够接收限制较少的类型T_J=T_H_T_J的消息。我们通过为恢复能力提供更高的优先级来解决恢复和恢复之间可能的冲突（因为它是比R更严格）。因此，当rT和roTJ重叠时，ro保持其类型，而r失去其类型以支持ro（即， T H T J/= 0）。当用新的能力扩展写入能力时，信道变得更限制，具有能力w<$SJJ<$其中SJJ=SHSJ。我们用r<$− <$/∈A表示不存在类型T使得r<$T<$∈A的事实。 符号w−/∈A和ro−/∈A的定义相似。表5：Join运算符K H KJ={γ|γ ∈ K和γ ∈ KJ}{a：AJJ|a：A ∈ K和a：AJ∈ KJ和AJJ=A H AJ}AH AJ={r|r <$T<$<$∈ A和r <$T j<$∈ AJ和T JJ= T H T J}你好|ro <$T <$<$∈ A和ro <$TJ<$<$∈ AJ和TJJ=T H T J}{w|w<$S<$<$∈ A且w <$SJ <$<$∈ AJ且SJJ= S H SJ}提议2.2i. （E，H）是交换幺半群; ii .（E，\）是交换群;三. H是环上的分配环，且（E，I，H）是环。证明很容易观察到H和\是交换的，并且空环境是单位元。H在\上的分布性可以通过将集合运算符转换为布尔运算符并使用真值表来简单地验证Q我们定义了一个清除函数，它根据时间的推移改变类型环境它减少通道类型的计时器，并删除计时器过期的类型它还删除了仅具有go功能的位置类型88G. 乔巴努角Prisacariu/理论计算机科学电子笔记164（2006）81>>Γ>定义2.3（函数）在标记的定位进程LPΓ的集合上，通过以下等式定义LPn（l[[P]]r）=l[[P]]rJ其中l可以是分布式系统的任何位置，从Γ获得ΓJ，使得每个通道lt都是{α}Δt，t>1且t/=∞是改变为{α}Δ（t−1），并且每个通道{α}Δ1是reminoved。 更重要的是，loc i ontypeloc{go}被移除。通过从Γ中移除信道类型，我们得到ΓJ，其中可能具有仅具有go能力的位置类型我们认为这些位置类型为空，因为唯一允许的动作是移动。即使我们在ΓJ中有k：loc{go}，并且一个过程的运动序列go k.go l.P，这个过程也可以简化为go l.P因为我们可以避免中间代码迁移到位置k而不丢失任何有用的效果。因此，从ΓJ中移除k：loc{go}。 移动到位置l的具有类型loc{go}的进程没有其他能力，因此当执行任何操作（通信或通道创建）时，它会引起运行时错误。为了模拟时间的流逝，我们使用一个时间步进函数φ，它定义在任意位置l上运行的进程集合Pl上。可能的通信在通用时钟的每个滴答执行;活动信道是那些可能参与这些通信的时间步进功能会选择在该时间点不进行通信的活动通道;被选择通道的计时器将减少一个时间单位。参与通信的通道与它们的计时器一起消失。在时间步进函数φ的定义中，为了简化表示，我们省略了输入和输出过程定义2.4（时步函数φ：Pl→ Pl）8aΔ（t−1）。（R，Q）如果P = aΔt。（R，Q），t >1且t/=∞>Δt>Q，如果P=a. （R，Q），t≤1φ（P）=>>：φ（R）|φ（Q） 如果P=R|Q（ν a：A）φ（R）若P=（ν a：A）RP否则我们还定义了一个带标记的时间步进函数φΔ，以处理缺失的类型。φΔ是使用局部函数φ定义的全局函数。将标记时步函数φΔ应用于标记定位过程（l[[P]]Γ），并通过应用清除来改变定位过程的类型环境函数定义2.5标记的时间步进函数φΔ：LPΓ→LPΓ通过使用φ：8l [[φ（P）]]'，若P = aΔt. （R，Q），t>1且t/=∞>Γ>或者如果P=aΔt>. （R，Q），t≤1>1φΔ（l[[P]]r）=>和Γ π：Γ（l，a）> φΔ（l[[R]]r）|φΔ（l[[Q]]Γ），如果P=R|Q>>（ν a@l：A）φΔ（l[[R]]Γ{a@l：A}）如果P=（ν a：A）R：l[[φ（P）]]'otherwise>G. 乔巴努角Prisacariu/理论计算机科学电子笔记164（2006）8189其中rJ是通过应用清除函数来获得的。tDπ的静态语义被定义为一组推理规则，这些规则描述了表达式及其相应类型之间的关系。 在本文中，我们认为类型环境是一个从自由名到类型的映射。类型环境与每个定位的进程相关联，以限制它可以访问的资源范围。 类型化规则描述了进程在其类型方面的行为。一个类型化系统被用来决定进程的良好类型性语法上我们写为ΓP，并说进程P相对于类型环境Γ是良好类型的。我们还写了ΓkP，并说P是在位置k处运行的良好类型。表6：打字系统（打字规则）过程（T-R）（T-RO）（T-W）rla：res{rT}ΔtΓla：res{roT}ΔtΓla：res{wT}Δtfv（ X） fv（Γ）=fv（ X） fv（Γ）=V：TΓ{X@l：T}{\displaystyle\pi}Γ►lPΓ►lPΓlQΓlQΓlQ你是谁？（X：T）。（P，Q）（T-NEWCH）你是谁？（X：T）。（P，Q）我来了！你好（P，Q）Γ（l）：loc{newch}a/∈fn（Γ）Γ{a@l：A}{lP}Γl（νa：A）P(T-R（新）（T-STR）Γ►lPΓlQls top，P|Q、*P(T-W（新）（T-GO）Γ（k）：loc{go}伊萨克山口我去。Pa：−/∈Γ（l）Γ<$lQ你是谁？（X：T）。（P，Q）定位过程a：−/∈Γ（l）Γ<$lQ我来了！你好（P，Q）（N-NEWCH）（N-RUN）ΔPΓ：Δ（N-SRT）ΓDMΓDNΓ（l）：loc{newch}a/∈fn（Γ）Γ{a@l：A}DNΓD l[[P]]ΔΓD0，M |NΓD（νa@l：A）N在表6中，我们给出了tDπ分型系统的规则。考虑规则（T-Rnew）和（T-Wnew），我们观察到来自Dπ的良型性的直观概念在tDπ中不再有效。在我们的演算中，我们接受带有缺失通道类型的标记定位进程（随着时间的推移，这些类型被删除），并且这些进程不会产生错误。为了说一个Δt！你好（R，Q）是良好类型的，相对于类型环境Γ在位置k处运行，以下语句应该成立：• rkv：T，这意味着v是位置k处的类型T的值;• 它意味着信道a存在于位置k处，并且可以在tJ个时间单位内发送类型T• 这意味着R和Q都是良好类型的，可以在位置K.对于一个带标记的定位过程k[[P]]Δ，其良型关系记为D90G. 乔巴努角Prisacariu/理论计算机科学电子笔记164（2006）81并且通过使用在位置k处运行的进程P的良好类型关系Rk来定义（参见表6中的规则（N-RUN））。如果一个进程在一个它没有能力的通道上通信，如果替代进程Q是良好类型的，它仍然可以是良好类型的我们把这第二个过程称为安全过程。这种行为反映在φΔ定义中的一种情况中。我们可以将流程动作CNOW想象成一棵二叉决策树，因为通道的语法类似于决策。在每个时间步，必须为动作选择以下选项之一：通信动作、计时器到期或移动动作（参见2.3节，以选择语法扩展go一个进程是好类型的，如果在动作树中存在一条从根到叶子的路径，并且该路径不会产生运行时错误。命题2.6[6]（弱化性质）(a) 如果Γ DN和Δ<：Γ，则Δ D N。（用于已标记的已定位进程）(b) 如果Γ ≠ kP且Δ<：Γ则Δ ≠kP。（用于流程）(c) 若Γ ≠ ka：A且Δ<：Γ，则Δ ≠ ka：A。（用于通道）弱化性质将过程的良型性从给定的类型环境Γ扩展到限制较少的环境Δ（具有更多的能力）。第二个语句可以理解为：如果P是良好类型的，在位置k处相对于类型环境T运行，并且Δ是T的子类型，则P也是良好类型的，在位置k处相对于类型环境Δ运行。由于cleanup函数通过移除chan来改变类型环境Δnel和location类型，我们感兴趣的是在新的类型环境ΔJ下进程是否仍然是良好类型的。引理2.7（良型性由清除函数保持）如果Γ D l [[P]] Δ，则Γ D <$（l [[P]] Δ）。换句话说，如果Γ D 1 [[P]] Δ，则Γ D 1 [[P]] ΔJ，其中Δ J通过从类型环境Δ中移除信道和位置类型来获得。证明通过对P的结构进行归纳来进行证明，每个过程表达式都有一个案例。我们在这里只举出最有趣和最重要的例子。 完整的证明见在线技术报告[12]。从（合成：R）推断的格|Q）。 根据等价规则（SΓ-SPLIT），我们有ΓDl[[R]] Δ|l[[Q]] Δ，根据规则（N-STR），对于定位过程，可将其变换为ΓDl [[R]] Δ和Γ Dl[[Q]] Δ。应用归纳假设，我们得到了ΓD（l[[R]]Δ）和ΓD（l[[Q]]Δ），通过应用，它们变成了ΓDl[[R]]ΔJ和ΓDl[[Q]]ΔJ。 对于这两个进程，我们有相同的ΔJ，因为对带标记的定位进程的应用只考虑了类型环境 ， 而 在 我 们 的 例 子 中 ， 类 型 环 境 是 相 同 的 Δ 。 应 用 关 系 式 （ SΓ-SPLIT），我们得到了结果ΓDl[[R|Q]] ΔJ，其表示ΓD（l[[R|Q]] Δ）。情况 从（限制：（νa：A）Q）推导。从（N-RUN）我们有Δl（νa：G. 乔巴努角Prisacariu/理论计算机科学电子笔记164（2006）8191A)Q和r：Δ。通过（T-NEWCH），我们推断Δ{a@l：A}<$lQ，并且我们还具有Γ{a@l：A}<：Δ{a@l：A}。通过应用弱化性质，我们推出了Γ{a@l：A}Dl[[Q]]Δ{a@l ： A}.应用归纳假设，我们得到了等价于Γ{a@l：A}Dl[[Q]] Δj{a@l：A}的Γ{a@l：A}D（l[Q]]Δ {a@l：A}），因为函数的应用并不排除新名称a。我们再次应用（T-NEWCH）规则，得到结构上等价于ΓD1[[（νa：A）Q]]ΔJ的ΓD（ν a：A）1[[Q]]Δj{a@1：A}。从（动作：go k.Q）推断的格。按照与前面相同的推理方式，我们有Δ l去k.Q和Γ<：Δ。通过（T-GO），我们得到ΔkQ和Δ（k）：loc{go}。使用（N-RUN）我们有ΓDk[[Q]]Δ，通过归纳法它意味着ΓDk[[Q]]ΔJ。我们现在推断ΔJkQ和Γ：ΔJ为真。 通过应用位置k函数，过程移动到位置k的能力不会丢失。这意味着ΔJ（k）<：loc{go}成立，并且连同我们上面获得的，并且通过使用规则（T-GO），我们有ΔJ<$lgo k.Q，并且再次有ΓD l[[go k.Q]] ΔJ。这是我们所寻找的另一种句法形式，即ΓD（l[[Q]]Δ）。如果我们使用新规则而不是（T-GO），则证明以相同的方式进行（T-GO 1）和（T-GO2）在第2.3节中定义。根据（输入：Δt？（X：T）。（R，Q））。如果我们考虑通道a具有类型ro_t，那么从Δ tlaΔt？（X：T）。（R，Q）和通过使用（T-RO）我们有以下陈述：Δla：res{roT}，fv（X）fv（Δ）=，ΔlR和ΔlQ。应用归纳假设，最后两个陈述被转化为ΓDl[[R]]Δ和ΓDl[[Q]]Δ，它们提供了以下两个真陈述：ΓD（l[[R]]Δ）和ΓD（l[[Q]]Δ）。这意味着（T-RO）所需的四个陈述中的三个（fv（X）<$fv（Δ）=R，ΔJ<$lR和ΔJ<$lQ）是真的。如果清除函数没有从功能设，则它在新的环境ΔJ中有效。因此，我们可以应用（T-RO），并获得ΓDl[[aΔt？（X：T）。（R，Q）]]ΔJ.另一方面，如果活动信道的类型缺失，则我们可以使用规则（T-Rnew）并且获得与之前相同的结果，该结果等价于期望的结果，即，（X：T）。（R，Q）]]Δ）。输出、复制和终止的情况是自然的，它们遵循上面给出Q下面的引理表明，时间的流逝不会干扰打字系统。引理指出，如果一个标记定位的进程是良好类型的，对于一个类型环境Γ，则应用标记的时间步进函数φΔ保持了它的良型性。引理2.8（标记时间流逝）如果Γ D l [[P]] Δ，则Γ D φΔ（l [[P]] Δ）。证明我们利用归纳法对ΓDl[[P]]Δ的推理深度进行了研究。从假设中我们导出Δ由（N-RUN）表示的P，以及Γ：Δ。利用弱性质得到了ΓlP。在φΔ的定义中，通过考虑每条线的一种情况来继续证明。92G. 乔巴努角Prisacariu/理论计算机科学电子笔记164（2006）81从（P=R）推断的情况|Q）。使用（T-STR）我们有ΔlR和ΔlQ，它等价于Δl[[R]];通过命题2.6我们得到ΓDl[[R]]Δ。对于过程Q也得到相同的结果。应用归纳假设，我们得到了ΓDφΔ（l[[R]]Δ）和ΓDφΔ（l[[Q]]Δ）。通过将φΔ应用于R，|Q，即rDφΔ（l[[P]] Δ）。由（P=aΔt）推断的情况。（R，Q），t≤1）。我们有两种子情况，一种是当a是输入通道时，另一种是当a是输出通道时。 将φΔ应用于P的结果是l[[Q]]ΔJ（ΔJ通过应用清除函数φ获得），因为t≤1。让我们考虑a是一个输出通道，因此ΔlaΔt！你好（R，Q）和Γ<：Δ。利用（T-W），我们得到ΔlQ，并通过引理2.7我们得到ΔJ<$lQ。 由于Γ：Δ：ΔJ，我们推断出ΓDl[[Q]]ΔJ。 类似的证明当我们考虑输入通道时，通过使用对应于以下的规则，输入通道的类型。由（P=aΔt）推断的情况。（R，Q），t>1且r = r（l，a））。这种情况与前一种情况类似，但我们使用（T-Rnew）和（T-Wnew）而不是使用正常的类型规则，因为a的能力不包括在类型环境中。由（P=aΔt）推断的情况。（R，Q），t>1且t/= ∞）。在这种情况下，我们考虑输入表达式，即ΔlaΔt？（X：T）。（R，Q）。在这种情况下，φΔ将通道计时器从Δt减小到Δt−1。从打字系统的角度来看，处理一个Δt？（X：T）。（R，Q）和Δt−1？（X：T）。（R，Q）是相同的，我们可以应用引理2.7并得到ΔjlaΔt？（X：T）。（R，Q）。由于Γ<：Δ<：ΔJ，我们得到结论：ΓDl [[aΔt？（X：T）。（R，Q）]]ΔJ.通道限制的情况与此类似，它使用类型规则（T-NEWCH）.Q定义2.9我们通过以下方式定义了时间通道上的语法等价aΔt1<$aΔt2当且仅当a1=a2且t1=t2。1 2如果相同通道名称的计时器具有不同的值，则相应的进程具有不同的行为。在定义时间互模拟时必须考虑这一方面[1]。我们定义了标记的结构等价关系。表7：标记的结构等效性（SΓ-垃圾）（SΓ-SPLIT）（SΓ-COPY）（SΓ-新）（SΓ-EXTR）（SΓ-ASSOC）（SΓ-COMMU）（SΓ-NEUTR）G. 乔巴努角Prisacariu/理论计算机科学电子笔记164（2006）8193l[[stop]]Γstopl [[P|[[P]] r|l [[Q]] Γl [[* P]] Γ|l [[* P]] rl[[（ν a：A）P]]Γ<$（ν a@l：A）l[[P]]Δifa/∈fn（Γ）<${l}其中Δ= Γ{a@l：A}M|（νa@k：A）N（νa@k：A）（M，|N）如果a/∈ fn（M）l [[P]] r|l [[Q|R]] Γl [[P|Q]]|l [[R]] rl [[P]] r|l [[Q]] r|l [[P]] rl [[P]] r|停止[[P]] Γ94G. 乔巴努角Prisacariu/理论计算机科学电子笔记164（2006）81主语归约性质指出，良型性由归约关系保持。这是函数式编程框架中的一种通用方法[4，11]。我们还感兴趣的是，证明良好的类型属性是保持结构等价关系。现在我们给出这样一个与结构等价关系有关的结果。 在第3节中给出了一个更一般的主题归约定理。如果我们有两个结构上等价的标记定位进程，其中一个进程相对于类型环境Γ是良类型的，那么另一个进程相对于类型环境Γ也是良类型的。定理2.10（标记等价关系的主语归约N，NJ，使得N<$NJ，r DN当且仅当r DN J。证明我们必须考虑表7中给出的所有等价性。由（SΓ-NEW）推导出的格。根据假设我们有ΓDl[[（νa：A）P]]Δ，这意味着Γ：Δ和Δ <$l（νa：A）P。通过使用（T-NEWCH），我们得到Δ{a@l：A}<$lP。通过应用（N-RUN），我们得到Δ{a@l：A}l[[P]]，并且与Γ{a@l：A}：Δ{a@l：A}一起，我们得到Γ{a@l：A}Dl[[P]]Δ{a@l：A}。我们再次将（T-NEWCH）应用于标记过程，得到结果，即ΓD（νa@l：A）l[[P]]Δ{a@l：A}.由（SΓ-SPLIT）推导出的情况。我们从Γ<：Δ和Δ πlP开始|利用（T-STR ） 得 到 了 ΔP 和 ΔQ 。 从 Γ ： Δ 和 （ N-RUN ） 我 们 得 到 ΓDl[[P]]Δ 和ΓDl[[Q]]Δ。 我们再次应用（N-STR），得到了结论ΓD1[[P]] Δ|l[[Q]] Δ。从（SΓ-COPY）推断的格。这个案例遵循了前一个案例的步骤，我们把它作为练习留给读者。由（SΓ-EXTR）推导出的格在这种情况下，我们使用定位进程的规则从M开始|（νa@k：A）N，利用（N-STR）得到了ΓDM和ΓD（νa@k：A）N.与（N-NEWCH）一起推出了Γ{a@k：A}DN。通过弱化，并且因为a/∈fn（Γ），我们得到Γ{a@k：A}DM。我们再次应用（N-STR），然后应用（N-NEWCH），我们得到所需的结果Γ D（νa@k：A）（M|N）。从（SΓ-GARBAGE）和其他规则推导出的情况类似于π-演算的幺半群定律。Q2.3操作语义我们处理N和M上的标记定位过程;我们可以把N和M看作形式l[[P]]Γ的过程表达式。我们用f →表示规则（RΓ-COM 1）和（RΓ-COM 2）不能被应用的事实。使用这些符号，我们给出以下归约规则，为tDπ提供操作语义。我们有两个通信规则，这取决于通信的类型G. 乔巴努角Prisacariu/理论计算机科学电子笔记164（2006）8195ΔΓΔΓ表8：tDπ的减少关系（R-GO）l[[P]]r/→（R-空闲）I[[go k.P]]Γ→n（k[[P]]r）l[[P]]r →φΔ （1[[P]]r）Γ（l，a）：res{r<$T <$}（RΓ-COM 1）l[[aΔt！你好（P，Q）]]| l[[aΔt' ?（X：T）。（PJ，QJ）]]→（l[[P]]Δ）|n（l[[PJ{v/X}]]r{v@l：T}）Γ（l，a）：res{roT}（Rr-COM 2）l[[aΔt！你好（P，Q）]]| l[[aΔt' ?（X：T）。（PJ，QJ）]]→（l [[P]] Δ）|n（l [[PJ{v/X}]] Γ）N→NJM →MJN →NJ（RΓ-PAR）N|M→NJ|MJ（Rr-RES）（ν a@l：A）N →（ν a@l：A）NJN<$NJN→M M<$MJ（RΓ-CONG）NJ→MJ频道频道在（RΓ-COM 2）中，我们考虑了随机信道，并且该过程可以使用接收到的信息而不向其类型环境Γ添加新类型，这与规则（RΓ-COM 1）的行为相反。通信规则和（RΓ-GO）不进入φΔ的范围。 在这种情况下，类型环境由cleanup函数清除。在（RΓ-IDLE）中，函数φΔ减少信道上的定时器，并且对于到期的定时器，函数丢弃信道并改变过程的状态。在通用时钟的每一个滴答声中，规则（RΓ-IDLE）被应用于不进入任何通信的进程。当应用规则（RΓ-PAR）时，如果进程M不具有内部通信约简，则它被规则（RΓ-IDLE）变换为MJ。同样的论点也适用于N。从类型环境中删除位置类型可能会导致由go操作生成的错误。我们通过使用类似于通道的选择语法扩展go的语法来解决这个问题;因此go l.P变成了go l。（P，Q）。如果如果没有定义Γ（l），则执行Q。如果l的位置类型包含能力，go，则执行P;否则，如果l的位置类型不包含能力go，则生成错误。我们应该在出现go操作符的地方因此，（T-GO）被翻译成（T-GO 1），（T-GO2）。（T-GO1）k/∈dom（Γ）Γ <$lQ我去K。（P，Q）（T-GO2）r（k）：loc{go}rkP我去K。（P，Q）产生误差的过程P记为P−e→rr。这种情况下，生成运行时错误的一组规则在表9中定义。robj（）、roobj（）、wobj（）是在信道类型集合上定义的部分函数，并且返回对应信道能力的类型。例如，考虑位置l处的类型环境Γ中的通道类型a：res{wT}，应用wobj（r（l，a））返回T。为了派生运行时错误，通道类型或位置类型必须在类型环境中。当进程试图对在其类型环境中累积的类型执行某些操作时，将出现运行时错误。当类型不在进程的类型环境中时，Γ96G. 乔