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 1), but const, 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?

  • $\begingroup$ What you are calling "head normal form" is actually weak head normal form. See, e.g. page 5 of Demonstrating Lambda Calculus Reduction. $\endgroup$ – Derek Elkins left SE May 25 '18 at 21:39
  • $\begingroup$ @DerekElkins thanks for clarifying that for me! I updated the question. $\endgroup$ – user23039 May 25 '18 at 21:58
  • $\begingroup$ If you claim that "const 1 may change" because we could apply it to 2, then you also have to agree that const (1, 2) may change because we could apply fst to it. I do not understand your question. And the title of your question is odd, did you mean "evaluation context" instead of "environment"? An environment is a mapping of variables to their values, but you are talking about closed expressions which are completely independent of the environment. $\endgroup$ – Andrej Bauer May 26 '18 at 18:18
  • $\begingroup$ @AndrejBauer yes, I agree, I didn't think of it that way. I suppose then what I'm looking for is "a WHNF that can be applied" vs. "a WHNF that cannot be applied". I suppose there are no terms for that? Perhaps you could add your comment as an answer. It doesn't answer the question directly, but does explain why it is a weird question. $\endgroup$ – user23039 May 28 '18 at 9:52
  • $\begingroup$ If I understand you correctly, you want to make application special. So of all eliminator forms applying to a term is special. It would be helpful to know the motivation for this. Where are you going with this? $\endgroup$ – Andrej Bauer May 28 '18 at 12:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy