I'm interested in the concept of "r-Turing completeness", as defined by Axelsen and Glück (2011). A system is r-Turing complete if it can compute the same set of functions as a reversible Turing machine, without producing any "garbage" data. This is the same as being able to compute every function that is both (a) computable, and (b) injective.
I would like to computationally explore the space of computable injective functions. In order to do this I'm looking for the "most minimal" reversible programming language --- something that can play the equivalent role for r-Turing computability that the lambda calculus plays for Turing computability.
I know that there are many reversible languages that people have developed and proven to be r-Turing complete. However, these are being developed with practical applications in mind, and so their authors concentrate on giving them expressive features rather than making them minimal.
Does anyone know if such a minimal invertible language has been described, or whether there is any research in such a direction? I'm fairly new to the literature on this topic, so I could easily have missed it. Alternatively, does anyone have any insight into how such a language could be created?
Below is a summary of what I'm looking for. I do not know whether it can be created by modifying the lambda calculus itself, or whether a completely different type of language would have to be used.
- r-Turing complete language - computes all computable invertible functions, and can only computes invertible functions
- Syntax and semantics as minimal as possible. (E.g. Lambda calculus has only function definitions and applications, and nothing else.) It isn't necessary for the syntax or semantics to be related to those of the lambda calculus, although they could be.
- Program = data. That is, the programs operate on expressions rather than any other kind of data. This guarantees that a program's output can always be interpreted as a program. This probably implies that it has to be a functional rather than an imperative style of language.
- There is some systematic way to convert a program into its inverse, which doesn't involve substantially more computation than that involved in actually performing the inverse computation. (Not all invertible languages have this property, but some do.)
I should emphasise that Axelsen and Glück's approach to reversible computing is quite different from the well-known approach due to Bennett, where an (in general non-invertible) program is made invertible by returning some information about the computation's history along with the output. r-Turing completeness is about being able to compute injective functions without any additional output. There are several things called variations of "reversible lambda calculus" that are reversible in Bennet's sense - those are not what I'm looking for.
