合流性

合流性（ごうりゅうせい、英: confluence）は項書き換えシステムなどの特性で、項を複数の方法で書き換え可能な場合に、その複数の方法で書き換えた結果は適切に書き換えてやれば合流するという性質のことである。合流性はチャーチ・ロッサー性と呼ばれる特性と等価である。合流性を持つシステムは書き換え規則の適用順序によらない一貫性を持ち、遅延評価、並行評価、部分評価などの柔軟な評価方法が可能になる。

合流性の例

一般的な算術の規則は項書き換え系と見なすことができる。次のような式があるとする。

(11 + 9) × (2 + 4).

この式を書き換える方法は2種類ある。最初の括弧の中を単純化するか、2番目の括弧の中を単純化するかである。最初の括弧の中を先に項書き換えで単純化すると、次のようになる。

20 × (2 + 4) = 20 × 6 = 120.

2番目の括弧の中を先に単純化すると、次のようになる。

(11 + 9) × 6 = 20 × 6 = 120.

算術式は複数の方法で書き換え可能で、どの方法でも最終的な結果正規形は同じになる。つまり、算術規則からなる項書き換え系は合流性を持つ。

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

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

定義

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

より形式的には、抽象書換え系 $\left\langle A,\to \right\rangle$ について、a から b への簡約化 (reduction) を a → b、簡約化の有限のステップを $a{\overset {*}{{}\to {}}}b$ と表現した場合、合流性の定義は以下のようになる。

\forall a,b,c\in A,\,\exists d\in A,\,a{\overset {*}{{}\to {}}}b\quad {\text{and}}\quad a{\overset {*}{{}\to {}}}c

\implies b{\overset {*}{{}\to {}}}d\quad {\text{and}}\quad c{\overset {*}{{}\to {}}}d

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

書き換え系が合流性を満たすとき、以下が成り立つ。

項 a の正規形は高々1個しか存在しない。
等式 a = b が成立するならば、適当な項 c が存在して $a{\overset {*}{{}\to {}}}c$ かつ $b{\overset {*}{{}\to {}}}c$ である。

なお、正規形が高々一個である事を指して「書き換え順序によらず、結果が一意に定まる」と言われることがあるが、そもそも正規形に辿り着くことが可能かどうか(つまりその順序での書き換えの「結果」と呼べるものが存在するかどうか)は書き換え順序によって変化する事があるため、厳密にはミスリーディングである。常に一意な結果があると言うには「結果」の定義に加え強正規化性等の性質が追加で必要になる。

関連する他の性質

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

チャーチ・ロッサー性

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

チャーチ・ロッサー性は合流性と等価である。チャーチ・ロッサー性はラムダ計算でのベータ簡約の合流性を示すチャーチ・ロッサーの定理で用いられた。

局所合流性

要素 a ∈ A が 局所合流性（Local confluence）を持つとは、 $c\,\leftarrow \,a\,\rightarrow \,b$ となる任意の b, c ∈ A について $c\,{\overset {*}{{}\to {}}}d\,{\overset {*}{{}\leftarrow {}}}b$ となるような d が存在することである。これを図で表現したものが図２である。

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

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

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

準合流性

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

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

強合流性

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

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

参考文献

Bezem, M. et al (ed). Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, 2003. ISBN 9780521391153
Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. ISBN 978-0521779203
外山芳人. 項書き換えシステム入門.(pdf) 信学技報, SS98-15, pp.31-38, 1998.