paragraph on normal order reduction in Untyped chapter

[peterthiemann]

The reduction strategy implemented by progress corresponds to the well-known normal order reduction.
This PR proposes a few paragraph that discuss normal order reduction.

[wenkokke]

Oh dear, have neither @wadler nor myself seen this PR for over a year? My apologies!

[peterthiemann]

I remembered it when I got to that point in the lecture.
IIRC @wadler wanted to edit the text.

[wenkokke]

@wadler Could you comment?

[wadler]

Thanks, Peter! Sorry for the delay.

I agree that explaining "normal order reduction" is a good idea. I'm happy to accept lines 543-549 (except delete from "We can see ..." on 549) and lines 566-569.

Lines 551-556 duplicate what has already been said, in a form that doesn't align well with what came before, e.g. in progress there are three subcases for application, not two. Lines 558-562 consider two alternatives. In the first alternative, "introduces a chance of non-termination" requires more explanation for beginning students. In the second alternative, "have more opportunities" requires more explanation, and arguably is not correct. The second alternative includes various forms of optimal reduction, where the total number of reduction steps can be reduced by applying reduction "early" to the body of the lambda abstraction. That requires much more explanation, and is arguably not appropriate for this level of text. Rather than delay with further back-and-forth over these paragraphs, I recommend deleting them and accepting the rest.

[proglang]

I trimmed the commit as per @wadler 's request

[wenkokke]

@wadler Are you content with these changes now? Shall we merge this?

[wadler]

Thank you!