O que exatamente são redes administrativos após a conversão do CPS?

Question

No contexto do esquema e Cps conversão, estou tendo um pouco de problema em decidir que administrativo Redexes (Lambdas) exatamente são:

• tudo as expressões lambda que são introduzidas pela conversão do CPS
• só As expressões Lambda que são introduzidas pela conversão do CPS, mas você não teria escrito se fizesse a conversão "manualmente" ou através de um conversor CPS mais inteligente

Se possível, uma boa referência seria bem -vinda.

Answer 1

O RedEx significa "expressão redutível", que é uma expressão que não é um valor. Portanto, um lambda não é um redel, mas é uma chamada.
No CPS, um redenvente administrativo é um redel cujo operador é um lambda de continuação. Esses Redexes podem ser reduzidos imediatamente porque você sabe qual função está chamando.
Por exemplo, ((lambda (u) ...) foo) é um redex administrativo, mas (k foo) não é.

Answer 2

Acho que encontrei minha resposta. (Editar: Eu aceitei a resposta de Dimvar, é mais curta e mais correta.)

Supondo que o programa de entrada não seja totalmente CPS, pelo menos um ponto de retorno do procedimento deverá ser convertido em uma continuação pela conversão do CPS. Portanto, esta continuação é introduzida pela conversão e necessário. Por ser necessário, você sempre precisaria fazer isso, também ao converter por mão, por exemplo. Portanto, os redes administrativos são apenas aqueles Lambdas introduzidos pela conversão do CPS que não são realmente necessários (minha segunda definição).

Achei um papel Isso explica assim (ênfase meu):

O codificação de Naîve λ no CPS, no entanto, gera uma inflamação bastante impressionante de lambdas, a maioria dos quais formam redes administrativos que podem ser reduzidos com segurança. Reduções administrativas produzem termos de CPS correspondentes ao que se poderia escrever manualmente. Portanto, tornou-se um desafio eliminar o maior número possível de redes administrativos, no tempo de transformação do CPS.

Ainda assim, quaisquer comentários ou sugestões são bem -vindos, é claro.