Automatic and deterministic function testing for associativity, commutativity, etc.

Question

Is it possible to build a higher-order function isAssociative , which takes another function of two arguments and determines whether this function is associative?

A similar question, but also for other properties, such as commutativity.

If this is not possible, is there a way to automate it in any language? If there is an Agda, Coq or Prolog solution, I wonder.

I can imagine a brute force solution that tests all possible combinations of arguments and never ends. But “never ends” is an undesirable property in this context.

Answer 1

I think Haskell is not very suitable for such things. Usually you are completely opposed to checking. You declare that your object has some properties and, therefore, can be used in some special way (see Data.Foldable ). Sometimes you can 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 need evidence systems, you can also look at the evidence assistants you talked about. The prologue is a logical language, and I do not think that it is also very suitable for this. But it can be used to write a simple helper. That is, apply the rule of associativity and see that at lower levels it is impossible to obtain equality.

Answer 2

The first solution that comes to my mind is QuickCheck .

 quickCheck $ \(x, y, z) -> fx (fyz) == f (fxy) z quickCheck $ \(x, y) -> fxy == fyx 

where f is the function we are testing. This will prove neither associativity nor commutativity; it's just the easiest way to write the brute force solution you were thinking about. The advantage of QuickCheck is its ability to select test parameters, which we hope will be angular for the tested code.

An isAssociative that you request can be defined as

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

In IO , because QuickCheck picks random random cases.