Двухслойный комбинатор "Y-style". Это распространено? У этого есть официальное название?

Я изучал, как языки, которые запрещают использование before-def и не имеют изменяемых ячеек (нет set! или же setq) тем не менее может обеспечить рекурсию. Я конечно наткнулся на (знаменитого? Печально известного?) Y комбинатора и друзей, например:

Когда я приступил к реализации семантики "letrec" в этом стиле (то есть, позволил определить локальную переменную так, чтобы она могла быть рекурсивной функцией, где под оболочками она никогда не ссылается на собственное имя), комбинатор Я закончил писать выглядит так:

Y_letrec = λf . (λx.x x) (λs . (λa . (f ((λx.x x) s)) a))

Или, учитывая U комбинатор:

U = λx.x x
Y_letrec = λf . U (λs . (λa . (f (U s)) a))

Прочитайте это как: Y_letrec - это функция, которая принимает функцию, подлежащую рекурсии f,f должна быть функция с одним аргументом, которая принимает s, где s это функция, которая f Можно позвонить, чтобы добиться саморекурсии. f ожидается определить и вернуть "внутреннюю" функцию, которая выполняет "реальную" операцию. Эта внутренняя функция принимает аргумент a (или в общем случае список аргументов, но это не может быть выражено в традиционных обозначениях). Результат вызова Y_letrec является результатом вызоваfи предполагается, что это "внутренняя" функция, готовая к вызову.

Причина, по которой я настроил все так, заключается в том, что я мог использовать форму дерева разбора функции, подлежащей рекурсии, напрямую, без изменений, просто оборачивая дополнительный функциональный слой вокруг нее во время преобразования при обработке letrec. Например, если оригинальный код:

(letrec ((foo (lambda (a) (foo (cdr a))))))

тогда преобразованная форма будет иметь вид:

(define foo (Y_letrec (lambda (foo) (lambda (a) (foo (cdr a))))))

Обратите внимание, что внутреннее тело функции идентично между ними.

Мои вопросы:

  • Моя функция Y_letrec широко используется?
  • У него есть устоявшееся имя?

Примечание. Первая ссылка выше ссылается на аналогичную функцию (на "шаге 5") как "Y-комбинатор аппликативного порядка", хотя у меня возникают проблемы с поиском авторитетного источника для этого наименования.

ОБНОВЛЕНИЕ 28 апреля 2013 г.:

Я понял, что Y_letrec, как определено выше, очень близок, но не идентичен комбинатору Z, как определено в Википедии. Согласно Википедии, Z-комбинатор и Y-комбинатор "по значению" - это одно и то же, и, похоже, это действительно то, что можно чаще называть "Y-комбинатором аппликативного порядка".

Итак, то, что я имею выше, не то же самое, что Y-комбинатор аппликативного порядка, как обычно пишется, но почти наверняка есть смысл, в котором они связаны. Вот как я сделал сравнение:

Начиная с:

Y_letrec = λf . (λx.x x) (λs . (λa . (f ((λx.x x) s)) a))

Примените внутренний U:

Y_letrec = λf . (λx.x x) (λs . (λa . (f (s s)) a))

Примените внешний U:

Y_letrec = λf . (λs . (λa . (f (s s)) a)) (λs . (λa . (f (s s)) a))

Переименуйте, чтобы соответствовать определению комбинатора Z в Википедии:

Y_letrec = λf . (λx . (λv . (f (x x)) v)) (λx . (λv . (f (x x)) v))

Сравните это с Z-комбинатором из Википедии:

Z        = λf . (λx . f (λv . ((x x) v))) (λx . f (λv . ((x x) v)))

Существенная разница в том, где функция f применяется Это имеет значение? Эти две функции эквивалентны, несмотря на эту разницу?

Источник

1 ответ

Решение

Да, это Y-комбинатор аппликативного порядка. Используя U внутри это совершенно нормально, я тоже это сделал (см. Комбинатор с фиксированной точкой в ​​lisp). Независимо от того, используется ли U для сокращения кода, есть имя или нет, я так не думаю. Это просто применение лямбда-термина, и да, это также делает его более понятным для ИМО.

То, что имеет имя, - это eta-преобразование, используемое в вашем коде для задержки оценки в аппликативном порядке, где значения аргументов должны быть известны до функционального применения.

С U, примененным насквозь, и eta-сокращением, выполненным в вашем коде ((λa.(f (s s)) a) ==> f (s s)), он становится привычным Y-комбинатором нормального порядка - то есть таким, который работает при оценке нормального порядка, где значения аргументов не требуются до функционального приложения, что может в конечном итоге не понадобиться им (или некоторым из них) в конце концов:

Y = λf . (λs.f (s s)) (λs.f (s s))

Кстати, задержка может быть применена немного по-другому,

Y_ = λf . (λx.x x) (λs.f (λa.(s s) a))

который также работает в соответствии с правилами оценки аппликативного порядка.

В чем разница? давайте сравним редукционные последовательности. Ваша версия,

Y_ = λf . (λx . (λv . (f (x x)) v)) (λx . (λv . (f (x x)) v))

((Y_ f) a) = 
  = ((λx . (λv . (f (x x)) v)) (λx . (λv . (f (x x)) v))) a
  = (λv . (f (x x)) v) a    { x := (λx . (λv . (f (x x)) v)) }
  = (f (x x)) a
  = | ; here (f (x x)) application must be evaluated, so 
    | ; the value of (x x) is first determined
    | (x x) 
    | = ((λx . (λv . (f (x x)) v)) (λx . (λv . (f (x x)) v))) 
    | = (λv . (f (x x)) v)     { x := (λx . (λv . (f (x x)) v)) }

и здесь f введен Так и здесь, хорошо себя ведет функция f получает свой первый аргумент, и он должен ничего не делать с ним. Так что, может быть, эти два точно эквивалентны.

Но на самом деле, мелочи определений лямбда-выражений не имеют значения, когда дело доходит до реальной реализации, потому что реальный язык реализации будет иметь указатели, и мы просто будем манипулировать ими, чтобы указывать правильно на содержащее тело выражения, а не на его копию. В конце концов, лямбда-исчисление делается карандашом и бумагой, как текстовое копирование и замена. Y комбинатор в лямбда-исчислении только эмулирует рекурсию. Истинная рекурсия - это истинная ссылка на себя; не получая копии, равные себе, через самостоятельное применение (каким бы умным оно ни было).

TL; DR: хотя определяемый язык может быть лишен таких забавных вещей, как присваивание и равенство указателей, язык, на котором мы его определяем, наверняка будет иметь их, потому что они нужны нам для эффективности. По крайней мере, его реализация будет иметь их под капотом.

см. также: комбинатор с фиксированной точкой в ​​lisp, esp. В Схеме, как вы используете лямбда для создания рекурсивной функции?,

Источник
Другие вопросы по тегам