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

I guess Haskell isn't very suited for such things. Usually you do totally opposite to check. You declare that your object have some properties and thus could be used in some special way (see Data.Foldable). Sometimes you might want to promote your system:

import Control.Parallel
import Data.Monoid

pmconcat :: Monoid a => [a] -> a
pmconcat [x] = x
pmconcat xs = pmconcat (pairs xs) where
    pairs [] = []
    pairs [x] = [x]
    pairs (x0 : x1 : xs') = y `par` (y : ys) where
        y = x0 `mappend` x1
        ys = pairs xs'

data SomeType

associativeSlowFold = undefined :: SomeType -> SomeType -> SomeType

data SlowFold = SlowFoldId
              | SlowFold { getSlowFold :: SomeType }

instance Monoid SlowFold where
    mempty = SlowFoldId
    SlowFoldId `mappend` x = x
    x `mappend` SlowFoldId = x
    x0 `mappend` x1 = SlowFold y where
        y = (getSlowFold x0) `associativeSlowFold` (getSlowFold x1)
    mconcat = pmconcat

If you really want proof systems you might want to look also at those proof assistants you mentioned. Prolog - is logical language and I don't think that it also very suitable for that. But it might be used to write some simple assistant. I.e. to apply associativity rule and see that at lower levels it's impossible to derive equality.