高等数理逻辑通讯与并发cc译文

1、Page236看到这一点，因此，我们可以预期，如果我们总是伴随着被这些符号(可能是交流的载体) 限制成分，那么确定性将被保留；也就是说，我们可以预期，如果P1和P2是确定的，那么由(P1|P2)L就有事实上，我们可以看到一个系统的流图只能用这样受限制的组合建立，将永远不会有两个弧共享一个端口，我们可以认为，这消除了各种能导致不确定性的竞争。但不幸的是还有另外一种竞争的形式。考虑P1a.0+b.0和P2.0。P1和P2都是确定的，但是受限制的组合(P1|P2)a强全等于.0 + b.0，而.0 + b.0是不确定的，因为它会不可预测地妨碍到b动作。这里的竞争是为了通过两个不同的端口访问到P1。有

2、了这种竞争的存在，那么，似乎没有可能存在约束形式的组合物，使其同时提供确定性和有用性（即允许一些通信）。然而，我们会发现一个更加完善的确定性形式，我们称之为汇流(confluence)，它真正地保存了上述类型受限制的组合。让我们通过学习Hoare的替代组合算子(连接算子Conjunction和隐藏算子Hiding，定义见第9章第二节)是如何带有确定性地运算来完成这一章吧。这里连接算子有一点难懂：命题7如果P和Q 都是确定的那么连接算子PK|L Q表示P : K 和 Q : L. 直观地说，原因很简单。如果一个动作P或者Q属于KL，它必须是一个同步，否则它必须出现不同步的；没有歧义。此外，没有R

3、动作是连接算子制造的，正如它们的组合构成。事实上伴随隐藏算子/ L一起这里出现了困难；很容易看到，考虑到(a.0+b.0)/ a .0 + b.0，隐藏算子并不提供确定性。显然，无论怎么选择（即用连接算子或隐藏算子），将观察到的动作转换为动作，我们将冒着失去确定性的风险。Page237然而，我们已经可以看到汇流，我们还没有定义，将由隐藏算子保持；因为这是一个特殊的情况，我们的承诺，某种受限制的组合将保持汇流。例如：并且Ever(a) (见第5章第5节) 它自身就是一个汇流。现在我们已经有了一些改善确定性的动力，我们将继续研究汇流。 练习3 试证命题7在一般情况下是假的，不使用条件P : K a

4、nd Q : L. 11.3汇流Confluence计算理论各部分不同的动机产生了不同形式汇流的概念。对于我们来说，这种动机是在保留受限制组合的同时加强确定性。再看看我们的例子，对于P1a.0+b.0, P2.0，我们可以发现(P1|P2)a-强全等于.0 + b.0(它是不确定的)。我们说，这是由于通过不同的端口访问P1的竞争。但是，更确切地说，它的产生是因为获胜动作，比方说，阻止其他动作b发生。如果用P1a.b.0+b.a.0代替，情况将大有不同；在这种情况下，获胜的动作只是推迟而不是阻止其他。事实上，我们发现， 它有完美的确定性。这是汇流的本质；任何两种可能的操作中，出现一种永远不会阻止

5、其他的。对于一个确切的定义，让我们先假设，我们不希望给动作任何的特殊地位。这种情况下，我们定义如下： 定义4 P是强汇流的，如果它有强确定性，并且为每一个P的衍生Q，能找到Q1 和 Q2并完成下图，其中Q-Q1 ，Q-Q1 ，： Page238请注意，强汇流是推导封闭的，因为我们需要的性质不仅有P的还包括其所有衍生的。还请注意，我们不要求与Q1和Q2是相同的，但必须是强互模拟等价的；这是为了确保强互模拟等价性保留强汇流。让我们记录下这些：命题8 强汇流是推导封闭的，并且由强互模拟等价性保留。证明 我们已经讨论过前半句了，让我们看看后半句。它清楚地变弱是为了显示出，如果QR，同时定义4的图中，对

6、于Q是封闭的，那么类似的图也对于R是封闭的。可以通过常规使用的强互模拟等价的定义得到。 我们应经常避免在如定义4的图中提及Q1和Q2，可能是通过一个点代表他们；因此，我们将简单地说P是强汇流，如果对每一个P的衍生Q 有图当时是完整的，其中，我们默认每个Q1和Q2上侧和左侧的推导存在。下面这个例子将对读者有所帮助。以下是强汇流代理的转换图： 事实上，此代理可以表示为a.0 | b.(c.0|d.0)。稍后我们将看到，缺乏求和和只有一个约束形式的通信（在这种情况下，没有）组合的使用，确保汇流。我们不会纠缠于强汇流，因为我们希望考虑到动作。这些都需要谨慎处理，就像他们在（弱）互模拟的定义。让我们回想

7、一下，我们有两个互模拟的描述；Page239一个是（定义5.5）使用一个单一的推导-，另一个是（命题7.1）使用复合推导=，其中sL*。我们也有两个汇流的描述。第一个显示如何一个单一（可能是无声的）动作与其他动作通勤：定义5 P是(弱)汇流的，如果每一个P的衍生Q可由下面的图完成： 这里要注意的有几点。首先，每个图中的顶行是一个单一的动作；这种表述是为了方便证明某些组合算子保留汇流。但很容易获得更一般的性质，这导致Q1和Q2分别在两种推导中对称：命题9 P是汇流的，当且仅当每一个P的衍生Q可由下面的图完成：证明 通过归纳每个图中顶端动作序列的长度。在证明的过程中，我们还需要使用的事实是，下面的

8、图总是可以被完成的(对于任意的Q，不一定是汇流的)：当然，这个对任何互模拟代替都保持，并且是命题7.1的一个复述。 Page240第二，该定义意味着确定性，但只是间接的。第四个图将代表确定性，如果我们能够表示出，在这个图中它必须是Q1Q2，事实上这将在接踵而至。 第三，命题9中很清楚，第三个和第四个图可粘在一起，得到复合的图，产生可能有一些共同动作的动作序列对。例如，我们可以推断出，如果P是汇流的，那么下图就可以被完成：这断言每一个动作序列aba和ca可以被进一步的序列延长，在另外一个中包含额外的动作，以达到一种常见的状态(最多是)。要获得这种说法的一般形式，让我们先来定义，对于两个序列r,

9、sL*，对于r超过s，我们会写作r/s。直观地说，为了得到r/s，我们从左至右遍历r删除任何在s中出现的标签，但要考虑多重出现。对于图中的序列，例如，我们有aba/ca = ba和ca/aba = c.。更确切地说： 定义6 对于r超过s，写作r/s。，也在r上被递归地定义为如下： 这个在序列上的二进制操作有几个很好的性质，目前我们只是记录一些被我们需要证明命题11的。如果读者愿意接受这个命题给出了一种汇流的替代描述，然后他就可以忽略引理在命题11之后阅读。引理10 对于所有的r, s, tL*(1) rs/rt = s/t (2) r/st = (r/s)/t (3) rs/t = (r/t

10、) (s/(t/r)Page241证明 通过对r在每一种情况下的归纳。 现在，我们可以建立我们的汇流的替代描述，这是非常简洁的：命题11 P是汇流的，当且仅当，对所有r, sL*，下图可以被完成： 证明 让我们说P有性质(*)如果上面的图对所有的P1,P2 和r, sL*可以被完成。 假设P有性质(*)。首先，我们将说明，每一个P的衍生Q也有性质(*)。让P =t=Q, tL*, 并且让然后还有 , 由此因为P有性质(*)。. 因此，从引理10，我们推断这表明Q有性质(*)。从这一点出发，P是汇流的，因为定义5的四个图中每个图都是Q的性质(*)的特殊的情况。现在，反过来考虑，假设P是汇流的。由

11、命题9开始，我们首先证明下面的图对于每一个P的衍生Q可以被完成(包括P自身)，lL, and rL*：Page242证明是由对r归纳得到。然后，我们通过对s归纳证明P的性质(*)。在这两个证明，我们借助于引理10。 读者可能会觉得，我们应该用命题11中的性质定义汇流，因为它比定义5更简洁，更令人难忘。然而也许是这样，很重要的一点是，两个描述都有好的出发点。(事实上，在许多证明中定义5更加有用)。下一个命题确立了汇流是一个互模拟等价类的性质，所以它是一个语义性质。命题12 如果PQ并且P是汇流的，那么Q也是。证明 一个简单的把图粘一起的练习。 接下来的两个命题确立了汇流作为确定性一个完善。 命题

12、13 如果P=Q并且P是汇流的，那么PQ。证明 只需证明，是一个在之上的互模拟。 练习4 完成这个证明。确保您知道为什么这里需要“在之上”。 命题13在概念上是很重要的。这表明，无声的动作不能改变汇流代理的状态，在之上，所以他们不能排除以前可能的动作。命题14 如果P是汇流的，那么P是确定的。证明 让P是汇流的，Q是任意一个P的衍生，并且让然后由命题9，我们推断，存在Q1, Q2，满足Q1 = Q1, Q2 = Q2 和Q1 Q2。现在，通过命题13，我们推断Q1 Q2，这是定义3为了Q的确定性所需的条件。 Page24311.4 保留汇流我们对汇流的主要兴趣是，它会变成以受限制的组成的形式保

13、留下来，这时我们看到的不是确定性的情况。让我们先记录一些简单的事实：命题15 如果P, P1 和P2是汇流的，那么也满足下式：(1) 0, .P 和PL. (2) Pf, f |L(P) 是单射。证明 显然。 和命题6相比，求和和组成在这里没有出现。让我们先来看一下求和，并回顾一下，虽然a.0+b.0是汇流的，a.b.0+b.a.0却是。这表明，我们定义了一个复合形式的前缀，如下：定义7 对于1,., n Act，n0，汇流的和(1| |n) .P被递归定义如下： 因此，例如，可以定义更丰富的形式，通过用动作序列更换i，但这种形式将足以满足我们目前的目的。以下很容易证明：命题16 如果P是汇流

14、的，那么(1| |n).P也是。 一个汇流和的例子是，我们在第5章第5节中建立的调度器中的细胞A；它可能会现在可以写为事实上，递归定义可以被用来展示保存汇流，所以Page244细胞A是汇流的。我们现在应该也看到，被用于建设调度器Sched的受限制的组合是一种保留汇合，从中我们可以得出结论：立即 - 它的行为没有任何具体的分析 - 附表本身是融合的。We shall now see also that the restricted Composition which was used in building the scheduler Sched is of the kind which pre

15、serves confluence, from which we can conclude immediately - without any specific analysis of its behaviour - that Sched itself is confluent. 定义8 对于LL我们定义受限制的组合 _ _ 我们称之为汇流的组合，如果L(P1)L (P2) = 并且L(P 1)L(P2)LL。 Thus the sorts in a Confluent Composition must be disjoint; the earlier example a.b.0 | a.0

16、shows the need for this, because it is indeterminate even though its components are not only determinate but even confluent. But - in contrast to Proposition 6(3) - we now allow the components P1 and P2 to communicate provided that all communication labels are restricted. Indeed, we now claim: 命题17

17、设P1 和P2是汇流的。那么如果P1 |L P2是汇流组合，它也是是汇流的。证明 Proof We shall not give the whole proof, since it is quite a long case-analysis, but we shall deal with one case in some detail. We work with the original definition of confluence, Definition 5. We first observe that every derivative of P1 |L P2 will take the

18、 form Q1 |L Q2 and will be a Confluent Composition of confluent agents; therefore we need only ensure that the four diagrams of Definition 5 can be completed for any Confluent Composition of confluent agents. We shall consider the proof for one diagram, and leave the rest to the reader. We wish to s

19、how that the diagram can be completed, and we consider the particular case in which the upper action is due to Q that is, we assume that Q1 -t- Q1 and that Q1Q2 . Now the condition of disjoint sorts ensures that l(Q2)* so the l in the left (vertical) derivation must also be performed by Q1, or more

20、exactly by a-descendant of Q1. In fact the derivation Q1 |L Q2 =t=Q1 |L Q2 may containactions arising from communications, so in general wePage245have _ _ _where r, s(LL)*. Hence l does not appear in any of r, s, r, s; this follows from the second condition on Confluent Composition. Thus rls/l = rs,

21、 l/rls =, and so we have (because Q1 is confluent) that can be completed. Now recalling that Q1Q2 we have and we are now able to complete the diagram for Q1 |L Q2 as required. The other diagrams raise no extra difficulties. The case treated above needs both of the conditions of Confluent Composition

22、. Exercise 5 Complete this proof. The situation with respect to Hoares alternative combinators, Conjunction and Hiding, is rather simpler; in our next proposition we state without proof the result that they both preserve confluence, as they are normally used. More precisely, we have to constrain the Conjunction P K|L Q by the condition that P : K and Q : L, and we shall call this constrained form Confluent Conjunction. We have chosen to give the proof for the somewhat more complex case of Confluent Composition, since it can also be adapted to analyse the preservation of confluenc