1、Page236看到這一點，因此，我們可以預期，如果我們總是伴隨著被這些符號(可能是交流的載體) 限制成分，那么確定性將被保留；也就是說，我們可以預期，如果P1和P2是確定的，那么由(P1|P2)L就有事實上，我們可以看到一個系統(tǒng)的流圖只能用這樣受限制的組合建立，將永遠不會有兩個弧共享一個端口，我們可以認為，這消除了各種能導致不確定性的競爭。但不幸的是還有另外一種競爭的形式?？紤]P1a.0+b.0和P2.0。P1和P2都是確定的，但是受限制的組合(P1|P2)a強全等于.0 + b.0，而.0 + b.0是不確定的，因為它會不可預測地妨礙到b動作。這里的競爭是為了通過兩個不同的端口訪問到P1。有

2、了這種競爭的存在，那么，似乎沒有可能存在約束形式的組合物，使其同時提供確定性和有用性（即允許一些通信）。然而，我們會發(fā)現(xiàn)一個更加完善的確定性形式，我們稱之為匯流(confluence)，它真正地保存了上述類型受限制的組合。讓我們通過學習Hoare的替代組合算子(連接算子Conjunction和隱藏算子Hiding，定義見第9章第二節(jié))是如何帶有確定性地運算來完成這一章吧。這里連接算子有一點難懂：命題7如果P和Q 都是確定的那么連接算子PK|L Q表示P : K 和 Q : L. 直觀地說，原因很簡單。如果一個動作P或者Q屬于KL，它必須是一個同步，否則它必須出現(xiàn)不同步的；沒有歧義。此外，沒有R

3、動作是連接算子制造的，正如它們的組合構成。事實上伴隨隱藏算子/ L一起這里出現(xiàn)了困難；很容易看到，考慮到(a.0+b.0)/ a .0 + b.0，隱藏算子并不提供確定性。顯然，無論怎么選擇（即用連接算子或隱藏算子），將觀察到的動作轉換為動作，我們將冒著失去確定性的風險。Page237然而，我們已經(jīng)可以看到匯流，我們還沒有定義，將由隱藏算子保持；因為這是一個特殊的情況，我們的承諾，某種受限制的組合將保持匯流。例如：并且Ever(a) (見第5章第5節(jié)) 它自身就是一個匯流?，F(xiàn)在我們已經(jīng)有了一些改善確定性的動力，我們將繼續(xù)研究匯流。 練習3 試證命題7在一般情況下是假的，不使用條件P : K a

4、nd Q : L. 11.3匯流Confluence計算理論各部分不同的動機產(chǎn)生了不同形式匯流的概念。對于我們來說，這種動機是在保留受限制組合的同時加強確定性。再看看我們的例子，對于P1a.0+b.0, P2.0，我們可以發(fā)現(xiàn)(P1|P2)a-強全等于.0 + b.0(它是不確定的)。我們說，這是由于通過不同的端口訪問P1的競爭。但是，更確切地說，它的產(chǎn)生是因為獲勝動作，比方說，阻止其他動作b發(fā)生。如果用P1a.b.0+b.a.0代替，情況將大有不同；在這種情況下，獲勝的動作只是推遲而不是阻止其他。事實上，我們發(fā)現(xiàn)， 它有完美的確定性。這是匯流的本質(zhì)；任何兩種可能的操作中，出現(xiàn)一種永遠不會阻止

5、其他的。對于一個確切的定義，讓我們先假設，我們不希望給動作任何的特殊地位。這種情況下，我們定義如下： 定義4 P是強匯流的，如果它有強確定性，并且為每一個P的衍生Q，能找到Q1 和 Q2并完成下圖，其中Q-Q1 ，Q-Q1 ，： Page238請注意，強匯流是推導封閉的，因為我們需要的性質(zhì)不僅有P的還包括其所有衍生的。還請注意，我們不要求與Q1和Q2是相同的，但必須是強互模擬等價的；這是為了確保強互模擬等價性保留強匯流。讓我們記錄下這些：命題8 強匯流是推導封閉的，并且由強互模擬等價性保留。證明 我們已經(jīng)討論過前半句了，讓我們看看后半句。它清楚地變?nèi)跏菫榱孙@示出，如果QR，同時定義4的圖中，對

6、于Q是封閉的，那么類似的圖也對于R是封閉的?？梢酝ㄟ^常規(guī)使用的強互模擬等價的定義得到。 我們應經(jīng)常避免在如定義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可由下面的圖完成： 這里要注意的有幾點。首先，每個圖中的頂行是一個單一的動作；這種表述是為了方便證明某些組合算子保留匯流。但很容易獲得更一般的性質(zhì)，這導致Q1和Q2分別在兩種推導中對稱：命題9 P是匯流的，當且僅當每一個P的衍生Q可由下面的圖完成：證明 通過歸納每個圖中頂端動作序列的長度。在證明的過程中，我們還需要使用的事實是，下面的

8、圖總是可以被完成的(對于任意的Q，不一定是匯流的)：當然，這個對任何互模擬代替都保持，并且是命題7.1的一個復述。 Page240第二，該定義意味著確定性，但只是間接的。第四個圖將代表確定性，如果我們能夠表示出，在這個圖中它必須是Q1Q2，事實上這將在接踵而至。 第三，命題9中很清楚，第三個和第四個圖可粘在一起，得到復合的圖，產(chǎn)生可能有一些共同動作的動作序列對。例如，我們可以推斷出，如果P是匯流的，那么下圖就可以被完成：這斷言每一個動作序列aba和ca可以被進一步的序列延長，在另外一個中包含額外的動作，以達到一種常見的狀態(tài)(最多是)。要獲得這種說法的一般形式，讓我們先來定義，對于兩個序列r,

9、sL*，對于r超過s，我們會寫作r/s。直觀地說，為了得到r/s，我們從左至右遍歷r刪除任何在s中出現(xiàn)的標簽，但要考慮多重出現(xiàn)。對于圖中的序列，例如，我們有aba/ca = ba和ca/aba = c.。更確切地說： 定義6 對于r超過s，寫作r/s。，也在r上被遞歸地定義為如下： 這個在序列上的二進制操作有幾個很好的性質(zhì)，目前我們只是記錄一些被我們需要證明命題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在每一種情況下的歸納。 現(xiàn)在，我們可以建立我們的匯流的替代描述，這是非常簡潔的：命題11 P是匯流的，當且僅當，對所有r, sL*，下圖可以被完成： 證明 讓我們說P有性質(zhì)(*)如果上面的圖對所有的P1,P2 和r, sL*可以被完成。 假設P有性質(zhì)(*)。首先，我們將說明，每一個P的衍生Q也有性質(zhì)(*)。讓P =t=Q, tL*, 并且讓然后還有 , 由此因為P有性質(zhì)(*)。. 因此，從引理10，我們推斷這表明Q有性質(zhì)(*)。從這一點出發(fā)，P是匯流的，因為定義5的四個圖中每個圖都是Q的性質(zhì)(*)的特殊的情況。現(xiàn)在，反過來考慮，假設P是匯流的。由

11、命題9開始，我們首先證明下面的圖對于每一個P的衍生Q可以被完成(包括P自身)，lL, and rL*：Page242證明是由對r歸納得到。然后，我們通過對s歸納證明P的性質(zhì)(*)。在這兩個證明，我們借助于引理10。 讀者可能會覺得，我們應該用命題11中的性質(zhì)定義匯流，因為它比定義5更簡潔，更令人難忘。然而也許是這樣，很重要的一點是，兩個描述都有好的出發(fā)點。(事實上，在許多證明中定義5更加有用)。下一個命題確立了匯流是一個互模擬等價類的性質(zhì)，所以它是一個語義性質(zhì)。命題12 如果PQ并且P是匯流的，那么Q也是。證明 一個簡單的把圖粘一起的練習。 接下來的兩個命題確立了匯流作為確定性一個完善。 命題

12、13 如果P=Q并且P是匯流的，那么PQ。證明 只需證明，是一個在之上的互模擬。 練習4 完成這個證明。確保您知道為什么這里需要“在之上”。 命題13在概念上是很重要的。這表明，無聲的動作不能改變匯流代理的狀態(tài)，在之上，所以他們不能排除以前可能的動作。命題14 如果P是匯流的，那么P是確定的。證明 讓P是匯流的，Q是任意一個P的衍生，并且讓然后由命題9，我們推斷，存在Q1, Q2，滿足Q1 = Q1, Q2 = Q2 和Q1 Q2?，F(xiàn)在，通過命題13，我們推斷Q1 Q2，這是定義3為了Q的確定性所需的條件。 Page24311.4 保留匯流我們對匯流的主要興趣是，它會變成以受限制的組成的形式保

13、留下來，這時我們看到的不是確定性的情況。讓我們先記錄一些簡單的事實：命題15 如果P, P1 和P2是匯流的，那么也滿足下式：(1) 0, .P 和PL. (2) Pf, f |L(P) 是單射。證明 顯然。 和命題6相比，求和和組成在這里沒有出現(xiàn)。讓我們先來看一下求和，并回顧一下，雖然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節(jié)中建立的調(diào)度器中的細胞A；它可能會現(xiàn)在可以寫為事實上，遞歸定義可以被用來展示保存匯流，所以Page244細胞A是匯流的。我們現(xiàn)在應該也看到，被用于建設調(diào)度器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