corollary

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) ∧ x ∈ g.carrier ⟹ g.plus 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.

Version Control Systems

I’m beginning to think that we should move HOL4 off Subversion and onto git, preferably hosted on github.com. Here’s why:

• Most importantly, git makes dealing with a certain class of contributor easier. Currently, the Subversion at SourceForge setup means that we can only support two sorts of developer: the regular developer that is allowed to make arbitrary commits across the whole source-tree; and the very occasional developer who mails a regular developer a patch. The regular developer makes the commit themselves, perhaps adding that the bug-fix, additional theory or whatever came from the very occasional developer.

  With git, we can have an intermediate class of developer, the occasional developer. These people can establish their own forks of the source-code, do their own stuff with it, and then make pull requests. If their commits do get incorporated into the “official” repository, their names will still be attached to the commit objects.

• An advantage of moving to github specifically is that it allows us (through “beta” software admittedly) to view a git repository as a Subversion one, meaning that existing HOL4 developers who don’t want to have to learn git can continue to make commits using the svn command-line tool, in a way that will remain familiar.

  This facility at github is described (in rather sketchy fashion) here.

• The last advantage is that git is just much cooler than Subversion in many ways. In particular, it gives developers good support for branching and merging, with complete local copies of repositories.

Possible disadvantages:

• The support for Subversion as a git client at github may not be robust.

• Our big existing Subversion branch (HOLω; see here) may prove difficult to graft onto the git repository in a nice way.

  My guess at the moment is that we could checkout master, dump the HOLω branch on top of that and do a fresh commit. In that way, we would encapsulate all of the existing history in one huge commit. The subsequent development of HOLω on that branch could use git’s good support for cherry-picking and merging in general to pull across new stuff from master.