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

29 Aug 2015

In 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 $A$ . 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 As.

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 $mod$ $5$ (represented here as $*$ ) over the set $\{1, 2, 3, 4\}$ . Multiplication $mod$ $5$ involves multiplying numbers together, dividing the result by 5, and taking the remainder of the result. For example:

$3 * 5 = 15$ $mod$ $5$

Since $5$ divides $15$ without a remainder, we get $0$ .

As another example:

$2 * 3 = 6$ $mod$ $5$

$5$ divides $6$ with a remainder of $1$ , so $2 * 3 = 1$ .

$*$ (multiplication $mod$ $5$ ) over $\{1, 2, 3, 4\}$ 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 $a * b = 0$ for any $a, b \in \{1, 2, 3, 4\}$ . That’s because mod 5 math can only yield an integer from $0$ to $4$ . So as long as $a * b$ never equals $0$ , 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 $0$ or a multiple of 5. You can check for yourself and see that there is no such pair $a$ and $b$ . 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 $mod$ $5$ . This is because we first multiply two elements and only then perform the $mod$ $5$ operation on the resulting value.

Do we have an identity element $e$ ? Yes, just the ordinary identity element for multiplication, which is $1$ . Any of $1$ through $4$ $mod$ $5$ 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 $\frac{1}{x}$ doesn’t work since such fractions are not members of $\{1, 2, 3, 4\}$ . 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 $a^{-1}$ , we have

$a * a^{-1} = a^{-1} * a = e$ (where in this case $e = 1$ )

the following mapping yields an inverse for every $a$ in $\{1, 2, 3, 4\}$ :

$1 \to 1$
$2 \to 3$
$3 \to 2$
$4 \to 4$

We have now shown that $*$ over $\{1, 2, 3, 4\}$ 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 $(x, y) \in A \times A$ .

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 $(x, y)$ into op (including when $x = y$ ), placing each method call in a try-catch. If op is not defined for some pair $(x, y)$ , 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 $(x, y, z) \in A \times A \times A$ . We need to check that

$(x * y) * z = x * (y * z)$

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 $x \in A$ one at a time, so we can dispense with for-comprehensions. The equation we need to check for is

$x * e = e * x = x$

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

$x * x^{-1} = x^{-1} * x = e$

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 $\{1, 2, 3, 4\}$ 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:

$a^n = a * a * ... * a$ (n times), where $*$ is the group operation.

Given a group $G$ , an element $a \in G$ , and the identity element $e \in G$ , if $a^x = e$ , then the order of $a$ is $x$ . A consequence of Lagrange’s Theorem is that if $G$ is a finite group, then for every element $a \in G$ , the order of $a$ 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” $a$ by itself will eventually yield $e$ . However, we have seen that if $a$ is a member of a finite group, and “multiplication” is the group operation, then we can be certain that multiplying $a$ by itself will eventually yield $e$ . That’s just another way of saying that the order of $a$ 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.

An Abstract Plane

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

Implementing Finite Groups

Verifying Finite Structures

Some Consequences

Conclusion

Related Posts

Safely Sharing Data: Reference Capabilities in Pony 06 Mar 2016

A CRDT Primer Part I: Defanging Order Theory 17 Nov 2015

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