# A programming language that can only implement computable bijective functions?

Are there programming languages(or logic) that can implement(or express) a function $f:\mathbb{N}\to \mathbb{N}$ if and only if $f$ is a computable bijective functions?

-
Somebody proved to me that it is impossible to create a language that accepts only terminating programs. Since you question is pretty similar, I guess no. – FUZxxl Nov 22 '12 at 21:34
It seems unlikely there would be such a programming language, I guess you could try to enforce it, but then you wouldn't be able to do simple things like sorting, at least not without it becoming horribly complex and painful. – Luke Mathieson Nov 22 '12 at 21:56
@FUZxxl This doesn't capture many terminating programs, In fact even the function f(x)=1 is impossible to express in this language. Also I have a feeling this kind of functions are captured by total functional programming since every function is a total function. – Chao Xu Nov 22 '12 at 22:04
@FUZxxl, I don't think that's right, but such a language would have to be limited. For example, a language that was equivalent to Finite deterministic automata would be guaranteed to terminate, but would be extremely limited in what it could calculate. – jmite Nov 23 '12 at 5:10
@FUZxxl, the details of such a statement are important. It is easy to design a programming language in which every program terminates. It is a different matter to design a language which we can express every computable function. – Vijay D Nov 23 '12 at 8:08

There is no such language.

However, have a look at Boomerang. It is a language for writing bijections between strings. I do not know how wide a class of maps is expressible in it, but I am sure you can find out if you search a bit.

It is reasonable to require of a programming language that the set of valid programs be recognizable by an interpreter or a compiler, i.e., that it be a computably enumerable set. Suppose then we had a programming language whose set of valid programs were computably enumerable and which implemented precisely all computable bijections $\mathbb{N} \to \mathbb{N}$. That would imply that we can computably enumerate all computable bijections (simply enumerate all valid programs in this programming language), but this is impossible by the next theorem.

Theorem: Suppose $f_0, f_1, f_2, \ldots$ is a computable sequence of computable bijections. Then there is a computable bijection which is not in the sequence.

Proof. We construct a bijection $g : \mathbb{N} \to \mathbb{N}$ as follows. To define the values $g(2 k)$ and $g(2 k + 1)$, we look at $f_k(2 k)$:

• if $f_k(2 k) = 2 k$ then set $g(2 k) = 2 k + 1$ and $g(2 k + 1) = 2 k$,
• if $f_k(2 k) \neq 2 k$ then set $g(2 k) = 2 k$ and $g(2 k + 1) = 2 k + 1$.

Clearly, for every $k \in \mathbb{N}$, $g$ is different from $f_k$ because $g(2 k) \neq f_k(2 k)$. Furthermore, $g$ is computable and it is a bijection because it is its own inverse. QED.

-
Why do you even need this $2k$ and $2k+1$ trick? Using $g(k)=f_k(k)+1$ should suffice. – FUZxxl Nov 23 '12 at 7:11
@FUZxxl: if you use $f_k(k)+1$ the resulting function is not surjective – Vor Nov 23 '12 at 8:35
You need to make sure that $g$ is bijective. – Andrej Bauer Nov 23 '12 at 15:38
The initial statement is wrong, there are many such languages in the literature. – Nathaniel Feb 2 '14 at 9:47
On the other hand your proof seems legit. Perhaps I'm confused somehow. I need to read Axelsen and Glück's paper (see my answer) carefully to figure out what's going on here. – Nathaniel Feb 2 '14 at 10:07