Комбинатор с фиксированной точкой в ​​lisp

;; compute the max of a list of integers

(define Y
  (lambda (w)
    ((lambda (f)
       (f f))
     (lambda (f)
       (w (lambda (x)
            ((f f) x)))))))

((Y
  (lambda (max)
    (lambda (l)
      (cond ((null? l) -1)
            ((> (car l) (max (cdr l))) (car l))
            (else (max (cdr l)))))))
 '(1 2 3 4 5))

Я хочу понять эту конструкцию. Может ли кто-нибудь дать ясное и простое объяснение этого кода?

Например, предположим, что я забыл формулу Y. Как я могу ее запомнить и воспроизвести спустя долгое время после работы с ней?

2 ответа

Решение

Вот некоторые связанные ответы (мной):

В основном, с Y определяется как λr.(λh.h h) (λg.r (λx.(g g) x)), приложение Y r уменьшает как

Y r
(λw.(λh.h h) (λg.w (λx.(g g) x))) r
(λh.h h) (λg.r (λx.(g g) x))
h h
    ;where
        h = (λg.r (λx.(g g) x))       <----\
                                           |
(λg.r (λx.(g g) x)) h                      |
r (λx.(g g) x)             <-------------- | ----------\
    ;where                                 |           |
        g = h                         -----/           |
        ;so that                                       |
        (g g) = (h h) = r (λx.(g g) x)           ------/

Так r должен ожидать два аргумента - первый представляет рекурсивную функцию для вызова, а второй - фактический аргумент:

        r = λf (λx. ....x.....(f y)...... )

чтобы (Y r) x уменьшает как

(r (λx.(g g) x)) x
(r f) x
    ;where
        f   = (λx.(g g) x) 
        f y = (λx.(g g) x) y = (g g) y = (r f) y  ; f is "fixed point" of r

Определение f = (λx.(g g) x) значит, когда f y называется, (g g) y будет называться, в какой момент g будет применяться самостоятельно, r "вытащил" изнутри g и результат (r f) называется с y аргумент. Т.е. любой звонок (f y) в теле лямбда-выражения в результате (r f) приложение, переводится обратно в (r f) y т.е. вызов того же тела с новым аргументом y,

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

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

Когда нет ссылок, как в чистом лямбда-исчислении, и параметры получают текстовые копии аргументов - то есть сокращение выполняется путем текстового переписывания - это все еще работает, потому чтоодни и те же копии реплицируются и передаются, передаваясь в качестве аргумента для себя, поэтому они доступны на следующей итерации, если это будет необходимо.

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

(let ((fact #f)) 
  (set! fact 
        (lambda (n) (if (< 2 n) 1 
                               (* n (fact (- n 1)))))) 
  fact)

На самом деле в вашем ответе дается определение Y-комбинатора аппликативного порядка. При нормальном порядке eta-Reduction может быть применено, не вызывая бесконечного цикла, чтобы получить Ynorm = (λw.(λh.h h) (λg.w (g g))) который канонически записан как

Ynorm = (λf.(λx.f (x x)) (λx.f (x x)))

в самом деле

Ynorm g
= (λx.g (x x)) (λx.g (x x))
= g ((λx.g (x x)) (λx.g (x x)))

Лучшее объяснение, которое я нашел до сих пор, это в книге "Маленький интриган", глава 9. Вся глава шаг за шагом объясняет, как работает Y-Combinator, и как вывести комбинатор, начиная с произвольной рекурсивной процедуры.,

Другие вопросы по тегам