[Haskell-cafe] help understanding lazy evaluation

[Malte Milatz]

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