弱頭部正規形
Weak Head Normal Form, WHNF
1番外側のconstructorまたはラムダ抽象まで評価したもの
完全な正規形まで簡約されていない、簡約途中な状態
簡約途中な項も(広義の)正規形とみなすことで、必要以上に簡約しないで済む
正規形 \sub弱頭部正規形
任意の正規形は弱頭部正規形である
Simon Peyton Jonesが作った言葉らしい ref
seq関数を使うことで弱頭部正規形まで評価できる
例
(1 + 1, 2 + 2) 1番外側は
(,) 内部の
1+1 などは正規形でなくて良い \x -> 2 + 2 一番外側はラムダ抽象
内部の
2+2 は正規形でなくて良い 'h' : ("e" ++ "llo") 一番外側は
(:) 内部の
"e"++"llo" は正規形でなくて良い 2 正規形なものは弱頭部正規形でもある
弱頭部正規形でない例
1 + 2 一番外側の関数適用
(+) が、簡約されていない (\x -> x + 1) 2 一番外側の関数適用
(\x -> x + 1) _ が、簡約されていない "he" ++ "llo" 一番外側の関数適用
(++) が、簡約されていない
参考
(redexは簡約項のこと)