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

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.

• Can you edit your question to articulate a specific question about it? It makes sense to me, so that makes it harder for me to understand what is puzzling to you. Also it would help to explain what is the intuitive notion that you want to compare to (perhaps you can give a quote or explanation). – D.W. Sep 13 at 18:04
• @D.W. For some reason, after I read your comment and reread my question, a lightbulb went off in my head. What I was having trouble with was the relation between laziness and non-terminating expressions. I suppose if an expression is lazy, it doesn't terminate, and vice-versa. I was having trouble making that connection. If you can elaborate on this connection in an answer, that would be helpful, although I have the gist of what's being said so that I can now make a connection between the formal definition and my intuition. – Allen Han Sep 13 at 18:11

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.