CPS 変換後の管理 Redexe とは正確には何ですか?

Question

スキームとのコンテキストでは、 CPS 変換、管理上の意味を決めるのに少し苦労しています レデックス (ラムダ) は正確には次のとおりです。

• 全て CPS 変換によって導入されるラムダ式
• のみ CPS 変換によって導入されるラムダ式ですが、「手動」で変換するか、よりスマートな CPS コンバーターを使用して変換を行った場合は記述しなかったでしょう。

可能であれば、良い参考資料をいただければ幸いです。

Answer 1

可約式は値ではありません表現である「還元性表現」、の略です。したがって、ラムダは可約式ではありませんが、呼び出しがあります。
CPSでは、行政可約式は、そのオペレータ継続ラムダで可約式です。あなたが呼び出している関数を知っているので、そのようなredexesはすぐに軽減することができます。
例えば、((lambda (u) ...) foo)が管理可約式ですが、(k foo)ではありません。

Answer 2

自分なりの答えが見つかったと思います。(編集： 代わりに dimvar の答えを受け入れました。それは短くてより正確です。)

入力プログラムが完全には CPS ではないと仮定すると、少なくとも 1 つのプロシージャ戻り点を CPS 変換によって継続に変換する必要があります。したがって、この継続は両方とも変換によって導入されます そして 必要。これは必要なため、手動で変換する場合などにも常に行う必要があります。したがって、管理用リデックスは、CPS 変換によって導入された、実際には必要のないラムダだけです (私の 2 番目の定義)。

見つけました 紙 それは次のように説明されます（私のものを強調してください）。

しかし、cpsにcpsにエンコードするナイブは、ラムダの非常に印象的なインフレを生成します。 ほとんど そのうち、安全に減らすことができる管理者の再編集。管理削減により、手作業で書くことができるものに対応するCPS用語が得られます。したがって、CPS変換時間に、できるだけ多くの管理的なredexを排除することは挑戦になりました。

もちろん、コメントや提案は大歓迎です。