合流性

出典: フリー百科事典『ウィキペディア(Wikipedia)』
移動: 案内検索

合流性: Confluence)は項書き換えシステムなどの特性で、項を複数の方法で書き換え可能な場合にどちらの方法で書き換えても最終的な結果が合流する(一意に定まる)という性質のことである。合流性はチャーチ・ロッサー性と呼ばれる特性と等価である。合流性を持つシステムは書き換え規則の適用順序によらない一貫性のある論理的な意味を持ち、遅延評価並行評価部分評価などの柔軟な評価方法が可能になる。

合流性の例[編集]

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

 (11 + 9) \times (2 + 4)

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

 20 \times (2 + 4) = 20 \times 6 = 120

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

 (11 + 9) \times 6 = 20 \times 6 = 120.

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

定義[編集]

図1: 合流性の定義

一般的な項書き換えシステムを考えると、特定の項を書き換え可能な規則や書き換え可能な部分が複数あるため、書き換えの流れは1通りとは限らない。合流性とは、途中の書き換えの道筋には関係なく唯一の正規形に書き換えられることで、任意の項 a を簡約化していって項 b, c を得たならば、必ず b, c から合流できる項 d が存在することである。

より形式的には、抽象書換え系 \left\langle A, \to \right\rangle について、a から b への簡約化 (reduction)a \rightarrow 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
\Rightarrow\,\, b\,\overset{*}{{}\to{}}d \quad\text{and}\quad c\,\overset{*}{{}\to{}}d

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

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

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

関連する他の性質[編集]

図2: 局所合流性の定義
図3: 準合流性の定義
図4: 強合流性の定義

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

チャーチ・ロッサー性[編集]

チャーチ・ロッサー性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{}} bab それぞれの方向に有限ステップで簡約できることを表す。

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

局所合流性[編集]

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

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

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

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

準合流性[編集]

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

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

強合流性[編集]

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

全ての要素が強合流性を持つならば、システムは合流性を持つ。強合流性は以下の定理と共に用いることができる: 抽象書換え系 \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) は合流性を持つ。

関連項目[編集]

参考文献[編集]

外部リンク[編集]