Are decidable set/languages EQUIVALENT to type 1 grammars (non-contracting)? Suppose a Turing Machine (TM_G) that generates natural numbers following &lt; or, equivalently, it generates words in lexicographical order.
Then, that language/set is decidable. Because it is trivial to devise a (halting) TM_R, using TM_G, that recognize/accepts the words/numbers of that language/set.
It is also clear (really?), that there must be a non-contracting grammar for the language of TM_G.
Now, let's suppose a we have a TM_G' that generates a decidable language not in lexicographical order. Because the language is decidable, there must exist a TM_R' that completely recognizes it. Now, it is not clear how to build TM_R' using TM_G' (probably this is a unsolvable problem (is it?). At least, it is easy how to have a semi-deciding TM_R' based on TM_G').
In any case, by assumption, TM_R' (the halting/complete recognizer) does exist. Then, we can use TM_R' to build a TM_G'' which generates the language in lexicographical order.  Hence (really?), there exists a non-contracting grammar for the language.
In sum, is the class of decidable languages equivalent to non-contracting grammars?
In other words, are there a decidable language that cannot be generated by a non-contracting grammar (type 1)?
Expressed in terms of Turing Machines: **is the power of all halting TM equivalent to the power of all linear bounded automata (a restricted type of TM equivalent to type-1 grammars).? **
Yuval's answer is absolutely right, but note that there's a more general principle in play here as well: diagonalization. Any time we have a class of decidable languages for which we have a &quot;decidable syntactic description&quot; (I'm being vague about this for a moment), we can diagonalize out of this class to get a decidable language not in the class. Basically, we whip up a notion of &quot;$n$th language in the class&quot; and then consider the new language which contains word $1...1$ ($n$ times) iff the $n$th language in the class does not contain that word (or something similar); granting the complexity assumption on the starting class, this results in a decidable language.
(In snappier computability-theoretic terminology: if $f(x,y)$ is a total computable function then there is a total computable $g(z)$ such that for each $x$ there is some $y$ with $f(x,y)\not=g(y)$.)
Classes like type $1$ grammars are defined by simple syntactic conditions, and so can be diagonalized out of. Of course this does not necessarily result in a natural example of a decidable language not in the starting class, but it does prove that that class misses many decidable languages.