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 functionallanguage, 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.