Unlike many other programming languages, functions in Standard ML can be designated by arbitrarily complex expressions. The general form of an application is e e', which is evaluated by first evaluating e to obtain some function and then evaluating e' to obtain some value and finally applying the function to the value. In general, the expression e can be quite complex and significant computation may be required before a function is returned. This rule for evaluation of function application uses the call-by-value parameter passing mechanism because the argument to a function is evaluated before the function is applied.
An alternative strategy is call-by-name. Here the expression e' is substituted for all the occurrences of the formal parameter. The resulting expression is then evaluated as normal. This might mean that we evaluate some expressions more than once. Clearly, call-by-value is more efficient. The following important theorems make precise the relationship between the two forms of evaluation.
Lazy languages do not use call-by-name evaluation; they use call-by-need. Here when the value of an expression is computed it is also stored so that it need never be re-evaluated, only retrieved. In practice, a lazy language might do more computation than strictly necessary, due to definition of functions by pattern matching. In these cases it would not meet the applicability criteria of the Second Church Rosser theorem because it imperfectly implements call-by-name.
Theorem (Church Rosser 1)
For a purely functional language, if call-by-value evaluation and call-by-name evaluation both yield a well-defined result then they yield the same result.
Theorem (Church Rosser 2)
If a well-defined result exists for an expression then the call-by-name evaluation strategy will find it where, in some cases, call-by-value evaluation will not.