完全懒惰的lambda浮动通行证？

我正在阅读实现函数式语言:一个教程,并在实现完全懒惰的lambda提升的浮动传递时遇到了问题.

我想描述浮动如何使这个问题清楚,如果你熟悉它,只需跳到下面的问题.

该概念在本文的第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)表达式右侧的MFE在引用左侧时不应该逃避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)

报纸错了吗？或者我只是误解了它.