# Learning Nominal Automata

20 Jan 2017

Joshua Moerman, Matteo Sammartino, Alexandra Silva, Bartek Klin and Michał Szynwelski

POPL 2017

## Abstract

We present an Angluin-style algorithm to learn nominal automata, which are acceptors of languages over infinite (structured) alphabets. The abstract approach we take allows us to seamlessly extend known variations of the algorithm to this new setting. In particular we can learn a subclass of nominal non-deterministic automata. An implementation using a recently developed Haskell library for nominal computation is provided for preliminary experiments.

## Links

doi: 10.1145/3009837.3009879

arXiv

Implementation

## Note (during rebuttal phase)

During the rebuttal one of the reviewers asked whether the problem of query learning can be solved polynomially or not. We settled the issue positively, but did not have the room to fit it in the paper. We added the proof in the rebuttal (so it’s not really peer reviewed). The original copy is found online on Matteo’s website. (The following is not properly typeset yet.)

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).