Clojure - тест на равенство выражений функций?

Question

Предположим, у меня есть следующие функции clojure:

(defn a [x] (* x x))

(def b (fn [x] (* x x)))

(def c (eval (read-string "(defn d [x] (* x x))")))

Есть ли способ проверить на равенство выражения функции - некоторый эквивалент

(eqls a b)

возвращает истину?

Answer 1

Это зависит от того, что именно вы подразумеваете под «равенством выражения функции».

Эти функции будут заканчиваться как байт-код, поэтому я мог бы, например, вывести байт-код, соответствующий каждой функции, в байт [], а затем сравнить два массива байт-кода.

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

В общем, невозможно сказать, что делает кусок кода без его запуска. Таким образом, невозможно сказать, эквивалентны ли два бита кода, не запустив их оба на всех возможных входах.

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

Проблема остановки неразрешима, так что общий ответ здесь определенно - нет (и не только для Clojure, но и для каждого языка программирования).

Answer 2

Я согласен с приведенными выше ответами в отношении того, что Clojure не имеет встроенной способности определять эквивалентность двух функций и что было доказано, что вы не можете тестировать программы функционально (также известный как тестирование черного ящика) для определения равенства из-за проблемы остановки (если входной набор конечен и определен).

Я хотел бы отметить, что алгебраически можно определить эквивалентность двух функций, даже если они имеют разные формы (разные байтовые коды).

Метод доказательства эквивалентности алгебраически был разработан в 1930-х годах Алонзо Черчем и известен как бета-сокращение в лямбда-исчислении. Этот метод, безусловно, применим к простым формам в вашем вопросе (которые также приводят к одному и тому же байтовому коду), а также к более сложным формам, которые дают разные байтовые коды.

Answer 3

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

Я знаю, что, вероятно, это не то, о чем просил автор, но в простых случаях это может быть сделано.