頭部簡約
head reduction
$ \lambda x_1,\cdots,x_n.(\lambda x.M_0)M_1M_2\cdots M_m
$ n\ge0, m\ge1
の
$ (\lambda x.M_0)M_1
を簡約する
頭部正規形
参考
『(理論)12 計算モデルの基礎理論』
p.97