One of the surprising aspect of the genome for lay-people is that it contains important non-coding DNA parts, which does not mean that they are all useless. I never paid so much attention to the fact, until very recently, when I realized that the same is apparently true of all computing formalisms I can think of ... but maybe I forgot some, which is part of my question.
If you consider finite state automata, you can always add an arbitrary finite chain of unreachable states, which may be read as the Gödel number of whatever statement you care to add to the FSA, whether a copyright statement or a complete formal proof that it recognizes a regular expression in some a priori chosen formalism.
But the same is actually true of CF grammars, of Turing Machines, of Post Correspondence Problems, of lambda-expressions, of Primitive Recursive programs, or of Partial Recursive programs, to name some of the more important computing formalisms. Actually I cannot think of a computing formalism that does not have that syntactic feature. This is also true of programming languages, often as an official syntactic feature called comment, which is not strictly necessary, but does save time and space.
I recently used the property to prove (hopefully correctly) that all primitive recursive functions can be implemented as a recursive set of Turing Machines. This may not be a very deep result, but my understanding from that proof is that the phenomenon is very general and may have other consequences.
To be precise about definition, I think one could call non-coding part of a formalism instance those parts that can be identified by a uniform decision procedure as computationally irrelevant.
Question: Is the property as general as I make it? Has it been analyzed more thoroughly, including causes (is it unescapable?), consequences, and theoretical or practical uses? Does it have a name?
I think that the property could somewhat be implied by general theorems about computability. But why should that extend to very simple formalisms like FSA.
My guess is that, given the above definition of non-coding part, it may be that for simpler formalisms like FSA there is a uniform recursive procedure that can remove all non coding parts: that procedure could be made part of the formalism specification, thus contradicting my universality statement. But such a procedure would not exist for a Turing complete formalism (Rice theorem?). And the fact remains that even the simpler formalisms we use are defined with this "comment" potential, even if it might be removable by a restriction to normal forms.
