ما هي بالضبط Redexes الإدارية بعد تحويل CPS؟

Question

في سياق المخطط و CPS التحويل ، أواجه مشكلة صغيرة في تحديد ما هي الإدارية Redexes (Lambdas) بالضبط:

• الكل تعبيرات Lambda التي يتم تقديمها بواسطة تحويل CPS
• فقط تعبيرات Lambda التي يتم تقديمها بواسطة تحويل CPS ولكن لم تكن قد كتبت إذا قمت بالتحويل "باليد"

إذا كان ذلك ممكنًا ، سيكون المرجع الجيد موضع ترحيب.

Answer 1

REDEX تعني "التعبير القابل للتخفيض" ، وهو تعبير ليس قيمة. لذلك ، فإن Lambda ليس Redex ، ولكن المكالمة.
في CPS ، REDEX الإداري هو REDEX الذي يشغله مشغل Lambda استمرار. يمكن تقليل هذه Redexes فورًا لأنك تعرف الوظيفة التي تتصل بها.
علي سبيل المثال، ((lambda (u) ...) foo) هو Redex إداري ، ولكن (k foo) ليس.

Answer 2

أعتقد أنني وجدت إجابتي. ((تعديل: لقد قبلت إجابة Dimvar بدلاً من ذلك ، إنها أقصر وأكثر صحة.)

على افتراض أن برنامج الإدخال ليس CPS بالكامل ، يجب تحويل نقطة إجراء إجراء واحدة على الأقل إلى استمرار بواسطة تحويل CPS. لذلك يتم تقديم هذا الاستمرار عن طريق التحويل و من الضروري. لأنه ضروري ، ستحتاج دائمًا إلى القيام بذلك ، أيضًا عند التحويل باليد على سبيل المثال. لذلك ، فإن Redexes الإدارية هي فقط تلك lambdas التي تم تقديمها بواسطة تحويل CPS والتي ليست ضرورية حقًا (تعريفي الثاني).

لقد وجدت ال ورق هذا يفسر ذلك مثل هذا (التأكيد لي):

ومع ذلك ، فإن الترميز naîve λ في CPS ، يولد تأثيرًا مثيرًا للإعجاب للغاية من lambdas ، عظم من أي شكل من أشكال REDSES الإدارية التي يمكن تقليلها بأمان. تخفيضات إدارية تسفر عن مصطلحات CPS المقابلة لما يمكن للمرء أن يكتبه باليد. لذلك أصبح من الصعب القضاء على أكبر عدد ممكن من Redexes الإدارية ، في وقت تحويل CPS.

ومع ذلك ، فإن أي ملاحظات أو اقتراحات ترحب بها بالطبع.