floating pass of fully lazy lambda lifting?

Question

I'm reading implementing functional languages: a tutorial, and encountered a problem when implementing floating pass of fully lazy lambda lifting.

I would like to describe how floating works to make this question clear, if you are familiar with it, just skip to the question below.

The concept is introduced at page 246 in the paper, and mainly implemented at page 256-257.

In case of let(rec) expression, it says:

we must put floated definitions of right-hand side before the let(rec) expression itself, since the right-hand side may depend on them.

for example:

\a ->
  let f = \b -> b + (let $mfe = a * a in $mfe)
  in f

The variable $mfe is a maximal free expression (MFE) which identified by previous pass, when dealing with let f expression, we float f out as one group and append it to [(1, [($mfe, a * a)])], which was obtained from right-hand side of let f. Here, the first component 1 indicates the free level of the group.

When backtracking to \a -> f abstraction, we found that both $mfe and f are bound by it, hence we should install them here:

\a ->
  let $mfe = a * a
  in
    let f = \b -> b + $mfe
    in f

The Question

Suppose we have a program like this:

f = \x -> \y ->
  letrec
    a = \p -> cons p (b x)
    b = \q -> cons q (a y)
  in pair (a 1) (b 2)

The free level of b x and a y will be 2, since y has level 2 and they are in a same group.

While free level of cons p (b x) and cons q (a y) is 3, thus b x and a y will be marked as MFEs (Did I make mistakes here?).

Using the algorithm given by SPJ, the program will be transformed into:

f = \x -> \y ->
  let $ay = a y -- `a` is not defined yet!
  in
    let $bx = b x -- and `b`
    in
      letrec
        a = \p -> cons p $bx
        b = \q -> cons q $ay
      in pair (a 1) (b 2)

I think the MFEs in the right-hand side of let(rec) expression should not escape the let(rec) scope whenever it referenced to the left-hand side, and the correct result might like this:

f = \x -> \y ->
  letrec
    $ay = a y
    $bx = b x
    a = \p -> cons p $bx
    b = \q -> cons q $ay
  in pair (a 1) (b 2)

Does the paper wrong? or I just misunderstood it.

Ethiopic

without reading the book, you can't float a y above letrec which defines a, obviously, and your 2nd transformation looks correct. – Signe

@WillNess yes, just capture the floated definitions which has same free level with the let(rec) expression and put them together will fix this issue. But I'm not sure if I missed sth when reading the paper or made some mistakes. – Yautia