What is the relation between the formal definition of strictness and its intuitive notion

Question

I am currently reading Functional Programming in Scala and have encountered a statement in the book I cannot quite make sense of.

On page 67, we are told the formal definition of strictness:

"If the evaluation of an expression runs forever or throws an error instead of returning a definite value, we say that the expression doesn't terminate, or that it evaluates to bottom. A function f is strict if the expression f(x) evaluates to bottom for all x that evaluate to bottom."

This definition is somewhat puzzling because the discussion of strictness that comes before this definition has discussed strictness in relation to lazy evaluation. To say that an expression is strict is to say that it is completely evaluated, and not lazy. What is not clear is how this notion of strictness and laziness is at all related to the formal definition given.

Answer 1

The intuition: if executing f(x) causes x to be evaluated, and evaluating x doesn't terminate, then this will cause f(x) to fail to terminate (because evaluating x doesn't terminate, so the execution of f(x) never completes).

So, if executing f(x) always causes x to be executed, then f will be strict by the formal definition above. That's why "f(x) completely evaluates x" implies "f(x) evaluates to bottom for all x that evaluate to bottom".

In contrast, with a lazy function, evaluating f(x) doesn't necessarily trigger evaluation of x, so it doesn't necessarily terminate (even if evaluating x wouldn't terminate). Thus, for a function that is intuitively lazy, it won't meet the formal definition of strict.