Think Stitch
PRINCIPIA  最近の更新


Scheme で CSP の表示的意味を計算する 〜 トレース編

CSP の式からその表示的意味の1つであるトレース集合を求める関数を作ってみます. 再帰のない簡単な場合だけを扱います.

CSP の表示的意味の表式は結構複雑なものが多いですよね. こういう定義の意味を理解するには,いくつも例を作って実際に計算してみるのが近道です. さらに,プログラムを書いてみると理解を深めることができるでしょう.

CSP コア言語の定義

まず始めに,対象とする CSP 式の範囲を定めます. 楽しみをすべてとってしまっては申し訳ないので,次のような小さな部分集合を設定することにします. いつものようにプロセスはS式で表します.

P ::= STOP
    | (! e P)
    | (alt P P)
    | (hide X P)
    | (par X P)

並行合成のインターフェイスと隠蔽のイベント集合は,シンボルのリストで表すことにします.

表示的意味の表現

トレースモデルでの表示的意味は,トレースの集合です. トレースはイベントの列ですから,そのまま Scheme のリストとして表すことにします. イベントは名前のシンボルで表します. 例を挙げるとこんな感じです.

(up down up down up)

トレースの集合はトレースのリストで表すことにします. したがってトレース集合は,シンボルのリストのリスト,つまりネストしたリストになります.

(()
 (up)
 (up down)
 (up down up)
 (up down up down)
 (up down up down up))

空のトレースは空列 () で表されることになります.

リストで集合を表すので,SRFI-1 の lset 系関数を使うことにします.

トレース集合を計算する関数 traces

トレース集合を計算する関数をそのままずばり traces とします. 以前に紹介したパターンマッチのマクロ dbind-case を使って CSP の式を分類していくことにします.

停止プロセス STOP

停止プロセス STOP のトレースは空列だけです.したがってトレース集合は 空列だけを要素とする集合,ここではリストになります.

(define (traces P)
  (dbind-case P
    (STOP '(()))
    ...

イベントの発生 Prefixing

イベントを発生させる式 Prefixing のトレースは次のように定義されています.

\[ \textit{traces}(a \rightarrow P) = \{ \langle \rangle \} \cup \{ \langle a \rangle^\smallfrown \textit{tr}\ |\ \textit{tr} \in \textit{traces}(P) \} \]

プロセス P の各トレースの先頭にイベントを付け加えればいいということになります. あと空列を加えておきます.

(define (traces P)
  (dbind-case P
    (STOP '(()))
    ((! ?e ?Q)
     (cons '()
           (map (lambda (tr) (cons ?e tr))
                (traces ?Q))))
    ...

選択 alt

選択のトレース集合は,引数である各プロセスのトレース集合の和集合になります.

\[ \textit{traces}(P\ \square\ Q) = \textit{traces}(P) \cup \textit{traces}(Q) \]

和集合を求める関数 lset-union を使えば,そのままの記述になります.

(define (traces P)
  (dbind-case P
    ...
    ((alt ?Q ?R)
     (lset-union eq? (traces ?Q) (traces ?R)))
    ...

隠蔽 hide

隠蔽されたプロセスのトレース集合は,元のプロセスのトレースから,イベントの集合 X に含まれるイベントを取り除いてできるトレースの集合になります. そこでトレース s からイベントの集合 X に含まれる要素を取り除いてできる残りのトレースを s \ X で表すことにすれば,トレース集合は次のようになります.

\[ \textit{traces}(P \setminus X) = \{ s \setminus X \ |\ s \in \textit{traces}(P) \} \]

s \ X は関数として次のように簡単に定義できます.

(define (trace-hide X s)
  (if (null? s)
      '()
      (if (memq (car s) X)
          (trace-hide X (cdr s))
          (cons (car s) (trace-hide X (cdr s))))))

あとは Prefixing のときと同じようにプロセス P のトレース集合に関数を適用すればいいのですが,一点注意すべきところがあります. それは元のプロセスの異なるトレースから,同一のトレースが生成される場合があるという点です. 例えば次の2つのトレースは,X = {e} の元で隠蔽すると同じトレースになります.

(a b e a b)
(a b a b e e)

単純に map を使うと,これらの要素が重複して現れてしまうので,代わりに fold-left を使って重複を取り除きながら集合を作ります.

(define (traces P)
  (dbind-case P
    ...
    ((hide ?X ?Q)
     (fold-left
      (lambda (acc s)
        (lset-adjoin equal? acc (trace-hide ?X s)))
      '() (traces ?Q)))
    ...

並行合成 par

並行合成もトレースに関する並行合成の関数を使って次のように定義されています.

\[ \textit{traces}(P\ \underset{X}{||}\ Q) = \{ s\ \underset{X}{||}\ t\ |\ s \in \textit{traces}(P) \land t \in \textit{traces}(Q) \} \]

トレースに関する並行合成は次のように定義されています. ここで変数 x と x' はイベントの集合 X に含まれているイベント,y, y' は含まれていないイベントとします. 表式は複雑ですが,平たくいうと,イベントの集合 X に含まれているイベントは同期しなければならず,含まれていない場合はインターリーブになるということです.

\[ s\ \underset{X}{||}\ t = t\ \underset{X}{||}\ s \] \[ \langle\rangle\ \underset{X}{||}\ \langle\rangle = \{\langle\rangle\} \] \[ \langle\rangle\ \underset{X}{||}\ \langle x \rangle = \{\} \] \[ \langle\rangle\ \underset{X}{||}\ \langle y \rangle = \{\langle y \rangle\} \] \[ \langle x \rangle^\smallfrown s\ \underset{X}{||}\ \langle y \rangle^\smallfrown t = \{\langle y \rangle^\smallfrown u\ |\ u \in \langle x \rangle^\smallfrown s \ \underset{X}{||}\ t \} \] \[ \langle x \rangle^\smallfrown s\ \underset{X}{||}\ \langle x \rangle^\smallfrown t = \{\langle x \rangle^\smallfrown u\ |\ u \in s \ \underset{X}{||}\ t \} \] \[ \langle x \rangle^\smallfrown s\ \underset{X}{||}\ \langle x' \rangle^\smallfrown t = \{\} \qquad \textrm{if}\ x \neq x' \] \[ \langle y \rangle^\smallfrown s\ \underset{X}{||}\ \langle y' \rangle^\smallfrown t = \{\langle y \rangle^\smallfrown u\ |\ u \in s \ \underset{X}{||}\ \langle y' \rangle^\smallfrown t \} \cup \{\langle y' \rangle^\smallfrown u\ |\ u \in \langle y \rangle^\smallfrown s \ \underset{X}{||}\ t \} \]

これを計算する関数は次のようになります. ちょっと冗長ですが,わかりやすさを優先しました. 結果は隠蔽の時と異なり,トレースではなく,トレースの集合になります.

(define (trace-par-prefix X e s t)
  (map (lambda (tr)
         (cons e tr))
       (trace-par X s t)))

(define (trace-par X s t)
  (cond ((and (null? s) (null? t))
         '(()))
        ((or (null? s) (null? t))
         (let ((u (if (null? s) t s)))
           (if (memq (car u) X)
               '()
               (trace-par-prefix X (car u) '() (cdr u)))))
        ((and (memq (car s) X) (memq (car t) X))
         (if (eq? (car s) (car t))
             (trace-par-prefix X (car s) (cdr s) (cdr t))
             '()))
        ((memq (car s) X)
         (trace-par-prefix X (car t) s (cdr t)))
        ((memq (car t) X)
         (trace-par-prefix X (car s) (cdr s) t))
        (else
         (lset-union equal?
           (trace-par-prefix X (car s) (cdr s) t)
           (trace-par-prefix X (car t) s (cdr t))))))

関数 traces の par 部分は次のようになります. fold-left を2つネストして,プロセス ?Q と ?R のトレースのすべての組み合わせを列挙します.

(define (traces P)
  (dbind-case P
    ...
    ((par ?X ?Q ?R)
     (fold-left
      (lambda (acc s)
        (fold-left
         (lambda (acc t)
           (lset-union equal?
             acc (trace-par ?X s t)))
         acc (traces ?R)))
      '(()) (traces ?Q)))
    ...

関数 traces

以上をまとめると,関数 traces は次のようになります.

(define (traces P)
  (dbind-case P
    (STOP '(()))
    ((! ?e ?Q)
     (cons '()
           (map (lambda (tr) (cons ?e tr))
                (traces ?Q))))
    ((alt ?Q ?R)
     (lset-union eq? (traces ?Q) (traces ?R)))
    ((hide ?X ?Q)
     (fold-left
      (lambda (acc s)
        (lset-adjoin equal? acc (trace-hide ?X s)))
      '() (traces ?Q)))
    ((par ?X ?Q ?R)
     (fold-left
      (lambda (acc s)
        (fold-left
         (lambda (acc t)
           (lset-union equal?
             acc (trace-par ?X s t)))
         acc (traces ?R)))
      '(()) (traces ?Q)))
    (else
     (assertion-violation 'traces "invalid process" P))))

計算例

(traces '(! a (alt (! b (! x STOP)) (! c (! y STOP)))))
=> (() (a c y) (a c) (a) (a b) (a b x))
(traces '(hide (b c)
           (! a (alt (! b (! x STOP)) (! c (! y STOP))))))
=> ((a x) (a) (a y) ())
(traces '(par (a)
           (! a (alt (! b STOP) (! c STOP)))
           (! x (! a (! y STOP)))))
=> ((x a b y) (x a y b) (x a b) (x a y) (x a) (x a c y)
    (x a y c) (x a c) (x) ())
2013/11/17
© 2013,2014,2015 PRINCIPIA Limited