Think Stitch
PRINCIPIA  最近の更新


Scheme で CSP の表示的意味を計算する 〜 安定失敗編

前回のトレース編からの続きで,安定失敗意味論での表示的意味を計算する関数を作ってみます. 「安定失敗」って日本語で書くと,いつも決まって失敗しているみたいな感じがします :P

CSP コア言語

対象とする CSP の式の範囲は,前回のものに1つ,非決定的選択を加えます. 選択(外部選択)と非決定的選択(内部選択)の区別ができるところが,安定失敗意味論のポイントなので,その点を見るためです. 今回も終了は扱いません.終了イベント tick は無視します.拡張してお楽しみください :P

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

表示的意味の表現

安定失敗意味論での表示は,トレースと拒否のペアの集合になります. トレースは前回と同じく,イベントを表すシンボルのリストで表します. 集合も前回同様リストで表すので,拒否はシンボルのリストになります. この2つをペアにして,さらにリストにします.

例えば,トレース (a b) を実行後の状態で {a, c, d} を拒否する場合は次のようになります.

((a b) . (a c d))

補助関数

あとで必要になる補助関数を2つ用意しておきます.

ベキ集合 lset-power

与えられた集合のベキ集合を求める関数を lset-powerset とします. アルファベットのすべての部分集合を求めるために使います.

(define (lset-powerset x)
  (if (null? x)
      '(())
      (let ((ps (lset-powerset (cdr x))))
        (append ps
                (map (lambda (s) (cons (car x) s)) ps)))))

安定失敗の同値 failture=?

2つの安定失敗 (trace . refusals) が同じかどうかを判定する述語を failure=? とします.

(define (failure=? p q)
  (and (equal? (car p) (car q))         ; trace
       (lset= eq? (cdr p) (cdr q))))    ; refusals

安定失敗集合を計算する関数 failures

安定失敗集合を計算する関数を failures とします. 拒否の計算をするにはプロセスのアルファベットが必要なので,関数 failures はプロセス P とアルファベット A の2つの引数をとることにします. はじめにアルファベット A のベキ集合 PA を求めておきます.

前回と同じく,ちょとはずかしいパターンマッチのマクロ dbind-case を使って CSP の式を分類していきます.

(define (failures P A)
  (let ((PA (lset-powerset A)))
    (define (F p)
      (dbind-case p
        (STOP
         ...

停止プロセス STOP

停止プロセスは空列 () だけをトレースとしてもち,すべてを拒否します. そこで,アルファベットのベキ集合 PA の各要素と () をペアにすれば求める表示が得られます.

\[ \textit{failures}(\textit{STOP}) = \{(\langle \rangle, X)\ |\ X \subseteq \Sigma \} \]

(define (traces P)
  (dbind-case P
    (STOP
     (map (lambda (X) (cons '() X)) PA))
    ...

イベントの発生 Prefixing

初期状態ではイベント a を含む集合は拒否しません. イベント a が発生した後は,プロセス P が拒否するものを拒否します.

\[ \begin{split} \textit{failures}(a \rightarrow P) = & \{(\langle \rangle, X)\ |\ a \notin X \} \cup \\ & \{(\langle a \rangle^\frown s, X)\ |\ (s, X) \in \textit{failures}(P) \} \end{split} \]

それぞれの項から生成される安定失敗はトレースが異なるので排他的です. したがって append で連結するだけで済みます.

(define (failures P A)
  (let ((PA (lset-powerset A)))
    (define (F p)
      (dbind-case p
        ...
        ((! ?a ?p)
         (append
          (map (lambda (X) (cons '() X))
               (remp (lambda (X) (memq ?a X)) PA))
          (map (lambda (p) (cons (cons ?a (car p)) (cdr p)))
               (F ?p))))
        ...

選択 alt

初期状態では,両方のプロセスが拒否するものだけを拒否します. どちらかが拒否しなければ,そちらが選択されるからです. それ以降は選択された方のプロセスが拒否するものを拒否します.

\[ \begin{split} \textit{failures}(P\ \square\ Q) = & \{(\langle \rangle, X)\ |\ (\langle \rangle, X) \in \textit{failures}(P) \cap \textit{failures}(Q)\} \cup \\ &\{(s, X)\ |\ (s, X) \in \textit{failures}(P) \cup \textit{failures}(Q) \land s \neq \langle \rangle \} \end{split} \]

(define (failures P A)
  (let ((PA (lset-powerset A)))
    (define (F p)
      (dbind-case p
        ...
        ((alt ?p ?q)
         (let ((Fp (F ?p))
               (Fq (F ?q)))
           (lset-union failure=?
             (filter (lambda (p) (null? (car p)))
                     (lset-intersection failure=? Fp Fq))
             (remp (lambda (p) (null? (car p))) Fp)
             (remp (lambda (p) (null? (car p))) Fq))))
        ...

非決定的選択 ndc

非決定的選択の安定失敗集合は,各プロセスのそれの単なる和集合になります.

\[ \textit{failures}(P\ \sqcap\ Q) = \textit{failures}(P) \cup \textit{failures}(Q) \]

(define (failures P A)
  (let ((PA (lset-powerset A)))
    (define (F p)
      (dbind-case p
        ...
        ((ndc ?p ?q)
         (lset-union failure=? (F ?p) (F ?q)))
        ...

隠蔽 hide

\[ \textit{failures}(P \setminus X) = \{ (s \setminus X, Y) \ |\ (s, Y \cup X) \in \textit{failures}(P) \} \]

トレースの隠蔽 s \ X を求めるには,前回定義した関数 trace-hide を使います. 定義はあまり計算には向かない形になっています. まず Y ∪ X が拒否でなければならないので,X を含む拒否 R を選びます. すると,Y ∪ X = R となる Y は,X の各部分集合 C について,R - C とすればよいことがわかります.

(define (failures P A)
  (let ((PA (lset-powerset A)))
    (define (F p)
      (dbind-case p
        ...
        ((hide ?X ?p)
         (let ((PX (lset-powerset ?X)))
           (fold-left
             (lambda (acc p)
               (let ((t (trace-hide ?X (car p)))
                     (Y_Un_X (cdr p)))
                 (fold-left
                   (lambda (acc C)
                     (lset-adjoin failure=?
                                  acc
                                  (cons t (lset-difference eq? Y_Un_X C))))
                   acc PX)))
             '() (filter (lambda (p) (lset<= eq? ?X (cdr p))) (F ?p))))))
        ...

並行合成 par

並行合成の安定失敗集合の定義は次のとおりです.

\[ \begin{split} \textit{failures}(P\ \underset{X}{||}\ Q) =& \{ (u, Y \cup Z) \ |\ & Y - X &= Z - X \land \\ & & (\exists s, t. & (s, Y) \in \textit{failures}(P) \land \\ & & & (t, Z) \in \textit{failures}(Q) \land \\ & & & u \in s\ \underset{X}{||}\ t) \} \end{split} \]

定義の意味は置いておくとして,計算はやや強引ですがそのままできます.

(define (failures P A)
  (let ((PA (lset-powerset A)))
    (define (F p)
      (dbind-case p
        ...
        ((par ?X ?p ?q)
         (fold-left
           (lambda (acc p)
             (fold-left
               (lambda (acc q)
                 (if (lset= eq? 
                            (lset-difference eq? (cdr p) ?X)
                            (lset-difference eq? (cdr q) ?X))
                     (fold-left
                       (lambda (acc u)
                         (lset-adjoin failure=? acc
                                      (cons u (lset-union eq? (cdr p) (cdr q)))))
                       acc (trace-par ?X (car p) (car q)))
                     acc))
               acc (F ?q)))
           '() (F ?p)))
        ...

関数 failures

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

(define (failures P A)
  (let ((PA (lset-powerset A)))
    (define (F p)
      (dbind-case p
        (STOP
         (map (lambda (X) (cons '() X)) PA))
        ((! ?a ?p)
         (append
          (map (lambda (X) (cons '() X))
               (remp (lambda (X) (memq ?a X)) PA))
          (map (lambda (p) (cons (cons ?a (car p)) (cdr p)))
               (F ?p))))
        ((ndc ?p ?q)
         (lset-union failure=? (F ?p) (F ?q)))
        ((alt ?p ?q)
         (let ((Fp (F ?p))
               (Fq (F ?q)))
           (lset-union failure=?
             (filter (lambda (p) (null? (car p)))
                     (lset-intersection failure=? Fp Fq))
             (remp (lambda (p) (null? (car p))) Fp)
             (remp (lambda (p) (null? (car p))) Fq))))
        ((hide ?X ?p)
         (let ((PX (lset-powerset ?X)))
           (fold-left
             (lambda (acc p)
               (let ((t (trace-hide ?X (car p)))
                     (Y_Un_X (cdr p)))
                 (fold-left
                   (lambda (acc C)
                     (lset-adjoin failure=?
                                  acc
                                  (cons t (lset-difference eq? Y_Un_X C))))
                   acc PX)))
             '() (filter (lambda (p) (lset<= eq? ?X (cdr p))) (F ?p)))))
        ((par ?X ?p ?q)
         (fold-left
           (lambda (acc p)
             (fold-left
               (lambda (acc q)
                 (if (lset= eq? 
                            (lset-difference eq? (cdr p) ?X)
                            (lset-difference eq? (cdr q) ?X))
                     (fold-left
                       (lambda (acc u)
                         (lset-adjoin failure=? acc
                                      (cons u (lset-union eq? (cdr p) (cdr q)))))
                       acc (trace-par ?X (car p) (car q)))
                     acc))
               acc (F ?q)))
           '() (F ?p)))
        (else
         (assertion-violation 'failures "invalid process" p))))
    (F P)))

計算例

停止プロセス STOP はすべてを拒否します.

(failures 'STOP '(a b))
=> ((()) (() b) (() a) (() a b))

選択は初期状態で何も拒否しません.結果の順序は見やすくするために入れ替えました.

(failures '(alt (! a STOP) (! b STOP)) '(a b))
=>
((())

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

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

これに対して非決定的選択では,初期状態で {a}, {b} を拒否します. しかし {a, b} 両方を提示すると拒否しません.必ずどちらかが発生するからです.

(failures '(ndc (! a STOP) (! b STOP)) '(a b))
=>
((())
 (() a)
 (() b)

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

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

次の2つのプロセスは同じ意味です.

(failures '(! a STOP) '(a e))
=> ((()) (() e) ((a)) ((a) e) ((a) a) ((a) a e))
(failures '(hide (e) (! e (! a STOP))) '(a e))
=> (((a) a) ((a) e a) ((a)) ((a) e) (()) (() e))

tau 遷移混在系を非決定的選択の標準形に変換した例です. 同じ意味であることが確認できます.

(define Fa
  (failures '(hide (x)
               (alt (! x (! b STOP)) (! a STOP)))
            '(a b x)))

(define Fb
  (failures '(ndc
              (! b STOP)
              (alt (! a STOP) (! b STOP)))
            '(a b x)))

(lset= failure=? Fa Fb)
=> #t

並行合成の例です. a または b だけを発生したあとは,もう一方を拒否しないことがわかります. インターリーブだからです.

(failures '(par (e)
             (alt (! a STOP) (! e STOP))
             (alt (! b STOP) (! e STOP)))
          '(a b e))
=>
((())

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

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

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

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

 ((e))
 ((e) e)
 ((e) b)
 ((e) b e)
 ((e) a)
 ((e) a e)
 ((e) a b)
 ((e) a b e))
2013/11/23
© 2013,2014,2015 PRINCIPIA Limited