Automatically and deterministicly testing a function for associativity, commutativity etc

Question

Is it possible to construct a higher order function isAssociative that takes another function of two arguments and determines whether that function is associative?

Similar question but for other properties such as commutativity as well.

If this is impossible, is there any way of automating it in any language? If there is an Agda, Coq or Prolog solution I'm interested.

I can envision a brute force solution that checks every possible combination of arguments and never terminates. But "never terminates" is an undesirable property in this context.

Answer 1

The first solution which comes to my mind is using QuickCheck.

quickCheck $ \(x, y, z) -> f x (f y z) == f (f x y) z
quickCheck $ \(x, y) -> f x y == f y x

where f is a function we're testing. It won't prove neither associativity nor commutativity; it's simply the simplest way to write a brute force solution you've been thinking about. QuickCheck's advantage is it's ability to choose tests' parameteres which will hopefully be corner cases for tested code.

An isAssociative you're asking for could be defined as

isAssociative
  :: (Arbitrary t, Show t, Eq t) => (t -> t -> t) -> IO ()
isAssociative f = quickCheck $ \(x, y, z) -> f x (f y z) == f (f x y) z

It's in IO as QuickCheck chooses test cases by random.