Quali sono esattamente i redexes amministrative dopo la conversione CPS?

Question

Nel contesto dello schema e CPS conversione, sto avendo un po ' difficoltà a decidere cosa redexes (lambda) sono esattamente:

• tutti le espressioni lambda che vengono introdotti dalla conversione CPS
• solo le espressioni lambda che vengono introdotti dalla conversione CPS, ma non avrebbe scritto se avete fatto la conversione "a mano" o attraverso un intelligente CPS-convertitore

Se possibile, un buon riferimento sarebbe il benvenuto.

Answer 1

Redex sta per "espressione riducibile", che è un'espressione che non è un valore. Pertanto, un lambda non è un Redex, ma una chiamata è.
In CPS, un Redex amministrativo è una redex cui operatore è un lambda continuazione. Tali redexes possono essere ridotti immediatamente perché non si sa quale funzione si sta chiamando.
Per esempio, ((lambda (u) ...) foo) è un Redex amministrativo, ma non è (k foo).

Answer 2

Credo di aver trovato la mia risposta. ( Modifica:. La risposta di dimvar ho accettato, invece, è più breve e più corretto)

Supponendo che il programma di input non è completamente CPS, almeno una procedura punto di ritorno dovrà essere convertito in una continuazione dalla conversione CPS. Quindi questa è sia la continuazione introdotta dalla conversione e necessarie. Perché è necessario, si sarebbe sempre bisogno di fare questo, anche quando si convertono a mano per esempio. Pertanto, redexes amministrativi sono solo quelle lambda introdotte dalla conversione CPS che non sono realmente necessari (la mia seconda definizione).

Ho trovato un carta che lo spiega così (sottolineatura mia):

  

Il Naive λ-codificazione nel CPS,   tuttavia, genera un abbastanza impressionante   l'inflazione di lambda, più di cui   formare redexes amministrative che possono   essere ridotta sicura. Amministrativo   riduzioni resa termini CPS   corrispondente a quanto si potrebbe scrivere   a mano. Si è quindi diventata una   sfida a eliminare il maggior numero   redexes amministrative possibili, a   tempo CPS-trasformazione.

Ancora, eventuali osservazioni o suggerimenti benvenuti, naturalmente.