不動点とプロセス代数 - henjin1goの日記

通信をenforceする再帰変数同士の並行結合( $\partial \Gamma(||)$ )は
通信に失敗する組合せを展開時に逐次 $\delta$ に変換して消してゆく
$\delta$ になった項は、展開をさかのぼって $\delta$ を伝播して消してゆく
$\delta$ を消しながら展開方向に対して逆進する伝播Fは、項の集合に対しては単調
最大展開された項の集合(T)に対してFを順次適用すると、 $F^0(T) \sqsupseteq F^1(T) \sqsupseteq ...\sqsupseteq F^m(T) = F^m(T)$
達する $F^m(T)$ は、 $x \sqsubseteq F(x)$ となる集合の最大不動点
なんかとが逆であるが、これはこの方式の家風
- Rがwining setならば逆進した $F(R)$ にRが含まれるはず？だから？？ $R \sqsubseteq F(R)$
ついでに以上の論理はsafty-gameの勝利集合を求める戦略と同じで
Acetoの"Reactive System"によると、LTSにおける強相模倣関係をもとめる戦略とも同じ。
通信をenforceする再帰変数同士の並行結合( $\partial \Gamma(||)$ )は、Fの最大不動点 $\nu X. F(X)$ をもとめてることに対応
$\nu X. F(X)$ のもとめかたは、もう自明ですね。
これで、「なんとなく展開して出来ているふうに見えるが、、、」という類のコメントを回避できます。