john7rv

β基が複数ある場合、どのβ変換からするか決められない場合もあります
またβ変換からまた別のβ変換ができはたして終わりがあるのかわからない場合もあります
これに対して
チャーチ・ロッサーの定理は

β変換によって
一つのλを２つのλにしたら
その２つのλをβ変換によってまた必ず一つのλに合流できる

ことを保証するものです
合流性ともいいます

これ以上ラムダ式を変換できない状態までβ変換したとき
それを正規形と言います
β基がもはや無い状態とも言えます
正規形はβ-nf(β-NormalForm)とも表記されます

ある一つのラムダ式に変換をどのような順序で行なっても
ただ一つの正規形に行き着くことをチャーチ・ロッサー性と言います

数学の関数はチャーチ・ロッサー性があり必ず一つの何らかの値に行き着きます
ひとつのラムダ式には正規形は一つしか無いという言い方もできます
これはチャーチ・ロッサーの定理を考えれば
あるラムダ式がβ変換でどんな枝分かれをしても必ず合流できるところから
わかります
たとえばMから２つの正規形J1とJ2ができたとしても
Mから変換されたものですから
必ずJ1とJ2は合流でき正規形はひとつになります
一意性とも言います

β基の中で最も左にあるものを最左基といいます

最も左のβ基からβ変換をする評価戦略
正規変換とも言う

あるラムダ式が正規形を持つならば
最左変換を繰り返すことで正規形を得られる

ことを保証します
ただしこの最左変換は有限の繰り返しで終わる場合で
無限に続いてしまう場合はそのラムダ式は正規形を持たないことになります