私は関数型言語の実装を読んでいます: チュートリアルで、完全に遅延したラムダ リフティングのフローティング パスを実装するときに問題が発生しました。
この質問を明確にするために、フローティングがどのように機能するかを説明したいと思います。慣れている場合は、以下の質問にスキップしてください。
この概念は論文の 246 ページで紹介されており、主に 256 ～ 257 ページで実装されています。
表現の場合は、次のlet(rec)ように言います。
let(rec)右辺はそれらに依存する可能性があるため、式自体の前に右辺の浮動定義を配置する必要があります。
例えば：
\a ->
let f = \b -> b + (let $mfe = a * a in $mfe)
in f
変数$mfeは、前のパスで識別された最大自由式 (MFE)let fであり、式を処理するときに、1 つのグループとして浮動し、 の右側から取得した にf追加します。ここで、最初のコンポーネントは、グループの空きレベルを示します。[(1, [($mfe, a * a)])]let f1
抽象化に戻ると、と\a -> fの両方が抽象化に拘束されていることがわかったので、ここにインストールする必要があります。$mfef
\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)
との空きレベルは2 になりますb x。これは、レベル 2 があり、同じグループに属しているためです。a yy
との無料レベルは3 ですが、したがってとは MFE としてマークされます (ここで間違いを犯しましたか?)。cons p (b x)cons q (a y)b xa y
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)
式の右側の MFE は、左側を参照するときはいつでもスコープをエスケープ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)
用紙がおかしい？または私はそれを誤解しました。