чаю лямбда-исчисление с книгой Грега Майклсона «Введение в функциональное программирование через лямбда-исчисление».

Я реализую примеры в Clojure, используя только подмножество языка. Я разрешаю только:

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

Пока у меня работают эти функции:

(def identity (fn [x] x))
(def self-application (fn [s] (s s)))

(def select-first (fn [first] (fn [second] first)))
(def select-second (fn [first] (fn [second] second)))
(def make-pair (fn [first] (fn [second] (fn [func] ((func first) second)))))    ;; def make-pair =  λfirst.λsecond.λfunc.((func first) second)

(def cond make-pair)
(def True select-first)
(def False select-second)

(def zero identity)
(def succ (fn [n-1] (fn [s] ((s False) n-1))))
(def one (succ zero))
(def zero? (fn [n] (n select-first)))
(def pred (fn [n] (((zero? n) zero) (n select-second))))

Но сейчас я застрял на рекурсивных функциях. Точнее на реализациюadd, Первая попытка, упомянутая в книге, такова:

(def add-1
  (fn [a]
    (fn [b]
      (((cond a) ((add-1 (succ a)) (pred b))) (zero? b)))))

((add zero) zero)

Правила лямбда-исчисления редукции силы для замены внутреннего вызоваadd-1 с фактическим определением, которое содержит само определение ... бесконечно.

В Clojure, который является языком заказа приложений,add-1 также с нетерпением оценивается перед любым исполнением любого рода, и мы получилиStackOverflowError.

После некоторых неуклюжих, книга предлагает хитрое изобретение, которое используется, чтобы избежать бесконечных замен предыдущего примера.

(def add2 (fn [f]
            (fn [a]
              (fn [b]
                (((zero? b) a) (((f f) (succ a)) (pred b)))))))
(def add (add2 add2))

Определениеadd расширяется до

(def add (fn [a] 
           (fn [b]
             (((zero? b) a) (((add2 add2) (succ a)) (pred b)))))) 

Что совершенно нормально, пока мы не попробуем! Вот что будет делать Clojure (ссылочная прозрачность):

((add zero) zero)
;; ~=>
(((zero? zero) zero) (((add2 add2) (succ zero)) (pred zero)))
;; ~=>
((select-first zero) (((add2 add2) (succ zero)) (pred zero)))
;; ~=>
((fn [second] zero) ((add (succ zero)) (pred zero)))

На последней строчке(fn [second] zero) лямбда, которая ожидает один аргумент при применении. Здесь аргумент((add (succ zero)) (pred zero)), Clojure является языком «аппликативного порядка», поэтому аргумент оценивается перед применением функции, даже если в этом случае аргумент вообще не будет использоваться. Здесь мы повторяем вadd это повторится вadd... пока стек не взорвется. На языке, подобном Хаскеллу, я думаю, что это было бы хорошо, потому что это ленивый (нормальный порядок), но я использую Clojure.

После этого в книге подробно описывается вкусный Y-комбинатор, который избегает шаблонов, но я пришел к такому же ужасному выводу.

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

Как подсказывает @amalloy, я определил комбинатор Z:

(def YC (fn [f] ((fn [x] (f (fn [z] ((x x) z)))) (fn [x] (f (fn [z] ((x x) z)))))))

Я определилadd2 нравится :

(def add2 (fn [f]
            (fn [a]
              (fn [b]
                (((zero? b) a) ((f (succ a)) (pred b)))))))

И я использовал это так:

(((YC add2) zero) zero)

Но я все еще получаю StackOverflow.

Я пытался расширить функцию «вручную», но после 5 раундов сокращения бета-версии, похоже, что она бесконечно расширяется в лесу паренов.

Так в чем же смысл сделать Clojure «нормальным порядком», а не «аппликативным порядком» без макросов. Это вообще возможно? Это даже решение моего вопроса?

Этот вопрос очень близок к этому:Как реализовать итерацию лямбда-исчисления по схеме lisp? , За исключением того, что моя речь идет о Clojure и не обязательно о Y-Combinator.