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.

• Anton Trunov: I think this question reveals that Seq doesn't work as it should.
• Gilles 'SO- stop being evil': @AntonTrunov It works but the semantics is bizarre, since display is basically evaluated in applicative order. And I don't see that specified in the lecture notes.
• Anton Trunov: Then why "hello" doesn't get printed after the first $\beta$-reduction? (when we substitute (display "hello") for $x$)).
• Anton Trunov: A quote from the notes: "This combinator guarantees that $x$ is evaluated before $y,ドル which is important in programs with side-effects." I understand it as -- Seq is a "universal" combinator, so it should work not only for display (it's for the case when we make (display ...) a special form).