The strongly-connection check fails for Pólya structures

[Kerl13]

In a specification such as the example below, singular tuning without the Method.FORCE flag fails because the expansion of the multi set as exp(\sum A(T^j)/j) yields a grammar that is not strongly connected. The initial grammar is strongly-connected though. Maybe the check should be done on the grammar provided by the user and not the expanded one?

from paganini import *

T, z = Variable(), Variable()
spec = Specification()
spec.add(T, z * MSet(T))
spec.run_singular_tuner(z)

----> 1 spec.run_singular_tuner(z)

File ~/.local/lib/python3.10/site-packages/paganini/specification.py:769, in Specification.run_singular_tuner(self, z, params, method)
    766 if method == Method.STRICT:
    767     # check theoretical conditions imposed on singular tuning.
    768     if not self._check_singular_tuner():
--> 769         raise ValueError("Given specification has not a strongly connected "
    770             "dependency graph. Please check the specification for "
    771             "possible errors, or consider using finite-size "
    772             "tuning for large values of the size parameter.")
    774 n = self.discharged_variables
    775 variables = cvxpy.Variable(n)

ValueError: Given specification has not a strongly connected dependency graph. Please check the specification for possible errors, or consider using finite-size tuning for large values of the size parameter.

[Sergey-A-Dovgal]

Since the grammar is truncated at a finite number of iterations, I am not completely sure it would be strongly connected.

[Kerl13]

But is this check relevant here in this case? What are the guaranties provided by paganini for Pólya operators? My understanding was that the usual Pólya operators were in the scope of the theory behind paganini.

[maciej-bendkowski]

@Kerl13 what would you expect, instead of the current behavior?

Pólya operators are supported, but as @Sergey-A-Dovgal mentioned, the grammar is in principle infinite, and so for practical purposes we need to truncate such operator. I recommend using finite tuning with a sufficiently large size parameter value. For finite tuning the grammar does not need to be strongly-connected. Instead, it suffices that all types are reachable from the one you tune.

[Kerl13]

@Kerl13 what would you expect, instead of the current behavior?

If the specification is covered by paganini and can be safely tuned using the singular tuner, I would expect the sanity check to pass. If my understanding of the tuning hypotheses is correct, then T = z * MSet(T) should pass the test (it is strongly connected) whereas something like T = MSet(A); A = z * Seq(z) should fail (it is not). I understand the need to internally truncate the specification but this is an implementation detail that should be hidden from the user I think.

I recommend using finite tuning with a sufficiently large size parameter value. For finite tuning the grammar does not need to be strongly-connected. Instead, it suffices that all types are reachable from the one you tune.

Okay got it, if you're saying that finite size tuning is more reliable, I should use this instead (and I know you've been telling me that for a while ^^)

[maciej-bendkowski]

I guess it's a matter of better error messages, then. Note that the exact error message you obtained is:

Given specification has not a strongly connected dependency graph"

You assumed that the dependency graph is built from the specification and nothing more. That's not the case, even already for simpler operators, such as Seq. I'm not sure what error message could be better. Any ideas @Sergey-A-Dovgal @Kerl13?