Think Stitch
PRINCIPIA  最近の更新


非決定的計算と並行計算

非決定的計算と並行計算について書きます。まず非決定的選択の話といくつかの準備をします。次にそれらを使った不思議なプログラムを紹介します。最後にこれを並行計算に置き換えてみます。

非決定的選択

双対性のところで命令型プログラムの非決定的選択演算子の話を書きました。2つの命令(文)A, B があったとき、どちらかを任意に選んで実行する文を次のように書きます。

\[ A \,\square\, B \]

例えば次の文を実行すると、実行後の変数 x の値は 1 または 2 のどちらかになります。

\[ x := 1 \,\square\, x := 2 \]

文の意味を状態空間上での関係として表すと、非決定的選択演算子の意味は関係の和集合になります。

\[ \mathcal{M}[\![A\ \square\ B]\!] = \mathcal{M}[\![A]\!] \cup \mathcal{M}[\![B]\!] \]

例えば先ほどの代入文の例で、変数は x 1つしかなくて、したがって状態を変数 x の値で表すことができるとすると、代入文 x := 1, x := 2 それぞれの意味は次のようになるでしょう。

\[ \begin{split} \mathcal{M}[\![x := 1]\!] &= \{\ldots, (-2, 1), (-1, 1), (0, 1), (1, 1), (2, 1), \ldots\} \\ \mathcal{M}[\![x := 2]\!] &= \{\ldots, (-2, 2), (-1, 2), (0, 2), (1, 2), (2, 2), \ldots\} \end{split} \]

代入で元の変数の値は失われてしまうので、要するにすべての値が 1 または 2 に対応するということです。

そうすると2つの代入文の非決定的選択の意味は、これらの和集合なので次のようになります。

\[ \begin{split} &\mathcal{M}[\![x := 1\,\square\,x := 2]\!] \\ =& \{\ldots, (-1, 1), (-1, 2), (0, 1), (0, 2), (1, 1), (1, 2), (2, 1), (2, 2), \ldots\} \end{split} \]

これも要するに各値について 1 と 2 が対応するということになります。これは1つの値に対して2つの値が対応していますから真に関係になっていて、関数で表すことはできません。非決定性がなければ命令型プログラムの意味を関数で表すことができます。

ガード

ここでもう1つ新しい文を導入します。ガードとかテストと呼ばれているもので、次のように書きます。

\[ p \rightarrow A \]

ここで p はプログラム変数からなる条件式、A は文です。ガードは単独の文というより文と条件式から新しい文を構成する演算子ということです。

文献によっては条件式だけから文を構成する流儀もあるようです。この場合は次のように書きます。

\[ p? \]

どちらの記法も(あと「ガード」という名前も) CSP と同じでややこしくてしょうがないのですけど、まあ仕方がありません。

このガードがどういう動作を表すかというと、条件式 p を評価して、その結果が真ならば文 A を実行し(p? の場合は次の文へ移行し)、そうでなければそこで停止するというんです。

プロセスだったら停止というのはわかりますけど(CSP なら STOP)、命令型プログラムの停止というのはあまり聞きなれないかもしれません。意味を見ると少しわかるかもしれません。ガードの意味は次のようになります。

\[ \mathcal{M}[\![p \rightarrow A]\!] = \{(i,o)\,|\,\mathcal{M}[\![p]\!]i \land (i,o) \in \mathcal{M}[\![A]\!]\} \]

ここで

\[ \mathcal{M}[\![p]\!]i \]

は事前状態 i で条件式 p を評価した結果、つまり真偽を表すとします。

ガードの意味を平たくいえば、文 A に対応する関係の要素のうち、条件式 p を満たすものだけを残すということです。

そうすると何が起こるかというと、ある事前状態 i に対応する関係の要素が存在しないということが起こりえます。したがって計算を実行することができないので停止するということのようです。

(これがチューリングマシンとかλ計算とどういう関係なのか知らないんですけど...簡約できない場合に対応するのでしょうか...)

このように、ある事前状態に対応する要素が欠けているような文を部分的というのだそうです。部分関数(partial function)、全域関数(total function)の部分(partial)と同じですね。理論的には考えることができるけど、実装はできないと考えるというようなことが書いてある本もありました。よくわかりませんが。

ガードを使うと文は部分的になってしまいますけど、非決定的選択と合わせると全域性(実現性)を復活させることができます。例えば if 文

\[ \mathrm{if}\ p\ \mathrm{then}\ A\ \mathrm{else}\ B\ \mathrm{fi} \]

を次のように表すことができます。

\[ p \rightarrow A \ \square\ \neg p \rightarrow B \]

これを見ると非決定的選択とガードは if 文よりもよりプリミティブな言語要素だと考えることができます。はさみとのりという感じです。この例だとガードの条件は排他的でかつ全域的(MECE というんですか?)ですけど、排他的でなければ非決定性が現れて、全域的でなければ(あたりまえですけど)部分的になります。

逐次実行

もう1つ演算子を見ます。文 A, B を逐次的に実行することを表す演算子で、セミコロンで表します。

\[ A; B \]

いろいろあったそうで(?)、一部の言語では文末の印になってしまいましたけど、文のセパレータだったこともあった(?)そうです。

\[ \mathrm{begin}\ S_1; S_2; \ldots; S_n\ \mathrm{end} \]

(つまり Snの後ろにはつけないと。あっても空文になるだけ、という言語もあるそうですけど。)

先ほどの if 文の例のように、セミコロン自体をもっと理論的に純化すると、文の連接演算子と見なすことができるというわけです。これも CSP と同じです(というかここから来たのだと思います。単位元が SKIP だし。)。

逐次実行の意味は次のようになります。(A, B は意味である関係と同一視)

\[ \mathcal{M}[\![A; B]\!] = \{(i,o)\,|\,\exists s. (i,s) \in A \land (s,o) \in B \lor (i,\bot) \in A \land o=\bot\} \]

⊥を使わない流儀ではもっとシンプルになります。

\[ \mathcal{M}[\![A; B]\!] = \{(i,o)\,|\,\exists s. (i,s) \in A \land (s,o) \in B \} \]

要するにこれは関係の合成そのものです(こちらはまじめに意味関数を書きました)。

\[ \mathcal{M}[\![A; B]\!] = \mathcal{M}[\![A]\!]; \mathcal{M}[\![B]\!] \]

不思議なプログラム

この逐次実行の連接演算子、一見あたりまえのことを言っているように見えますけど、実はこれらを使うと不思議なプログラムが書けるんです。配列 v (大きさ N)が与えられたとき、要素の中から条件 p(x) を満たすものを求めたいとします。命令型プログラムならふつうはループを書きますよね。次のコードを見てください。

\[ (k:=0\,\square\,k:=1\,\square\,\cdots\,\square\,k:=N-1); p(v[k]) \rightarrow x := v[k] \]

もし非決定的選択演算子の限量子版が与えられているとすると、もっとかっこよく書けます。

\[ \left(\square_{j=0}^{N-1}k := j\right); p(v[k]) \rightarrow x := v[k] \]

何をしている(言っている)のかというと、まず配列のインデックスを非決定的に1つ選んで変数 k に代入します。そしてもし配列の要素 v[k] が条件 p(v[k]) を満たしていたら変数 x に代入しろというのです。

もし条件を満たすものがなければもちろんプログラムはガードのところで停止してしまいます。しかし仮に条件を満たす要素があったとしても、インデックスを非決定的に選んでいるので、たまたま条件を満たさないものが選ばれてしまえばプログラムは停止してしまうように見えます。

ところがそうではないのです。もし配列の中に条件を満たすものがあれば、このプログラムは必ずそれを見つけます。関係の意味に置き換えて考えてみてください。最初の非決定的選択の意味では、すべての状態がすべてのインデックスに対応することになりますよね。これとガードを結合すると、逐次実行演算子の意味、すなわち関係の連接演算によって、(あれば)かならず条件を満たすインデックスが選ばれることになります。定義の中にある存在限量が探索的な役割を果たしてしまうのです。そういう意味で、逐次実行演算子の意味はあまり"あたりまえ"ではないのですね。

非決定的選択演算子 amb

ではこのプログラムを本当に実行することができるのかというと、できます。ご存知の方も多いと思いますけれども、SICP の 4.3 節で非決定性計算と称してオペレータ amb というものが紹介されています。元は John McCarthy さんの論文 A BASIS FOR A MATHEMATICAL THEORY OF COMPUTATION の 2.5 Ambiguous Functions で紹介されたものだそうです。元論文の方を見ると導入本来の動機は、一群の複雑な関数についての性質を議論するための道具という意味合いであったようです。複数の値から非決定的に選択して返すことができる関数の拡張のようなものを考えて、その性質を議論します。これを使って間接的に複雑な関数の性質を証明しようということだそうです。命令や関数の性質を論理式、例えば事前・事後条件で表すと非決定性が現れることがあります。これと同じことを関数を拡張した枠組みの中でやろうという話のように見えました。

一方 SICP の方では非決定的選択演算子を実際に動くように実装しようという話が書いてあります。存在限量の部分をバックトラックによって自動的に探索します。そういう意味では論理型計算のある実装に似ています。バックトラック、つまり深さ優先探索なので、探索の順序によっては存在する解が見つからない場合もあるようです。効率が悪いという問題もあるでしょう。

非決定性と詳細化関係

効率というと実践的な話だけのようにも思えますが、実は理論的にも深い意味があります。上の不思議なプログラムを M として、これをループで書き直したふつうのプログラムを L とすると、この2つの間には詳細化関係(正当性関係)が成立ちます。

\[ M \sqsubseteq L \]

逆は成立ちません。ふつうループで書いたプログラムに非決定性はありませんけど、M には非決定性が残っているからです。一般的にいって、プログラムを詳細化するということは非決定性を減らして、ある意味効率よく動くプログラムに変換するということです。これは CSP の詳細化でも同じことです。

非決定的計算の並行実行

深さ優先探索の欠点を克服するために、もっと革新的な方法があります。SICP の 4.3.1 節でも言及されていますが、非決定的選択が現れたところでそれぞれの選択肢にプロセッサを割り当て、同時並行的に計算を進めるという方法です。計算の実行が継続できなくなった選択肢(ガード、あるいは amb ならば選択肢なし)に割り当てられているプロセッサは解放します。計算の分岐を消滅させるということです。

Peter Henderson さんの Functional Programming(邦訳:関数型プログラミング)では、実際にこの方法で非決定的計算を実行せよという演習問題があります。この本では amb ではなく or と none という2つのプリミティブが使われています。おおざっぱにいうと次のような対応になります。

\[ \begin{split} A\ \mathbf{or}\ B &= \mathtt{(amb}\ A\ B \mathtt{)} \\ \mathbf{none} &= \mathtt{(amb)} \end{split} \]

この本では(これもおそらく有名だと思いますが)SECD 機械という仮想機械を使って LISP を実装しています。仮想機械自体も LISP で書かれていて、仮想機械のインスタンスを簡単に複数生成して並行実行することができます(演習でそうしなさいと書いてあるだけですけど)。そこで文字通り、or が現れたら仮想機械を複製して並行に実行します。none に出会った仮想機械は消滅します。こうすればバックトラックと異なり最短の時間で必ず解を見つけることができます。深さ優先探索に比較していえば、並行幅優先探索といったところでしょうか。

CSP による並行探索

非決定的選択演算子や amb は命令型、関数型のスタイルのままでより抽象度の高いレベルで解を記述するという意味合いが強いと思われるので、手作業で並行プロセスに書き換えることは記述という面ではそれほど興味深いわけではないのですけど、それでもおおまかにいえば、非決定的選択演算子を並行合成演算子に置き換えればよいわけで、対応という面ではそれなりに面白いと思われます。ただし、解が見つかったあとの処理や、解が存在しなかった場合の処理をきちんとする必要があるでしょう。この点は上の話でも同じですけど。

いつものように単純な問題で考えて見ます。プロセス D はチャネル a を通して配列を受け取るとします。その要素の中に与えられた条件を満たすものが1つでもあれば任意に(つまり非決定的に)選んで、チャネル f を通じて出力します。もし条件を満たすものがなければイベント e を発生させるものとしましょう。

基本的な戦略は上の不思議な計算と同じです。非決定的選択演算子を並行合成演算子に置き換えて、配列要素の数だけ条件を調べるプロセスを生成します。要素はプロセス生成時にプロセスパラメータとして渡すことにします。

各プロセス Pk は条件を満たせば値をチャネル c を通じて出力し、条件を満たさなければイベント d を発生させるものとします。これらをインターリーブして、プロセス C で受けます。プロセス C は初めて c.x を受け取ったら即座に f.x を出力します。2個目以降の c.x' に対しては f.x' は出しません。並行して c.x と d の数をそれぞれ数えます。合計が配列の大きさと同じになったらすべてのプロセスが処理を完了したということです。このとき d の数が配列の大きさと一致していたら解がなかったということですからイベント e を発生させます。

イベント・チャネル定義

プロセス構成図にあるとおりにイベントとチャネルを定義します。配列はリストで表します。要素に重複が生じるように組み合わせを使いました。後に出てくる遷移リストを見てください。

(define N 3)

(define DI (interval 0 N))
(define DD (map list DI))
(define DL
  (map list
       (combinations
        (map (lambda (k) DI) DI))))

(define-channel a (v) DL)
(define-channel c (x) DD)
(define-channel f (x) DD)
(define-event d)
(define-event e)

プロセス D

プロセス D はまずチャネル a を通じてリストを受け取ります。 そうしたら各要素についてプロセス P を起動します。 非決定的選択演算子の限量子を xpar に置き換えたということになります。 加えて、結果を集積するプロセス C を起動します。

(define-process D
  (? a (v)
     (par (list c d)
       (xpar x v '() (P x))
       (C (length v) 0 0))))

プロセス P

プロセス P は担当する配列の要素をプロセスパラメータ x として受け取ります。 ここでは簡単のために条件判定は要素が 0 であるかどうかとします。 条件が成立てばチャネル c から出力し、成立たなければイベント d を発生させます。 いずれの場合も処理後終了します。

(define-process (P x)
  (if (= x 0)
      (! c (x) SKIP)
      (! d SKIP)))

プロセス C

プロセス C は結果を集積するプロセスです。3つのプロセスパラメータ n, i, j を持ちます。 n は配列の大きさです。i, j はそれぞれ条件が成立した数としなかった数です。

条件成立の報をチャネル c からはじめて受け取ったときには、即座に f.x を出力します。 これは後段をできるだけ早く起動して並行性を高めるためです。

あとは成立・不成立の数を数えて、すべて不成立だったときだけイベント e を発生させます。

(define-process (C n i j)
  (if (= n (+ i j))
      (if (= n j)
          (! e SKIP)
          SKIP)
      (alt
        (? c (x)
           (if (= i 0)
               (! f (x) (C n 1 j))
               (C n (+ i 1) j)))
        (! d (C n i (+ j 1))))))

シミュレーション

0が存在しない場合、1つだけある場合、2つある場合と3つの場合について見てみます。

0がない場合はすべてのプロセス P がイベント d を発生させます。

イベント d が1つ発生したところです。プロセス木を見るとプロセス C のカウント j が 1 になったことがわかります。

j が配列の大きさ 3 になると、条件未成立のイベント e が発生します。

0が1個含まれている場合、c.0 が発生したらすぐに f.0 が発生します。ただし、別のプロセスが発生させた d を先に受けてしまう場合もあります。これについてはあとで検討します。

解が複数ある場合は並行性から来る非決定性が現れることになります。f.0 が発生するのは最初の c.0 の直後だけです。

正当性検査

仕様プロセスを作って正当性検査をしてみます。仕様は以下のとおりです。

(define-process SPEC
  (? a (v)
     (if (memv 0 v)
         (! f (0) SKIP)
         (! e SKIP))))

シミュレーションしてみるとこうなります。

仕様と比較するために、内部で使用しているイベントを隠蔽します。

(define-process DH
  (hide (list c d) D))

検査結果は以下のとおりです。完全に一致することがわかります。

パフォーマンスの改善

上の設計では、結果の集積プロセス C が不成立イベント d も受け取るので、チャネル通信部分の実装によっては成立したプロセスからの通知が待たされてしまう可能性があります。そこで並行性をさらに高めるために、集積プロセスを2つに分けることにします。

おおまかにいうと、プロセス E は条件が成立した際の通知 c.x だけを受け取り、プロセス F は不成立のイベント d を受け取ります。このようにして E と F を並列に動かせば、成立した場合の通知をできるだけ早く後段に送ることができます。

単に分離しただけだと、すべての処理が完了したことを知ることができず、さらに条件が成立する要素が1つもなかった場合を識別することができません。そこで、先のプロセス C が行っていたカウントの仕事はプロセス F が行うことにして、E は成功した場合をイベント h で通知することにします。

これでプロセス F は完了を知ることができるようになりましたが、プロセス E は終了のタイミングを知ることができません。そこで終了についてはプロセス F からイベント g で教えてもらうことにします。これは c.x との並行待ちになりますが、最後に発生するだけなのでパフォーマンスには影響しません。

モデルを以下のように修正します。

(define-event h)
(define-event g)
(define-process D2
  (? a (v)
     (par (list d h g)
       (F (length v) 0 0)
       (par (list c)
         (xpar x v '() (P x))
         (E 0)))))
(define-process (E i)
  (alt
    (? c (x)
       (if (= i 0)
           (! f (x)
              (! h (E 1)))
           (! h (E (+ i 1)))))
    (! g SKIP)))
(define-process (F n i j)
  (if (= n (+ i j))
      (if (= n j)
          (! e (! g SKIP))
          (! g SKIP))
      (alt
        (! h (F n (+ i 1) j))
        (! d (F n i (+ j 1))))))
(define-process D2H
  (hide (list c d h g) D2))

検査によって質的な動作は同じであることがわかります。

まとめ

非決定的計算と並行計算について書きました。 まず命令型プログラミング言語の要素を3つ紹介しました。

これらを使った不思議なプログラムを紹介しました。非決定的なプログラムは、何か上の方から俯瞰して、先を見通して適切な選択肢を選べるような感じがしました。それは関係の連接に含まれる存在限量のおかげでした。

SICP で紹介されている amb オペレータを使えば、非決定的プログラムをそのままで実際に動かすことができます。これは適切な選択肢をバックトラックによって探索するというものです。しかし利用者はそのことを意識せずに解を記述することができます。

非決定性と詳細化の関係について触れました。

最後に非決定的プログラムを並行プログラムに書き換えてみました。こちらは探索の構造をやや意識する感じになりますが、解を効率よく確実に見つけることができます。

2014/03/15
© 2013,2014,2015 PRINCIPIA Limited