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

04 Sep 2015In 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:

- All programmers are from Saturn.
- Fido is a programmer.
- 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:

- Every frog we’ve seen so far is green.
- 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)
true
}
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.passed
}
```

`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.is(as.op(x, as.inv(x)), as.e) && as.is(as.op(as.inv(x), x), as.e)
})
```

We can use this property to check `IntAdd`

as follows:

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

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.