Estoy estudiando cálculo lambda con el libro "Introducción a la programación funcional a través del cálculo lambda" de Greg Michaelson.

Implemento ejemplos en Clojure usando solo un subconjunto del lenguaje. Solo permito:

símbolosfunciones lambda de un argumentoaplicación de funcionesdefinición var por conveniencia.

Hasta ahora tengo esas funciones funcionando:

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

Pero ahora estoy atrapado en funciones recursivas. Más precisamente en la implementación deadd. El primer intento mencionado en el libro es este:

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

((add zero) zero)

Las reglas de cálculo Lambda de la fuerza de reducción para reemplazar la llamada interna aadd-1 con la definición real que contiene la definición misma ... sin fin.

En Clojure, que es un lenguaje de orden de aplicación,add-1 también se evalúa ansiosamente antes de cualquier ejecución de cualquier tipo, y obtuvimos unStackOverflowError.

Después de algunas dudas, el libro propone un artilugio que se utiliza para evitar los reemplazos infinitos del ejemplo anterior.

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

La definición deadd se expande a

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

¡Lo cual está totalmente bien hasta que lo intentemos! Esto es lo que hará Clojure (transparencia referencial):

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

En la ultima linea(fn [second] zero) es una lambda que espera un argumento cuando se aplica. Aquí el argumento es((add (succ zero)) (pred zero)). Clojure es un lenguaje de "orden aplicativo", por lo que el argumento se evalúa antes de la aplicación de la función, incluso en ese caso el argumento no se utilizará en absoluto. Aquí nos repetimos enadd eso se repetirá enadd... hasta que la pila explote. En un lenguaje como Haskell, creo que estaría bien porque es flojo (orden normal), pero estoy usando Clojure.

Después de eso, el libro sigue presentando el sabroso combinador en Y que evita la repetitiva pero llegué a la misma conclusión horrible.

EDITAR

Como sugiere @amalloy, definí el combinador Z:

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

Definíadd2 Me gusta esto :

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

Y lo usé así:

(((YC add2) zero) zero)

Pero sigo teniendo un StackOverflow.

Traté de expandir la función "a mano", pero después de 5 rondas de reducción beta, parece que se expande infinitamente en un bosque de padres.

Entonces, ¿cuál es el truco para hacer Clojure "orden normal" y no "orden aplicativo" sin macros. ¿Es posible? ¿Es incluso la solución a mi pregunta?

Esta pregunta está muy cerca de esta:¿Cómo implementar la iteración del cálculo lambda usando el esquema lisp? . Excepto que el mío es sobre Clojure y no necesariamente sobre Y-Combinator.