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

Question

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

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

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

Answer 1

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

Answer 2

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

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

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

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

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