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.