**Alg** is a program for enumeration of finite models of single-sorted first-order theories. These include groups, rings, fields, lattices, posets, graphs, and many more. Alg was written as a class project by Aleš Bizjak, a student of mine whose existence I cannot confirm with a URL. I joined the effort, added bells and whistles, as well as an alternative algorithm that works well for relational structures. Alg is ready for public consumption, although it should be considered of “beta” quality. Instructions for downloading alg are included at the end of this post.

Suppose we want to know how many rings of size $n$ there are. If $n$ happens to be the square of a prime we are lucky because a theorem says there are exactly 11 of them. Otherwise we can look up the numbers on the on The On-Line Encyclopedia of Integer Sequences (OEIS). But what if we want to know the number of semirings of a given size? Unfortunately OEIS does not seem to have an answer. And what if we want the list of 52 non-isomorphic commutative rings of size 8?

Alg comes in handy when you need the list or the count of non-isomorphic copies of an ad-hoc structure. For example, the number of non-isomorphic rings satisfying the additional equation $x \cdot y \cdot x = 0$ is:

$ ./alg.native theories/ring.th --axiom 'x * y * x = 0' --size 1-8 --count ... size | count -----|------ 1 | 1 2 | 1 3 | 1 4 | 4 5 | 1 6 | 1 7 | 1 8 | 19

We could have guessed that there would be at least one such ring of each size, namely the one with zero multiplication. But what are the non-trivial examples of size 4?

$ ./alg.native --size 4 theories/ring.th \ --axiom 'x * y * x = 0' --axiom 'exists x y, x * y <> 0' # Theory ring_with_extras Constant 0. Unary ~. Binary + *. Axiom plus_commutative: x + y = y + x. Axiom plus_associative: (x + y) + z = x + (y + z). Axiom zero_neutral_left: 0 + x = x. Axiom zero_neutral_right: x + 0 = x. Axiom negative_inverse: x + ~ x = 0. Axiom negative_inverse: ~ x + x = 0. Axiom zero_inverse: ~ 0 = 0. Axiom inverse_involution: ~ (~ x) = x. Axiom mult_associative: (x * y) * z = x * (y * z). Axiom distrutivity_right: (x + y) * z = x * z + y * z. Axiom distributivity_left: x * (y + z) = x * y + x * z. # Extra command-line axioms Axiom: exists x y, x * y <> 0. Axiom: x * y * x = 0. # Size 4 ### ring_with_extras_4_1 ~ | 0 a b c --+------------ | 0 a b c + | 0 a b c --+------------ 0 | 0 a b c a | a 0 c b b | b c 0 a c | c b a 0 * | 0 a b c --+------------ 0 | 0 0 0 0 a | 0 0 0 0 b | 0 0 a a c | 0 0 a a - - - - - - - - - - - - - - - - - - - - - - - - - - - - ### ring_with_extras_4_2 ~ | 0 a b c --+------------ | 0 a c b + | 0 a b c --+------------ 0 | 0 a b c a | a 0 c b b | b c a 0 c | c b 0 a * | 0 a b c --+------------ 0 | 0 0 0 0 a | 0 0 0 0 b | 0 0 a a c | 0 0 a a - - - - - - - - - - - - - - - - - - - - - - - - - - - - # Statistics size | count -----|------ 4 | 2

Interesting. Or maybe not. Anyhow, it is easy to play with alg this way.

The supported output formats are text (actually Markdown), HTML, LaTeX and JSON. If you generate three or more sizes, alg outputs a URL for checking the numbers in OEIS.

On my dekstop with Intel Core 2 Duo E8500 @ 3.16 Ghz groups of size up to 9 are enumerated in 3.4 seconds, up to size 10 in 50 seconds, and up to size 11 in 9.5 minutes. Clearly, we are hitting a combinatorial explosion here. As there are $n^{n^2}$ multiplication tables of size $n \times n$, alg has to do something better than trying out $10^{100}$ possible multiplication tables to enumerate groups of size 10. Indeed, alg fights the combinatorial explosion by filling in the tables in a smart way. It uses two algorithms:

- The default algorithm fills in the tables in all possible ways, where with each new entry it also checks the axioms to see what else could be filled in. The algorithm works well for equational theories, such as groups, rings, and lattices.
- The alternative algorithm, which is enabled with the
`--sat`

command-line option, transforms the axioms into a set of constraints that it then satisfies in all possible ways. The algorithm works well for relational theories, such as posets and graphs.

Each new solution is compared for isomorphism with previously found ones. Since isomorphism testing is hard, alg uses simple invariants to quickly test for non-isomorphism. The memory footprint is very low. As I type this alg is using measly 880 kB of memory for enumeration of groups of size 11.

Alg is possibly the right tool for you if you want to:

- list or count non-isomorphic structures satisfying certain axioms, and you cannot find the data on the web
- quickly check a hypothesis such as “In which rings does $x^5 + x^3 + 1 = 0$ have a solution?”
- quickly check if two axiomatizations describe the same structures (count models of both and compare)

Can you trust alg? Well, we do not have a formal proof of correctness. If the results seem fishy there are several things you can do:

- Check the counts at OEIS.
- Compare the answers given by the default and the alternative algorithm.
- Use the
`--paranoid`

option for double-checking of results.

Here are the promised download instructions. You may:

**Check out the source code**from the GitHub repository and make sure you use the stable branch:git clone https://github.com/andrejbauer/alg.git git checkout stable

and compile the program yourself (you need Ocaml 3.11 and menhir, as described in the manual).

**Download the archived source code**from GitHub repository.**Download****precompiled executables**with the manual and example theories included. We have prepared executables for Linux, MacOS X and Windows 7 (this is likely to be obsolete).

The alg manual explains how to compile and use alg and how to write your own theories.

Alg is open source software released under the simplified BSD license. Feedback and bug reports are appreciated!

So I guess it would make sense to prove the algorithm correct in Coq and use code extraction? Or the other way around, aside from generating Markdown/etc, also generate a Coq proof which would basically just be an enumeration of the models.

Inefficiency of code extracted by Coq would be a serious obstacle here. Maybe the

`Program`

facility in Coq could help, up to a point. Alg uses a combination of imperative features and continuations for good performance. Performance is everything in this case. I would even venture to say that performance comes first and correctness second. I know it is a heretic thought, but which is more useful an unusably slow correct program or a fast mostly correct program? The way to go is to add double-checks and to have several alternative implementations whose results can be compared against each other.Also, I am not sure Coq would actually help catching all the errors. For example, here is a buggy function that tells whether an equation is the law of associativity:

Can you spot the error? How would Coq help finding the bug in this case?

Agreed, Coq probably won’t help you here (depending on where and how you use this definition). I’d say this is an example of incorrect specification, which is a problem in any formalization effort.

Thanks for elaborating!