On reversible Turing machines and their function universality

We provide a treatment of the reversible Turing machines (RTMs) under a strict function semantics. Unlike many existing reversible computation models, we distinguish strictly between computing the function λ x.f(x) and computing the function λ x. (x, f(x)) , or other injective embeddings of f . We reinterpret and adapt a number of important foundational reversible computing results under this semantics. Unifying the results in a single model shows that, as expected (and previously claimed), the RTMs are robust and can compute exactly all injective computable functions. Because injectivity entails that the RTMs are not strictly Turing-complete w.r.t. functions, we use an appropriate alternative universality definition, and show how to derive universal RTMs (URTMs) from existing irreversible universal machines. We then proceed to construct a URTM from the ground up. This resulting machine is the first URTM which does not depend on a reversible simulation of an existing universal machine. The new construction has the advantage that the interpretive overhead of the URTM is limited to a (program dependent) constant factor. Another novelty is that the URTM can function as an inverse interpreter at no asymptotic cost.