β正規形
innermost redex
再内基
とも言う
部分項
として
β基
を持たない
β基
のことを
β正規形
と呼ぶ
β正規形
は持つなら一意
$ M_1{}_\beta\xleftarrow{\ast}M\xrightarrow{\ast}_\beta M_2
ならばで、
$ P,Q
が共に
β正規形
ならば、
$ P\equiv Q
β正規形
を持たない
ラムダ抽象
もある
ex.
Ω-コンビネータ
例
$ (\lambda xy.x)(Iu)(I(Iv))
の部分項のうちの
$ Iu
や
$ Iv