Плавающий проход полностью ленивый лямбда-лифтинг?

Question

Я читаю реализацию функциональных языков: учебное пособие, и столкнулся с проблемой при реализации плавающего прохода полностью ленивого лямбда-лифтинга.

Я хотел бы описать, как работает плавающий, чтобы прояснить этот вопрос, если вы знакомы с ним, просто перейдите к вопросу ниже.

Эта концепция представлена ​​на странице 246 в документе и в основном реализована на странице 256-257.

В случае let(rec) выражение, оно говорит:

мы должны поместить плавающие определения правой части перед let(rec) Само выражение, так как от них может зависеть правая часть.

например:

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

Переменная $mfe является максимальным свободным выражением (MFE), которое было идентифицировано предыдущим проходом при работе с let f выражение, мы плаваем f как одна группа и добавить его к [(1, [($mfe, a * a)])], который был получен с правой стороны let f, Здесь первый компонент 1 указывает на свободный уровень группы.

Когда возвращаемся к \a -> f абстракция, мы обнаружили, что оба $mfe а также f связаны этим, поэтому мы должны установить их здесь:

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

Вопрос

Предположим, у нас есть такая программа:

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

Свободный уровень b x а также a y будет 2, так как y имеет уровень 2, и они находятся в одной группе.

Пока свободный уровень cons p (b x) а также cons q (a y) 3, таким образом b x а также a y будут помечены как MFEs (я здесь сделал ошибки?).

Используя алгоритм, заданный SPJ, программа будет преобразована в:

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)

Я думаю, что МФУ в правой части let(rec) выражение не должно ускользать от let(rec) область видимости всякий раз, когда он ссылается на левую часть, и правильный результат может выглядеть так:

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)

Бумага не так? или я просто неправильно понял.