In mathematics, logic and computer science, a formal language (a set of finite sequences of symbols taken from a fixed alphabet) is called recursive if it is a recursive subset of the set of all possible finite sequences over the alphabet of the language.
Equivalently, a formal language is recursive if there exists a Turing machine that, when given a finite sequence of symbols as input, always halts and accepts it if it belongs to the language and halts and rejects it otherwise.
For one such example, some familiarity with mathematical logic is required: Presburger arithmetic is the first-order theory of the natural numbers with addition (but without multiplication).
While the set of well-formed formulas in Presburger arithmetic is context-free, every deterministic Turing machine accepting the set of true statements in Presburger arithmetic has a worst-case runtime of at least
for some constant c [citation needed], the set of valid formulas in Presburger arithmetic is not context-sensitive.
On positive side, it is known that there is a deterministic Turing machine running in time at most triply exponential in n that decides the set of true formulas in Presburger arithmetic.