Myhill isomorphism theorem

In computability theory the Myhill isomorphism theorem, named after John Myhill, provides a characterization for two numberings to induce the same notion of computability on a set.

It is reminiscent of the Schröder–Bernstein theorem in set theory and has been called a constructive version of it.

[1] A many-one reduction from a set

is a total computable function

Myhill's isomorphism theorem: Two sets

As a corollary, two total numberings are one-equivalent if and only if they are recursively isomorphic.

These functionals operate on computable partial functions, yielding numbers as results in cases of termination.

Notably, they adhere to a specific effectiveness criterion and exhibit continuity as functionals.

Considering the notion of the Myhill isomorphism, which states there exists a total computable bijection, which maps elements reducible to each other in both directions, given the functions are extensional, this one specifies the definition for recursive functionals.

be two sets and assume that there are injective, total computable functions

total computable and bijective such that for all

As in most proofs of the Schröder-Bernstein theorem, we use an analysis of the "chains" formed by successive applications of

between which we want to construct a bijection, and we consider an integer in the first copy, which is sent by

(These copies are blue and green in the pictures opposite.)

Depending on what happens when starting from some element and walking back on the chain, there are three possible types of chains: To construct a bijection in the context of the Schröder-Bernstein theorem, it suffices to pair the elements along each chain: on a one-sided chain, use

depending on the color of the first element, and on a two-sided chain or cycle, either one can be used.

For Myhill's theorem, this does not work since the constructed bijection need not be computable.

Instead, we build the bijection by successively pairing elements.

At each stage, we take the next unpaired element from the blue copy of

and pair it with some unpaired element of the green copy, then we do the same with the next unpaired element from the green copy.

This ensures that every element of both copies is paired at some point.

Suppose we want to pair some blue element (the case of a green element is symmetric).

to advance to the next green element in the chain, and repeat until an un-paired green element is found.