Skip to content

RagnarGrootKoerkamp/automata

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

47 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

This code was written by Ragnar Groot Koerkamp and accompanies the paper Automata and Finite Order Elements in the Nottingham Group, by Jakub Byszewski, Gunther Cornelissen, and Djurre Tijsma (arXiv), for finding all 2-automata on at most 5 vertices generating a power series \sigma(t) = t + O(t^2) of compositional order 2 or 4.

Specifically, this program find 2-automata on at most 5 vertices satisfying the following conditions:

  • Leading zeros invariant, e.g. outgoing 0 edges point to vertices of the same label.
  • Minimal: there exists no smaller automaton generating the same power series.
  • The power series \sigma generated by the automaton satisfies a_0 = 0 and a_1 = 1, i.e. it starts with \sigma = t + O(t^2).
  • The power series \sigma has compositional order 2 or 4, i.e. \sigma(\sigma(t)) = t or \tau(t) := \sigma(\sigma(t)) satisfies \tau(\tau(t)) = t.

The first three pages of the paper (up to and including Example 1.2) contain formal definitions of 2-automata, their corresponding power series, and their compositional order.

Implementation notes

The search over automata works as follows:

  • Iterate over the number of vertices 1\leq n \leq 5. Vertices are numbered 0 to n-1. Vertex 0 is the start vertex, and the 1-edge out of 0 always points to vertex n-1.
  • Iterate over 1\leq z \leq n-1, the number of vertices with label 0.
  • Vertices 0 to z-1 get label 0, vertices z to n-1 get label 1.
  • Iterate over all possible combinations of 0- and 1-edges out of all vertices, where 0 edges must go to other vertices of the same label.
  • To break symmetry, the 0-edge out of vertex 0 must go to either vertex 0 or vertex 1, and the 0-edge out of n-1 must go to either n-2 or n-1.
  • Skip automata with unreachable states, and those for which the corresponding power series \sigma is not of the form t + O(t^2).
  • Check whether the automaton is minimal. If not, skip it.
  • For each automaton compute the corresponding power series \sigma up to degree 2^k (we have taken k = 12, since for k < 12 one finds false positives). Then compute \sigma(\sigma(t)) \mod t^{2^k+1} and \tau(\tau(t)) \mod t^{2^k+1}, where \tau=\sigma(\sigma(t)), to determine if it is a candidate for an order 2 or 4 series. If at least one of these series equals t, we store the automaton and its power series, and check if this automaton is isomorphic to any previous encountered automaton with the same power series.
  • Using Sage, we check if the power series corresponding to the automaton indeed has order 2 or 4.

Output format

Each automaton in the output first lists the labels of the vertices, followed by a description of the edges. The ith line contains the destination of the 0-edge followed by the destination of the 1-edge.

For example:

Vertex labels: 0 0 1 1 1
Edges:
0 4
1 2
4 2
3 4
3 1

This automaton has 5 vertices, where vertices 0 and 1 have label 0 and vertices 2, 3, and 4 have label 1. The 0-edge out of 0 goes to 0, and the 1-edge out of 0 goes to 4. This is the power series \sigma_{min} from the paper.

Output data

  • results.txt contains all 2-automata on at most 5 vertices whose corresponding power series have compositional order 2 or 4.

Build and Run

Run make all to build the program and regenerate results.txt. See the makefile for details.

Note that a recent standard library with (partial) C++20 support is required for e.g. countr_zero.

Run make verify to verify all automata listed in results.txt using additional checks in verify_finite_order.sage. This should finish without errors, note however that this can take up to 30 minutes (resulting from a time consuming computation of an elimination ideal in Sage). This checks that:

  • All the automata listed in results.txt indeed have compositional order 2 or 4. This is done by first calculating from the automaton an algebraic equation satisfied by the power series \sigma. Using an elimination ideal computation in Sage one then computes an algebraic equation for respectively \sigma(\sigma(t)) or \tau(\tau(t)) with \tau=\sigma(\sigma(t)). Using this equation we can check whether respectively \sigma(\sigma(t))=t or \tau(\tau(t))=t holds.

Some open questions

  • To which degree d do we need to check that \sigma(\sigma(t)) \equiv t \mod t^d to be sure equality holds as well, same question for the four fold composition of \sigma.
  • Given an automaton A generating \sigma(t) can we find a combinatorial way to compute the automaton for \sigma(\sigma(t)) using only the combinatorial description of A (note, it is possible to compute the automaton for \sigma(\sigma(t)) using algebra)?
  • More general, is there an automaton to automaton mapping that gives for \sigma(t) the automaton corresponding to \sigma(\sigma(t))?