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

Question

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

• http://www.ece.uc.edu/~franco/C511/html/Scheme/ycomb.html
• http://okmij.org/ftp/Computation/fixed-point-combinators.html
• http://www.angelfire.com/tx4/cus/combinator/birds.html
• http://en.wikipedia.org/wiki/Fixed-point_combinator

Когда я пошел к реализации " 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 это функция, которая принимает к -be-recursed function 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», хотя у меня возникли проблемы с поиском авторитетного источника для этого наименования.

UPDATE 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)) 

Rename, чтобы соответствовать определению Википедии комбинатора 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 прикладывается. Это имеет значение? Являются ли эти две функции эквивалентными, несмотря на эту разницу?

Answer 1

Да, это комбинатор Y-аппликативного порядка. Использование U внутри вполне нормально, я тоже это сделал (см. fixed point combinator in lisp). Является ли использование U для сокращения кода именем или нет, я так не думаю. Это просто применение лямбда-термина, и да, это также делает его более ясным ИМО.

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

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

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

BTW затягивания может применяться несколько иначе,

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: хотя определенный язык может быть лишен таких забавных вещей, как присвоение и равенство указателей, язык, в котором мы его определяем, безусловно, будет иметь их, потому что мы нуждаемся в них для повышения эффективности. По крайней мере, его реализация будет иметь их под капотом.

см. Также: fixed point combinator in lisp, esp. In Scheme, how do you use lambda to create a recursive function?.