# Adventures in Abstract Algebra Part II: Verifying Implementations of Finite Groups in Scala

29 Aug 2015In Part I of this series, we looked at how we can implement a variety of algebraic structures in Scala. We saw that an algebraic structure is defined by the algebraic properties it satisfies. However, in our implementations we simply assumed that programmers instantiating these structures knew what they were doing. We did nothing to check that purported instances really satisfied the relevant properties.

In this part, we’re going to begin to address this shortcoming. We’ll look at how
we can implement *finite groups* and prove that an implementation satisfies the relevant
properties by checking every possible combination of elements. We’ll then see how
proving an implementation is really a finite structure allows us to use the theorems
of abstract algebra to infer further properties of methods defined on that
implementation. We’ll wait until Part III to investigate how we can verify that
implementations of infinite structures satisfy the relevant properties.

If you are unfamiliar with algebraic structures or their corresponding properties, I recommend you go back and read Part I before proceeding.

### Implementing Finite Groups

A **finite group** is a group with a finite set . Addition over integers
is a group, but it’s not a *finite* group since there are infinite integers.

We’re going to take a different approach to implementing finite structure than
our more general approach in Part I.
In particular, we’re going to require that the
relevant set be defined as a `val`

. This allows us to add a couple of utility methods.
First, we can check the **order** of the group (i.e. the size of the set).
And we can also check if the group contains a given element. Here’s the code:

```
trait FiniteAlgStruct[A] extends AlgStruct[A] {
//Contains a finite set
val set: Set[A]
def order = set.size
def contains(x: A) = set.contains(x)
}
```

We mix in `op`

and `is`

from our earlier `AlgStruct`

trait and add the requirement
that one provide a set of `A`

s.

Now it’s a straightforward exercise to create finite versions of the rest of our algebraic structures from Part I:

```
trait FiniteSemiGroup[A] extends SemiGroup[A] with FiniteAlgStruct[A]
trait FiniteMonoid[A] extends Monoid[A] with FiniteSemiGroup[A]
trait FiniteGroup[A] extends Group[A] with FiniteMonoid[A]
```

Now we need a concrete example of a finite group. We’re going to look at multiplication (represented here as ) over the set . Multiplication involves multiplying numbers together, dividing the result by 5, and taking the remainder of the result. For example:

Since divides without a remainder, we get .

As another example:

divides with a remainder of , so .

(multiplication ) over forms a group. This is a little more difficult to see than in our examples from Part I. Let’s examine the relevant properties one by one.

Our binary operation is a function defined for all
members of the set, so we have *totality*.

Is it *closed* over our set (that is, does it map each pair of members of
our set to another member of the set)? In
order to determine that, we have to determine whether for
any . That’s because mod 5 math can only yield an integer
from to . So as long as never equals ,
we know our operation is closed. Another way to frame the same question is to
ask whether multiplying any two members of our set yields either or a
multiple of 5. You can check for yourself and see that there is no such pair
and . Our operation is closed over our set.

Next, we need to see if our operator is *associative*. It turns out that since
multiplication is associative, so is multiplication . This is because
we first multiply two elements and only then perform
the operation on the resulting value.

Do we have an *identity element* ? Yes, just the ordinary identity element
for multiplication, which is . Any of through
equals itself.

Finally, does every element of our set have an *inverse element*? In this case,
there is no simple formula for deriving an inverse. The ordinary multiplicative
inverse doesn’t work since such fractions are not members of
. And recall that we must map each element in the set to an
inverse element that is also a member of the set. In this case, we’re going to
have to define a mapping one element at a time. It turns out that this can be
done.

Keeping in mind that for an inverse , we have

(where in this case )

the following mapping yields an inverse for every in :

We have now shown that over is *total*, *closed*, and
*associative*, has an *identity element*, and contains an *inverse* for every member.
Therefore, we have shown that it is indeed a group. Let’s implement this group
in code:

```
case class MultMod5over1to4 extends FiniteGroup[Int] {
val set: Set[Int] = Set(1, 2, 3, 4)
def op(a: Int, b: Int): Int = (a * b) % 5
val e = 1
def inv(a: Int): Int = a match {
case 1 => 1
case 2 => 3
case 3 => 2
case 4 => 4
}
}
```

### Verifying Finite Structures

So far we have simply trusted that the people implementing our algebraic structures know what they’re doing. We’ve done nothing to programmatically check that the structure in question really has the properties it’s supposed to have. It’s time to remedy that situation. Fortunately, with (reasonably small) finite structures, this is a relatively straightforward exercise.

First, let’s make sure we’re restricting our methods to only operate on members of our set. We can do this by adding the following:

```
def op(a: Int, b: Int): Int = {
require(set.contains(a) && set.contains(b))
//... rest of implementation ...
}
def inv(a: Int): Int = {
require(set.contains(a))
//... rest of implementation ...
}
```

To check that the relevant algebraic properties hold, we’re going to use a
method I’ll call **exhaustion**. This method dictates that for each property,
we check every possible combination of elements to see if the property holds.
Because of combinatorial explosion, we’ll have to restrict this method to
structures with reasonably small sets.

The first thing we need to do is define a test function for each property.
Let’s begin with the properties required to count as a binary operation in
the first place, *totality* and *closure*. Closure is already guaranteed by the
signature of `op`

, which is `(A, A) => A`

. So we only need to check that
`op`

is defined for every pair .

Since *totality* must hold for any finite algebraic structure, our
function testing this property can expect a `FiniteAlgStruct`

and return
a `Boolean`

. We’ll pass every possible pair into `op`

(including when ), placing each
method call in a try-catch. If `op`

is not defined for some pair ,
we’ll catch the exception and return `false`

. Otherwise we’ll return `true`

,
indicating `op`

is defined for that pair.

We’ll use a for-comprehension to collect the results of each tested pair into
a sequence of Booleans. Finally, we’ll use `forall`

on that sequence to
check that every pair returned `true`

. If even one pair returned `false`

,
then we know the operation is not a total function.

Here’s the code:

```
def definedForAllElementsOn[A](as: FiniteAlgStruct[A]): Boolean = {
(for (
x <- as.set;
y <- as.set
) yield {
try {
as.op(x, y)
true
}
catch {
case _: Throwable => false
}
}).forall(result => result)
}
```

We will follow a similar pattern for the other properties we’ll be checking.
For example, in order to check for *associativity*, we’ll check every possible
triple . We need to check that

In code, we’ll use our `is`

method to check for equality and test whether the associativity equation holds
with the following:

```
as.is(as.op(as.op(x, y), z), as.op(x, as.op(y, z)))
```

This isn’t the easiest line to parse, but you can check that it matches
the equation above. Once again using `forall`

to check that every test
returns `true`

, we get the following code for our test function:

```
def associativityOn[A](as: FiniteAlgStruct[A]): Boolean = {
(for (
x <- as.set;
y <- as.set;
z <- as.set
) yield {
as.is(as.op(as.op(x, y), z), as.op(x, as.op(y, z)))
}).forall(result => result)
}
```

For *identity* we need only check each one at a time, so we can
dispense with for-comprehensions. The equation we need to check for is

Two equality checks will suffice, testing both orders of application:

```
def identityOn[A](as: FiniteMonoid[A]): Boolean = {
as.set.forall(x => {
as.is(as.op(x, as.e), x) && as.is(as.op(as.e, x), x)
})
}
```

Notice that `identityOn`

takes a `FiniteMonoid`

instead of a
`FiniteAlgStruct`

. This is because we need to ensure that the
identity element `e`

has been implemented.

The test for *inverse elements* is similar. This time we are checking the
equation

Here we expect a `FiniteGroup`

since we need to ensure that `inv`

has been implemented:

```
def inverseOn[A](as: FiniteGroup[A]): Boolean = {
as.set.forall(x => {
as.is(as.op(x, as.inv(x)), as.e) && as.is(as.op(as.inv(x), x), as.e)
})
}
```

We can now define tests that check whether an alegebraic structure is
of a particular kind by composing the property tests we’ve written so far.
To check that an implementation of `FiniteAlgStruct`

is really an
*algebraic structure*, we need only use `definedForAllElementsOn`

. To
check if an implementation of `FiniteMonoid`

is really a *monoid*, we must
also use `identityOn`

. And to check that an implementation of
`FiniteGroup`

is really a *group*, we add `inverseOn`

. Our tests are as
follow:

```
def isAlgStruct[A](m: FiniteAlgStruct[A]): Boolean = {
definedForAllElementsOn[A](m)
}
def isSemiGroup[A](s: FiniteSemiGroup[A]): Boolean = {
isAlgStruct(s) && associativityOn[A](s)
}
def isMonoid[A](m: FiniteMonoid[A]): Boolean = {
isSemiGroup(m) && identityOn[A](m)
}
def isGroup[A](g: FiniteGroup[A]): Boolean = {
isMonoid(g) && inverseOn[A](g)
}
```

Finally, we can add an assertion to the end of our implementation of over to make sure it’s a group:

```
case class MultMod5over1to4 extends FiniteGroup[Int] {
val set: Set[Int] = Set(1, 2, 3, 4)
def op(a: Int, b: Int): Int = (a * b) % 5
val e = 1
def inv(a: Int): Int = a match {
case 1 => 1
case 2 => 3
case 3 => 2
case 4 => 4
}
assert(isGroup(this))
}
```

### Some Consequences

One interesting result of proving that a data structure is an instance of a
group is that we can infer that the theorems of group theory apply to it.
We’ll consider one example involving the *order* of elements of finite
groups.

In group theory, **exponents** are defined in terms of the group operation:

(n times), where is the group operation.

Given a group , an element , and the identity element ,
if , then the **order** of is . A consequence of
Lagrange’s Theorem is
that if is a finite group, then for
every element , the order of is finite.

We’ll use this theorem to reason about a new method on `FiniteGroup`

.
In particular, we will infer that a recursive function used to calculate
the order of a member of `set`

will always terminate. Here’s the method
in question:

```
def elOrder(x: A): Int = {
require(contains(x))
if (x == e) return 1
def loop(cur: A, count: Int): Int = {
val newCur = op(x, cur)
if (newCur == e) {
count
} else {
loop(newCur, count + 1)
}
}
loop(x, 2)
}
```

Just looking at this function in isolation, it appears there is no way to
determine if it will terminate. After all, there is nothing in the code
that ensures that repeatedly “multiplying” by itself will eventually
yield . However, we have seen that if is a member of a
finite group, and “multiplication” is the group operation, then we can be
certain that multiplying by itself will eventually yield . That’s
just another way of saying that the *order* of is finite.

Based on a theorem of group theory, we infer that this piece of code will always terminate (provided the implementation is free of bugs).

### Conclusion

We have seen how to implement finite algebraic structures and how to verify that
a putative implementation really has the properties it is supposed to by
employing the method of *exhaustion*. We’ve also
considered an interesting result of verifying that an implementation is
the genuine article: the theorems of abstract algebra regarding the relevant
algebraic structure will apply to our implementation as well, allowing us
to infer properties of methods implemented on that structure.

Unfortunately, exhaustion will not work for infinite structures. There is of course no way to test a property on every possible combination of members of an infinite set. In Part III, we will consider a different approach. Instead of deductively proving that an implementation is the genuine article, we’ll reason inductively, relying on ScalaCheck’s generative testing to test a reasonably large subset of the structure in question.