Think Stitch
PRINCIPIA  最近の更新


Isabelle による並行プログラミング言語の操作的意味論と表示的意味論の同値性証明

Theorem Prover Advent Calendar 2013の参加エントリです.

Lisp Advent Calendar 2013の方で,並行プロセスの理論 CSP (Communicating Sequential Processes) に基づいた小さな並行プログラミング言語を作りました.

ここでは,その並行プログラミング言語の2つの意味,操作的意味と表示的意味を定義して,2つの意味論が同値であることを証明してみたいと思います.

並行プログラミング言語の構文

並行プログラミング言語の構文は次のようなものです.実装したものと少し変えました.

プロセス式 ::=
      STOP
    | (! イベント プロセス式)
    | (alt プロセス式1 プロセス式2)
    | (par イベントリスト プロセス式1 プロセス式2)

変えたのは3カ所でです.1つは終了 SKIP の代わりに停止するプロセス STOP を入れました.終了の扱いはちょっと面倒なので手抜きです.もう1つはプロセス名を指定してそのプロセスに移行する構文を削りました.これがあると再帰が書けてしまうので,証明が恐ろしく難しくなるからです.3つ目は,alt と par で指定できるプロセスの数を2つに固定しました.これは書くのが面倒になるだけで表現力は失っていません.

おおまかな意味については,元の文書を見てください.

代数的データ型で構文とプログラムを表す

プログラムの意味を表すには,まずプログラムそのものをデータとして扱えるようにしなければなりません.そこで,上のS式による構文を Isabelle の代数的データ型で表します.

datatype 'e process =
  Stop
  | Prefix 'e "'e process"
  | Alt "'e process" "'e process"
  | Par "'e set" "'e process" "'e process"

'e はイベントを表す型パラメータです.コンストラクタはアルファベット大文字で始めなければならないので,適当に名前を付けました.並行合成 par のイベントリストは集合に変えました.

例えばイベント a, b を順に発生させた後に停止するプロセスは次のように表すことができます.

Prefix a (Prefix b Stop)

プロセスを動的に生成する場合は次のようになります.

Prefix a
  (Par {c}
    (Prefix b (Prefix c Stop))
    (Prefix c (Prefix d Stop)))

操作的意味論

操作的意味論はふつう推論規則で表します.例えばプロセス Prefix e P はイベント e を発生させることができて,発生後にはプロセス P に移行します.これを次のように書きます.

|-  Prefix e P  -e->  P

ここで |- はターンスタイルのつもり, P -e-> Q はプロセス P がイベント e を発生させてプロセス Q に移行することを表します.

選択 alt の場合は,前提を持つ2つの規則があります.

P -e-> P'  |-  Alt P Q  -e->  P'
Q -e-> Q'  |-  Alt P Q  -e->  Q'

並行合成には3つの推論規則があります.まず2つのプロセスが同期する場合です.

P -e-> P', Q -e-> Q'  |-  Par X P Q  -e->  Par X P' Q' (e : X)

あと2つは同期しない場合です.各プロセスが独立に遷移します.

P -e-> P'  |-  Par X P Q  -e->  Par X P' Q   (e ~: X)
Q -e-> Q'  |-  Par X P Q  -e->  Par X P Q'   (e ~: X)

停止プロセス STOP は遷移を持ちません.

帰納的定義集合

Isabelle には集合を帰納的に定義する機能があります.例えば次のようなものです.

  1. 0 は集合 E に含まれる.
  2. n が集合 E に含まれているならば n + 2 も E に含まれる.
  3. 以上の規則によるものだけが E の要素である.

最後の条件は「以上の条件を満たす集合の中で最小のものを E とする」と言われることもあります.

Isabelle では上の集合 E の定義を次のように書くことができます.

inductive_set E :: "nat set" where
 "0 : E" |
 "n : E ==> n + 2 : E"

操作的意味論を帰納的定義集合で表す

集合を帰納的に定義する機能を使って,操作的意味を表すことにします.

まず遷移 P -e-> Q を三つ組 (P, e, Q) で表すことにします.Isabelle には三つ組がないので,ペアを組み合わせて (P, (e, Q)) とすることにします.

どのようなプログラムが存在するかということは構文からわかります.それらの間にどのような遷移があるかということは操作的意味論からわかります.そこで操作的意味の表現として,すべてのプロセスのすべての遷移を格納した集合 transitions というものを考えます.定義は次のようになります.

inductive_set
  transitions :: "('e process * 'e * 'e process) set"
where
  prefix: "(Prefix e P, (e, P)) : transitions" |
  alt1:   "(P, (e, P')) : transitions
       ==> (Alt P Q, (e, P')) : transitions" |
  alt2:   "(Q, (e, Q')) : transitions
       ==> (Alt P Q, (e, Q')) : transitions" |
  par_async1: "[| (P, (e, P')) : transitions; e ~: X |]
       ==> (Par X P Q, (e, Par X P' Q)) : transitions" |
  par_async2: "[| (Q, (e, Q')) : transitions; e ~: X |]
       ==> (Par X P Q, (e, Par X P Q')) : transitions" |
  par_sync: "[| (P, (e, P')) : transitions;
                (Q, (e, Q')) : transitions; e : X |]
       ==> (Par X P Q, (e, Par X P' Q')) : transitions"

ごらんのとおり,操作的意味論そのままになります.各条件の前についている "prefix" 等は,証明の際に規則を参照するための名前です.つまり操作的意味論の推論規則の名前ということになります.

この集合 transitions にはすべての可能な遷移が含まれていて,それ以外には余計なものが入っていないということです.

表示的意味論

ここではトレース意味論という表示的意味論を使うことにします.トレースというのは,プロセスが初期状態から発生したイベントを時系列に並べたもののことをいいます.あるプロセスが与えられたとき,そのプロセスが発生しうるすべてのトレースを考えると,プロセスの動きを把握したことになります.そこでプロセスの"意味"として,可能なすべてのトレースの集合を考えます.これをプロセスのトレース集合といいます.

CSP の教科書によると,各構文のトレース集合は次のように定義されています.

\begin{align} & \textit{traces}(\textrm{STOP}) = \{\langle \rangle\} \\ & \textit{traces}(e \rightarrow P) = \{\langle \rangle\} \cup \{e^\smallfrown tr\,|\,tr \in \textit{traces}(P)\} \\ & \textit{traces}(P\ \square\ Q) = \textit{traces}(\textrm{P}) \cup \textit{traces}(\textrm{Q}) \\ & \textit{traces}(P\ \underset{X}{||}\ Q) = \\ & \qquad \{tr\,|\,\exists tr_1, tr_2. \\ & \qquad \qquad tr_1 \in \textit{traces}(P) \land \\ & \qquad \qquad tr_2 \in \textit{traces}(Q) \land \\ & \qquad \qquad \textrm{sync}\ \textit{tr}\ X\ \textit{tr}_1\ \textit{tr}_2 \} \end{align}

それぞれ上から順に STOP, イベント発生 Prefix, 選択 alt, 並行合成(プロセス生成)par を表す数学的記号とそのトレース集合です.述語 sync は,2つのプロセスがイベント集合 X の元でトレース tr1, tr2 を発生させるとき,それを並行合成したプロセスのトレースが tr であることを表します.定義は次のとおりです.

\begin{align} & \textrm{sync}\ \langle \rangle\ X\ \textit{tr}_1\ \textit{tr}_2 \equiv \textit{tr}_1 = \langle \rangle \land \textit{tr}_2 = \langle \rangle \\ & \textrm{sync}\ {\langle e \rangle^\smallfrown \textit{tr}}\ X\ \textit{tr}_1\ \textit{tr}_2 \equiv \\ & \qquad (e \in X \land \textrm{hd}\ \textit{tr}_1 = \textrm{hd}\ \textit{tr}_2 = e \land \\ & \qquad \qquad \textrm{sync}\ \textit{tr}\ X\ (\textrm{tl}\ \textit{tr}_1)\ (\textrm{tl}\ \textit{tr}_2)) \lor \\ & \qquad (e \notin X \land \\ & \qquad \qquad (\textrm{hd}\ \textit{tr}_1 = e \land \textrm{sync}\ \textit{tr}\ X\ (\textrm{tl}\ \textit{tr}_1)\ \textit{tr}_2) \lor \\ & \qquad \qquad (\textrm{hd}\ \textit{tr}_2 = e \land \textrm{sync}\ \textit{tr}\ X\ \textit{tr}_1\ (\textrm{tl}\ \textit{tr}_2))) \end{align}

表示的意味を関数で表す

表示的意味を関数で表します.まず述語 sync です.定義どおりです.

fun sync :: "'e list => 'e set => 'e list => 'e list => bool"
where
  "sync [] X s t = (s = [] & t = [])" |
  "sync (a#tr) X s t =
    ((a : X & s ~= [] & t ~= [] &
              hd s = a & hd t = a &
              sync tr X (tl s) (tl t)) |
     (a ~: X & ((s ~= [] & hd s = a & sync tr X (tl s) t) |
                (t ~= [] & hd t = a & sync tr X s (tl t)))))"

つづいてトレース集合を定義します.こちらも定義どおりです.

fun traces :: "'e process => 'e list set" where
  "traces Stop = {[]}" |
  "traces (Prefix e P) =
     ({[]} Un {tr. EX tr1. tr = e#tr1 & tr1 : traces P})" |
  "traces (Alt P Q) = (traces P) Un (traces Q)" |
  "traces (Par X P Q) =
     {tr. EX tr1 tr2. tr1 : traces P &
                      tr2 : traces Q &
                      sync tr X tr1 tr2}"

遷移関係からトレース集合を求める

以上で2つの意味論の記述は終わりました.次にこの2つが同値であること,つまり同じ"意味"であることを証明します.

しかしこのままでは表現が異なりますから比較することができません.そこで遷移関係からトレース集合を求めることにします.

まず遷移関係から,各プロセスが持つトレースをすべて求めます.これは再び帰納的定義を使えばかんたんです.

  1. すべてのプロセスは空のトレース [] を持ちます.
  2. プロセス Q がトレース tr を持っていて,P -e-> Q という遷移が存在したら,プロセス P は e#tr というトレースを持ちます.
inductive_set
  otraces_set :: "('e process * 'e list) set"
  where
  base [intro]: "(P, []) : otraces_set" |
  step [intro]: "[| (P, (e, Q)) : transitions;
                    (Q, tr) : otraces_set |]
            ==> (P, e#tr) : otraces_set"

この集合 otraces_set を使うと,操作的意味論に基づいたトレース集合 otraces P を定義できます.

definition otraces :: "'e process => 'e list set" where
  "otraces P == {tr. (P, tr) : otraces_set}"

これで比較の準備が整いました.

2つの意味論が同値あることの証明

説明抜きで証明だけ示します.

lemma t0 [dest]: "(Stop, (e, P)) : transitions ==> False"
apply(erule transitions.cases)
apply(auto)
done

lemma t1 [dest]: "(Stop, tr) : otraces_set ==> tr = []"
apply(erule otraces_set.cases)
apply(auto)
done

lemma t2: "(Prefix e P, a, Q) : transitions
  ==> a = e & Q = P"
apply(erule transitions.cases)
apply(auto)
done

lemma t3: "(Prefix e P, tr) : otraces_set
  ==> tr = [] |
      (EX tr1. tr = e#tr1 & (P, tr1) : otraces_set)"
apply(erule otraces_set.cases)
apply(auto dest: t2)
done

lemma t4: "(P, e#tr) : otraces_set
 ==> EX Q. (P, (e, Q)) : transitions &
           (Q, tr) : otraces_set"
apply(erule otraces_set.cases)
apply(auto)
done

lemma t5: "(P, tr) : otraces_set
 ==> (Alt P Q, tr) : otraces_set"
apply(case_tac tr)
apply(auto)
apply(drule t4)
apply(clarsimp)
apply(rule_tac Q="Qa" in otraces_set.step)
apply(erule transitions.alt1)
apply(clarsimp)
done

lemma t6: "(Q, tr) : otraces_set
  ==> (Alt P Q, tr) : otraces_set"
apply(case_tac tr)
apply(auto)
apply(drule t4)
apply(clarsimp)
apply(rule_tac Q="Qa" in otraces_set.step)
apply(erule transitions.alt2)
apply(clarsimp)
done

lemma t7: "(Alt P Q, (e, R)) : transitions ==>
  (P, (e, R)) : transitions |  (Q, (e, R)) : transitions"
apply(erule transitions.cases)
apply(auto)
done

lemma t8: "(Alt P Q, tr) : otraces_set ==>
  (P, tr) : otraces_set | (Q, tr) : otraces_set"
apply(erule otraces_set.cases)
apply(auto dest: t7)
done

lemma t9 [rule_format]:
  "ALL P Q tr1 tr2 X. (P, tr1) : otraces_set &
      (Q, tr2) : otraces_set &
      sync tr X tr1 tr2 
  --> (Par X P Q, tr) : otraces_set"
apply(induct_tac tr)
apply(auto)
apply(case_tac tr)
apply(auto)
apply(case_tac tr1)
apply(auto)
apply(case_tac tr2)
apply(auto)
apply(drule t4)
apply(drule t4)
apply(clarsimp)
apply(rename_tac tr P Q X tr1 e tr2 P' Q')
apply(rule_tac Q="Par X P' Q'" in otraces_set.step)
apply(rule transitions.par_sync)
apply(auto)
apply(blast)

apply(case_tac tr1)
apply(auto)
apply(case_tac tr2)
apply(auto)
apply(drule t4)
apply(drule t4)
apply(clarsimp)
apply(rename_tac tr P Q X tr1 e tr2 P' Q')
apply(rule_tac Q="Par X P' Q'" in otraces_set.step)
apply(rule transitions.par_sync)
apply(auto)
apply(blast)

apply(case_tac tr1)
apply(auto)
apply(drule t4)
apply(clarsimp)
apply(rule_tac Q="Par X Qa Q" in otraces_set.step)
apply(rule transitions.par_async1)
apply(auto)
apply(blast)

apply(case_tac tr2)
apply(auto)
apply(drule t4)
apply(clarsimp)
apply(rule_tac Q="Par X P Qa" in otraces_set.step)
apply(rule transitions.par_async2)
apply(auto)
apply(blast)
done

lemma t10 [rule_format]:
  "ALL P Q X. (Par X P Q, tr) : otraces_set
  -->
  (EX tr1 tr2.
  (P, tr1) : otraces_set &
  (Q, tr2) : otraces_set &
  sync tr X tr1 tr2)"
apply(induct_tac tr)
apply(auto)
apply(erule otraces_set.cases)
apply(clarsimp)
apply(clarsimp)
apply(erule transitions.cases)
apply(auto)
apply(drule_tac x="P'" in spec)
apply(drule_tac x="Qb" in spec)
apply(drule_tac x="Xa" in spec)
apply(clarsimp)
apply(rule_tac x="ea#tr1" in exI)
apply(rule conjI)
apply(rule_tac Q="P'" in otraces_set.step)
apply(auto)

apply(drule_tac x="Pa" in spec)
apply(drule_tac x="Q'" in spec)
apply(drule_tac x="Xa" in spec)
apply(clarsimp)
apply(rule_tac x="tr1" in exI)
apply(auto)

apply(drule_tac x="P'" in spec)
apply(drule_tac x="Q'" in spec)
apply(drule_tac x="Xa" in spec)
apply(auto)
apply(rule_tac x="ea#tr1" in exI)
apply(auto)
done


theorem "traces P = otraces P"
apply(unfold otraces_def)
apply(induct_tac P)
apply(auto)
apply(rule_tac Q="process" in otraces_set.step)
apply(rule transitions.prefix)
apply(clarsimp)
apply(rule_tac x="tl x" in exI)
apply(drule t3)
apply(clarsimp)
apply(erule t5)
apply(erule t6)
apply(auto dest: t8)
apply(rule t9)
apply(auto)
apply(drule t10)
apply(auto)
done

補足

CSP の教科書には,2つの意味論が同値であることを congruence というと書いてありました.ここではそのほんのささやかな部分だけを証明したことになります.

プロセス定義が再帰を含む場合には,トレース集合は方程式の解として求める必要があります.これはプロセスの定義式から定まるトレース集合のある関数 F の不動点になります.この場合について congruence であることを証明するのはなかなかたいへんです.興味のある方は CSP の教科書を見てください.

2013/12/16
© 2013,2014,2015 PRINCIPIA Limited