相互作用シーケンシャルプロセス(CSP)の理論の概要、パート2

プロセスの微積分の代数に関する一連の記事を続けます。 このテキストは翻訳であり、 チャールズE.ホア による本の冒頭の章の要約された語りです。 この理論は、並列システムの動作を正式に説明するために使用されます。 その実用的なアプリケーションの例は、Erlang、Go、Limboなどのプログラミング言語です。

選択肢



再帰とプレフィックスを使用して、可能な線形動作のみを持つオブジェクトを記述することができます。 ただし、多くのオブジェクトは外部条件の影響を受けます。つまり、状況に応じて何らかの方法で反応するように反応することができます。 たとえば、自動販売機には1ルーブルコインと2ルーブルコイン用の開口部があり、購入者がどのコインをマシンに挿入するかによって異なります。 したがって、xとyが異なるイベントである場合、エントリは次のようになります。

(x→P | y→Q)


最初にxまたはyイベントに参加するオブジェクトを記述します。 イベントxが発生すると、オブジェクトはPとしてさらに動作し、yが発生すると、Qのように動作します。 xとyは異なるイベントであり、PとQの間の選択は、最初のxまたはyが発生するイベントによって事前に決定されます。 前と同じように、アルファベットの不変性、つまり:

α(x→P | y→Q)=αP=αQ、つまり{x、y}⊆αP


スティック「|」 「選択」と発音:「x、P、y、Qの順に選択」。



  1. ボード上のポインターの可能な動き:



    次のように説明されます。

    (上→停止|右→右→上→停止)
  2. 交換機。これにより、ユーザーは交換方法を選択できます(前述の交換機と比較してください)。

      CH5C = in5p→(out1p→out1p→out1p→out2p→CH5C
             |  out2p→out1p→out2p→CH5C) 
  3. チョコレートまたはキャラメルのいずれかを販売する自動販売機:

    VMCT =μX•コイン→(choc→X |タフィー→X)
  4. 使用するコインと受け取るチョコレートバーのサイズを購入者に選択させる、より複雑なトレーディングマシン:

      VMC =(in2p→(大→VMC
                    | 小→out1p→VMC)
            |  in1p→(小→VMC
                      |  in1p→(大→VMC
                                |  in1p→STOP)))) 


    多くの複雑なマシンと同様に、設計上の欠陥があります。 多くの場合、マシン自体を修正するよりもユーザーの指示を変更する方が簡単なので、マシンに書き込みましょう。

    「注意:3枚の1ルーブルコインを連続して挿入しないでください。」 (私たちがだれを欺くとしても、私たちの状況では、これは機械のジャムを引き起こすだけです)
  5. ユーザーを信頼し、チョコレートバーを試してから支払いができるマシン:

      VMCRED =μX•(コイン→チョコ→X
                    | チョコ→コイン→X) 
  6. 損失を防ぐため、最初の支払いを使用してVMCREDを使用する特権を取得します。

    VMS2 =(コイン→VMCRED)


    このマシンでは、2枚のコインを連続して挿入し、2枚のチョコレートを連続して入手できますが、支払われたコインよりも多くのチョコレートを贈ることはできません。
  7. コピープロセスは、次のイベントに関与します。

    • in.0-入力ゼロ
    • in.1-入力へのユニットの提出
    • out.0-出力にゼロを送ります
    • out.1-終了するフィードユニット


    プロセスの動作には、入出力ペアの繰り返しが必要なので、次のように記述できます。

      COPYBIT =μX•(in.0→out.0→X
                     |  in.1→out.1→X) 


    このプロセスでは、入力に適用するものを選択できますが、出力には選択できないことに注意してください。 プロセス間のメッセージの転送についてさらに議論するとき、プロセスの入力と出力の主な違いはこの機能です。


選択の定義は、より多くのイベントに自然に拡張できます。

(x→P | y→Q | ... | z→R)


文字「|」に注意してください はプロセスの演算子ではなく、P |と書くのは構文的に正しくありません。 Q、プロセスPおよびQ。このルールの理由は、次のレコードの値の決定を避けたくないからです。

(x→P | x→Q)


これは選択肢を与えるようですが、実際にはしません。 この問題は、動作に不確実性を導入することで将来解決されます。



したがって、x、y、zが異なるイベントの場合、次のようになります。

(x→P | y→Q | z→R)


3つの引数P、Q、Rを持つ1つの演算子として解釈される必要があります。この演算子はレコードと等しくありません。

(x→P |(y→Q | z→R))


これは構文的に間違っています。



要約すると、Bがイベントのセットであり、P(x)がBの各xのプロセスを定義する式である場合、式は次のようになります。

(x:B→P(x))


最初にBからイベントyを選択するプロセスを定義します。その後、P(y)のように動作します。 この式は、「 Bからx 、次にyからP 」と発音される必要があります。 この構成では、xはローカル変数です。したがって、

(x:B→P(x))=(y:B→P(y))


セットBはプロセスのメニューを比fig的に話すことを定義しています 。 プロセスが応答できるアクション。





  1. アルファベットから常にすべてのイベントに参加できるプロセス:

    αRUNA = A

    RUN A =(x:A→RUN A



特別なケースでは、メニューに含まれるeイベントが1つだけの場合:

(x:{e}→P(x))=(e→P(e))


さらに特別なケースでは、メニューが空の場合、何も起こりません。

(x:{}→P(x))=(y:{}→P(y))=停止




したがって、停止、接頭辞、およびバイナリ選択は、一般的な表記法の特殊なケースであり、プロセスに関する一般的な法則をさらに策定し、その実装を説明するときに非常に便利です。



間接再帰



定期的な再帰により、プロセスを1つの方程式の解として定義できます。 この手法は、複数の未知の方程式系に簡単に拡張できます。 このシステムが正しいためには、右側が保護され、すべての未知のプロセスがシステムの方程式の右側に少なくとも1回現れることが必要です。





  1. 飲み物の自動販売機には、「オレンジ」と「レモン」の2つのボタンがあり、クリックすると、それぞれセトオレンジとセトレモンのイベントがアクティブになります。 注がれる飲み物の選択は、対応するボタンを押すことによって行われます。 ボタンに触れると、ディスペンスは特定の飲み物をディスペンスします。 モードが選択されなかった前に、飲み物は瓶詰めされません。この初期状態をDDと書きます。 2つの補助プロセスOとLを使用して、DDのアルファベットと動作を説明します。

    αDD=αO=αL= {セトレンジ、セトレモン、ディスペンス}

    DD =(セトレンジ→O |セトレモン→L)

    O =(分注→O | setlemon→L | setorange→O)

    L =(ディスペンス→L | setorange→O | setlemon→L)


    最初にモードを選択した後(マシンの初期設定と呼びましょう)、マシンは2つの状態のいずれかであり、それぞれの状態で特定の飲み物を注ぎ、そこから2番目の状態に移行できることがわかります。 「オレンジ」モードで「オレンジ」ボタンを押すことができますが、効果はありません。

  2. 番号付き変数を使用して、無限の数の方程式を定義できます。 オブジェクトが地面から始まり、地面上を移動できるようにし(このアクションを呼び出しましょう)、立ち上がることができます(このアクションを呼び出しましょう)。 空中にある物体は、上昇(上昇)または下降(下降)することができますが、地上では、さらに下降することはできません。 したがって、n個の自然数(0、1、2、...)のセットを取得すると、このオブジェクトの動作を次のように書き留めることができます。

    CT 0 =(上→CT 1 |周囲→CT 0

    CT n + 1 =(上→CT n + 2 |下→CT n


    最初の方程式は、地球上のオブジェクトと空中の他のすべてのオブジェクトの動作を説明します。



    したがって、間接再帰により、プロセスの操作を記述する無限の数のルールを定義しました。


おわりに



読み書きの便宜のために、記事のサイズをわずかに小さくします。これにより、より頻繁に書くことができればと思います。



次のパートでは、プロセスのグラフィカルな表現、基本的な法則の導出、プロセスモデルの実装を示します。 本の最後はLispの助けを借りて実装されましたが、多くの人にとってより馴染みやすく理解しやすいように、Pythonの例を書き直そうとします。



All Articles