合流性

日本語活用形辞書

合流性

読み方：ごうりゅうせい

名詞「合流」に、接尾辞「性」がついたもの。

» 「合流」の意味を調べる

日本語活用形辞書はプログラムで機械的に活用形や説明を生成しているため、不適切な項目が含まれていることもあります。ご了承くださいませ。 お問い合わせ。

ウィキペディア

合流性

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2023/08/07 06:30 UTC 版)

合流性（ごうりゅうせい、英: 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: 合流性の定義

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

より形式的には、抽象書換え系 $\left\langle A,\to \right\rangle$

図２: 局所合流性の定義

図３: 準合流性の定義

図４: 強合流性の定義

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

チャーチ・ロッサー性

チャーチ・ロッサー性（Church-Rosser property）とは、抽象書き換え系 $\left\langle A,\to \right\rangle$

• ドイツ

ウィキペディア小見出し辞書

合流性

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/08/26 07:52 UTC 版)

「Constraint Handling Rules」の記事における「合流性」の解説

合流性（Confluence）とは、書き換えが可能な部分式が複数存在する際に、どの書き換え規則をどの部分式に適用して書き換えたとしても最終的な結果が合流する(一意に定まる) という性質のことである。合流性の無いプログラムは、最終的な実行結果が実行ごとに異なる可能性がある。一般的な項書き換えシステムと同様、停止性を持つCHRプログラムの合流性には、決定可能な必要条件と十分条件がある。停止性と合流性を持つCHRプログラムはルールの適応順序によらない一貫性のある論理的な意味を持ち、解くべき問題の異なった部分に対してルールを並列に適用できるような、並行してインクリメンタルに問題を解くアルゴリズムをインプリメントできる。