Is there a language actually in use that can't be recognized by a linear bounded automaton? I only know of ones that don't have a practical use, like "the set of pairs of equivalent regular expressions with exponentiation" (Wikipedia). Or would any such language be too slow to recognize to be useful?
A language that is not even context-sensitive?
3
$\begingroup$
computer-science
-
0Automated proof checkers are computer programs that recognize the language of all valid proofs in some system. I don't think this language can be recognized by a linear bounded automaton, but I don't actually know. – 2012-02-25
2 Answers
3
The set of true statements in Presburger Arithmetic is not context sensitive (as it has been shown that it is not $\text{NPSPACE}(n)$ decideable).
As for being in actual use, don't know.
0
I think any problem with non-elementary complexity should do, e.g. "correctly typed programs" for some complex type theories might be just an example you look for ;-)