Adventures in Abstract Algebra Part III: Using ScalaCheck to Verify Infinite Algebraic Structures

In Part I of this series, we looked at the basics of abstract algebra and provided some initial implementations of algebraic structures. In Part II, we turned our attention to finite groups and used a method I called exhaustion to prove that an implementation really satisfied the algebraic properties it was supposed to. In this part, we’re going to look at a method for verifying implementations of infinite structures.

It turns out that implementations of large structures are the closest we can get to infinite ones. That’s because it would require infinite space to represent an infinite structure. However, if we have reason to think that very large members of our set have no special properties, then sampling from a set of smaller members can be enough to increase our confidence that the infinite version also satisfies the properties we’re testing.

If you’ll recall, our implementation of addition over the integers in Part I was not technically an implementation of an infinite group. That’s because we relied on the Scala type Int which is actually bounded. However, as far as the method of exhaustion is concerned, an implementation using Int might as well be infinite. That’s because checking every 2-combination of 4 billion elements would take a very long time. In this post, we’re going to explore an alternative to exhaustion for cases where it’s impractical.

What’s nice about exhaustion is that it provides a definitive proof that a property holds. Having checked every possibility, we can deduce the existence of the property. For infinite (or very large) groups, we’re going to forgo deductive reasoning and reason inductively instead. In particular, we’re going to check a subset of possible combinations. If the property fails to hold for even one combination, then we can definitively say that it fails to hold for the structure in question. If it turns out to hold for every combination considered, then we can infer that it is somehow probable that the property holds for the structure.

Before considering how to achieve this, we’re going to briefly dwell on the difference between inductive and deductive reasoning to make this distinction clearer.

Inductive Reasoning

A deductive argument is an argument whose premises necessarily entail its conclusion. That means that if the premises of the argument are true, it is impossible for its conclusion to be false. Here’s an example:

  1. All programmers are from Saturn.
  2. Fido is a programmer.
  3. Therefore, Fido is from Saturn.

This is a deductively valid argument. If and are true, then the conclusion must be true. Of course the first premise is actually false (and probably the second premise as well), so the argument is not sound. Successful mathematical proofs are deductively valid arguments built on true premises. If a proof with a theorem as its conclusion meets these requirements, then we can be certain the theorem is true.

Inductive arguments, on the other hand, do not get us certainty. They only justify a certain amount of confidence in their conclusions. We are not talking about mathematical induction (the kind of argument that begins with a base case and a step from to ), but rather arguments like the following:

  1. Every frog we’ve seen so far is green.
  2. Therefore, all frogs are green.

If is true, it is still possible that the conclusion is false. It might be that there’s a blue frog right around the corner, and we haven’t happened to have encountered it yet. Empirical reasoning is normally inductive in character. We draw generalizations based on patterns of experience.

There is an asymmetry between proof and disproof in inductive reasoning involving generalizations. No matter how many green frogs we see, we can never rule out the possibility that the next one will be blue. So at best, we can continue to increase our confidence in the proposition that “all frogs are green”. On the other hand, it only takes a single counterexample to disprove the proposition definitively. A single blue frog suffices to render “all frogs are green” false.

We can think of our algebraic properties as generalizations of this kind. To say that a structure satisfies associativity is to say that “for every triple , ”. If our set is infinite, then no matter how many distinct triples we test from that satisfy the property, it’s always possible that the next triple will fail to satisfy it. However, even one counterexample is enough to prove that the property fails to hold for .

This is one reason why mathematicians provide clever (deductive) proofs that properties hold for infinite structures instead of testing a bunch of combinations by hand. But since automating such a clever proof-generator is a difficult problem, to say the least, we’re going to stick to an inductive (and much more brute) approach.

For each property, we’re going to test a limited number of combinations. If our test ever fails, we’ll know that the structure fails to satisfy the property. If our test succeeds in every case, then we’ll have increased our confidence that the property really holds. And maybe that will encourage us that it would be worthwhile to look for a deductive proof.

ScalaCheck Tests

In order to implement this kind of test, we’re going to use ScalaCheck , a generative testing framework that suits our use case well. With ScalaCheck, you define some properties you want to test and specify a generator that automatically generates test cases. ScalaCheck is based on QuickCheck, which can be surprisingly effective at catching obscure bugs quickly, as illustrated in this entertaining talk by QuickCheck creator John Hughes.

Catching a bug corresponds to proving that a property fails to hold. What this means in practice is that we can use ScalaCheck to quickly find falsifying counterexamples to structures that purport (in code) to have certain properties. I’ll illustrate with some examples.

Let’s start with checking whether an operation is defined for all pairs in a set. We’re going to modify definedForAllElementsOn from Part II to create a ScalaCheck property. The new version will take an AlgStruct (which, as we discussed in Part I , just requires a binary operation) and a ScalaCheck generator. It will return a ScalaCheck property:

  def definedForAllElementsOn[A](as: AlgStruct[A], genFor: Gen[List[A]]) = forAll(genFor)(l => {
    val x = l(0)
    val y = l(1)
    try {
      as.op(x, y)
    catch {
      case _: Throwable => false

This creates a ScalaCheck forAll property with a generator passed in. We also pass in a function that takes a List provided by the generator, grabs the first two elements from the list and tries the op on them.

We can now create a generator for creating two-element lists:

  def listOfN[A](n: Int, gen: Gen[A]): Gen[List[A]] = Gen.listOfN(n, gen).suchThat(_.size == n)

  def listOf2[A](gen: Gen[A]): Gen[List[A]] = listOfN[A](2, gen)

listOf2 takes a generator that generates single instances of type A and returns a generator that creates lists of length 2.

Finally, we’ll create a ScalaCheck parameter that sets how many tests are to be generated for a property:

  val tests10000 = new Parameters.Default {
    override val minSuccessfulTests = 10000

We can use our property, list generator, and parameter to define an isAlgStruct test:

  def isAlgStruct[A](m: AlgStruct[A], gen: Gen[A]): Boolean = {
    val result = Test.check(tests10000, definedForAllElementsOn[A](m, listOf2[A](gen)))

result is the result of running Test.check with our minSuccessfulTests parameter and our property. We return res.passed which records whether the check passed.

In order to use this function, we need an implementation of an AlgStruct and a generator of items of type A. As an example, consider division over Ints:

    case class IntDivide extends AlgStruct[Int] {
      def op(a: Int, b: Int): Int = a / b

It is worth mentioning that op here is not actually ordinary division. That’s because in Scala, dividing an Int by an Int returns the floor of the result. So technically our operation is not division but “division and then floor”. If we used simple division, the signature of op would have to be (Int, Int) => Double, which would violate closure.

In order to test whether “division and then floor” is defined for all Ints, we need to first come up with an Int generator:

  val intGen = Gen.choose(-1000, 1000)

This uses the built-in ScalaCheck choose generator. In this case, we’re telling it to choose an Int from -1000 to 1000, which will suffice for our purposes. We are now ready to check if IntDivide is really an algebraic structure:

  isAlgStruct[Int](IntDivide(), intGen)

IntDivide() spins up a new instance of the case class IntDivide, which is then used in the test. Sure enough, this test returns false. Dividing by 0 was the culprit. “Division and then floor” is not defined for any pair of the form .

Our test will pass for addition over Ints:

  case class IntAdd extends AlgStruct[Int] {
    def op(a: Int, b: Int): Int = a + b

  isAlgStruct[Int](IntAdd(), intGen)

We get true, as expected. However, there is a problem. Scala Ints wrap around when you add large enough numbers. So just testing up to 1000 is not very convincing. Let’s create a new generator that will better capture this kind of edge case.

What we want is a generator that both samples from the Ints near 0 and also samples from the Ints near Int.MaxValue and Int.MinValue. We’ll use Gen.frequency, which allows us to set how likely the generator is to choose from one of a list of possible generators on each pass. I’m choosing to bias toward the Ints around 0 with lower odds that a very large or very small Int will be chosen:

  val intGen = Gen.frequency(
    (10, Gen.choose(-1000, 1000)),
    (1, Gen.choose(Int.MaxValue - 1000, Int.MaxValue)),
    (1, Gen.choose(Int.MinValue, Int.MinValue + 1000))

We can try isAlgStruct again with this new generator. We find that addition is also defined around the fringes (this is a function of the fact that the Ints wrap).

From here, we need to implement ScalaCheck properties for all the other algebraic properties we’re interested in. And once we’ve done this, we can write code to check whether an implementation of a particular structure really satisfies all the relevant properties. Of course, we must keep in mind that “verify” here means “inductively confirm” and not “prove”.

We’ll try implementing one more, an inductive version of inverseOn from Part II. I’ve chosen this property because it isn’t clear that we’ll be able to find an inverse for every Scala Int. To see why, recall that in order to satisfy this property, we must be able to find an inverse for every element in our structure satisfying the following equation:

, where is the identity element.

Now Scala Ints range from -2,147,483,648 to 2,147,483,647. The identity element for addition is , so for each between these two extremes we need to find some that we can add to to get . For ordinary addition over integers, we simply take the negative of the integer in question. For any integer , . Does this work for the Ints?

It would seem to work for Int.MaxValue, since its negative -2,147,483,647 is available. However, what is the inverse of Int.MinValue? After all, it seems like its negative is 2,147,483,648, but the Ints don’t go that high. Let’s implement an inductive version of inverseOn and see if we can prove that Int.MinValue has no inverse. Here’s the code:

  def inverseOn[A](as: Group[A], genFor: Gen[A]) = forAll(genFor)(x => {, as.inv(x)), as.e) &&, x), as.e)

We can use this property to check IntAdd as follows:

  val result = Test.check(tests10000, inverseOn[A](g, gen))

Sure enough, no matter how many times we run this test, we never find a counterexample. It turns out Int.MinValue has an inverse after all. Moreover, you get its inverse the same way you get the inverse of any other Int; simply subtract it from 0. It turns out that for Scala Ints, 0 - Int.MinValue is equal to Int.MinValue. Adding Int.MinValue to itself yields 0. Thus, Int.MinValue is its own additive inverse.

If you’re interested in how you might implement other properties, you can take a look at my GitHub project algebraic structures in Scala. Or maybe you’d rather try your hand at it instead.