How to check if two functions are the same?

Question

I found a piece of code somewhere on the Internet:

(letrec ([id (lambda (v) v)] [ctx0 (lambda (v) `(k ,v))] ..... ..... (if (memq ctx (list ctx0 id)) <---- condition always return false ..... 

where ctx is also a function:

However, I could never force test-statement to return true.

Then I have the following test:

 (define ctx0 (lambda (v) `(k ,v))) (define ctx1 (lambda (v) `(k ,v))) (eq? ctx0 ctx1) => #f (eqv? ctx0 ctx1) => #f (equal? ctx0 ctx1) => #f 

Which makes me suspect that the two functions are always different, because they have different memory locations.

But if the functions can be compared with other functions, how can I check if the two functions are the same? and what if they have a different variable name? eg:

(lambda (x) (+ x 1)) and (lambda (y) (+ y 1))

PS I use DrRacket to check the code.

Answer 1

You can not. Functions are considered as opaque values: they are compared only by identity, and nothing more. This is by design.

---

But why? Can't languages ​​implement meaningful ways to compare functions that can sometimes be useful? Well, not really, but sometimes it's hard to see why without the details. Let's look at your example from your question - these two functions seem equivalent:

 (define ctx0 (lambda (v) '(k ,v))) (define ctx1 (lambda (v) '(k ,v))) 

And indeed, they are. But what could a comparison of these functions do for equality? In the end, we could just as easily implement another function:

 (define ctx2 (lambda (w) '(k ,w))) 

This function, in every sense and purpose, is identical to the previous two, but it would not pass the test of naive equality!

To decide if two values ​​are equivalent, we need to define some algorithm that determines equality. Given the above examples, such an algorithm seems obvious: two functions should be considered equal if (and only if) they are α -equivalent . With this in mind, we can now meaningfully check if the two functions are equal!

... right?

 (define ctx3 (lambda (v) (list 'kv))) 

Oh. This function does the same, but is not implemented exactly the same, so it does not pass the equality test. Of course we can fix it. The quasiquotation and use of the list constructor are almost the same, so we can define them as equivalent in most cases.

 (define ctx4 (lambda (v) (reverse (list v 'k)))) 

Gah! It is also operationally equivalent, but still not consistent with our equivalence algorithm. How can we do this work?

---

Turns out we can't, really. Functions are units of abstraction - by nature we don’t need to know how they are implemented, just what they do. This means that functional equality can really only be correctly defined in terms of operational equivalence; that is, the implementation does not matter, only the behavior matters.

This is an insoluble problem in any non-trivial language. It is impossible to determine if any two functions are functionally equivalent, because if we could, we could solve the stop problem .

Programming languages ​​can theoretically provide a best-effort algorithm for determining equivalence of functions, possibly using α -equivalency or some other kind of metric. Unfortunately, this would really be useless - depending on the implementation of the function, and not on its behavior, defining the semantics of a program violates the fundamental law of functional abstraction, and therefore any program that depends on such a system will be antipattern.

Equality of functions is a very tempting problem that needs to be solved when simple cases seem so simple, but most languages ​​use the right approach and do not even try. This does not mean that it is a futile idea: if it were possible, it would be incredibly useful! But since it is not, you have to use another tool to work.

Answer 2

Semantically, the two functions f and g are equal if they are consistent for each input, i.e. if for all x we have (= (fx) (gx)) . Of course, there is no way to verify this for any possible value of x .

If all you want to do is reasonably confident that (lambda (x) (+ x 1)) and (lambda (y) (+ y 1)) same, then you can try to argue that

 (map (lambda (x) (+ x 1)) [(-5) (-4) (-3) (-2) (-1) 0 1 2 3 4 5]) 

and

 (map (lambda (y) (+ y 1)) [(-5) (-4) (-3) (-2) (-1) 0 1 2 3 4 5]) 

same in your unit tests.