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.
-
2Do you really need arithmetic functions or are you just curious about comparing functions? In the latter case, take a look at normalization in typed lambda calculi.– lukstafiJun 11, 2013 at 15:51
-
@lukstafi just curious, but I'll take a look on it.– MaiaVictorJun 11, 2013 at 16:17
-
7Your connective "but" is out of place, it should rather be "so". ;-)– lukstafiJun 11, 2013 at 16:49
-
1@lukstafi you're right.– MaiaVictorJun 11, 2013 at 17:22
-
2@IvanCastellanos That sounds great, until you want to prove equivalence of two binary functions and suddenly that 4 billion domain size became 16 quintillion, and your previous 1-minute test suite became a 10000-year test suite.– Daniel WagnerSep 15, 2017 at 3:53
6 Answers
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.
-
8Are you sure he isn't just looking for sbv or quickcheck? With SBV:
prove $ \(x::SInt32) -> 2*x .== x + x
results inQ.E.D.
Jun 11, 2013 at 16:38 -
@ThomasM.DuBuisson Great suggestion! I'll add it to the answer. Jun 11, 2013 at 18:14
-
I was actually looking for a deeper overview of the problem, exactly what Daniel provided. Sep 19, 2017 at 16:47
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
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.
-
1You 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)
? Oct 12, 2016 at 5:12 -
1"(\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.– lukstafiOct 13, 2016 at 13:34
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.
-
2There 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. Oct 24, 2015 at 5:18
-
2@user3237465 The link provided no longer works. This research paper is available here: academia.edu/2718995/Rethinking_supercompilation Feb 24, 2019 at 19:05
-
14 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. Feb 24, 2019 at 21:14
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.
-
But, however
(x \[Function] x + x) == (y \[Function] 2 y)
is somehing it doesn't even try.– user5920214Sep 15, 2017 at 14:43
Proving two functions equal is undecidable in general but one can still prove functional equality in special cases as in your question.
Here's a sample proof in Lean
def foo : (λ x, 2 * x) = (λ x, x + x) :=
begin
apply funext, intro x,
cases x,
{ refl },
{ simp,
dsimp [has_mul.mul, nat.mul],
have zz : ∀ a : nat, 0 + a = a := by simp,
rw zz }
end
One can do the same in other dependently typed language such as Coq, Agda, Idris.
The above is a tactic style proof. The actual definition of foo
(the proof) that gets generated is quite a mouthful to be written by hand:
def foo : (λ (x : ℕ), 2 * x) = λ (x : ℕ), x + x :=
funext
(λ (x : ℕ),
nat.cases_on x (eq.refl (2 * 0))
(λ (a : ℕ),
eq.mpr
(id_locked
((λ (a a_1 : ℕ) (e_1 : a = a_1) (a_2 a_3 : ℕ) (e_2 : a_2 = a_3), congr (congr_arg eq e_1) e_2)
(2 * nat.succ a)
(nat.succ a * 2)
(mul_comm 2 (nat.succ a))
(nat.succ a + nat.succ a)
(nat.succ a + nat.succ a)
(eq.refl (nat.succ a + nat.succ a))))
(id_locked
(eq.mpr
(id_locked
(eq.rec (eq.refl (0 + nat.succ a + nat.succ a = nat.succ a + nat.succ a))
(eq.mpr
(id_locked
(eq.trans
(forall_congr_eq
(λ (a : ℕ),
eq.trans
((λ (a a_1 : ℕ) (e_1 : a = a_1) (a_2 a_3 : ℕ) (e_2 : a_2 = a_3),
congr (congr_arg eq e_1) e_2)
(0 + a)
a
(zero_add a)
a
a
(eq.refl a))
(propext (eq_self_iff_true a))))
(propext (implies_true_iff ℕ))))
trivial
(nat.succ a))))
(eq.refl (nat.succ a + nat.succ a))))))