Supongamos que tengo las siguientes funciones: clojureClojure: prueba de la igualdad de la expresión de la función?
(defn a [x] (* x x))
(def b (fn [x] (* x x)))
(def c (eval (read-string "(defn d [x] (* x x))")))
¿Hay una manera de probar la igualdad de la expresión de la función - algún equivalente de
(eqls a b)
vuelve verdadera?
Acepto las respuestas anteriores con respecto a que Clojure no tiene una capacidad integrada para determinar la equivalencia de dos funciones y que se ha demostrado que no se pueden probar programas funcionalmente (también conocido como prueba de caja negra) para determinar igualdad debido al problema de detención (a menos que el conjunto de entrada sea finito y definido).
Me gustaría señalar que es posible determinar algebraicamente la equivalencia de dos funciones, incluso si tienen formas diferentes (código de bytes diferente).
El método para probar la equivalencia algebraicamente fue desarrollado en la década de 1930 por Alonzo Church y se conoce como reducción beta en Lambda Calculus. Este método es ciertamente aplicable a las formas simples en su pregunta (que también arrojaría el mismo código de bytes) y también para formas más complejas que producirían diferentes códigos de bytes.
Depende de lo que quiere decir con "igualdad de expresión de la función".
Estas funciones van a terminar como bytecode, por lo que podría, por ejemplo, volcar el bytecode correspondiente a cada función en un byte [] y luego comparar las dos matrices de bytecode.
Sin embargo, hay muchas maneras diferentes de escribir métodos semánticamente equivalentes, que no tendrían la misma representación en bytecode.
En general, es imposible decir qué código hace sin ejecutarlo. Por lo tanto, es imposible determinar si dos bits de código son equivalentes sin ejecutar ambos, en todas las entradas posibles.
Esto es al menos tan malo, desde un punto de vista computacional, como el problema de detención, y posiblemente peor.
El problema de detención es indecidible tal como está, por lo que la respuesta en este caso es definitivamente no (y no solo para Clojure sino para cada lenguaje de programación).
No puedo agregar a las excelentes respuestas de otros, pero me gustaría ofrecer otro punto de vista que me haya ayudado. Si es, por ejemplo, probando que la función correcta se devuelve desde su propia función, en lugar de comparar el objeto de función que podría salirse con solo devolver la función como 'symbol.
Sé que esto probablemente no es lo que el autor solicitó, pero para casos simples podría hacer.
Imposible: la equivalencia de funciones es indecidible. –
Vaya, disculpe el formato de comentario de recompensa: no me di cuenta de que el formato no funcionaría de la misma manera. –
Hola Omri. Si ve mi respuesta a continuación, verá que hablo de dos funciones que tienen el mismo código de byte JVM que su cuerpo. Eso es efectivamente igualdad intensional. También afirmo que la igualdad intensional implica la igualdad extensional (pero que lo contrario no es cierto). Si el bytecode termina siendo diferente (como podría suceder con algunos de los ejemplos que usted brinda), entonces estamos de vuelta tratando de lograr la igualdad extensional, que como sabemos es indecidible.Espero que las cosas sean un poco más claras: la igualdad intensional (más algunos casos especiales) es probablemente lo mejor que podemos esperar. – kittylyst