Normal order sequencing vs applicative order sequencing

Question

I'm trying to understand this lecture, section 2.7. Why would the normal order sequencing print out "hello" "world" and not "world" "hello"? I may be misinterpreting the order in which the arguments are applied.

It looks like the expression

$$ ((Seq (display "hello"))\; (display "world")) $$

would evaluate to

$$ \lambda z.((display "world")\; (display "hello")) $$

and that would, under normal order, would print out "world" "hello".

My question is whether the assumption I'm making is correct. If not, could you show the correct derivation of the end-expression?

Answer 1

You're misreading the combinator. In these lecture notes, lambda abstraction binds tighter than application (the opposite convention is more common — it's apparent from the spacing but the author should state that explicitly). I'll use extra (redundant) parentheses in my answers to avoid any potential for ambiguity. The combinator is $$ \mathit{Seq} = \lambda x. \lambda y. ((\lambda z.y) \: x)$$ So $$ \begin{align} & ((\mathit{Seq} \; (\text{display "hello"})) \; (\text{display "world"})) \\ &\qquad = (((\lambda x. \lambda y. ((\lambda z.y) \; x)) \; (\text{display "hello"})) \; (\text{display "world"})) \\ &\qquad \to^2 ((\lambda z. (\text{display "world"})) \; (\text{display "hello"})) \\ &\qquad \xrightarrow{\text{display "hello"}} (\text{display "world"}) \\ &\qquad \xrightarrow{\text{display "world"}} \mathord{?} \\ \end{align} $$ where $M \xrightarrow{\text{action}} N$ means that $M$ evaluates to $N$ performing the specified action.