27 Lazy Evaluation
We have seen short-circuiting evaluation (Section 21.6), which is a particular instance of lazy evaluation where some sub-expression is conditionally evaluated.
In this chapter, we consider call-by-name, which is another of form of lazy evaluation in defining the semantics of function call \(e_1\texttt{(}e_2\texttt{)}\). In contrast to call-by-value, call-by-name semantics does not evaluate the function argument to a value before starting to evaluate the function body. Instead, it takes the unevaluated argument expression and substitutes it for the formal parameter.
Consider two possible \(\TirName{DoCall}\) rules:
\(\inferrule[DoCallByValue]{ }{ (\texttt{(}x\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1) \texttt{(} v_2 \texttt{)} \longrightarrow {}[v_2/x]e_1 }\)
\(\inferrule[DoCallByName]{ }{ (\texttt{(}x\texttt{)} \mathrel{\texttt{=}\!\texttt{>}} e_1) \texttt{(} e_2 \texttt{)} \longrightarrow {}[e_2/x]e_1 }\)
It is one tiny difference on paper that is a substantively different semantically. The \(\TirName{DoCallByValue}\) rule requires that the argument be eagerly evaluated to a value before applying the substitution, while the \(\TirName{DoCallByName}\) rule does not. Call-by-name is lazy in that if \(e_1\) does not end up using the parameter \(x\) in the subsequent evaluation, then \(e_2\) will not be evaluated (i.e., like being “short-circuited”).
## Formalization - formalize when an expression is reducible given the parameter passing mode