A programming language that can only implement computable bijective functions?

Question

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?

• fuz: 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.
• Luke Mathieson: 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.
• Chao Xu: @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.
• Joey Eremondi: @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.
• Vijay D: @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.

Answer 1

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.

• fuz: Why do you even need this 2ドルk$ and 2ドルk+1$ trick? Using $g(k)=f_k(k)+1$ should suffice.
• Vor: @FUZxxl: if you use $f_k(k)+1$ the resulting function is not surjective
• Andrej Bauer: You need to make sure that $g$ is bijective.
• N. Virgo: The initial statement is wrong, there are many such languages in the literature.
• N. Virgo: 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.