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