How to compare two functions for equivalence, as in (λx.2*x) == (λx.x+x)?

Question

Is there a way to compare two functions for equality? For example, (λx.2*x) == (λx.x+x) should return true, because those are obviously equivalent.

Solution 1

It's pretty well-known that general function equality is undecidable in general, so you'll have to pick a subset of the problem that you're interested in. You might consider some of these partial solutions:

• Presburger arithmetic is a decidable fragment of first-order logic + arithmetic.
• The universe package offers function equality tests for total functions with finite domain.
• You can check that your functions are equal on a whole bunch of inputs and treat that as evidence for equality on the untested inputs; check out QuickCheck.
• SMT solvers make a best effort, sometimes responding "don't know" instead of "equal" or "not equal". There are several bindings to SMT solvers on Hackage; I don't have enough experience to suggest a best one, but Thomas M. DuBuisson suggests sbv.
• There's a fun line of research on deciding function equality and other things on compact functions; the basics of this research is described in the blog post Seemingly impossible functional programs. (Note that compactness is a very strong and very subtle condition! It's not one that most Haskell functions satisfy.)
• If you know your functions are linear, you can find a basis for the source space; then every function has a unique matrix representation.
• You could attempt to define your own expression language, prove that equivalence is decidable for this language, and then embed that language in Haskell. This is the most flexible but also the most difficult way to make progress.

Solution 2

This is undecidable in general, but for a suitable subset, you can indeed do it today effectively using SMT solvers:

$ ghci
GHCi, version 8.0.1: http://www.haskell.org/ghc/  :? for help
Prelude> :m Data.SBV
Prelude Data.SBV> (\x ->  2 * x) === (\x -> x + x :: SInteger)
Q.E.D.
Prelude Data.SBV> (\x ->  2 * x) === (\x -> 1 + x + x :: SInteger)
Falsifiable. Counter-example:
  s0 = 0 :: Integer

For details, see: https://hackage.haskell.org/package/sbv

Solution 3

In addition to practical examples given in the other answer, let us pick the subset of functions expressible in typed lambda calculus; we can also allow product and sum types. Although checking whether two functions are equal can be as simple as applying them to a variable and comparing results, we cannot build the equality function within the programming language itself.

ETA: λProlog is a logic programming language for manipulating (typed lambda calculus) functions.

Solution 4

2 years have passed, but I want to add a little remark to this question. Originally, I asked if there is any way to tell if (λx.2*x) is equal to (λx.x+x). Addition and multiplication on the λ-calculus can be defined as:

add = (a b c -> (a b (a b c)))
mul = (a b c -> (a (b c)))

Now, if you normalize the following terms:

add_x_x = (λx . (add x x))
mul_x_2 = (mul (λf x . (f (f x)))

You get:

result = (a b c -> (a b (a b c)))

For both programs. Since their normal forms are equal, both programs are obviously equal. While this doesn't work in general, it does work for many terms in practice. (λx.(mul 2 (mul 3 x)) and (λx.(mul 6 x)) both have the same normal forms, for example.

Solution 5

In a language with symbolic computation like Mathematica:

Or C# with a computer algebra library:

MathObject f(MathObject x) => x + x;
MathObject g(MathObject x) => 2 * x;

{
    var x = new Symbol("x");

    Console.WriteLine(f(x) == g(x));
}

The above displays 'True' at the console.

View more solutions

Comments

[Thomas M. DuBuisson]

Are you sure he isn't just looking for sbv or quickcheck? With SBV: prove $ \(x::SInt32) -> 2*x .== x + x results in Q.E.D.

[Daniel Wagner]

@ThomasM.DuBuisson Great suggestion! I'll add it to the answer.

[effectfully]

There is a technique called "supercompilation" (I recommend this paper). I guess a mature supercompiler can unify your functions, even if they are defined by recursion and pattern-matching.

[Daniel Wagner]

You say, "checking whether two functions are equal can be as simple as applying them to a variable and comparing results". I'm having a hard time believing this, though; as a simple example, would this really validate the equality (\x -> 2*x) == (\x -> x*2)?

[lukstafi]

"(\x -> 2*x) == (\x -> x*2)" is not necessarily true, it depends on how you interpret "*" and "2". For example, you could define "==" on ground terms to be identity modulo some term rewriting system.

[Admin]

But, however (x \[Function] x + x) == (y \[Function] 2 y) is somehing it doesn't even try.

[MaiaVictor]

I was actually looking for a deeper overview of the problem, exactly what Daniel provided.

[Stephane Rolland]

@user3237465 The link provided no longer works. This research paper is available here: academia.edu/2718995/Rethinking_supercompilation

[MaiaVictor]

4 years have passed, and I want to add yet another remark: while this works in this case, such a thing is mostly the exception. Functions can be defined in wildly different ways and still be equivalent, so a way to manipulate equalities manually is useful.