In my understanding, a lambda expression is a normal form (NF) when it has no redexes. For instance, $\lambda x.x$ is a NF, but $(\lambda x.x)y$ is not. A lambda expression is a weak head normal form (WHNF) if the root expression is not a redex. For instance, $\lambda x.(\lambda y.y)x$ is a WHNF, but not a NF as it reduces to $\lambda x.x$.
When implementing functional programming languages we call the opposite of an expression in WHNF a thunk. Thus, taking Haskell as an example,
const 1 2 is a thunk (it evaluates to
const 1 and
(1,const 1) are WHNFs (the first two are unsaturated applications; the last is a constructor).
I'm looking for term to distinguish
const (1,2) and
(1,const 1). They are both WHNFs, neither is in NF, however, the root constructor of the latter (
(,)) will not change any more while that of the former (
const) may still change, if it is applied to some other expression (to
(,)). Are there terms that distinguish WHNFs of which the head can/cannot change in any environment?