強合流性
出典: フリー百科事典『ウィキペディア(Wikipedia)』 (2020/02/17 13:50 UTC 版)
強合流性(Strong confluence)は局所合流性を強くした性質である。要素 a ∈ A が強合流性を持つとは、 c ← a → b {\displaystyle c\,\leftarrow \,a\,\rightarrow \,b} となる任意の b, c ∈ A について c → = d ← ∗ b {\displaystyle c\,{\overset {=}{{}\to {}}}d\,{\overset {*}{{}\leftarrow {}}}b} となるような d が存在することである。ここで c → = d {\displaystyle c\,{\overset {=}{{}\to {}}}d} とは、 c → d {\displaystyle c\,{{}\to {}}d} か c = d {\displaystyle c\,=d} のいずれかが成立することを表す。これを図で表現したものが図4である。 全ての要素が強合流性を持つならば、システムは合流性を持つ。強合流性は以下の定理と共に用いることができる:抽象書換え系 ⟨ A , → 1 ⟩ {\displaystyle \left\langle A,\to _{1}\right\rangle } , ⟨ A , → 2 ⟩ {\displaystyle \left\langle A,\to _{2}\right\rangle } で → 1 ⊆ → 2 ⊆ → ∗ 1 {\displaystyle \rightarrow _{1}\,\subseteq \,\rightarrow _{2}\,\subseteq \,{\overset {*}{\to }}_{1}} かつ ( A , → 2 ) {\displaystyle (A,\rightarrow _{2})} が強合流性を持つならば、 ( A , → 1 ) {\displaystyle (A,\rightarrow _{1})} は合流性を持つ。
※この「強合流性」の解説は、「合流性」の解説の一部です。
「強合流性」を含む「合流性」の記事については、「合流性」の概要を参照ください。
- 強合流性のページへのリンク