チャーチ・ロッサー性
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2020/02/17 13:50 UTC 版)
チャーチ・ロッサー性（Church-Rosser property）とは、抽象書き換え系 ⟨ A , → ⟩ {\displaystyle \left\langle A,\to \right\rangle } の任意の a , b ∈ A {\displaystyle a,\,b\in \,A} について a ↔ ∗ b {\displaystyle a{\overset {*}{{}\leftrightarrow {}}}b} ならば a → ∗ c and b → ∗ c {\displaystyle a\,{\overset {*}{{}\to {}}}c\quad {\text{and}}\quad b\,{\overset {*}{{}\to {}}}c} となるような c が存在することである。ここで a ↔ ∗ b {\displaystyle a{\overset {*}{{}\leftrightarrow {}}}b} は a と b それぞれの方向に有限ステップで簡約できることを表す。 チャーチ・ロッサー性は合流性と等価である。チャーチ・ロッサー性はラムダ計算でのベータ簡約の合流性を示すチャーチ・ロッサーの定理で用いられた。
※この「チャーチ・ロッサー性」の解説は、「合流性」の解説の一部です。
「チャーチ・ロッサー性」を含む「合流性」の記事については、「合流性」の概要を参照ください。
チャーチ・ロッサー性
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2021/04/12 16:37 UTC 版)
一般にラムダ式の中にβ-変換できる部分式が複数ある場合、どこから評価を行うかによって評価の経過は複数存在する。それらの複数の経過からさらに評価することによって、同じラムダ式を得られる性質をチャーチ・ロッサー性、もしくは合流性と呼ぶ（チャーチ・ロッサーの定理）。また、あるラムダ式から一回のβ-簡約によって得られた二つのラムダ式が、同じラムダ式にβ-変換されるという性質は弱チャーチ・ロッサー性と呼ばれる。チャーチ・ロッサー性を持つ体系は弱チャーチ・ロッサー性も持つが、逆は必ずしもなりたたない。 チャーチ・ロッサー性は本稿で取り扱っている型無しラムダ計算の体系では成立することが知られている。しかしその他の体系、例えば型を付けて拡張されたラムダ計算の体系などに関しては、必ずしも成り立つとは限らない。
※この「チャーチ・ロッサー性」の解説は、「ラムダ計算」の解説の一部です。
「チャーチ・ロッサー性」を含む「ラムダ計算」の記事については、「ラムダ計算」の概要を参照ください。
- チャーチ・ロッサー性のページへのリンク
