The problem of learning a nominal automaton is polynomial (in the number of
orbits) for the equality symmetry.

Proof (sketch)

The problem can in fact be proven to be polynomial (in the number of orbits, it
will not be polynomial in the dimension of the nominal automaton). In order to
see this we need to alter the algorithm slightly. In a way this can be seen as
an optimization. Note that the paper already states that the number of cells is
polynomial, so it remains to show that filling them with membership queries can
be done polynomially.

We will use the same notation as in the paper (n is number of orbits, k is
dimension and p is the dimension of the alphabet). As noted in the paper, the
support for a row will grow during the execution of the algorithm, until it hits
the bound k. Let's say that at a current stage of the algorithm the size of the
support for a particular row is k' (<= k). We consider the same rows as we
would normally do (without the optimization). Now to fill the cells for such an
extension, we only have to consider a support of at most k'+p (the k' comes from
the original row and p comes from the alphabet). Suppose the column has at most
length q(n,k) for some polynomial q (as proven in the paper), then the number of
data values is at most p * q(n, k). Thus the number of orbits of such a product
is at most f_A(k' + p, p * q(n, k)), which is polynomial in n (and not
polynomial in k). Some more details for the function f_A are given below (be
aware that this function depends on the symmetry).

If we now do the above throughout the algorithm (meaning that we carefully keep
track of the supports of rows, and also propagate this information to the
extensions), then the relevant data values for each row are bounded by k+p.
Indeed, all the cells in the table will have polynomially many orbits (in n).
Combined with the fact that there are polynomially many cells in total, this
proves that the number of membership queries is polynomial in n.

Note that the soundness for this optimization follows from consistency: the
possibility of having too small support is ruled out as the same extensions are
considered, so if a data value matters, the extensions will have different rows
(maybe after several steps). Each inconsistency will lead to new columns (just
as before), which will show at some point that a data value is in the support.

The number of equivalence queries was already proven to be polynomial. So the
number of queries in total is polynomial in n (but not in k).

End of proof.



Bonus: One may question whether we can do something similar to the columns,
bounding their support to k. The answer is no, because the reverse of a regular
nominal language is not necessarily accepted by an orbit-finite nominal automaton
(and by reversing a language one reverses the roles of the rows and columns).


Additional notes on f_A (where A is the countably infinite set of names with
permutations).

As defined in the paper f_A(n, m) defines the number of orbits in A^(n) x A^(m),
that is the product of distinct n-tuples with distinct m-tuples. An orbit in
this product possibly matches some of the first n values with some of the next m
values. We can compute the number of orbits where such a match has size i with
the following formula. With n and i fixed, it gives a polynomial bound in m:

  matchings_i = (n choose i) * (m choose i) * i!
             <= (n choose i) * i! * m^i

The equality is explained as such: we may choose i values of either set
independently, and then choose how to match them (i!). Now f_A(n, m) is the sum
of matchings_i for i = 0 to n. This gives the formula and bound

  f_A(n, m) = Sum_{i = 0}^{n} matchings_i
           <= constant_n * m^{n+1}

where constant_n is some constant depending on n. In particular this expression
is polynomial in m. Furthermore, we have a symmetry f_A(n, m) = f_A(m, n),
meaning that it is also polynomial in n (if m is fixed). Note, however, that
f_A(n, n) is not polynomial in n. In the above proof, n (the number of orbits),
occurs in only one of the two places, making it polynomial in n.

In this counting argument we used the fact that these orbits correspond to
matchings. This does not hold in other symmetries. For example the structure (Q,
<), i.e. the dense linear order, has a bigger growing rate for f_Q(n,m). Some
general results on these growing rates can be found in notes by Peter Cameron on
oligomorphic permutation groups (can also be found in his 1990 book).