recursion - programacion - funciones recursivas jquery

¿Cómo implementar una función recursiva en cálculo lambda utilizando un subconjunto de lenguaje Clojure?

Question

Estoy estudiando cálculo lambda con el libro "Una Introducción a la Programación Funcional a través del Cálculo Lambda" por Greg Michaelson.

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

• símbolos
• one-arg lambda funciones
• aplicación de función
• definición de var para mayor comodidad.

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 atascado en funciones recursivas. Más precisamente sobre la implementación de add . 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)

Reglas Lambda de la fuerza de reducción para reemplazar la llamada interna a add-1 con la definición real que contiene la definición misma ... sin fin.

En Clojure, que es un lenguaje de solicitud, add-1 también se elogia ansiosamente antes de cualquier ejecución de cualquier tipo, y obtenemos StackOverflowError .

Después de algunos cambios furtivos, el libro propone un artilugio que se usa 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 de add 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 Clojure hará (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 última línea (fn [second] zero) hay una lambda que espera un argumento cuando se aplica. Aquí el argumento es ((add (succ zero)) (pred zero)) . Clojure es un lenguaje de "orden de aplicación" por lo que el argumento se evalúa antes de la aplicación de la función, incluso si en ese caso el argumento no se utilizará en absoluto. Aquí recurrimos en add que se repetirá en add ... 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 se completó presentando el sabroso Y-combinator que evita la repetición, pero llegué a la misma conclusión espantosa.

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

add2 así:

(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 todavía obtengo 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 parens.

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

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

Answer 1

Para lenguajes estrictos, necesita el combinador Z en lugar del combinador Y. Es la misma idea básica, pero reemplazando (xx) con (fn [v] (xx) v) para que la autorreferencia esté envuelta en una lambda, lo que significa que solo se evalúa si es necesario.

También debe corregir su definición de booleanos para que funcionen en un lenguaje estricto: no puede simplemente pasarle los dos valores que le interesan y seleccionarlos. En su lugar, le pasa los procesos para calcular los dos valores que le interesan y llama a la función apropiada con un argumento ficticio. Es decir, al igual que arreglas el combinador en Y expandiendo eta la llamada recursiva, arreglas los booleanos mediante eta expandiendo las dos ramas del if y eta-reduce el boolean en sí mismo (no estoy 100% seguro de que eta-reduction es el término correcto aquí).

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

Tenga en cuenta que ambas ramas de if están ahora envueltas con (fn [_] ...) , y el if está envuelto con (... b) , donde b es un valor que elegí arbitrariamente para pasar; podría pasar zero lugar, o cualquier cosa en absoluto.

Answer 2

El problema que estoy viendo es que tienes un acoplamiento demasiado fuerte entre tu programa Clojure y tu programa Lambda Calculus

1. estás usando Clojure lambdas para representar LC lambdas
2. está usando variables / definiciones de Clojure para representar las variables / definiciones de LC
3. está utilizando el mecanismo de aplicación de Clojure (evaluador de Clojure) como mecanismo de aplicación de LC

Entonces, en realidad está escribiendo un programa de clojure (no un programa de LC) que está sujeto a los efectos del compilador / evaluador de clojure, lo que significa una evaluación estricta y recursión de dirección de espacio no constante. Miremos a:

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

Como programa de Clojure, en un entorno estrictamente evaluado, cada vez que llamamos add2 , evaluamos

1. (zero? b) como value1
2. (value1 a) como value2
3. (succ a) como value3
4. (f value2) como value4
5. (pred b) como value5
6. (value2 value4) como value6
7. (value6 value5)

Ahora podemos ver que llamar a add2 siempre da como resultado una llamada al mecanismo de recursión f , por supuesto, el programa nunca termina y obtenemos un desbordamiento de la pila.

Tienes pocas opciones

1. Las sugerencias de per @ amalloy, usan thunks para retrasar la evaluación de ciertas expresiones y luego forzarlas (ejecutarlas) cuando estés listo para continuar con el cálculo, aunque no creo que esto te enseñe mucho

2. puede usar el loop / recur o el trampoline de Clojure para las recursiones de espacio constante para implementar su combinador Y o Z Aquí hay un pequeño problema porque solo desea soportar lambdas de parámetro único, y va a ser complicado (tal vez imposible) para hacerlo en un evaluador estricto que no optimiza las llamadas finales

   Hago mucho de este tipo de trabajo en JS porque la mayoría de las máquinas JS sufren el mismo problema; Si está interesado en ver soluciones alternativas de homebrew, consulte: ¿Cómo reemplazo bucles while con una alternativa de programación funcional sin optimización de la cola de llamada?

3. escriba un evaluador real, esto significa que puede desacoplar la representación de su programa Lambda Calculus de los tipos de datos y comportamientos de Clojure y el compilador / evaluador de Clojure; puede elegir cómo funcionan esas cosas porque usted es el que escribe el evaluador

   Nunca he hecho este ejercicio en Clojure, pero lo he hecho un par de veces en JavaScript: la experiencia de aprendizaje es transformadora. La semana pasada, escribí https://repl.it/Kluo, que usa un modelo de evaluación de sustitución de orden normal. El evaluador aquí no es apilable para grandes programas LC, pero se puede ver que la recursión es compatible a través de Y de Curry en la línea 113 - admite la misma profundidad de recursión en el programa LC que la máquina subyacente JS. Aquí hay otro evaluador que usa la memorización y el modelo de entorno más familiar: https://repl.it/DHAT/2 - también hereda el límite de recursión de la máquina JS subyacente

   Hacer la recursión segura de la pila es realmente difícil en JavaScript, como he vinculado anteriormente, y (a veces) se deben realizar considerables transformaciones en el código antes de que pueda ser apilable. Me tomó dos meses de muchas noches de insomnio adaptar esto a un evaluador de call-by-need apto para apilar, seguro y de orden normal: https://repl.it/DIfs/2 - esto es como Haskell o Racket''s #lang lazy

   En cuanto a hacer esto en Clojure, el código de JavaScript podría adaptarse fácilmente, pero no conozco lo suficiente Clojure para mostrarle cómo podría ser un programa de evaluación sensato : en el libro Estructura e interpretación de programas informáticos (capítulo 4) , los autores te muestran cómo escribir un evaluador para Scheme (un Lisp) utilizando Scheme. Por supuesto, esto es 10 veces más complicado que el cálculo Lambda primitivo, por lo que es lógico pensar que si puede escribir un evaluador de esquema, también puede escribir un LC. Esto podría ser más útil para usted porque los ejemplos del código se parecen mucho más a Clojure

un punto de partida

Estudié un poco de Clojure para ti y se me ocurrió esto; es solo el comienzo de un evaluador estricto, pero debería darte una idea de lo poco que se necesita para acercarte a una solución funcional.

Tenga en cuenta que usamos un fn cuando evaluamos un ''lambda pero este detalle no se revela al usuario del programa. Lo mismo es cierto para el env , es decir, el entorno es solo un detalle de implementación y no debería ser una preocupación del usuario.

Para vencer a un caballo muerto, puede ver que tanto el evaluador de sustitución como el evaluador basado en el entorno llegan a las respuestas equivalentes para el mismo programa de aportación (no puedo dejar de insistir en cómo estas opciones dependen de usted ) en el SICP, incluso los autores continúe para cambiar el evaluador y utilizar un modelo simple basado en registros para variables de vinculación y procesos de llamada. Las posibilidades son infinitas porque hemos elegido controlar la evaluación; escribir todo en Clojure (como lo hiciste originalmente) no nos da ese tipo de flexibilidad

;; lambda calculus expression constructors
(defn variable [identifier]
  (list ''variable identifier))

(defn lambda [parameter body]
  (list ''lambda parameter body))

(defn application [proc argument]
  (list ''application proc argument))

;; environment abstraction
(defn empty-env []
  (hash-map))

(defn env-get [env key]
  ;; implement
)

(defn env-set [env key value]
  ;; implement
)

;; meat & potatoes
(defn evaluate [env expr]
  (case (first expr)
    ;; evaluate a variable
    variable (let [[_ identifier] expr]
               (env-get env identifier))

    ;; evaluate a lambda
    lambda (let [[_ parameter body] expr]
             (fn [argument] (evaluate (env-set env parameter argument) body)))

    ;; evaluate an application
    ;; this is strict because the argument is evaluated first before being given to the evaluated proc
    application (let [[_ proc argument] expr]
                  ((evaluate env proc) (evaluate env argument)))

    ;; bad expression given
    (throw (ex-info "invalid expression" {:expr expr}))))


(evaluate (empty-env)
          ;; ((λx.x) y)
          (application (lambda ''x (variable ''x)) (variable ''y))) ;; should be ''y

_{* o podría arrojar un error para el identificador desatado ''y; tu elección}