Is a unary language regular iff its exponent is a linear function? While doing the current assignment for my formal languages and automata course, I kind of got stuck on exercises involving unary languages (I hope that's the right term), i.e., languages which build upon a single letter. I don't want to ask about the specific exercises, though, but rather about a much more general conjecture I've come up with:

Let $\Sigma=\{a\}$ and $L=\{a^{f(n)}\in\Sigma^*:n\in\mathbb N_0\}$. My conjecture is:
$$L\text{ is regular}\Leftrightarrow \exists x,y\in\mathbb N_0:f(n)=x\cdot n+y$$

Has this question seen any scientific treatment before? Is it "obviously" true / false? 

To me, obviously the "$\Leftarrow$" direction is true because one can just construct a DFA with $x+y$ states that cycles through the $x$ states after having read through $y$ states and accepts iff it is at state number $y$.
Linear is close, but the technical term you're looking for is semilinear:, that is, a finite union of linear sets.

Half of the proof of this is a corollary of Parikh's Theorem, which says that any context-free language has a semi-linear Parikh map (that is, the set of vectors containing the occurrences of each letter in the alphabet).

For a unary language, the parikh map of the language is the language itself (i.e. each word is uniquely identified by how many letters it has), so every unary regular language is semi-linear.

The other half of the proof is showing that you can construct a regular language containing every unary semi-linear set. This takes a bit of work, but it's not too hard if you use regular expressions:


$a^k$ recognizes the language $\{ k \}$
$(a^k)^*$ recognizes $\{xk \mid x \in \mathbb{N}_0 \}$
$R_1 R_2$ recognizes $S_1 + S_2$ if $R_1$ recognizes $S_1$ and $R_2$ recognizes $S_2$, where $+$ here is element-wise addition
$R_1 | R_2$ recognizes $S_1 \cup S_2$ if $R_1$ recognizes $S_1$ and $R_2$ recognizes $S_2$, where $|$ here is regular-expression union.