高等數(shù)理邏輯通訊與并發(fā)cc譯文

1、Page236看到這一點(diǎn)，因此，我們可以預(yù)期，如果我們總是伴隨著被這些符號(hào)(可能是交流的載體) 限制成分，那么確定性將被保留；也就是說(shuō)，我們可以預(yù)期，如果P1和P2是確定的，那么由(P1|P2)L就有事實(shí)上，我們可以看到一個(gè)系統(tǒng)的流圖只能用這樣受限制的組合建立，將永遠(yuǎn)不會(huì)有兩個(gè)弧共享一個(gè)端口，我們可以認(rèn)為，這消除了各種能導(dǎo)致不確定性的競(jìng)爭(zhēng)。但不幸的是還有另外一種競(jìng)爭(zhēng)的形式。考慮P1a.0+b.0和P2.0。P1和P2都是確定的，但是受限制的組合(P1|P2)a強(qiáng)全等于.0 + b.0，而.0 + b.0是不確定的，因?yàn)樗鼤?huì)不可預(yù)測(cè)地妨礙到b動(dòng)作。這里的競(jìng)爭(zhēng)是為了通過(guò)兩個(gè)不同的端口訪問(wèn)到P1。有

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

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

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

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

6、于Q是封閉的，那么類似的圖也對(duì)于R是封閉的?？梢酝ㄟ^(guò)常規(guī)使用的強(qiáng)互模擬等價(jià)的定義得到。 我們應(yīng)經(jīng)常避免在如定義4的圖中提及Q1和Q2，可能是通過(guò)一個(gè)點(diǎn)代表他們；因此，我們將簡(jiǎn)單地說(shuō)P是強(qiáng)匯流，如果對(duì)每一個(gè)P的衍生Q 有圖當(dāng)時(shí)是完整的，其中，我們默認(rèn)每個(gè)Q1和Q2上側(cè)和左側(cè)的推導(dǎo)存在。下面這個(gè)例子將對(duì)讀者有所幫助。以下是強(qiáng)匯流代理的轉(zhuǎn)換圖： 事實(shí)上，此代理可以表示為a.0 | b.(c.0|d.0)。稍后我們將看到，缺乏求和和只有一個(gè)約束形式的通信（在這種情況下，沒(méi)有）組合的使用，確保匯流。我們不會(huì)糾纏于強(qiáng)匯流，因?yàn)槲覀兿Ｍ紤]到動(dòng)作。這些都需要謹(jǐn)慎處理，就像他們?cè)冢ㄈ酰┗ツM的定義。讓我們回想

7、一下，我們有兩個(gè)互模擬的描述；Page239一個(gè)是（定義5.5）使用一個(gè)單一的推導(dǎo)-，另一個(gè)是（命題7.1）使用復(fù)合推導(dǎo)=，其中sL*。我們也有兩個(gè)匯流的描述。第一個(gè)顯示如何一個(gè)單一（可能是無(wú)聲的）動(dòng)作與其他動(dòng)作通勤：定義5 P是(弱)匯流的，如果每一個(gè)P的衍生Q可由下面的圖完成： 這里要注意的有幾點(diǎn)。首先，每個(gè)圖中的頂行是一個(gè)單一的動(dòng)作；這種表述是為了方便證明某些組合算子保留匯流。但很容易獲得更一般的性質(zhì)，這導(dǎo)致Q1和Q2分別在兩種推導(dǎo)中對(duì)稱：命題9 P是匯流的，當(dāng)且僅當(dāng)每一個(gè)P的衍生Q可由下面的圖完成：證明 通過(guò)歸納每個(gè)圖中頂端動(dòng)作序列的長(zhǎng)度。在證明的過(guò)程中，我們還需要使用的事實(shí)是，下面的

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

9、sL*，對(duì)于r超過(guò)s，我們會(huì)寫(xiě)作r/s。直觀地說(shuō)，為了得到r/s，我們從左至右遍歷r刪除任何在s中出現(xiàn)的標(biāo)簽，但要考慮多重出現(xiàn)。對(duì)于圖中的序列，例如，我們有aba/ca = ba和ca/aba = c.。更確切地說(shuō)： 定義6 對(duì)于r超過(guò)s，寫(xiě)作r/s。，也在r上被遞歸地定義為如下： 這個(gè)在序列上的二進(jìn)制操作有幾個(gè)很好的性質(zhì)，目前我們只是記錄一些被我們需要證明命題11的。如果讀者愿意接受這個(gè)命題給出了一種匯流的替代描述，然后他就可以忽略引理在命題11之后閱讀。引理10 對(duì)于所有的r, s, tL*(1) rs/rt = s/t (2) r/st = (r/s)/t (3) rs/t = (r/t

10、) (s/(t/r)Page241證明 通過(guò)對(duì)r在每一種情況下的歸納。 現(xiàn)在，我們可以建立我們的匯流的替代描述，這是非常簡(jiǎn)潔的：命題11 P是匯流的，當(dāng)且僅當(dāng)，對(duì)所有r, sL*，下圖可以被完成： 證明 讓我們說(shuō)P有性質(zhì)(*)如果上面的圖對(duì)所有的P1,P2 和r, sL*可以被完成。 假設(shè)P有性質(zhì)(*)。首先，我們將說(shuō)明，每一個(gè)P的衍生Q也有性質(zhì)(*)。讓P =t=Q, tL*, 并且讓然后還有 , 由此因?yàn)镻有性質(zhì)(*)。. 因此，從引理10，我們推斷這表明Q有性質(zhì)(*)。從這一點(diǎn)出發(fā)，P是匯流的，因?yàn)槎x5的四個(gè)圖中每個(gè)圖都是Q的性質(zhì)(*)的特殊的情況?，F(xiàn)在，反過(guò)來(lái)考慮，假設(shè)P是匯流的。由

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

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

13、留下來(lái)，這時(shí)我們看到的不是確定性的情況。讓我們先記錄一些簡(jiǎn)單的事實(shí)：命題15 如果P, P1 和P2是匯流的，那么也滿足下式：(1) 0, .P 和PL. (2) Pf, f |L(P) 是單射。證明 顯然。 和命題6相比，求和和組成在這里沒(méi)有出現(xiàn)。讓我們先來(lái)看一下求和，并回顧一下，雖然a.0+b.0是匯流的，a.b.0+b.a.0卻是。這表明，我們定義了一個(gè)復(fù)合形式的前綴，如下：定義7 對(duì)于1,., n Act，n0，匯流的和(1| |n) .P被遞歸定義如下： 因此，例如，可以定義更豐富的形式，通過(guò)用動(dòng)作序列更換i，但這種形式將足以滿足我們目前的目的。以下很容易證明：命題16 如果P是匯流

14、的，那么(1| |n).P也是。 一個(gè)匯流和的例子是，我們?cè)诘?章第5節(jié)中建立的調(diào)度器中的細(xì)胞A；它可能會(huì)現(xiàn)在可以寫(xiě)為事實(shí)上，遞歸定義可以被用來(lái)展示保存匯流，所以Page244細(xì)胞A是匯流的。我們現(xiàn)在應(yīng)該也看到，被用于建設(shè)調(diào)度器Sched的受限制的組合是一種保留匯合，從中我們可以得出結(jié)論：立即 - 它的行為沒(méi)有任何具體的分析 - 附表本身是融合的。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 對(duì)于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、設(shè)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