Think Stitch
  Updates


Formal Proof of the Congruence Theorem between Operational Semantics and Denotational Semantics on Traces of CSP in Isabelle/HOL

Communicating Sequential Processes (CSP) has a variety of semantics: at least five denotational semantics, operational semantics, and algebraic semantics. Each semantics has important roles in the applications. On the other hand, having more than one semantics for a formal language gives rise to a question whether those semantics are consistent or not. It is known as congruence problems.

I have formally proved the congruence theorems between operational semantics and denotational semantics on traces of CSP using the theorem prover Isabelle/HOL. This article will explain the outline of the formalism of the problem on Isabelle/HOL and the proof.

Overview of the Problem

Syntax Definitions

CSP syntax is defined as an algebraic datatype.

\[\begin{split}P & ::= & \mathrm{STOP} \\& | & a \rightarrow P \\& | & P \ \square\ Q \\& | & \ldots\end{split}\]

Trace Semantics

The trace semantics assigns a set of traces to each process:

\[\mathcal{M}[\![P]\!] = \mathrm{traces}(P)\]

The equivalence of processes are defined as the equivalence of the set:

\[P =_T Q \quad \triangleq \quad \mathrm{traces}(P) = \mathrm{traces}(Q)\]

The traces set are defined inductively on the process syntax:

\[\begin{split}& \mathrm{traces}(\mathrm{STOP}) = \{ \langle \rangle \} \\& \mathrm{traces}(a \rightarrow P) = \{ \langle \rangle \} \cup \{\langle a \rangle {}^\frown s \,|\, s \in \mathrm{traces}(P) \} \\& \mathrm{traces}(P \ \square\ Q) = \mathrm{traces}(P) \cup \mathrm{traces}(Q) \\& \ldots\end{split}\]

再帰的に定義されたプロセスには,定義式から定まるトレース集合間の関数の最小不動点を割り当てます.最小不動点の存在は関数の単調性によって保証されます.

\[P = F(P) \quad \Longleftrightarrow \quad \mathrm{traces}(P) = \mu F_\mathcal{T}\]

例えば \(P = F(P) = a \rightarrow P\) の場合は次のようになります:

\[F_\mathcal{T}(X) = \{ \langle \rangle \} \cup \{\langle a \rangle {}^\frown s \,|\, s \in X \}\]

より一般的には,プロセスの定義は複数のプロセス名についての相互再帰(連立方程式)になります.そこでプロセス名とパラメータを合わせたものをインデックスで区別して \(P_k\) と表します.インデックスの集合を \(\Lambda\) ,プロセス(構文)の集合を \(\mathbb{P}\)とすると,プロセス定義は以下の関数で表すことができます:

\[D : \Lambda \rightarrow \mathbb{P}\]

ただし,再帰呼び出しの部分ではインデックスを指定するものとします.そのために構文にインデックス指定を行う要素を追加します.\($\) は再帰呼び出しを示す記号(構文を表す代数的データ型のコンストラクタ)です.

\[\begin{split}P & ::= & \mathrm{STOP} \\& | & a \rightarrow P \\& | & P \ \square\ Q \\& | & \ldots \\& | & $k\end{split}\]

例として次のような相互再帰を考えます:

\[\begin{split}& P_0 = a \rightarrow P_1 \\& P_1 = b \rightarrow P_0\end{split}\]

これは次のように \(D\) を与えることで定義できます:

\[\begin{split}& D(0) = a \rightarrow $1 \\& D(1) = b \rightarrow $0 \\\end{split}\]

次に,すべてのトレース集合からなる集合を \(\mathcal{T}\) として関数 \(\mathrm{traces}(P)\) に引数 \(M : \Lambda \rightarrow \mathcal{T}\) を加えて拡張します:

\[\mathrm{traces} : \mathbb{P} \rightarrow (\Lambda \rightarrow \mathcal{T}) \rightarrow \mathcal{T}\]

\[\begin{split}& \mathrm{traces}(\mathrm{STOP})(M) = \{ \langle \rangle \} \\& \mathrm{traces}(a \rightarrow P)(M) = \{ \langle \rangle \} \cup \{\langle a \rangle {}^\frown s \,|\, s \in \mathrm{traces}(P) \} \\& \mathrm{traces}(P \ \square\ Q)(M) = \mathrm{traces}(P) \cup \mathrm{traces}(Q) \\& \ldots \\& \mathrm{traces}($k)(M) = M(k)\end{split}\]

以上の設定により,プロセス定義 \(D\) から定まるトレース集合上での関数 \(F_\mathcal{T}\) は次のように書くことができます:

\[F_\mathcal{T}(D) \triangleq \lambda M . \lambda k . \mathrm{traces}(D(k))(M) : (\Lambda \rightarrow \mathcal{T}) \rightarrow (\Lambda \rightarrow \mathcal{T})\]

するとプロセス定義 \(D\) に対するトレース集合(上での関数)の方程式は

\[M = F_\mathcal{T}(D)(M)\]

となります.前に上げた例の未知数(トレース集合) \(X\) が関数 \(M\) になったわけです.この解として \(F_\mathcal{T}\) の最小不動点を採用します:

\[M = \mu F_\mathcal{T}(D)\]

Operational Semantics

操作的意味論はプロセス間の遷移を定めます.これを遷移関係として帰納的に定義します:

\[R : (\Lambda \rightarrow \mathbb{P}) \rightarrow \mathcal{P}(\mathbb{P} \times \Sigma^\tau \times \mathbb{P})\]

\[\begin{split}& a \rightarrow P \xrightarrow{\quad a \quad} P \in R(D) \\& P \xrightarrow{\quad a \quad} P' \in R(D) \Rightarrow P\ \square\ Q \xrightarrow{\quad a \quad} P' \in R(D) \\& P \xrightarrow{\quad \tau \quad} P' \in R(D) \Rightarrow P\ \square\ Q \xrightarrow{\quad \tau \quad} P' \ \square\ Q \in R(D) \\& \ldots\end{split}\]

遷移関係から計算列を定義します(\(R(D)\)を省略します):

\[P \xrightarrow{\quad \sigma \quad} P' \quad \triangleq \quad \forall i . 0 \le i < n \Rightarrow P_i \xrightarrow{\quad a_i \quad} P_{i+1} \land P_0 = P \land P_n = P'\]

\[\sigma = \left\langle (P_0, a_0, P_1), (P_1, a_1, P_2), \ldots, (P_{n-1}, a_{n-1}, P_n) \right\rangle\]

計算列からプロセスと \(\tau\) を除いてトレースによる遷移を定義します:

\[P \overset{s}{\Longrightarrow} P' \quad \triangleq \quad \exists \sigma. s = \mathrm{comp\_to\_trace}(\sigma) \land P \xrightarrow{\quad \sigma \quad} P'\]

\[\begin{split}& \mathrm{comp\_to\_trace}(\langle \rangle) = \langle \rangle \\& \mathrm{comp\_to\_trace}(\langle (P, a, P') \rangle {}^\frown \sigma) = \langle a \rangle {}^\frown \mathrm{comp\_to\_trace}(\sigma) \\& \mathrm{comp\_to\_trace}(\langle (P, \tau, P') \rangle {}^\frown \sigma) = \mathrm{comp\_to\_trace}(\sigma)\end{split}\]

以上の設定から操作的意味論においてもトレース集合を定義することができます(トレースによる遷移,計算列による遷移,および \(R\) をとおしての \(D\) への依存が隠れています):

\[\mathrm{traces_{op}}(D)(P) = \{s \,|\, \exists P'. P \overset{s}{\Longrightarrow} P' \}\]

プロセス定義 \(D\) に対する,操作的意味論から導出した表示は以下のようになります:

\[\mathcal{O}_\mathcal{T}(D) = \lambda k. \mathrm{traces_{op}}(D)($k)\]

The Congruence of the Semantics

これでトレース意味論と操作的意味論のそれぞれの同値性について比較ができるようになりました.証明すべきは任意の定義 \(D\) について表示が一致すること,つまり次の式です:

\[\mu F_\mathcal{T}(D) = \mathcal{O}_\mathcal{T}(D)\]

The Outline of the Proof

反対称律を使って証明を2つに分けます(\(D\) を省略しています):

\[\mu F_\mathcal{T} \sqsubseteq \mathcal{O}_\mathcal{T} \land\mathcal{O}_\mathcal{T} \sqsubseteq \mu F_\mathcal{T}\]

最小不動点の定義は次のとおりです:

\[\mu f = \mathrm{inf}\{x \,|\, f(x) \sqsubseteq x \}\]

したがってまず \(\mu F_\mathcal{T} \sqsubseteq \mathcal{O}_\mathcal{T}\) を証明するには\(F_\mathcal{T}(\mathcal{O}_\mathcal{T}) \sqsubseteq \mathcal{O}_\mathcal{T}\) であることがいえれば十分です.これを展開して整理すると次のような式になります:

\[\mathrm{traces}(P)(\lambda k . \mathrm{traces_{op}}(D)($k)) \sqsubseteq \mathrm{traces_{op}}(D)(P)\]

これを証明するには,まずプロセス \(P\) の構文に対する帰納法を適用します.すると各演算子に対応するサブゴールが出るので,それぞれに対し,計算列の長さに関する帰納法を適用すると容易に証明することができます.

続いて \(\mathcal{O}_\mathcal{T} \sqsubseteq \mu F_\mathcal{T} \) を証明します.中間点を設けて次のようにします:

\[\mathcal{O}_\mathcal{T} \sqsubseteq \mathcal{D} \land \mathcal{D} \sqsubseteq \mu F_\mathcal{T}\]

ここで \(\mathcal{D}\) は次のものです:

\[\mathcal{D} = \mathrm{sup}\{x \,|\, \exists n. x = F_\mathcal{T}^n(\bot) \}\]

これはよく知られた極限による不動点の表現です.つまり \(\mu F_\mathcal{T}\) と同じものですが,同じであるこというには \(F_\mathcal{T}\) の連続性が必要です.実際 CSP の演算子から導出される関数は連続なのですが,ここでは連続性を使いません.

\(\mu F_\mathcal{T}\) は最小不動点,したがって最大下界ですから \(\mathcal{D} \sqsubseteq \mu F_\mathcal{T}\) をいうには \(\mathcal{D}\) が下界の1つであることをいえば十分です.したがって \(F_\mathcal{T}(x) \sqsubseteq x\) を満たす任意の \(x\) について \(\mathcal{D} \sqsubseteq x\) であることがいえればよいことになります.

そこでそのような任意の \(x\) をとると,まず \(\bot \sqsubseteq x\) がいえます.すると \(F_\mathcal{T}\) の単調性から \(F_\mathcal{T}(\bot) \sqsubseteq F_\mathcal{T}(x) \) となり,さらに仮定から \(F_\mathcal{T}(\bot) \sqsubseteq x\) となります.

一般に任意の \(n\) について \(F_\mathcal{T}^n(\bot) \sqsubseteq x\) を仮定すると,同様の議論から \(F_\mathcal{T}^{n+1}(\bot) \sqsubseteq x\) がいえるので,任意の \(n\) についていえることになります.するとこの \(x\) は 集合 \(\{x \,|\, \exists n. x = F_\mathcal{T}^n(\bot) \}\) の上界の1つということになります.\(\mathcal{D}\) は上限,したがって最小上界ですから,\(\mathcal{D} \sqsubseteq x \) がいえました.

残りは \(\mathcal{O}_\mathcal{T} \sqsubseteq \mathcal{D}\) です.これは本当は関数の間の順序なのですが,関数の順序は pointwise に定義されているので,ちょっとラフな議論になりますがわかりやすさを優先して値の集合とみなすことにします.

まず視点を要素に移すと次のようになります:

\[\mathcal{O}_\mathcal{T} \sqsubseteq \mathcal{D} \quad \Leftrightarrow \quad\forall m. m \in \mathcal{O}_\mathcal{T} \Rightarrow m \in \mathcal{D}\]

集合の包含関係を順序とするトレース集合において,上限は和集合で定義されています:

\[\begin{split}\mathcal{D} & = & \mathrm{sup}\{x \,|\, \exists n. x = F_\mathcal{T}^n(\bot) \} \\& = & \bigcup \{x \,|\, \exists n. x = F_\mathcal{T}^n(\bot) \}\end{split}\]

したがって \(m \in \mathcal{D}\) をいうには \(m \in F_\mathcal{T}^n(\bot)\) となる \(n\) が存在すればいいことになります.つまり証明すべき式は次の式です:

\[m \in \mathcal{O}_\mathcal{T} \Rightarrow \exists n. m \in F_\mathcal{T}^n(\bot)\]

この式が表現していることを端的にいうと,操作的意味論で定義されたトレースを任意に1つとってくると,ある \(n\) が存在して,プロセスの定義を高々 \(n\) 回展開した式のトレースになっているということです.トレースは有限の長さなので十分大きな \(n\) をとればこれがいえることは明らかなことのように思えます.しかし操作的意味論で定義された前件には無限の循環(coinductive な性質)が含まれているために,直接証明することが困難です.

そこで再び中間点を設けて分離します.表示的意味論と同じように,定義を高々 \(n\) 回だけしか展開しない操作的意味論による表示というものを作ります.これを \(\mathcal{O}_n'\) とします.

\[\begin{split}& m \in \mathcal{O}_\mathcal{T} \Rightarrow \exists n. m \in \mathcal{O}_n' \quad \land \\& \forall n. m \in \mathcal{O}_n' \Rightarrow m \in F_\mathcal{T}^n(\bot)\end{split}\]

この \(\mathcal{O}_n'\) の定義について,まず例を使って簡単に説明します.例えば \(P = F(P)\) という再帰的定義があったら,定義の展開を高々 \(n\) 回に制限するために次のような定義を作ればよいことになります:

\[\begin{split}P_0 & = & \mathrm{STOP} \\P_1 & = & F(P_0) \\P_2 & = & F(P_1) \\\cdots\\P_n & = & F(P_{n-1})\end{split}\]

一般の場合については次のようなトリックをつかいます.プロセス定義において再帰呼び出しの部分にはプロセスインデックス \($k\) があります.これをインデックスの残りの展開可能回数を表す自然数のペアに \($(k, n)\) にすりかえます.そして定義を展開する推論規則の部分で回数を \(-1\) し,定義式に現れるすべてのプロセスインデックス部分に埋め込みます.具体的には次のように定義します:

\[\mathcal{O}'_n \triangleq \lambda k . \mathrm{traces_{op}}(G(D))(k, n)\]

\[G(D) \triangleq \lambda (k, n). \mathrm{if}\ n=0\ \mathrm{then}\ \mathrm{STOP}\ \mathrm{else}\ \phi(n-1, D(k))\]

ここで関数 \(\phi(n, P) \) はプロセス \(P\) の構文木に出現する再帰呼び出しのためのプロセスインデックス部分 \($k\) を \($(k, n)\) に置き換える関数です:

\[\begin{split}&\phi(n, \mathrm{STOP}) = \mathrm{STOP} \\&\phi(n, a \rightarrow P) = a \rightarrow \phi(P) \\&\phi(n, P \ \square\ Q) = \phi(P) \ \square\ \phi(Q)\\&\cdots\\&\phi(n, $k) = $(k, n)\end{split}\]

k0 k1 k2 (k0, n) (k1, n) (k2, n) ||X X

さて,証明すべき2つの式のうちの後半:

\[\forall n. m \in \mathcal{O}_n' \Rightarrow m \in F_\mathcal{T}^n(\bot)\]

これは \(\mathcal{O}'_n \subseteq F_\mathcal{T}^n(\bot)\) ということです.これを \(n\) についての数学的帰納法で証明します.

まず \(n=0\) の場合は \(\mathrm{STOP} \subseteq \bot\) ですから成り立ちます(2つは同じものです).次に帰納段階です:

\[\mathcal{O}'_n \subseteq F_\mathcal{T}^n(\bot) \ \Rightarrow\ \mathcal{O}'_{n+1} \subseteq F_\mathcal{T}^{n+1}(\bot)\]

ここでもし \(\mathcal{O}'_{n+1} \subseteq F_\mathcal{T}(\mathcal{O}'_n)\) がいえれば,帰納法の仮定と \(F_\mathcal{T}\) の単調性とから

\[\begin{split}\mathcal{O}'_{n+1} & \subseteq & F_\mathcal{T}(\mathcal{O}'_n) \\ & \subseteq & F_\mathcal{T}(F_\mathcal{T}^n(\bot)) \\ & \subseteq & F_\mathcal{T}^{n+1}(\bot)\end{split}\]

となるので証明ができたことになります.\(\mathcal{O}'_{n+1} \subseteq F_\mathcal{T}(\mathcal{O}'_n)\) については,まずプロセスの構文に関する帰納法を適用し,つづいて計算列の長さに関する帰納法を適用すると証明することができます.

残りは次の式です:

\[m \in \mathcal{O}_\mathcal{T} \Rightarrow \exists n. m \in \mathcal{O}_n'\]

これを展開して整理すると次のようになります:

\[s \in \mathrm{traces}(D)(P) \Rightarrow s \in \mathrm{traces_{op}}(G(D))(\phi(n, P))\]

これをトレース,実質計算列の長さに関する帰納法で証明します.この計算列は先頭の部分が \(P\) で固定されていることと,\(P\) に含まれる再帰のインデックス部分は関数 \(\phi\) によって展開回数がそろっていることから,列を前に伸ばす方向で帰納法を使うことは適切ではありません.そこで後ろに伸ばす形で帰納法を適用します.

長さが0の場合は自明です.帰納の段階では\(\mathcal{O}_\mathcal{T}\) にある計算列 \(\sigma\) に対応する \(\mathcal{O}_n'\) の計算列 \(\sigma'\) があって,さらにもう1遷移伸ばすことになります.ある遷移があったときに,遷移元プロセスのすべてのインデックスの部分にある同じ自然数 \(m\) が付いた \(\mathcal{O}_n'\) の遷移が存在することはすぐに示せます.ところがこれを \(\sigma'\) に連結することはできません.なぜなら,\(\sigma'\) は各遷移の中で再帰部分が任意に展開されてきている可能性があるので,インデックスに付随する展開回数がそろっていないからです.

そこでつぎのような工夫をします.まずある \(\mathcal{O}_n'\) の計算列 \(\sigma'\) があるとします.先頭のプロセスのインデックス部分の展開回数はそろっています.これらすべてに対し,任意の自然数 \(j\) を同時に加えると,計算列末尾のインデックス部分の各展開回数は一様に \(+j\) されるという補題を証明することができます.

次に \(\mathcal{O}_n'\) の任意の遷移について,各インデックスの展開回数に任意の自然数を加えた遷移も存在することが示せます.こちらはバラバラの値を加えてもよいということです.

以上の2つを組み合わせると,計算列 \(\sigma'\) の末尾と遷移の事前状態を合わせることができます.これで連結ができるので,証明ができたことになります.

k0 k1 k2 (k0, a) (k1, b) (k2, c) ||X X k0 k1 k2 (k0, m) (k1, m) (k2, m) ||X X

The Formalism of the Problem on Isabelle/HOL

The Definition of the Syntax of CSP

datatype 
 ('p,'a) proc
    = STOP

    | Act_prefix     "'a" "('p,'a) proc"      ("(1_ /-> _)" [150,80] 80)

    | Ext_pre_choice "'a set" "'a => ('p,'a) proc"
                                               ("(1? :_ /-> _)" [900,80] 80)
    | Ext_choice     "('p,'a) proc" "('p,'a) proc"  
                                               ("(1_ /[+] _)" [72,73] 72)
    | Int_choice     "('p,'a) proc" "('p,'a) proc"  
                                               ("(1_ /|~| _)" [64,65] 64)
    | Rep_int_choice "nat set" "nat => ('p,'a) proc"
                                               ("(1!! :_ .. /_)" [900,68] 68) 
    | IF             "bool" "('p,'a) proc" "('p,'a) proc"
                                 ("(0IF _ /THEN _ /ELSE _)" [900,88,88] 88)
    | Parallel       "('p,'a) proc" "'a set" "('p,'a) proc"  
                                               ("(1_ /|[_]| _)" [76,0,77] 76)
    | Hiding         "('p,'a) proc" "'a set"   ("(1_ /-- _)" [84,85] 84)

    | Renaming       "('p,'a) proc" "('a * 'a) set"
                                               ("(1_ /[[_]])" [84,0] 84)
    | Proc_name      "'p"                      ("$_" [900] 90)

Denotational Semantics

The Definition of Traces Set

primrec traces_r :: "('p, 'a) proc => ('p => 'a domT) => 'a list set" where
  "traces_r STOP M = {[]}"
| "traces_r (a -> P) M = {t. t = [] | (EX s. t = a#s & s : traces_r P M)}"
| "traces_r (? :A -> Pf) M =
                  {t. t = [] |
                      (EX a s. t = a#s & a : A & s : traces_r (Pf a) M)}"
| "traces_r (P [+] Q) M = (traces_r P M) Un (traces_r Q M)"
| "traces_r (P |~| Q) M = (traces_r P M) Un (traces_r Q M)"
| "traces_r (!! :A .. Pf) M = {[]} Un Union {(traces_r (Pf n) M) | n. n : A}"
| "traces_r (IF b THEN P ELSE Q) M = (if b then traces_r P M else traces_r Q M)"
| "traces_r (P |[X]| Q) M =
             {u. EX s t. u : sync X s t &
                         s : (traces_r P M) &
                         t : (traces_r Q M)}"
| "traces_r (P -- X) M = {t. EX s. t = ceal X s & s : traces_r P M}"
| "traces_r (P[[R]]) M = {t. EX s. rename_tr R s t & s : traces_r P M}"
| "traces_r ($p) M = Rep_domT (M p)"

Traces Set as a Type (Domain)

トレース意味論の領域となる,すべてのトレース集合からなる集合 domT を定義します.トレース集合は空列を含み,prefix に関して閉じている必要があります.これを健全性条件といいます.

definition prefix :: "'a list => 'a list => bool" where
"prefix x y == (EX z. y = x @ z)"

definition prefix_closed :: "'a list set => bool" where
"prefix_closed s == ALL x y. x : s & prefix y x --> y : s"

definition HC_T1 :: "'a list set => bool" where
"HC_T1 s == (s ~= {} & prefix_closed s)"

definition "domT  = {s::('a list set). HC_T1 s}"

このあとトレース集合族に完備束の構造を入れます.完備束の定義は Isabelle/HOL のライブラリにあり,型クラスとして実装されています.これを利用するためにトレース集合の型を定義します.

typedef 'a domT = "domT :: 'a list set set"
apply (simp add: domT_def HC_T1_def)
apply (rule_tac x ="{[]}" in exI)
apply(simp add: prefix_closed_def prefix_def)
done

Instantiation of the Type Class Complete_Lattice

Isabelle/HOL のライブラリに含まれている,完備束に至る型階層は次のようになっています:

g ord ord preorder preorder preorder->ord order order order->preorder inf inf sup sup semilattice_inf semilattice_inf semilattice_inf->order semilattice_inf->inf semilattice_sup semilattice_sup semilattice_sup->order semilattice_sup->sup lattice lattice lattice->semilattice_inf lattice->semilattice_sup bot bot bot->order top top top->order bounded_lattice_bot bounded_lattice_bot bounded_lattice_bot->lattice bounded_lattice_bot->bot bounded_lattice_top bounded_lattice_top bounded_lattice_top->lattice bounded_lattice_top->top bounded_lattice bounded_lattice bounded_lattice->bounded_lattice_bot bounded_lattice->bounded_lattice_top Inf Inf Sup Sup complete_lattice complete_lattice complete_lattice->bounded_lattice complete_lattice->Inf complete_lattice->Sup

宣言部分だけを取り出してくると以下のとおりです:

class ord
  fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"

class preorder = ord +

class order = preorder +

class inf =
  fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)

class sup = 
  fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)

class semilattice_inf =  order + inf +

class semilattice_sup = order + sup +

class lattice = semilattice_inf + semilattice_sup

class bot = order +
  fixes bot :: 'a ("\<bottom>")

class top = order +
  fixes top :: 'a ("\<top>")

class bounded_lattice_bot = lattice + bot

class bounded_lattice_top = lattice + top

class bounded_lattice = bounded_lattice_bot + bounded_lattice_top

class Inf =
  fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)

class Sup =
  fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)

class complete_lattice = bounded_lattice + Inf + Sup +

必要な定義を与え証明義務を証明して,トレース集合を完備束のインスタンスにします.

instantiation domT :: (type) complete_lattice
begin

domT_less_eq_def: "p <= q == (Rep_domT p <= Rep_domT q)"
domT_less_def: "p < q == (Rep_domT p < Rep_domT q)"
domT_inf_def: "inf p q == Abs_domT (Rep_domT p Int Rep_domT q)"
domT_sup_def: "sup p q == Abs_domT (Rep_domT p Un Rep_domT q)"
domT_bot_def: "bot == Abs_domT {[]}"
domT_top_def: "top == Abs_domT UNIV"
domT_Inf_def: "Inf s  = Abs_domT (Inter {Rep_domT p | p. p : s})"
domT_Sup_def: "Sup s  = (if s={} then Abs_domT {[]} else Abs_domT (Union {Rep_domT p | p. p : s}))"

The Definition of the Denotations on Denotational Semantics

型の上での抽象的な traces 関数を定義します.

definition traces :: "('p, 'a) proc => ('p => 'a domT) => 'a domT" where
  "traces p M = Abs_domT (traces_r p M)"

定義 D からトレース上の関数を導出する関数を定義します.

definition F :: "('p => ('p, 'a) proc) => ('p => 'a domT) => ('p => 'a domT)" where
"F = (%D. %M. %p. traces (D p) M)"

この関数が単調であることを証明します.

lemma mono_csp: "mono (F D)"
...
done

以上の準備の下で,表示的意味論の表示が最小不動点として定義できます.

definition deno_sem :: "('p => ('p, 'a) proc) => ('p => 'a domT)" where
"deno_sem D = lfp (F D)"

Operational Semantics

Adding tau event

datatype 'a event = Tau | Ev 'a

The Definition of the Transition Relation

inductive_set
  ptrans :: "('p => ('p, 'a) proc) => (('p, 'a) proc * 'a event * ('p, 'a) proc) set"
  for D :: "'p => ('p, 'a) proc"
  where
ptrans_prefix: "(a -> P, (Ev a, P)) : ptrans D" |
ptrans_prefix_choice: "a : A ==> (? :A -> Pf, (Ev a, Pf a))  : ptrans D" |
ptrans_ext_choice1: "(P, (Ev e, P')) : ptrans D
                      ==> (P [+] Q, (Ev e, P')) : ptrans D" |
ptrans_ext_choice2: "(Q, (Ev e, Q')) : ptrans D
                      ==> (P [+] Q, (Ev e, Q')) : ptrans D" |
ptrans_ext_choice3: "(P, (Tau, P')) : ptrans D
                      ==> (P [+] Q, (Tau, P' [+] Q)) : ptrans D" |
ptrans_ext_choice4: "(Q, (Tau, Q')) : ptrans D
                      ==> (P [+] Q, (Tau, P [+] Q')) : ptrans D" |
ptrans_int_choce1 [intro!]:
  "(P |~| Q, Tau, P) : ptrans D" |
ptrans_int_choce2 [intro!]:
  "(P |~| Q, Tau, Q) : ptrans D" |
ptrans_rep_int_choce:
  "x:A ==> (!! :A .. Pf, Tau, Pf x) : ptrans D" |
ptrans_par1: "[| (P, (Ev e, P')) : ptrans D; e ~: X |]
                  ==> (P |[X]| Q, (Ev e, P' |[X]| Q)) : ptrans D" |
ptrans_par2: "[| (Q, (Ev e, Q')) : ptrans D; e ~: X |]
                  ==> (P |[X]| Q, (Ev e, P |[X]| Q')) : ptrans D" |
ptrans_par3: "[| (P, (Ev e, P')) : ptrans D;
                (Q, (Ev e, Q')) : ptrans D; e : X |]
                  ==> (P |[X]| Q, (Ev e, P' |[X]| Q')) : ptrans D" |
ptrans_par4: "[| (P, (Tau, P')) : ptrans D |]
                  ==> (P |[X]| Q, (Tau, P' |[X]| Q)) : ptrans D" |
ptrans_par5: "[| (Q, (Tau, Q')) : ptrans D |]
                  ==> (P |[X]| Q, (Tau, P |[X]| Q')) : ptrans D" |
ptrans_hide1: "[| (P, (Ev e, P')) : ptrans D; e ~: X |]
                  ==> (P -- X, (Ev e, P' -- X)) : ptrans D" |
ptrans_hide2: "[| (P, (Ev e, P')) : ptrans D; e : X |]
                  ==> (P -- X, (Tau, P' -- X)) : ptrans D" |
ptrans_hide3: "[| (P, (Tau, P')) : ptrans D |]
                  ==> (P -- X, (Tau, P' -- X)) : ptrans D" |
ptrans_rename1: "[| (P, Ev a, P') : ptrans D; (a, b) : R |]
                 ==> (P[[R]], Ev b, P'[[R]]) : ptrans D" |
ptrans_rename2: "(P, Tau, P') : ptrans D
                 ==> (P[[R]], Tau, P'[[R]]) : ptrans D" |
ptrans_if1: "b ==> (IF b THEN P ELSE Q, Tau, P) : ptrans D" |
ptrans_if2: "~b ==> (IF b THEN P ELSE Q, Tau, Q) : ptrans D" |
ptrans_pn: "(D p, u, Q) : ptrans D
   ==> ($p, Tau, D p) : ptrans D"

The Definition of the φ-function and its inverse

primrec ptel :: "nat => ('p, 'a) proc => ('p * nat, 'a) proc" where
  "ptel m STOP = STOP" |
  "ptel m (a->P) = a->(ptel m P)" |
  "ptel m (?:A->Pf) = (?:A->(%a. ptel m (Pf a)))" |
  "ptel m (P[+]Q) = (ptel m P)[+](ptel m Q)" |
  "ptel m (P|~|Q) = (ptel m P)|~|(ptel m Q)" |
  "ptel m (!!:A..Pf) = (!!:A..(%a. ptel m (Pf a)))" |
  "ptel m (P|[X]|Q) = (ptel m P) |[X]| (ptel m Q)" |
  "ptel m (P--X) = (ptel m P)--X" |
  "ptel m (P[[R]]) = (ptel m P)[[R]]" |
  "ptel m (IF b THEN P ELSE Q) = (IF b THEN (ptel m P) ELSE (ptel m Q))" |
  "ptel m ($p) = $(p, m)"
primrec rmtel :: "('p * nat, 'a) proc => ('p, 'a) proc" where
  "rmtel STOP = STOP" |
  "rmtel (a->P) = a->(rmtel P)" |
  "rmtel (?:A->Pf) = (?:A->(%a. rmtel (Pf a)))" |
  "rmtel (P[+]Q) = (rmtel P)[+](rmtel Q)" |
  "rmtel (P|~|Q) = (rmtel P)|~|(rmtel Q)" |
  "rmtel (!!:A..Pf) = (!!:A..(%a. rmtel (Pf a)))" |
  "rmtel (P|[X]|Q) = (rmtel P) |[X]| (rmtel Q)" |
  "rmtel (P--X) = (rmtel P)--X" |
  "rmtel (P[[R]]) = (rmtel P)[[R]]" |
  "rmtel (IF b THEN P ELSE Q) = (IF b THEN (rmtel P) ELSE (rmtel Q))" |
  "rmtel ($pm) = ($(fst pm))"

The Definition of the Transformation for a Bounded Processes

definition G :: "('p => ('p, 'a) proc) => (('p * nat) => ('p * nat, 'a) proc)" where
  "G D = (%(p, n). if n=0 then STOP else ptel (n - 1) (D p))"

The Definition of Computations

inductive_set
  comps :: "('p => ('p, 'a) proc) => (('p, 'a) proc * 'a event * ('p, 'a) proc) list set"
  for D :: "'p => ('p, 'a) proc"
  where
comps_base [simp, intro!]: "[] : comps D" |
comps_step1 [intro!]: "[| (P, u, P') : ptrans D |]
                 ==> [(P, u, P')] : comps D" |
comps_step2: "[| (P, u, P')#cs : comps D; (P'', u', P) : ptrans D |]
                 ==> (P'', u', P)#(P, u, P')#cs : comps D"

The Definition of the Transformation from Computations to Traces

fun comp_to_trace :: "('q * 'a event * 'q) list => 'a list" where
  "comp_to_trace [] = []"
| "comp_to_trace ((P, Tau, P')#cs) = comp_to_trace cs"
| "comp_to_trace ((P, Ev e, P')#cs) = e # (comp_to_trace cs)"

The Definition of Traces Set by Operational Semantics

definition otraces_r :: "('p => ('p, 'a) proc) => ('p, 'a) proc => 'a list set" where
  "otraces_r D P =
         {tr. tr = [] | (EX P' u cs. tr = comp_to_trace ((P, u, P')#cs) &
                                     (P, u, P')#cs : comps D)}"
definition otraces :: "('p => ('p, 'a) proc) => ('p, 'a) proc => 'a domT" where
  "otraces D P = Abs_domT (otraces_r D P)"

The Proof of the Congruence Theorem

lemma operational_denotational_congruence:
  "(%p. otraces D ($p)) = deno_sem D"
...
done

Remarks

操作的意味論の推論規則で,定義を展開するところは次のように定義しています.

ptrans_pn: "(D p, u, Q) : ptrans D
   ==> ($p, Tau, D p) : ptrans D"

推論規則の形で書くとこうです:

\[\frac{\quad \exists Q. D\ p \xrightarrow{\quad a \quad} Q \quad}{$p \xrightarrow{\quad \tau \quad} D\ p} \qquad (A)\]

ここの規則にはいくつか流儀があります.1つは前提を取り除いたもの:

\[\frac{}{\quad $p \xrightarrow{\quad \tau \quad} D\ p \quad} \qquad (B)\]

あるいは定義右辺式とプロセス名は同じ遷移を持ち,\(\tau\) を入れないものがあります:

\[\frac{\quad D\ p \xrightarrow{\quad a \quad} Q \quad}{$p \xrightarrow{\quad a \quad} Q} \qquad (C)\]

試行錯誤の結果,今回は (A) で証明に成功しました.(B) でも証明可能だと予想しています(回数制限付きの計算列を連結するための2つの補題だけ証明が済んでいません).(C) で証明できるかどうかはわかっていません.

2016/12/03

© 2013-2016 PRINCIPIA Limited