generated at
β簡約の合流性
β簡約の合流性
confluent
β簡約がChurch-Rosserの定理を満たす\Leftrightarrowβ簡約がβ簡約の合流性を持つ

定義
任意のラムダ抽象Mについて、
M_1{}_\beta\xleftarrow{\ast}M\xrightarrow{\ast}_\beta M_2ならば
あるラムダ抽象Nが存在して、
M_1\xrightarrow{\ast}_\beta N{}_\beta\xleftarrow{\ast}_\beta M_2が成り立つ