Реализация последовательности Фибоначчи с использованием чистого лямбда-исчисления и чисел Чёрча в Racket

Я уже довольно давно борюсь с лямбда-исчислением. Есть много ресурсов, которые объясняют, как уменьшить количество вложенных лямбда-выражений, но меньше, чтобы помочь мне в написании моих собственных лямбда-выражений.

Я пытаюсь написать рекурсивное решение Фибоначчи в Racket, используя чистое лямбда-исчисление (то есть функции с одним аргументом, числа Черча).

Вот определения церковных цифр, которые я использовал:

(define zero  (λ (f) (λ (x) x)))
(define one   (λ (f) (λ (x) (f x))))
(define two   (λ (f) (λ (x) (f (f x)))))
(define three (λ (f) (λ (x) (f (f (f x))))))
(define four  (λ (f) (λ (x) (f (f (f (f x)))))))
(define five  (λ (f) (λ (x) (f (f (f (f (f x))))))))
(define six   (λ (f) (λ (x) (f (f (f (f (f (f x)))))))))
(define seven (λ (f) (λ (x) (f (f (f (f (f (f (f x))))))))))
(define eight (λ (f) (λ (x) (f (f (f (f (f (f (f (f x)))))))))))
(define nine  (λ (f) (λ (x) (f (f (f (f (f (f (f (f (f x))))))))))))

И это те функции с одним аргументом, которые я пытался включить:

(define succ   (λ (n) (λ (f) (λ (x) (f ((n f) x))))))
(define plus   (λ (n) (λ (m) ((m succ) n))))
(define mult   (λ (n) (λ (m) ((m (plus n)) zero))))
(define TRUE   (λ (t) (λ (f) t)))
(define FALSE  (λ (t) (λ (f) f)))
(define COND   (λ (c) (λ (x) (λ (y) ((c x) y)))))
(define iszero (λ (x) (x ((λ (y) FALSE) TRUE))))
(define pair   (λ (m) (λ (n) (λ (b) (((IF b) m) n)))))
(define fst    (λ (p) (p TRUE)))
(define snd    (λ (p) (p FALSE)))
(define pzero  ((pair zero) zero))
(define psucc  (λ (n) ((pair (snd n)) (succ (snd n)))))
(define pred   (λ (n) (λ (f) (λ (x) (((n (λ (g) (λ (h) (h (g f))))) (λ (u) x))(λ (u) u))))))
(define sub    (λ (m) (λ (n) ((n pred) m))))
(define leq    (λ (m) (λ (n) (iszero ((sub m) n))))) ;; less than or equal
(define Y      ((λ (f) (f f)) (λ (z) (λ (f) (f (λ (x) (((z z) f) x))))))) ;; Y combinator

Я начал с написания рекурсивного Фибоначчи в Racket:

(define (fib depth)
  (if (> depth 1)
    (+ (fib (- depth 1)) (fib (- depth 2)))
  depth))

Но в моих многочисленных попытках мне не удавалось написать его с использованием чистого лямбда-исчисления. Даже начать было нелегко.

(define fib
   (λ (x) ((leq x) one)))

Который я звоню (например):

(((fib three) add1) 0)

Это, по крайней мере, работает (правильно возвращает ноль или единицу Church), но добавление чего-либо сверх этого все ломает.

У меня очень мало опыта работы с Racket, а лямбда-исчисление - это настоящая головная боль для человека, который никогда не использовал его до недавнего времени.

Я хотел бы понять, как построить эту функцию и включить рекурсию с комбинатором Y. Я особенно признателен за объяснение вместе с любым кодом. Было бы достаточно заставить его работать с fib(zero) до fib(six), так как я могу беспокоиться о расширении определений Церкви в более позднее время.

РЕДАКТИРОВАТЬ:

Моя iszero функция была в моей реализации скрытым саботажником. Вот правильная версия с обновленными логическими значениями из ответа Алекса:

(define iszero (λ (x) ((x (λ (y) FALSE)) TRUE)))
(define TRUE   (λ (t) (λ (f) (t))))
(define FALSE  (λ (t) (λ (f) (f))))

С этими изменениями и включением преобразователей все работает как надо!


lambda fibonacci racket lambda-calculus
person jsifferman    schedule 28.09.2018    source источник

Ответы (1)


arrow_upward
5
arrow_downward

Формы разветвления и короткое замыкание

Если вы используете нетерпеливый (а не ленивый) язык, такой как Racket, вам нужно быть осторожным при кодировании форм ветвления, таких как ваша функция COND.

Ваши существующие определения логических и условных выражений:

(define TRUE   (λ (t) (λ (f) t)))
(define FALSE  (λ (t) (λ (f) f)))
(define COND   (λ (c) (λ (x) (λ (y) ((c x) y)))))

И они работают в таких простых случаях:

> (((COND TRUE) "yes") "no")
"yes"
> (((COND FALSE) "yes") "no")
"no"

Однако, если «ветвление не выполнено» приведет к ошибке или бесконечному циклу, тогда хорошая форма ветвления приведет к «короткому замыканию», чтобы избежать его запуска. Хорошая форма ветвления должна оценивать только ту ветвь, которую ей нужно принять.

> (if #true "yes" (error "shouldn't get here"))
"yes"
> (if #false (error "shouldn't trigger this either") "no")
"no"

Однако ваш COND оценивает обе ветви просто потому, что приложение-функция Racket оценивает все аргументы:

> (((COND TRUE) "yes") (error "shouldn't get here"))
;shouldn't get here
> (((COND FALSE) (error "shouldn't trigger this either")) "no")
;shouldn't trigger this either

Использование дополнительных лямбда-выражений для реализации короткого замыкания

Способ, которым меня учили обходить это на страстном языке (например, без переключения на #lang lazy), заключался в передаче преобразователей в формы ветвления, например:

(((COND TRUE) (λ () "yes")) (λ () (error "doesn't get here")))

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

(define TRUE (λ (t) (λ (f) (t))))   ; note the extra parens in the body
(define FALSE (λ (t) (λ (f) (f))))  ; same extra parens

Форма COND может быть определена так же, как и раньше, но вам придется использовать ее по-другому. Чтобы перевести (if c t e), где раньше вы писали:

(((COND c) t) e)

Теперь с новым определением логических значений вы должны написать:

(((COND c) (λ () t)) (λ () e))

Я собираюсь сократить (λ () expr) до {expr}, чтобы вместо этого я мог написать это так:

(((COND c) {t}) {e})

Теперь то, что раньше не удавалось с ошибкой, возвращает правильный результат:

> (((COND TRUE) {"yes"}) {(error "shouldn't get here")})
"yes"

Это позволяет вам писать условные выражения, в которых одна из ветвей является «базовым случаем», когда она останавливается, а другая ветвь - «рекурсивным случаем», когда она будет продолжаться.

(Y (λ (fib)
     (λ (x)
       (((COND ((leq x) one))
         {x})
        {... (fib (sub x two)) ...}))))

Без этих дополнительных (λ () ....) и нового определения логических значений это будет бесконечным циклом из-за нетерпеливого (не ленивого) вычисления аргументов Racket.

person Alex Knauth    schedule 28.09.2018
comment
Я очень ценю подробный ответ здесь. Вы объяснили важный нюанс по поводу Racket, о котором я не знал. Однако мне не удалось успешно реализовать ваши предложения. Похоже, что он все еще неправильно использует оценку короткого замыкания. Я редактирую свой вопрос, чтобы отразить изменения и мою последнюю попытку. - person jsifferman; 30.09.2018
comment
Еще одно продолжение здесь: ваши предложения на самом деле были недостающим звеном в моем понимании Racket. Однако то, что не было учтено, было проблемой с моей функцией iszero. После того, как я изменил свои логические значения для запуска функций вместо условий возврата, включил преобразователи в условные переходы и исправил iszero, он работает как шарм. Спасибо! - person jsifferman; 30.09.2018