スキームとCPS変換のコンテキストでは、管理用の正規表現(ラムダ) が正確に何であるかを判断するのに少し苦労しています。
- CPS 変換によって導入されるすべてのラムダ式
- CPS 変換によって導入されるラムダ式のみですが、「手動で」またはよりスマートな CPS コンバーターを介して変換を行った場合は記述しませんでした。
良ければ参考になれば幸いです。
スキームとCPS変換のコンテキストでは、管理用の正規表現(ラムダ) が正確に何であるかを判断するのに少し苦労しています。
良ければ参考になれば幸いです。
Redex は「還元可能な式」の略で、値ではない式です。したがって、ラムダはリデックスではありませんが、呼び出しはリデックスです。
CPS では、管理者の redex は、演算子が継続ラムダである redex です。このような redex は、呼び出している関数がわかっているため、すぐに減らすことができます。
たとえば、((lambda (u) ...) foo)
は管理上のリデックスですが、(k foo)
そうではありません。
私は自分の答えを見つけたと思います。(編集:代わりにdimvarの回答を受け入れました。より短く、より正確です。)
入力プログラムが完全にCPSでない場合、少なくとも1つのプロシージャー戻りポイントをCPS変換によって継続に変換する必要があります。したがって、この継続は、変換によって導入され、必要なものです。必要なので、たとえば手動で変換する場合も、常にこれを行う必要があります。したがって、管理上のリデックスは、CPS変換によって導入されたラムダであり、実際には必要ありません(私の2番目の定義)。
私はそれをこのように説明する論文を見つけました(私の強調):
ただし、CPSへのナイーブなλエンコードは、ラムダの非常に印象的な膨張を生成します。ラムダのほとんどは、安全に削減できる管理上のやり直しを形成します。管理上の削減により、手作業で記述できるものに対応するCPS用語が生成されます。したがって、CPS変換時に、可能な限り多くの管理上のやり直しを排除することが課題になっています。
それでも、コメントや提案はもちろん歓迎します。