functional programming – How are applications of the normal/applicative order sequencing combinators evaluated?

From Programming Distributed Computing Systems, there is a section under the chapter for lambda calculus:

2.7 Sequencing Combinator

The normal order sequencing combinator is:

Seq = λx.λy.(λz.y x),

where z is chosen so that it does not appear free in y.

This combinator guarantees that x is evaluated before y, which is
important in programs with side-effects. Assuming we had a “display”
function sending output to the console, an example is

((Seq (display “hello”)) (display “world”)).

The combinator would not work in applicative order (call by value)
evaluation because evaluating the display functions before getting
them passed to the Seq func- tion would defeat the purpose of the
combinator: to sequence execution. In particular, if the arguments are
evaluated right to left, execution would not be as expected.

The applicative-order sequencing combinator can be written as follows:

ASeq = λx.λy.(y x),

where y is a lambda abstraction that wraps the original last
expression to evaluate. The same example above would be written as
follows:

((ASeq (display “hello”)) λx.(display “world”)),

with x fresh, that is, not appearing free in the second expression.

(1) In Seq = λx.λy.(λz.y x), is y required to be a lambda abstraction i.e. a function definition? (I guess so, because (λz.y x) is evaluated to (y,x)?)

(2) How is ((Seq (display “hello”)) (display “world”)) evaluated? Is “hello” supposed to be printed before “world”? Is it evaluated

  • first to (λy.(λz.y (display “hello”)) (display “world”)), in normal order
  • then to (λz.(display “world”) (display “hello”)), in normal order
  • then to (display “world”), in normal order.
  • then to nil?

So is (display “hello”) not evaluated?

(3) Similarly, how is ((ASeq (display “hello”)) λx.(display “world”)) evaluated? Is “hello” supposed to be printed before “world”? Is it evaluated

  • first evaluate the argument (display “hello”) to nil,
  • then evaluate the application ((ASeq nil) λx.(display “world”)) to (λy.(y nil) (display “world”)),
  • then evaluate the argument (display “world”) to nil,
  • then evaluate the application (λy.(y nil) nil) to (nil nil),
  • then evaluate (nil nil) to nil?