В контексте преобразования Scheme и CPS я немного затрудняюсь решить, что административные редексы (лямбды) точно такие:
Если возможно, хорошая ссылка будет приветствоваться.
Redex означает «приводимое выражение», то есть выражение, не являющееся значением. Следовательно, лямбда — это не редекс, а вызов.
В CPS административный редекс — это редекс, оператором которого является лямбда-продолжение. Такие редексы можно сразу уменьшить, потому что вы знаете, какую функцию вызываете.
Например, ((lambda (u) ...) foo) — это административный редекс, а (k foo) — нет.
Думаю, я нашел свой ответ. (Редактировать: вместо этого я принял ответ dimvar, он короче и правильнее.)
Предполагая, что входная программа не является полностью CPS, по крайней мере одна точка возврата процедуры должна быть преобразована в продолжение путем преобразования CPS. Таким образом, это продолжение вводится преобразованием и необходимо. Поскольку это необходимо, вам всегда нужно будет делать это, например, при конвертации вручную. Следовательно, административные редексы — это только те лямбда-выражения, введенные преобразованием CPS, которые на самом деле не нужны (мое второе определение).
Я нашел статью, в которой это объясняется следующим образом ( выделение мое):
Однако наивное λ-кодирование в CPS порождает довольно впечатляющее раздувание лямбда-выражений, большинство из которых образуют административные редексы, которые можно безопасно сократить. Административные сокращения дают термины CPS, соответствующие тому, что можно было бы написать от руки. Таким образом, устранение как можно большего количества административных редексов во время преобразования CPS стало проблемой.
Тем не менее, любые замечания или предложения приветствуются, конечно.
