A structural approach to reversible computation
From MaRDI portal
Abstract: Reversibility is a key issue in the interface between computation and physics, and of growing importance as miniaturization progresses towards its physical limits. Most foundational work on reversible computing to date has focussed on simulations of low-level machine models. By contrast, we develop a more structural approach. We show how high-level functional programs can be mapped compositionally (i.e. in a syntax-directed fashion) into a simple kind of automata which are immediately seen to be reversible. The size of the automaton is linear in the size of the functional term. In mathematical terms, we are building a concrete model of functional computation. This construction stems directly from ideas arising in Geometry of Interaction and Linear Logic---but can be understood without any knowledge of these topics. In fact, it serves as an excellent introduction to them. At the same time, an interesting logical delineation between reversible and irreversible forms of computation emerges from our analysis.
Recommendations
- An axiomatic approach to reversible computation
- A Design-Based Model of Reversible Computation
- Foundations of generalized reversible computing
- Theory of reversible computing
- Reversible computation in term rewriting
- scientific article; zbMATH DE number 1189113
- Reversible computing from a programming language perspective
- Applying reversibility theory for the performance evaluation of reversible computations
- Reversibility in space-bounded computation
- Quantitative Analysis of Concurrent Reversible Computations
Cites work
- Applying dispersion correction to numerical approximations of the two‐dimensional wave equation ‐ eigenproblems
- Automatic Sequences
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Categories for Types
- Database query languages embedded in the typed lambda calculus
- Elementary complexity and geometry of interaction
- Full abstraction for PCF
- Games and full completeness for multiplicative linear logic
- Geometry of Interaction and linear combinatory algebras
- scientific article; zbMATH DE number 4179372 (Why is no real title available?)
- scientific article; zbMATH DE number 3875232 (Why is no real title available?)
- scientific article; zbMATH DE number 42059 (Why is no real title available?)
- scientific article; zbMATH DE number 49833 (Why is no real title available?)
- scientific article; zbMATH DE number 53661 (Why is no real title available?)
- scientific article; zbMATH DE number 4123722 (Why is no real title available?)
- scientific article; zbMATH DE number 1042221 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- scientific article; zbMATH DE number 1479606 (Why is no real title available?)
- scientific article; zbMATH DE number 1489627 (Why is no real title available?)
- scientific article; zbMATH DE number 1754652 (Why is no real title available?)
- scientific article; zbMATH DE number 1761434 (Why is no real title available?)
- scientific article; zbMATH DE number 194911 (Why is no real title available?)
- scientific article; zbMATH DE number 1373517 (Why is no real title available?)
- scientific article; zbMATH DE number 3993540 (Why is no real title available?)
- scientific article; zbMATH DE number 771635 (Why is no real title available?)
- scientific article; zbMATH DE number 786500 (Why is no real title available?)
- scientific article; zbMATH DE number 3310089 (Why is no real title available?)
- Irreversibility and Heat Generation in the Computing Process
- Linear logic
- Linear realizability and full completeness for typed lambda-calculi
- Logical Reversibility of Computation
- New foundations for the geometry of interaction
- Retracing some paths in process algebra
- Reversible, irreversible and optimal \(\lambda\)-machines
- Term Rewriting and All That
- The semantics and proof theory of linear logic
- Traced monoidal categories
- Unique decomposition categories, Geometry of Interaction and combinatory logic
Cited in
(40)- Reversible computation in term rewriting
- Quantum walks: a comprehensive review
- On one application of computations with oracle
- A unification of probabilistic choice within a design-based model of reversible computation
- The \(\aleph \)-calculus. A declarative model of reversible programming
- From reversible programs to univalent universes and back
- Reversible effects as inverse arrows
- From reversible programming languages to reversible metalanguages
- Reversing algebraic process calculi
- Reversibility in the higher-order \(\pi\)-calculus
- Reversible computing from a programming language perspective
- On reversible combinatory logic
- From reversible to irreversible computations
- Reversibility in space-bounded computation
- Information effects
- Quantitative Analysis of Concurrent Reversible Computations
- Generating reversible circuits from higher-order functional programs
- Isomorphic interpreters from logically reversible abstract machines
- Reversible Flowchart Languages and the Structured Reversible Program Theorem
- Periodicity and Immortality in Reversible Computing
- scientific article; zbMATH DE number 1189113 (Why is no real title available?)
- The monoidal structure of Turing machines
- Transactions on Computational Science XXIV. Special issue on reversible computing.
- lambda!-calculus, Intersection Types, and Involutions
- Abelian Invertible Automata
- Operational semantics of reversibility in process algebra
- A Design-Based Model of Reversible Computation
- Mathematics of Program Construction
- Musings around the geometry of interaction, and coherence
- Towards a taxonomy for reversible computation approaches
- Compact inverse categories
- Reversible simulation of space-bounded computations
- Principal types as partial involutions
- -symsym: an interactive tool for playing with involutions and types
- Two views on unification: terms as strategies
- Reversible computations are computations
- A class of reversible primitive recursive functions
- Fundamentals of reversible flowchart languages
- Reversible parallel computation: An evolving space-model
- Undoing the effects of action sequences
This page was built for publication: A structural approach to reversible computation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2581367)