Related papers: Reversible Computation in Term Rewriting
This paper is concerned with the expressivity and denotational semantics of a functional higher-order reversible programming language based on Theseus. In this language, pattern-matching is used to ensure the reversibility of functions. We…
We report on an inversion tool for a class of oriented conditional constructor term rewriting systems. Four well-behaved rule inverters ranging from trivial to full, partial and semi-inverters are included. Conditional term rewriting…
There is one, and only one way, consistent with fundamental physics, that the efficiency of general digital computation can continue increasing indefinitely, and that is to apply the principles of reversible computing. We need to begin…
Term rewriting has a significant presence in various areas, not least in automated theorem proving where it is used as a proof technique. Many theorem provers employ specialised proof tactics for rewriting. This results in an interleaving…
Reversible algorithms are algorithms in which each step represents a partial injective function; they are useful for performance optimization in reversible systems. In this study, using Janus, a reversible imperative high-level programming…
Reversible computation requires that intermediate data be explicitly undone rather than discarded. In quantum programming, this principle appears as uncomputation, usually treated as a technical cleanup mechanism. We instead present…
Janus is a paradigmatic example of a reversible programming language. Indeed, Janus programs can be executed backwards as well as forwards. However, its current small-step semantics (useful, e.g., for debugging or as a basis for extensions…
Deterministic synchronous systems consisting of two finite automata running in opposite directions on a shared read-only input are studied with respect to their ability to perform reversible computations, which means that the automata are…
Reactive languages are dedicated to the programming of systems which interact continuously and concurrently with their environment. Values take the form of unbounded streams modeling the (discrete) passing of time or the sequence of…
Reversible forms of computations are often interesting from an energy efficiency point of view. When the computation device in question is an automaton, it is known that the minimal reversible automaton recognizing a given language is not…
Reversible simulation of irreversible algorithms is analyzed in the stylized form of a `reversible' pebble game. While such simulations incur little overhead in additional computation time, they use a large amount of additional memory space…
Turing's famous 'machine' framework provides an intuitively clear conception of 'computing with real numbers'. A recursive counterexample to a theorem shows that the theorem does not hold when restricted to computable objects. These…
Algorithms are ways of mapping problems to solutions. An algorithm is invertible precisely when this mapping is injective, such that the initial problem can be uniquely inferred from its solution. While invertible algorithms can be…
In programming models with a reversible semantics, computational steps can be undone. This paper addresses the integration of reversible semantics into process languages for communication-centric systems equipped with behavioral types. In…
We explore several concepts for analyzing the intuitive notion of computational irreducibility and we propose a robust formal definition, first in the field of cellular automata and then in the general field of any computable function f…
To reversify an arbitrary sequential algorithm $A$, we gently instrument $A$ with bookkeeping machinery. The result is a step-for-step reversible algorithm that mimics $A$ step-for-step and stops exactly when $A$ does. Without loss of…
In the last decades, great achievements have been made in the development of computing machines. However, due to exponential growth of transistor density and in particular due to tremendously increasing power consumption, researchers expect…
The program Reverse Mathematics (RM for short) seeks to identify the axioms necessary to prove theorems of ordinary mathematics, usually working in the language of second-order arithmetic $L_{2}$. A major theme in RM is therefore the study…
Language models now provide an interface to express and often solve general problems in natural language, yet their ultimate computational capabilities remain a major topic of scientific debate. Unlike a formal computer, a language model is…
There are several forms of irreducibility in computing systems, ranging from undecidability to intractability to nonlinearity. This paper is an exploration of the conceptual issues that have arisen in the course of investigating speed-up…