β簡約の合流性
β簡約の合流性
confluent
β簡約がChurch-Rosserの定理を満たす$ \Leftrightarrowβ簡約がβ簡約の合流性を持つ
https://gyazo.com/f674a3020a25fba18edee662d006bd8e
定義
任意のラムダ抽象$ 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が成り立つ