﻿ Formal Proof of the Congruence Theorem between Operational Semantics and Denotational Semantics on Traces of CSP in Isabelle/HOL - Think Stitch - PRINCIPIA
Think Stitch
﻿

# 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}$

$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}$

$\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}$

$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}$

$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$

$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}$

$\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

$\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 \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$ となります．

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

$\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}$

$\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}$

さて，証明すべき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$ によって展開回数がそろっていることから，列を前に伸ばす方向で帰納法を使うことは適切ではありません．そこで後ろに伸ばす形で帰納法を適用します．

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

# 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)


### 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 (rule_tac x ="{[]}" in exI)
done


### Instantiation of the Type Class Complete_Lattice

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

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

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


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

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
...
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)$

2016/12/03