¿Qué son exactamente las redecciones administrativas después de la conversión de CPS?

Question

En el contexto del esquema de conversión y CPS, estoy teniendo un poco de problemas para decidir qué administrativa redexes (lambda) son exactamente:

• todas las expresiones lambda que se introducen por la conversión de CPS
• solamente las expresiones lambda que se introducen por la conversión de CPS, pero que no habría escrito si se hizo la conversión "a mano" o por medio de un convertidor inteligente CPS-

Si es posible, una buena referencia sería bienvenida.

Answer 1

Redex significa "expresión reducible", que es una expresión que no es un valor. Por lo tanto, una lambda no es un redex, sino una llamada.
En CPS, un redex administrativo es un redex cuyo operador es una continuación lambda. Tales redexes pueden reducirse inmediatamente porque usted sabe a qué función está llamando.
Por ejemplo, ((lambda (u) ...) foo) es un redex administrativo, pero (k foo) no lo es.

Answer 2

Creo que encontré mi respuesta. (Editar:. He aceptado la respuesta de dimvar En cambio, es más corto y más correcta)

Suponiendo que el programa de entrada no es totalmente CPS, al menos un procedimiento de punto de retorno tendrá que ser convertidos en una continuación por el CPS conversión. Entonces esta continuación es introducida por la conversión y necesaria. Debido a que es necesario, siempre tendrá que hacer esto, también al convertir a mano, por ejemplo. Por lo tanto, los redex administrativos son solo aquellos lambdas introducidos por la conversión de CPS que no son realmente necesarios (mi segunda definición).

encontré una paper que explica de la siguiente (el énfasis es mío):

los ingenuos λ-codificación en CPS, sin embargo, genera una impresionante la inflación de lambdas, más de los cuales formar redexos administrativos que pueden ser reducidos con seguridad. Las reducciones administrativas producen los términos de CPS que corresponden a lo que se podría escribir a mano. Por lo tanto, se ha convertido en un desafío para eliminar tantas redexes administrativas como sea posible, en CPS-transformation time.

Aún así, cualquier comentario o sugerencia bienvenida, por supuesto.