A structural approach to reversible computation
From MaRDI portal
Publication:2581367
DOI10.1016/J.TCS.2005.07.002zbMATH Open1081.68019arXiv1111.7154OpenAlexW2015392385WikidataQ57006662 ScholiaQ57006662MaRDI QIDQ2581367FDOQ2581367
Authors: Samson Abramsky 
Publication date: 10 January 2006
Published in: Theoretical Computer Science (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1111.7154
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
- The semantics and proof theory of linear logic
- Title not available (Why is that?)
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Reversible, irreversible and optimal \(\lambda\)-machines
- Full abstraction for PCF
- Irreversibility and Heat Generation in the Computing Process
- Title not available (Why is that?)
- Title not available (Why is that?)
- Categories for Types
- Automatic Sequences
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Logical Reversibility of Computation
- Linear logic
- Elementary complexity and geometry of interaction
- Title not available (Why is that?)
- Geometry of Interaction and linear combinatory algebras
- Traced monoidal categories
- Term Rewriting and All That
- Retracing some paths in process algebra
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Linear realizability and full completeness for typed lambda-calculi
- Title not available (Why is that?)
- Games and full completeness for multiplicative linear logic
- Title not available (Why is that?)
- Title not available (Why is that?)
- Database query languages embedded in the typed lambda calculus
- Title not available (Why is that?)
- Title not available (Why is that?)
- New foundations for the geometry of interaction
- Applying dispersion correction to numerical approximations of the two‐dimensional wave equation ‐ eigenproblems
- Unique decomposition categories, Geometry of Interaction and combinatory logic
- Title not available (Why is that?)
Cited In (36)
- Musings around the geometry of interaction, and coherence
- Reversibility in the higher-order \(\pi\)-calculus
- Mathematics of Program Construction
- Towards a taxonomy for reversible computation approaches
- Abelian Invertible Automata
- Reversible parallel computation: An evolving space-model
- Isomorphic interpreters from logically reversible abstract machines
- The monoidal structure of Turing machines
- From reversible programs to univalent universes and back
- lambda!-calculus, Intersection Types, and Involutions
- Reversible computing from a programming language perspective
- Reversible effects as inverse arrows
- Periodicity and Immortality in Reversible Computing
- Quantum walks: a comprehensive review
- From reversible programming languages to reversible metalanguages
- Compact inverse categories
- A class of reversible primitive recursive functions
- Generating reversible circuits from higher-order functional programs
- Quantitative Analysis of Concurrent Reversible Computations
- Fundamentals of reversible flowchart languages
- Reversing algebraic process calculi
- On one application of computations with oracle
- Information effects
- Title not available (Why is that?)
- On reversible combinatory logic
- Reversible computation in term rewriting
- A Design-Based Model of Reversible Computation
- The \(\aleph \)-calculus. A declarative model of reversible programming
- Transactions on Computational Science XXIV. Special issue on reversible computing.
- Reversible Flowchart Languages and the Structured Reversible Program Theorem
- From reversible to irreversible computations
- A unification of probabilistic choice within a design-based model of reversible computation
- Reversibility in space-bounded computation
- Operational semantics of reversibility in process algebra
- Undoing the effects of action sequences
- Reversible simulation of space-bounded computations
Uses Software
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)
