Lambda calculus: evaluation by value would not terminate but normal evaluation terminates

Question

I'm wondering if it is possible that evaluation by value would not terminate but normal evaluation terminates.

Because in normal evaluation we will evaluate until we reach a normal form meaning that we cannot evaluate further, but in by-value, we evaluate everything except the last lambda and we evaluate all the arguments even the ones that are not used.

So I don't think it would be possible because normal evaluation is more eager than by-value.

Answer 1

Yes, it is possible that evaluation by value (which fires a $\beta$-redex only if the argument is a value, i.e. an abstraction or a variable) does not terminate but normal evaluation (which fires the leftmost-outermost $\beta$-redex) terminates.

Consider for instance the term $(\lambda y. I) (\Delta \Delta)$, where $I = \lambda x.x$ and $\Delta = \lambda x. xx$. We have:

• normal evaluation $\to_\beta$ terminates because $(\lambda y. I) (\Delta \Delta) \to_\beta I$, since there are no free occurrences of the variable $y$ in $I$;
• evaluation by value $\to_{\beta_v}$ does not terminate because $(\lambda y. I) (\Delta \Delta) \to_{\beta_v} (\lambda y. I) (\Delta \Delta) \to_{\beta_v} (\lambda y. I) (\Delta \Delta) \to_{\beta_v} \dots$, since evaluation by value forces to evaluates $\Delta \Delta$ first, and $\Delta \Delta \to_{\beta_v} \Delta \Delta \to_{\beta_v} \dots$.