Mathematics and Computation

A blog about mathematics for computers

Alg

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:

  1. 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.
  2. 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:

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:

  1. Check the counts at OEIS.
  2. Compare the answers given by the default and the alternative algorithm.
  3. Use the --paranoid option for double-checking of results.

Here are the promised download instructions. You may:

  1. Check out the source code from the GitHub repository and make sure you use the stable branch: <pre class="brush: plain; gutter: false; title: ; notranslate" title="">git clone https://github.com/andrejbauer/alg.git git checkout stable

</pre>

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

  * [**Download the archived source code**](https://github.com/andrejbauer/alg/archive/stable.zip) from GitHub repository.
  * [**Download** **precompiled executables**](/wp-content/uploads/alg/) with the manual and example theories included. We have prepared executables for Linux, MacOS X and Windows 7 (this is likely to be obsolete).</ol> 

The [alg manual](http://hg.andrej.com/alg/raw-file/tip/doc/manual.pdf) 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](http://www.opensource.org/licenses/bsd-license.php). Feedback and bug reports are appreciated!

Comments

Tweets that mention Alg « Mathematics and Computation -- Topsy.com

[...] This post was mentioned on Twitter by Planet OCamlCore, Andrej Bauer. Andrej Bauer said: A program for enumeration of (small) first-order structures http://math.andrej.com/2011/01/22/alg/ (#algebra, #math) [...]

Martijn Vermaat

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.

Andrej Bauer

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: [sourcecode gutter="false"] let is_assoc = function | (Binary (op1, Binary (op2, Var a1, Var b1), Var c1), Binary (op3, Var a2, Binary (op4, Var b2, Var c2))) | (Binary (op3, Var a2, Binary (op4, Var b2, Var c2)), Binary (op1, Binary (op2, Var a1, Var b1), Var c1)) when op1 = op2 && op2 = op3 && op3 = op4 && a1 = a2 && b1 = b2 && c1 = c2 -> true | _ -> false </pre> Can you spot the error? How would Coq help finding the bug in this case?

Martijn Vermaat

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!

Andrey Mokhov

Thank you very much for the tool! I've successfully used to for proving minimality of several sets of axioms. Extremely useful! Andrey

How to comment on this blog: At present comments are disabled because the relevant script died. If you comment on this post on Mastodon and mention andrejbauer@mathstodon.xyz, I will gladly respond. You are also welcome to contact me directly.