CSE230  THURSDAY FEBRUARY 12, 1998



NORMAL ORDER EVALUATION

Question: is there any evaluation policy that always terminates
	when termination is possible?

Yes: the "normal order" policy, which is called normal because
	it always finds a normal form if one exists.

The normal policy:
	reduce the redex that starts furthest to the left.

Intuitively, evaluating inside an abstraction first may cause some
	arguments to be discarded.

Exercise (difficult!): prove that if some reduction order terminates,
	then normal order terminates.	



AN EXAMPLE OF NORMAL ORDER

Consider standard and normal order applied to the expression
	(fn x => (fn y => 5) (h x x)) 3
where h is a non-terminating function.

For example h could be the recursive function
	fun h x y = h y x;
Note as mentioned before, the link between recursion and naming.

Standard order gives 
	(fn x => (fn y => 5) (h x x)) 3  ->  (fn y => 5) (h 3 3)
                                         ->  (fn y => 5) (h 3 3)  -> ...
Normal order gives
	(fn x => (fn y => 5) (h x x)) 3  ->  (fn y => 5) (h 3 3)
                                         ->  5


LAZY EVALUATION

Normal order is "lazy" about evaluating arguments because they
are evaluated only when needed.

Normal order evaluation can be very inefficient because arguments
	may be duplicated, then evaluated repeatedly.

Consider for example
	(fn x: int => x + x) (fact x)
where (fact x) is expensive to compute



CACHING

Lazy evaluation is normal order made efficient by caching.

"Caching" means replacing an argument expression everywhere it appears
by its value AFTER the first time it is evaluated.

Caching is also called tabling, tabulating, memoing, and memoizing:
the idea has been independently rediscovered many times.

Caching is only correct with referential transparency,
i.e. in the absence of side-effects.



STOPPING LAZY EVALUATION

When should lazy evaluation stop?
Answer: as soon as something printable is reached, i.e.
the first part of the final result is known.
This is the top-level constructor of the result.

Consider the expression providing the value of "series" here.
Nothing needs to be evaluated when processing this
declaration in a lazy version of ML:

	- val rec series = 2 :: map inc series;

Lazy ML could respond

	val series = (:: ? ?) : int list;

giving some information on the result but more than absolutely needed.

Let's assume here that "inc" is a builtin function and that "map"
is defined as

	- fun map f [] = []
            | map f (h::t) =  (f h)::(map f t);

Note that in standard ML only function declarations may be recursive.
Declarations of lists may not be.



WEAK HEAD NORMAL FORM

Formally, lazy evaluation repeatedly reduces an expression following
normal order policy untul weak head normal form is reached.

Definition: An expression is in weak HEAD normal form if
	the top-level redex involves a constructor function.

We can start printing an expression in weak head normal form
even without finishing its evaluation.

Weak head normal form is the appropriate notion for infinite values.



AN EXAMPLE OF LAZY EVALUATION

Suppose we want the third item of "series", i.e. to reduce to WHNF

	- hd (tl (tl series))

In order to reduce the outermost redex, we must be able to
pattern-match on its argument, i.e. (tl (tl series)) must be in WHNF.

In order to achieve this, we must first reduce (tl series) to WHNF.

We have that (tl series) -> map inc series
but this is not yet in WHNF.

In order to reduce this redex involving "map", similarly to before
we need "series" to be in WHNF, which it is.

So (tl series) -> (map inc series) -> (inc 2)::(map inc (map inc series))
which is in WHNF.

Now (tl (tl series)) ->* (tl (inc 2)::(map inc (map inc series)))
	-> map inc (map inc series) 
	-> map inc (inc 2)::(map inc (map inc series))
	-> (inc (inc 2))::(map inc (map inc (map inc series)))
which is in WHNF

So (hd (tl (tl series))) 
	->* hd (inc (inc 2))::(map inc (map inc (map inc series)))
	-> (inc (inc 2))
	-> (inc 3)
	-> 4



NON-CONSTRUCTOR FUNCTIONS ARE STRICT UNDER LAZY EVALUATION

All non-constructor functions, i.e. all programmer-defined functions
and all builtin functions, require their arguments to be evaluated
until WHNF.

In particular hd and tl are strict.



COMMENTS ON LAZY EVALUATION

The principle of "information-hiding" is that programs should be decomposed
	into highly independent pieces, with restricted interfaces.
A user of an independent piece need only understand the interface.
Most of the detail of each piece is hidden from its users.

This principle underlies several slogans:
	"retargetable frontends"
	"divide and conquer"
	"separation of concerns"

Lazy evaluation is a control abstraction:
	control details are filled in automatically.

It allows specification of what a function computes
	independent of how (in what order) it is computed.

It is similar to Prolog backtracking.



THE PREDICTABILITY OF RUNTIMES

Lazy evaluation has a major drawback from a software verification
point of view: functions do not have well-defined running times.

With eager evaluation, for each function F there is a time function t
such that the time to evaluate F(A) is                               F

	time(F(A)) = t (value(A)) + time(A)
                      F

With eager evaluation running time is a compositional property
that depends on the semantics of arguments (i.e. their values)
but not on their syntax (i.e. what expressions denote them).

But lazy evaluation destroys the compositionality of runtime.