Stefan O'Rear wrote:
As is usual for mathematical things, there are many equivalent definitions. My two favorites are:
1. Normal order reduction
In the λ-calculus, lazy evaluation can be defined as the (unique up to always giving the same answer) evaluation method, which, if *any* evaluation order would finish, works. This is a rather subtle theorem, not a trivial definition, so it could be hard to use.
Hudak in his HSoE book gives a less precise, but more concrete definition of normal-order reduction (shamelessly quoted here): “If a rule or rules can be applied to more than one position in an expression, use the rule corresponding to the *outermost* position in the expression.” Bulat Ziganshin wrote elsewhere:
simple example: consider evaluation of "head [1..]".
With the rule above, we have: head [1..] {- We cannot apply the definition of head yet, because the first element of the list ist not visible, so we apply the definition of [..] -} = head (1 : [(succ 1)..]) {- Now we could apply either the definition of succ 1, or [..], or head. But head is the outermost, so: -} = 1. Malte