合流性のソースを表示

{{No footnotes|date=2023年8月}}
'''合流性'''（ごうりゅうせい、{{lang-en-short|''confluence''}}）は[[項書き換え]]システムなどの特性で、項を複数の方法で書き換え可能な場合に、その複数の方法で書き換えた結果は適切に書き換えてやれば合流するという性質のことである。合流性は''チャーチ・ロッサー性''と呼ばれる特性と等価である。合流性を持つシステムは書き換え規則の適用順序によらない一貫性を持ち、[[遅延評価]]、[[並行計算|並行評価]]、[[部分評価]]などの柔軟な評価方法が可能になる。

== 合流性の例 ==
一般的な算術の規則は[[項書き換え]]系と見なすことができる。次のような式があるとする。
: {{math|(11 + 9) &times; (2 + 4)}}.
この式を書き換える方法は2種類ある。最初の括弧の中を単純化するか、2番目の括弧の中を単純化するかである。最初の括弧の中を先に項書き換えで単純化すると、次のようになる。
: {{math|1=20 &times; (2 + 4) = 20 &times; 6 = 120}}.
2番目の括弧の中を先に単純化すると、次のようになる。
: {{math|1=(11 + 9) &times; 6 = 20 &times; 6 = 120}}.
算術式は複数の方法で書き換え可能で、どの方法でも最終的な結果[[正規化 (項書き換え)|正規形]]は同じになる。つまり、算術規則からなる[[項書き換え]]系は合流性を持つ。

これを項書き換えの流れとして表現すると以下のようになる。

:<math>
\begin{array}{|rcccl|}
\hline
\color{MidnightBlue}{\mbox{eval left}}&&(11+9)\times(2+4)&&\color{MidnightBlue}{\mbox{eval right}}\\
&\color{MidnightBlue}{\swarrow}&&\color{MidnightBlue}{\searrow}&\\
20\times(2+4)&&&&(11+9)\times 6\\
&\color{MidnightBlue}{\searrow}&&\color{MidnightBlue}{\swarrow}&\\
\color{MidnightBlue}{\mbox{eval right}}&&20 \times 6&&\color{MidnightBlue}{\mbox{eval left}}\\
&&\color{MidnightBlue}{\downarrow}&&\\
&&120&&\\
\hline
\end{array}
</math>

== 定義 ==
[[Image:Confluence.svg|thumb|right|図1: 合流性の定義]]

一般的な[[項書き換え]]システムを考えると、特定の項を書き換え可能な規則や書き換え可能な部分が複数あるため、書き換えの流れは1通りとは限らない。合流性とは、同じ項から始まる相異なるかも知れない書き換えの流れから二つの項を取り出した時、常に両項を同じ形に書き換えることが可能である事、即ち任意の項 ''a'' を簡約化していって項 ''b'', ''c'' を得たならば、必ず ''b'', ''c'' から合流できる項 ''d'' が存在することである。

より形式的には、抽象書換え系 <math>\left\langle A, \to \right\rangle</math> について、''a'' から ''b'' への簡約化 {{lang|en|(reduction)}} を {{math|''a'' &rarr; ''b''}}、簡約化の有限のステップを <math>a \overset{*}{{}\to{}} b</math> と表現した場合、合流性の定義は以下のようになる。
:<math>\forall a,b,c\in A,\,\exists d\in A,\,a\overset{*}{{}\to{}}b \quad\text{and}\quad a\overset{*}{{}\to{}}c </math>
::<math>\implies b\overset{*}{{}\to{}}d \quad\text{and}\quad c\overset{*}{{}\to{}}d </math>

これを図で表現したものが図１である。実線は[[全称記号]]、点線は[[存在記号]]を意味し、* は簡約化の有限のステップを表す。

書き換え系が合流性を満たすとき、以下が成り立つ。
* 項 ''a'' の正規形は高々1個しか存在しない。
* 等式 {{math|1=''a'' = ''b''}} が成立するならば、適当な項 ''c'' が存在して <math>a \overset{*}{{}\to{}} c</math> かつ <math>b \overset{*}{{}\to{}} c</math> である。
なお、正規形が高々一個である事を指して「書き換え順序によらず、結果が一意に定まる」と言われることがあるが、そもそも正規形に辿り着くことが可能かどうか(つまりその順序での書き換えの「結果」と呼べるものが存在するかどうか)は書き換え順序によって変化する事があるため、厳密にはミスリーディングである。常に一意な結果があると言うには「結果」の定義に加え[[正規化 (項書き換え)|強正規化性]]等の性質が追加で必要になる。

== 関連する他の性質 ==
[[Image:Local-confluence.svg|thumb|right|図２: 局所合流性の定義]]
[[Image:Semi-confluence.svg|thumb|right|図３: 準合流性の定義]]
[[Image:Strong-confluence.svg|thumb|right|図４: 強合流性の定義]]

合流性に関連した性質として、局所合流性、準合流性、強合流性、チャーチ・ロッサー性などがある。

=== チャーチ・ロッサー性 ===
'''チャーチ・ロッサー性'''（{{lang|en|''Church-Rosser property''}}）とは、抽象書き換え系 <math>\left\langle A, \to \right\rangle</math> の任意の <math>a,\,b \in\,A</math> について <math>a \overset{*}{{}\leftrightarrow{}} b</math> ならば <math>a\,\overset{*}{{}\to{}}c \quad\text{and}\quad b\,\overset{*}{{}\to{}}c </math> となるような ''c'' が存在することである。ここで <math>a \overset{*}{{}\leftrightarrow{}} b</math> は ''a'' と ''b'' それぞれの方向に有限ステップで簡約できることを表す。

チャーチ・ロッサー性は合流性と等価である。チャーチ・ロッサー性は[[ラムダ計算]]でのベータ簡約の合流性を示す[[チャーチ・ロッサーの定理]]で用いられた。
=== 局所合流性 ===
要素 {{math|''a'' &isin; ''A''}} が '''局所合流性'''（{{lang|en|''Local confluence''}}）を持つとは、<math>c\,\leftarrow\,a\,\rightarrow\,b</math> となる任意の {{math|''b'', ''c'' &isin; ''A''}} について <math>c\,\overset{*}{{}\to{}}d\,\overset{*}{{}\leftarrow{}}b </math> となるような ''d'' が存在することである。これを図で表現したものが図２である。

局所合流性は、''弱合流性''（{{lang|en|''Weak confluence''}}）あるいは''弱チャーチ・ロッサー性''（{{lang|en|''Weak Church-Rosser property''}}）と呼ばれることもある。

局所合流性は合流性より弱い性質で、全ての要素が局所合流性を持つ場合でも、例えば書き換え規則にループが含まれる場合など、システム全体の合流性が成立するとは限らない。

ただし、システムが停止性と局所合流性とを持つ場合、システムは合流性を持つ（''ニューマンの補助定理''、{{lang|en|Newman's lemma}}）。

=== 準合流性 ===
要素 {{math|''a'' &isin; ''A''}} が  '''準合流性'''（{{lang|en|''Semi-confluence''}}）を持つとは、<math>c\,\leftarrow\,a\,\overset{*}\rightarrow\,b</math> となる任意の {{math|''b'', ''c'' &isin; ''A''}} について <math>c\,\overset{*}{{}\to{}}d\,\overset{*}{{}\leftarrow{}}b </math> となるような ''d'' が存在することである。これを図で表現したものが図3である。

全ての要素が準合流性を持つならば、システムは合流性を持つ。

=== 強合流性 ===
'''強合流性'''（{{lang|en|''Strong confluence''}}）は局所合流性を強くした性質である。要素 {{math|''a'' &isin; ''A''}} が強合流性を持つとは、<math>c\,\leftarrow\,a\,\rightarrow\,b</math> となる任意の {{math|''b'', ''c'' &isin; ''A''}} について <math>c\,\overset{=}{{}\to{}}d\,\overset{*}{{}\leftarrow{}}b </math> となるような ''d'' が存在することである。ここで <math>c\,\overset{=}{{}\to{}}d</math> とは、 <math>c\,{{}\to{}}d</math> か <math>c\,= d</math> のいずれかが成立することを表す。これを図で表現したものが図４である。

全ての要素が強合流性を持つならば、システムは合流性を持つ。強合流性は以下の定理と共に用いることができる：
抽象書換え系 <math>\left\langle A, \to_1 \right\rangle</math>, <math>\left\langle A, \to_2 \right\rangle</math> で <math>\rightarrow _1\,\subseteq\, \rightarrow _2\, \subseteq\, \overset{*} \to _1</math> かつ <math>(A,\rightarrow _2)</math> が強合流性を持つならば、<math>(A,\rightarrow _1)</math> は合流性を持つ。

== 参考文献 ==
* Bezem, M. et al (ed). ''Term Rewriting Systems''. Cambridge Tracts in Theoretical Computer Science, 2003. ISBN 9780521391153
* Franz Baader and Tobias Nipkow. [http://www.forsoft.de/~nipkow/TRaAT/ ''Term Rewriting and All That'']. Cambridge University Press, 1998. ISBN 978-0521779203 
* 外山芳人. [http://www.nue.riec.tohoku.ac.jp/lab-intro/TRS-intro/98ss_intro_trs.pdf ''項書き換えシステム入門''].(pdf) 信学技報, SS98-15, pp.31-38, 1998.

== 関連項目 ==
* [[項書き換え]]
* [[ラムダ計算]]
* [[グレブナー基底]]
* [[クヌース・ベンディックス完備化アルゴリズム]]

== 外部リンク ==
* {{MathWorld | urlname=Confluent | title=Confluent}}
* [http://www.nue.riec.tohoku.ac.jp/lab-intro/TRS-intro/index.html ''項書き換えシステム入門'']. 東北大学 電気通信研究所

{{Normdaten}}
{{DEFAULTSORT:こうりゆうせい}}

[[Category:形式言語]]
[[Category:形式手法]]
[[Category:数理論理学]]
[[Category:計算理論]]
[[Category:数学に関する記事]]