# What is an 'effective' encoding?

Computability is usually defined using functions on the Natural numbers. The question I have is - what is the 'correct' definition to extend this notion to other sets?

For instance, Nigel Cutland's book about Computability has a small section about "Computability on other Domains", where a 'coding' of a domain D is an 'explicit and effective injection' α: D → Nat. Then, f: D → D is naturally coded by the function f* : Nat → Nat, which maps the code of d to the code of f(d).

My question is - What exactly is an "explicit and effective" injection? We are defining computability here, which doesn't really talk about arbitary domains. I am guessing that 'intuitively uncomputable' functions cannot be 'explicit and effective' injections?

Note: I do think that we often want to extend the notion of computability to other sets - maybe to compare programming languages, maybe to use halting problem arguments to prove incompleteness, etc.

• Effective means ajgorithmic, computable. It means that we can write a piece of software to compute the code corresponding to the expression. Commented Jul 28 at 14:01
• @MauroALLEGRANZA - That makes sense, but seems like a meta-level / intuitive argument. Can we have a definition of 'effective', and actually prove that some functions are effective? Commented Jul 28 at 14:02
• Yes, recursive function, automata, Turing machine Post, Markov. Many different formal models available. Commented Jul 28 at 14:05
• @MauroALLEGRANZA - I think we are circling back to the same question again. These formal models define computability on the natural numbers. The question was to 'lift' this to other domains in our metalogic. The question itself mentions a book about Computability Commented Jul 28 at 14:12
• You could be interested in Andrej Bauer's Notes on realizability. Commented Jul 28 at 15:01

Computability is not always defined using natural numbers. For instance Turing machines work with tapes, and the natural contents of those tapes are strings, collections of which are called languages. In this setting, you must explain how natural numbers are encoded as strings for a machine to operate on. Of course, there are other ways of defining computation where natural numbers are the basic objects, in which case you will have to explain how to encode strings.

A general theory for how mathematical objects are encoded for computation is realizability, and the comments linked some notes that seem very thorough. I'll try to explain a quick overview, though.

Realizability starts with an abstract computation system called a "partial combinatory algebra." These are basically models of the SKI combinator calculus, and the appeal is that the 'algorithms' and the 'data' that the algorithms operate on are the same thing. In a system like Turing machines, this corresponds to the existence of a universal machine that accepts a description as input. You can just pretend that the descriptions 'are' the machines, so you only have to worry about one sort of object.

Once you have a PCA $$\cal A$$, the 'simple' notion of how a mathematical object is encoded in it is an "assembly." These are given by:

• A set $$S$$ to be encoded
• A relation $$\Vdash_S$$ from $$\cal A$$ to $$S$$ where ...
• for all $$s \in S$$ there is at least one $$a \in \cal A$$ such that $$a \Vdash s$$

The idea being that the relation specifies which elements of $$\cal A$$ represent a value of $$S$$. You can also imagine this as $$\newcommand{\E}{\mathsf{E}} \E_S : S → \cal P_+(A)$$ where $$\cal P_+$$ is the non-empty powerset, and $$\E_S(s)$$ is the set of representatives of $$s$$. Note that at this point it's meaningless to talk about whether the representation relation is 'computable' or whatnot, because we're defining how we're even going to talk about $$S$$ for the purpose of computation.

You can also require that each $$a \in \cal A$$ represents at most one $$s \in S$$. Such assemblies are called, "modest," and they include a lot of typical specifications of 'computable numbers' and such. But, assemblies that aren't modest can be useful for some purposes as well.

The idea of all this is that an assembly $$(S, \Vdash_S)$$ is a specification of how to encode $$S$$ for the purposes of computability. Then, computable functions are maps of assemblies $$(S, \Vdash_S) → (T, \Vdash_T)$$, which are given by:

• A function $$f : S → T$$ ...
• ... such that there exists $$\hat f \in \cal A$$ that 'tracks' $$f$$ meaning ...
• ... for all $$a \in \cal A$$, if $$a \Vdash_S s$$, then $$\hat f \cdot a$$ is well defined and $$\hat f \cdot a \Vdash_T f(s)$$

Once you have these, there are standard ways of interpreting a considerable amount of logic and mathematics in terms of assemblies. You can also go a bit further to build a topos, which allows you to interpret a language similar to set theory or type theory. The significant difference from ordinary mathematics is that the logic is intuitionistic/constructive, even though we started with computability in classical mathematics. Realizability supports many additional principles beyond plain constructive mathematics, though, because the idea is that 'anything that is computable,' is valid.

So, inside this setting, you can specify the assembly $$ℕ$$ of natural numbers and some other assembly $$D$$ which characterizes your other domain of computation. If there is an injection $$ℕ → D$$, then it is necessarily an 'effective injection' in terms of the encodings of $$ℕ$$ and $$D$$ in whatever computational system $$\cal A$$ is. If you were working in the underlying logic, then this would be a characterization of what an 'effective injection' is, using assemblies to characterize what it means to represent mathematical objects.

One 'quirk' to note is that there are some assemblies that do not behave like you might expect. For instance, for any set $$S$$, we can form the assembly $$\nabla S$$, where $$a \Vdash_S s$$ is just always true. Then, every $$f : S → T$$ is a 'computable map' $$\nabla S → \nabla T$$ (tracked by e.g. the identity element of $$\cal A$$). The reason is that the representations of $$\nabla S$$ contain no actual information about what is being represented, so it is trivial to map between representations like these. The lesson is that there can be many ways to 'represent' a set, and which one you choose can matter a lot. $$\nabla ℝ$$ is not the usual 'computable reals,' and $$\nabla ℕ$$ is not the usual encoding of the natural numbers.

If you stick to modest assemblies, these quirks mostly won't happen. I think the modest assemblies are how people typically conceive of computable versions of things.

So, ultimately, there is no one encoding of a mathematical object for computation. There are many, and various choices can have essentially the same, or very different properties. You have to pick one that makes sense for what you're doing, and (as another answer says) there is strictly speaking no formal method for that in all cases. But ...

The fact that you can interpret so much mathematics internal to assemblies means that there are well defined choices for many things. Assemblies form a category, and there is a standard notion of a 'natural numbers object' in a category. When you carry this out in assemblies, you get something equivalent to the usual encoding of natural numbers for computation. Similarly, when you interpret a(n appropriate constructive) definition of the real numbers, you get something equivalent to the computable reals in e.g. the (type 1) Turing machine setting. So, this framework can help guide you by interpreting 'normal' mathematical specifications of the sets to generate the 'right' computational representation, in that it will fill a similar mathematical role.

(Side note: by the usual cardinality argument, there cannot be a modest assembly $$(ℝ, \Vdash_ℝ)$$ for e.g. (type 1) Turing machines, because $$\cal A$$ consists of finite strings in that case, of which there are countably many. So, the assembly you get above is not one for representing all of $$ℝ$$ in the underlying set theory. But, it is representing a subset of the underlying $$ℝ$$ that plays a similar role 'within' the mathematics of assemblies. You do (I believe) get all of $$ℝ$$ for "type 2" Turing machines, because those operate on infinite bit streams. But, this shows how sometimes you must be content with not representing 'all' elements of a set, and how realizability can help guide you to the 'right' subset.)

As a final note, much of the above mathematical machinery can be seen as a rarefied version of what computers actually do every day. When you work with data on a (typical) computer, it's all ultimately represented as bit strings at a conceptual machine level. But actually, the bit strings are represented as physical voltages or magnetization (or ...). Someone had to pick the somewhat arbitrary mapping between bits and voltages, numbers and bits, etc. If you want to translate between genuinely different computational mechanisms, you might need a physical device to do so, and worrying about the translation being "computable" ceases to make sense. You need to worry about whether you can physically realize it.

• Thanks a lot for the answer. I was wondering if realizability theory also has something to say about 'simulation' - Turing machines can simulate other notions of computation, etc. and whether there are caveats like the fact that these simulation proofs must be constructive? Commented Jul 28 at 20:00
• I think people might study this directly at the PCA level, because there is no need for encoding arbitrary sets. As I recall, there is a notion of a map of PCAs that is like a simulation. E.G. such a map is a function $h : \cal A → B$ and element $a \in \cal B$ such that $h(f \cdot_{\mathcal{A}} x) = a \cdot_{\mathcal{B}} h(f) \cdot_{\mathcal{B}} h(x)$. So, $h$ is how to encode $\cal A$ terms in $\cal B$, and $a$ 'implements' the computational application of represented $\cal A$ elements in $\cal B$. For examples like Turing machines and lambda calculus (at least), it can all be constructive. Commented Jul 28 at 20:40
• I was wondering if we have 'a version' of the halting problem for all PCAs? For example, turing machines form a PCA, and so does python code. Can we prove the halting problem once at the PCA level? Commented Aug 8 at 0:37
• I don't know. It's not a trivial proposal, because there are differences in what the theorems look like at the PCA level. For Turing machines, the theorem says (roughly) there is no total $h \in \cal A$ such that $h \cdot e$ produces an encoded boolean indicating the behavior of $e$. However, this is not the interesting version for lambda terms, because for those $h$ is only able to apply $e$ to things, not inspect its internals like in the TM case. So a generic version would require encoding, and I'm not sure if the PCA structure is sufficient to define it, or if it is extra structure. Commented Aug 9 at 1:52

There is no and there cannot be any a formal definition of this. For example, take for $$D$$ the set of graphs. There are many possible encodings of a graph as a natural number: for example, you could write an adjacency list, or an adjacency matrix, as a binary string, then view that as an integer written in binary, or you could use the product of some primes selected among the $$n^2$$ first primes (where $$n$$ is the number of vertices) so that a prime being selected or not corresponds to there being an edge or not, or … The encodings I just gave are essentially equivalent, in the sense that if given a graph as a natural number written in any of these encodings, you could convert it to any of the other encodings. But you could also imagine silly encodings which break this property. For example, take a graph on $$n$$ vertices which is encoded by $$k$$ with one of the "normal" encodings, and encode it by $$2k+1$$ if the $$n$$-th Turing machine halts or $$2k$$ otherwise. Now, if you want to convert a graph from a standard representation to this representation, you have to solve the halting problem.

Think of it in this way: When writing math, we often leave things implicit if writing them out explicitly would just be tedious without bringing more clarity. For example, we say "let $$X$$ be a partially ordered set and let $$Y$$ be a totally ordered subset of $$X$$", where it is implicit that the order we put on $$Y$$ is the order induced by the order on $$X$$. In the same way, when we talk about computable functions taking or returning things like (finite) graphs, strings, rational numbers, etc., we are implicitly working with some encoding. We don't really need to specify it because all “reasonable” encodings are equivalent from the computability perspective. (They may not be equivalent from a complexity perspective, e.g., switching from adjacency lists to adjacency matrices and vice-versa has complexity implications. This doesn't matter for computability because it is not interested in efficiency.)

Your concern is also known as Montague's problem from his paper:

Towards a General Theory of Computability. Montague, R., Synthese, Vol. 12, No. 4 (Dec., 1960), pp. 429-438

The natural procedure is to restrict consideration to those correspondences which are in some sense 'effective', and hence to characterize a computable function on $$S$$ as a function $$f$$ such that, for some effective correspondence between $$S$$ and the set of natural numbers, the function induced by $$f$$ under this correspondence is computable in Turing's sense. But the notion of effectiveness remains to be analyzed, and would indeed seem to coincide with computability. p.431

There are several (philosophical/mathematical) positions in this debate (see also the keywords deviant encoding and acceptable notation). One problem with notation and encoding is that for some unacceptable notations or deviant encodings we can falsify some well-known theorems. Of course, this only means that our notations or encodings are unacceptable or deviant, not that our theorems don't hold. But it is not so easy to specify what we mean by unacceptable or non-deviant, and there is, in my opinion, no published work that answers these questions in a completely satisfactory way. For a recent summary of some positions and some references, see e.g:

The dependence of computability on numerical notations. Brauer, E., Synthese 198, 10485–10511 (2021). https://doi.org/10.1007/s11229-020-02732-x