Beta normal form とは

ラムダ計算では、ベータの削減ができない場合は、ベータ正規形式になります。ベータ削減やηの削減が不可能な場合、ベータηの正規形になります。頭の位置にベータ・リデックスがない場合、用語は頭部の標準形である。