「合流性」の版間の差分

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

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

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

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

* 項 ''a'' の正規形は高々１1個しか存在しない。

'''チャーチ・ロッサー性'''（{{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\in\,A</math> が '''準合流性'''（{{lang|en|''Semi-confluence''}}）を持つとは、<math>c\,\leftarrow\,a\,\overset{*}\rightarrow\,b</math> となる任意の <math>b,\,c\,\in\,A</math> について <math>c\,\overset{*}{{}\to{}}d\,\overset{*}{{}\leftarrow{}}b </math> となるような ''d'' が存在することである。これを図で表現したものが図３3である。

'''強合流性'''（{{lang|en|''Strong confluence''}}）は局所合流性を強くした性質である。要素 <math>a\in\,A</math> が強合流性を持つとは、<math>c\,\leftarrow\,a\,\rightarrow\,b</math> となる任意の <math>b,\,c\,\in\,A</math> について <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> のいずれかが成立することを表わす。これを図で表現したものが図４である。