Algorithm to test whether a language is regular Is there an algorithm/systematic procedure to test whether a language is regular?

In other words, given a language specified in algebraic form (think of something like $L=\{a^n b^n : n \in \mathbb{N}\}$), test whether the language is regular or not.  Imagine we are writing a web service to help students with all their homeworks; the user specifies the language, and the web service responds with "regular",  "not regular", or "I don't know".  (We'd like the web service to answer "I don't know" as infrequently as possible.)  Is there any good approach to automating this?  Is this tractable?  Is it decidable (i.e., is it possible to guarantee that we never need to answer "I don't know")?  Are there reasonably efficient algorithms for solving this problem, and be able to provide an answer other than "don't know" for many/most languages that are likely to arise in practice?

The classic method for proving that a language is not regular is the pumping lemma.  However, it looks like requires manual insight at some point (e.g., to choose the word to pump), so I'm not clear on whether this can be turned into something algorithmic.

A classic method for proving that a language is regular would be to use the  Myhill–Nerode theorem to derive a finite-state automaton.  This looks like a promising approach, but it does requires the ability to perform basic operations on languages in algebraic form.  It's not clear to me whether there's a systematic way to symbolically perform all of the operations that may be needed, on languages in algebraic form.



To make this question well-posed, we need to decide how the user will specify  the language.  I'm open to suggestions, but I'm thinking something like this:

$$L = \{E : S\}$$

where $E$ is a word-expression and $S$ is a system of linear inequalities over the length-variables, with the following definitions:


Each of $x,y,z,\dots$ is a word-expression.  (These represent variables that can take on any word in $\Sigma^*$.)
Each of $x^r,y^r,z^r,\dots$ is a word-expression.  (Here $x^r$ represents the reverse of the string $x$.)
Each of $a,b,c,\dots$ is a word-expression.  (Implicitly, $\Sigma=\{a,b,c,\dots\}$, so $a,b,c,\dots$ represent a single symbol in the underlying alphabet.)
Each of $a^\eta,b^\eta,c^\eta,\dots$ is a word-expression, if $\eta$ is a length-variable.
The concatenation of word-expressions is a word-expression.
Each of $m,n,p,q,\dots$ is a length-variable.  (These represent variables that can take on any natural number.)
Each of $|x|,|y|,|z|,\dots$ is a length-variable.  (These represent the length of a corresponding word.)


This seems broad enough to handle many of the cases we see in textbook exercises.  Of course, you can substitute any other textual method of specifying a language in algebraic form, if you have a better suggestion.
The answer is no. Deciding whether a given context-free grammar generates a regular language is an undecidable problem. 

Update. I gave this negative answer to the general question


  Given a language specified in algebraic form, test whether the
  language is regular or not


since context-free languages are solutions of algebraic equations in languages: see Chapter II, Theorems 1.4 and 1.5 in the book of J. Berstel Transductions and Context-Free Languages.

However, the same question is decidable for deterministic context-free languages, a nontrivial result due to Stearns [1] and improved by Valiant [2]:
[1] R. E. Stearns, A Regularity Test for Pushdown Machines, Information and Control  11 323-340 (1967). DOI:10.1016/S0019-9958(67)90591-8.
[2] L. G. Valiant. Regularity and related problems for deterministic pushdown automata J. ACM 22 (1975), pp. 1–10.

There is another positive result, closer to the specifications given in the second part of the question. Recall that the semilinear subsets of $\mathbb{N}^k$ are exactly the sets definable in Presburger arithmetic. There are also the rational subsets of $\mathbb{N}^k$. In particular, a subset of $\mathbb{N}^k$ defined by linear inequations is rational. Now, given a rational subset $R$ of $\mathbb{N}^k$, it is decidable whether the language
$$
  L(R) = \{ u_1^{n_1} \dotsm  u_k^{n_k} \mid (n_1, ...,n_k) \in R \}
$$
is regular. Indeed, it is known [Ginsburg-Spanier] that $L(R)$ is regular if and only if $R$ is a recognizable subset of $\mathbb{N}^k$ and it is decidable [Ginsburg-Spanier] whether a given rational subset of $\mathbb{N}^k$ is recognizable. 

S. Ginsburg and E. H. Spanier., Semigroups, Presburger formulas, and languages,  Pacific J. Math. 16 (1966), 285-296.

S. Ginsburg and E. H. Spanier. Bounded regular sets, Proc. of the American Math. Soc. 17, 1043–1049 (1966).

This does not solve the second part of the question, which might be undecidable because of the word variables, but it gives a reasonable fragment to start with.