Что такое административные переопределения после преобразования CPS?

Question

В контексте преобразования Scheme и CPS у меня возникли небольшие проблемы с определением, какие именно административные переопределения (лямбды):

• все лямбда-выражения, представленные преобразованием CPS
• только лямбда-выражения, представленные преобразованием CPS, но вы бы не написали, если бы выполняли преобразование "вручную" или с помощью более интеллектуального преобразователя CPS

Если возможно, хорошая ссылка будет приветствоваться.

Answer 1

Redex означает "приводимое выражение", которое не является значением. Следовательно, лямбда - это не переопределение, а вызов.
В CPS административный redex - это redex, оператором которого является лямбда-продолжение. Такие переопределения могут быть сокращены немедленно, потому что вы знаете, какую функцию вы вызываете.
Например, ((lambda (u) ...) foo) это административный редекс, но (k foo) нет.

Answer 2

Я думаю, что нашел свой ответ. (Изменить: я принял ответ Димвара, он короче и правильнее.)

Предполагая, что входная программа не является полностью CPS, по крайней мере одна точка возврата процедуры должна быть преобразована в продолжение преобразованием CPS. Так что это продолжение вводится как преобразованием, так и необходимым. Поскольку это необходимо, вы всегда должны будете делать это, в том числе и при ручном преобразовании, например. Поэтому административные переопределения - это только те лямбды, которые были введены преобразованием CPS, которые на самом деле не нужны (мое второе определение).

Я нашел статью, которая объясняет это так (выделено мной):

Наивное λ-кодирование в CPS, однако, генерирует довольно внушительное количество лямбд, большинство из которых образуют административные переопределения, которые можно безопасно сократить. Административные сокращения дают CPS условия, соответствующие тому, что можно было написать вручную. Поэтому стало проблемой устранить как можно больше административных переопределений во время преобразования CPS.

Тем не менее, любые замечания или предложения приветствуются, конечно.