# How to formally show computational equivalence or universality using encodings?

I want to formally show that a computational system $$\mathcal M$$ is computationally universal by showing it is computationally equivalent to some already known universal system, i.e. some UTM.

To show that system $$\mathcal M$$ is computationally equivalent I need to prove something along the lines of this following definition:

Definition(Computationally Equivalent Systems) Let $$A, B, A_0 , B_0$$ be alphabets and let $$\mathcal M$$ and $$\mathcal N$$ be computational systems with their computed functions being of the form $$f_M : A^* \to B^*$$ and $$f_N : A_0^* \to B_0^*$$. Then if there exist encoding functions $$e_1 : A^* \to A_0^*$$ and $$e_2 : B^* \to B_0^*$$ such that $$e_2 \circ f_M = f_N \circ e_1$$ holds we say $$\mathcal M$$ and $$\mathcal N$$ are computationally equivalent w.r.t. the encodings $$e_1$$ and $$e_2$$.

The problem is I can't find a useful definition for encodings. They obviously should be total and Turing computable (and possibly reversible) functions. However, they must not be too powerful since if the encodings partake in the actual computation any systems can be "equivalent" and that is not what we want.

Example: If you want to compare a machine that computes addition on a pair of numbers (in base 10) with a machine that computes addition on a pair of binary numbers those should be equivalent in their computation since only the representation they use for input and output changes. However, if you now consider an "encoding function" that it self performs the addition and returns the result, the first machine would be "equivalent" to a machine that simply performs the identity function. This is obviously not an intended result of the definitions above. In this example it is easy to see intuitively that the "encoding" was to "strong". But how can I describe that formally? How can I further restrict the computational power of encodings to be lower than the computation that I am studying?

The same problem arises when comparing machines regarding computational universality. How can I define encodings that are not able to perform universal computations themselves (so that they don't interfere in the results I am trying to prove), but that are still powerful enough to be useful for actual translations of complex representations of inputs and outputs?

My initial idea was to restrict the encodings to functions that can be computed by some kind of automata that is provably less powerful than a TM. For example a linear-bounded TM. However (if I am not mistaken) such a linear-bounded TM would already be to weak, since it can not compute functions like $$\text{DecToBin}: \{0,1,2,...,9\}^* \to \{0,1\}^*$$ since the length of the output grows exponentially compared to the input.

Edit: I am mistaken. A linear-bounded TM CAN compute functions like decimal to binary conversion, since their growth is linear and NOT exponential. So maybe functions computable by linear-bounded TMs would be a solution?

An other idea I think might be useful to incorporate is some semantic preservation property. I.e. if the if the words over the input and output alphabets are equipped with some notion of semantic we require that the encodings preserve this semantic.

However this does feel like "cheating" at feels not at all formally sound.

This leads me to the question: How can one formally restrict the computational power of encodings such that a formally sound study of universality is possible?

All proofs of universality I've read so far simply brush over the fact that some kind of encoding is happening. If you know of a work where this was explicitly discussed I would be very interested.

Thank you!