β基
β-redex
β可簡約項
、
簡約基
、βリデックスともいう
$ (\lambda x.N)M
の形の
ラムダ抽象
のこと
まだ簡約できる状態のもの
これ以上簡約できないところまで簡約しきったらそれを
正規形
と呼ぶ
正規形はβ基ではない
つまり
ラムダ抽象
は、
β基
か
β正規形
の2種類しかない、といえる
また、
$ [x\to N]M
のことを
コントラクタム
(
contractum
)と呼ぶ