Wednesday, 15 February 2012

Abstract Algebra in HOL4

Listening to:

Mahler, symphony no. 1, “Titan”; Royal Concertgebouw Orchestra, conducted by Leonard Bernstein.

By algebra I mean stuff like group theory. This has always been difficult in HOL, mostly because of the relative inexpressiveness of its simple type theory. In particular, there’s no good way to set up a type of all possible groups, which is the natural thing to want. The best thing possible would be to get a type of groups over a parameter corresponding to the type of the carrier set. In other words, you could set up a type operator group of arity one, so that the type α group would be the set of all possible groups with carrier sets that have elements from the type α.

The funny thing is that most people don't seem to do this. Instead, they work with what you might call a pre-group. Such a thing might be a triple of carrier set, group operation, and group identity. Not all such triples are really groups because the required group axioms may not be satisfied.

The standard approach is to then define a predicate isGroup over the pre-groups. Then isGroup(pg) is true when the pre-group pg does satisfy the appropriate group axioms. You might then manage to prove a bunch of theorems of the form

  ⊢ isGroup(g) ∧ xg.carrier ⟹ g.identity x = x

You can do a whole lot of group theory this way, but just about every theorem you ever prove is going to have a isGroup pre-condition of some form. The experiment I want to perform is taking the subset of pre-groups corresponding to those triples that really are groups, and to then define a genuine HOL type on that basis.

You might still get theorems that require elements to be members of the underlying carrier set, but it’d still be an improvement, I reckon. Nor can I really see a possible down-side, at least as far as groups are concerned.

The only fiddle necessary is when you move on to rings and fields where the algebraic structure is usually understood to contain at least two elements (the zero and the one). You can’t then construct such a structure uniformly for all possible carrier types in HOL, because types may only contain one element. There are two possible work-arounds:

  • Make the carrier type actually be α option or some such, so that you can be sure that the type really is always big enough. This is pretty ick really.
  • Allow rings and fields to have zeroes and ones that are the same. I don’t know at this point how much violence this would do to the general theory.

Better yet, I have a potential student ready to start doing just this experiment, so I may be able to report back shortly.