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

by

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.

More Related Contents:

  1. How to compare two functions for extensional equivalence, as in (λx.2*x) == (λx.x+x)?
  2. Is there a Haskell idiom for updating a nested data structure?
  3. Haskell: moving image on horizontal line
  4. What is a monad?
  5. Getting started with Haskell
  6. What does (f .) . g mean in Haskell?
  7. How do you represent a graph in Haskell?
  8. What are paramorphisms?
  9. Is monad bind (>>=) operator closer to function composition (chaining) or function application?
  10. How do functors work in haskell?
  11. Large-scale design in Haskell? [closed]
  12. What are “n+k patterns” and why are they banned from Haskell 2010?
  13. Is Haskell truly pure (is any language that deals with input and output outside the system)?
  14. Applicative functor evaluation is not clear to me
  15. Ordering of parameters to make use of currying
  16. Why is lazy evaluation useful?
  17. Lambda for type expressions in Haskell?
  18. Pattern matching identical values
  19. What is a monad?
  20. How to increment a variable in functional programming?
  21. What part of Hindley-Milner do you not understand?
  22. Why are side-effects modeled as monads in Haskell?
  23. Abusing the algebra of algebraic data types – why does this work?
  24. Iterate over all pair combinations without repetition in Haskell
  25. How to interpret bind/>>= of the function instance?
  26. What’s the status of multicore programming in Haskell?
  27. What does “pure” mean in “pure functional language”?
  28. Functional lenses
  29. ‘some’ and ‘many’ functions from the ‘Alternative’ type class [duplicate]
  30. Sampling sequences of random numbers in Haskell

Leave a Comment