nach oben

2020 | Buch

Kapitel lesen Erstes Kapitel lesen

Reversible Computation

12th International Conference, RC 2020, Oslo, Norway, July 9-10, 2020, Proceedings

herausgegeben von: Dr. Ivan Lanese, Mariusz Rawski

Verlag: Springer International Publishing

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This book constitutes the refereed proceedings of the 12th International Conference on Reversible Computation, RC 2020, held in Oslo, Norway, in July 2020. The 17 full papers included in this volume were carefully reviewed and selected from 22 submissions.

The papers are organized in the following topical sections: theory and foundation; programming languages; circuit synthesis; evaluation of circuit synthesis; and applications and implementations.

Inhaltsverzeichnis

Frontmatter

Invited Talks

Frontmatter

Inverse Problems, Constraint Satisfaction, Reversible Logic, Invertible Logic and Grover Quantum Oracles for Practical Problems

Abstract

It is well-known that the “Unsorted Database” quantum algorithm by Grover gives quadratic speedup to several important combinatorial and enumerative problems, such as: SAT, Graph Coloring, Maximum Cliques, Travelling Salesman and many others. Recently, quantum programming languages such as Quipper start to be used to design, verify and simulate practical quantum algorithms for important problems in Quantum Machine Learning. So far, however, no methodologies have been created to program Grover Oracles for particular classes of problems. In contrast, such methodologies have been already created for classical Constraint Satisfaction Problems. The goal of this invited talk is to show results of some initial research towards creating systematic methodologies to program quantum computers that solve search problems in Artificial Intelligence, Logic Design and Machine Learning. Our methods are based on unified oracle blocks for such problem representations as set partition algebra, cube calculus and optimal mappings. For instance, several important problems in CAD and Machine Learning can be solved using only two basic operations on set partitions; Π₁ ≤ Π₂ and Π₁ · Π₂. Moreover, building oracles is the fundamental concept in the new approach to solve CSP proposed here and based on Invertible Logic introduced recently by Supriyo Datta and his team.

Marek Perkowski

Foundations

Frontmatter

Reversible Occurrence Nets and Causal Reversible Prime Event Structures

Abstract

One of the well-known results in concurrency theory concerns the relationship between event structures and occurrence nets: an occurrence net can be associated with a prime event structure, and vice versa. More generally, the relationships between various forms of event structures and suitable forms of nets have been long established. Good examples are the close relationship between inhibitor event structures and inhibitor occurrence nets, or between asymmetric event structures and asymmetric occurrence nets. Several forms of event structures suited for the modelling of reversible computation have recently been developed; also a method for reversing occurrence nets has been proposed. This paper bridges the gap between reversible event structures and reversible nets. We introduce the notion of reversible occurrence net, which is a generalisation of the notion of reversible unfolding. We show that reversible occurrence nets correspond precisely to a subclass of reversible prime event structures, the causal reversible prime event structures.

Hernán Melgratti, Claudio Antares Mezzina, Iain Phillips, G. Michele Pinna, Irek Ulidowski

Involutory Turing Machines

Abstract

An involutory function, also called involution, is a function \(f\) that is its own inverse, i.e., \(f(f(x))=x\) holds whenever \(f(x)\) is defined. This paper presents a computational model of involution as a variant of Turing machines, called an involutory Turing machine. The computational model is shown to be complete in the sense that not only does an involutory Turing machine always compute an involution but also every involutory computable function can be computed by an involutory Turing machine. As any involution is injective (hence reversible), any involutory Turing machine forms a standard reversible Turing machine that is backward deterministic. Furthermore, the existence of a universal involutory Turing machine is shown under an appropriate redefinition of universality given by Axelsen and Glück for reversible Turing machines. This work is motivated by characterizing bidirectional transformation languages.

Keisuke Nakano

Event Structures for the Reversible Early Internal -Calculus

Abstract

The \(\pi \)-calculus is a widely used process calculus, which models communications between processes and allows the passing of communication links. Various operational semantics of the \(\pi \)-calculus have been proposed, which can be classified according to whether transitions are unlabelled (so-called reductions) or labelled. With labelled transitions, we can distinguish early and late semantics. The early version allows a process to receive names it already knows from the environment, while the late semantics and reduction semantics do not. All existing reversible versions of the \(\pi \)-calculus use reduction or late semantics, despite the early semantics of the (forward-only) \(\pi \)-calculus being more widely used than the late. We define \(\pi \)IH, the first reversible early \(\pi \)-calculus, and give it a denotational semantics in terms of reversible bundle event structures. The new calculus is a reversible form of the internal \(\pi \)-calculus, which is a subset of the \(\pi \)-calculus where every link sent by an output is private, yielding greater symmetry between inputs and outputs.

Eva Graversen, Iain Phillips, Nobuko Yoshida

Programming Languages

Frontmatter

Hermes: A Language for Light-Weight Encryption

Abstract

Hermes is a domain-specific language for writing light-weight encryption algorithms: It is reversible, so it is not necessary to write separate encryption and decryption procedures, and it avoids several types of side-channel attacks, both by ensuring no secret values are left in memory and by ensuring that operations on secret data spend time independent of the value of this data, thus preventing timing-based attacks. We show a complete formal specification of Hermes, argue absence of timing-based attacks (under reasonable assumptions), and compare implementations of well-known light-weight encryption algorithms in Hermes and C.

Torben Ægidius Mogensen

Reversible Programming Languages Capturing Complexity Classes

Abstract

We argue that there is a link between implicit computational complexity theory and the theory of reversible computation. We show that the complexity classes \(\text {ETIME}\) and \(\text {P}\) can be captured by inherently reversible programming languages.

Lars Kristiansen

On the Expressivity of Total Reversible Programming Languages

Abstract

SRL is a reversible programming language conceived as a restriction of imperative programming languages. Each SRL program that mentions n registers defines a bijection on n-tuples of integers. Despite its simplicity, SRL is strong enough to grasp a wide class of computable bijections and to rise non-trivial programming issues. We advance in the study of its expressivity. We show how to choose among alternative program-branches by checking if a given value is positive or negative. So, we answer some longstanding questions that the literature poses. In particular, we prove that SRL is primitive recursive complete and that its program equivalence is undecidable.

Armando B. Matos, Luca Paolini, Luca Roversi

Toward a Curry-Howard Equivalence for Linear, Reversible Computation

Work-in-Progress

Abstract

In this paper, we present a linear and reversible language with inductive and coinductive types, together with a Curry-Howard correspondence with the logic

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-52482-1_8/MediaObjects/501864_1_En_8_Figa_HTML.gif

: linear logic extended with least and greatest fixed points allowing inductive and coinductive statements. Linear, reversible computation makes an important sub-class of quantum computation without measurement. In the latter, the notion of purely quantum recursive type is not yet well understood. Moreover, models for reasoning about quantum algorithms only provide complex types for classical datatypes: there are usually no types for purely quantum objects beside tensors of quantum bits. This work is a first step towards understanding purely quantum recursive types.

Kostia Chardonnet, Alexis Saurin, Benoît Valiron

A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper

Abstract

We introduce dependently typed Proto-Quipper, or Proto-Quipper-D for short, an experimental quantum circuit programming language with linear dependent types. We give several examples to illustrate how linear dependent types can help in the construction of correct quantum circuits. Specifically, we show how dependent types enable programming families of circuits, and how dependent types solve the problem of type-safe uncomputation of garbage qubits. We also discuss other language features along the way.

Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger

Fractional Types

Expressive and Safe Space Management for Ancilla Bits

Abstract

In reversible computing, the management of space is subject to two broad classes of constraints. First, as with general-purpose computation, every allocation must be paired with a matching de-allocation. Second, space can only be safely de-allocated if its contents are restored to their initial value from allocation time. Generally speaking, the state of the art provides limited partial solutions, either leaving both constraints to programmers’ assertions or imposing a stack discipline to address the first constraint and leaving the second constraint to programmers’ assertions.

We propose a novel approach based on the idea of fractional types. As a simple intuitive example, allocation of a new boolean value initialized to

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-52482-1_10/MediaObjects/501864_1_En_10_Figa_HTML.gif

also creates a value

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-52482-1_10/501864_1_En_10_IEq1_HTML.gif

that can be thought of as a garbage collection (GC) process specialized to reclaim, and only reclaim, storage containing the value

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-52482-1_10/501864_1_En_10_IEq2_HTML.gif

. This GC process is a first-class entity that can be manipulated, decomposed into smaller processes and combined with other GC processes.

We formalize this idea in the context of a reversible language founded on type isomorphisms, prove its fundamental correctness properties, and illustrate its expressiveness using a wide variety of examples. The development is backed by a fully-formalized Agda implementation (https://github.com/DreamLinuxer/FracAncilla).

Chao-Hong Chen, Vikraman Choudhury, Jacques Carette, Amr Sabry

Circuit Synthesis

Frontmatter

Quantum CNOT Circuits Synthesis for NISQ Architectures Using the Syndrome Decoding Problem

Abstract

Current proposals for quantum compilers involve the synthesis and optimization of linear reversible circuits and among them CNOT circuits. This class of circuits represents a significant part of the cost of running an entire quantum circuit and therefore we aim at reducing the size of CNOT circuits. In this paper we present a new algorithm for the synthesis of CNOT circuits based on the solution of the syndrome decoding problem. Our method addresses the case of ideal hardware with an all-to-all qubit connectivity and the case of near-term quantum devices with restricted connectivity. Benchmarks show that our algorithm outperforms existing algorithms in both cases of partial and full connectivity.

Timothée Goubault de Brugière, Marc Baboulin, Benoît Valiron, Simon Martiel, Cyril Allouche

Maximality of Reversible Gate Sets

Abstract

We investigate collections of reversible gates closed under parallel and serial composition. In order to better understand the structure of these collections of reversible gates, we investigate the lattice of closed sets and the maximal members of this lattice, that is, collections that are not all gates, but the addition of a single new gate will allow us to construct all gates. We find the maximal closed sets over a finite alphabet.

We then extend to ancilla and borrow closure for reversible gates. Here we find some structural results, including some examples.

Tim Boykett

Search-Based Transformation Synthesis for 3-Valued Reversible Circuits

Abstract

A novel bounded search transformation-based synthesis approach is presented that finds a reversible circuit implementation for a given reversible function. Methods for simplifying the circuit post-synthesis are presented. Quantum implementation constraints are also considered. Experimental results for all 2-input 3-valued functions show the effectiveness of the new approaches compared to earlier transformation-based synthesis approaches. Other examples are given to show both the effectiveness and limitations of the new approach which point to a number of key areas for further research.

D. Michael Miller, Gerhard W. Dueck

Tools and Applications

Frontmatter

ReverCSP: Time-Travelling in CSP Computations

Abstract

This paper presents reverCSP, a tool to animate both forward and backward CSP computations. This ability to reverse computations can be done step by step or backtracking to a given desired state of interest. reverCSP allows us to reverse computations exactly in the same order in which they happened, or also in a causally-consistent way. Therefore, reverCSP is a tool that can be especially useful to comprehend, analyze, and debug computations. reverCSP is an open-source project publicly available for the community. We describe the tool and its functionality, and we provide implementation details so that it can be reimplemented for other languages.

Carlos Galindo, Naoki Nishida, Josep Silva, Salvador Tamarit

Reversible Computations in Logic Programming

Abstract

In this work, we say that a computation is reversible if one can find a procedure to undo the steps of a standard (or forward) computation in a deterministic way. While logic programs are often invertible (e.g., one can use the same predicate for adding and for subtracting natural numbers), computations are not reversible in the above sense. In this paper, we present a so-called Landauer embedding for SLD resolution, the operational principle of logic programs, so that it becomes reversible. A proof-of-concept implementation of a reversible debugger for Prolog that follows the ideas in this paper has been developed and is publicly available.

Germán Vidal

Towards a Formal Account for Software Transactional Memory

Abstract

Software transactional memory (STM) is a concurrency control mechanism for shared memory systems. It is opposite to the lock based mechanism, as it allows multiple processes to access the same set of variables in a concurrent way. Then according to the used policy, the effect of accessing to shared variables can be committed (hence, made permanent) or undone. In this paper, we define a formal framework for describing STMs and show how with a minor variation of the rules it is possible to model two common policies for STM: reader preference and writer preference.

Doriana Medić, Claudio Antares Mezzina, Iain Phillips, Nobuko Yoshida

Encoding Reversing Petri Nets in Answer Set Programming

Abstract

Reversing Petri nets (RPNs) have been proposed as a reversible approach to Petri nets, which allows the transitions of a net to be reversed. This work presents an approach towards an implementation of RPNs to support their simulation and analysis. Specifically, we define how to model RPNs in Answer Set Programming (ASP), a declarative programming framework with competitive solvers. We highlight how the methodology can be used to reason about the behavior of RPN models.

Yannis Dimopoulos, Eleftheria Kouppari, Anna Philippou, Kyriaki Psara

A Reversible Runtime Environment for Parallel Programs

Abstract

We present a reversible runtime environment for simple parallel programs and its experimental implementation. We aim at a light-weight implementation of the backtrack reversibility by the state-saving mechanism using stacks. We translate a program to a sequence of simple commands of an executable intermediate representation for reversible stack machines. The parallel composition is implemented using the multiprocessing feature of Python. While executing the commands, the stack machines collect the information for the backward execution in the auxiliary stacks for the update history of the variables and the history of jumps. The commands for the backward execution is obtained by reversing the commands for the forward execution by replacing each command with the corresponding reversed command. In the purpose of behaviour analysis with reversibility such as debugging, our runtime is more portable than the source-to-source translation of a high-level programming language.

Takashi Ikeda, Shoji Yuen

Backmatter

Titel: Reversible Computation
herausgegeben von: Dr. Ivan Lanese
Mariusz Rawski
Verlag: Springer International Publishing
Electronic ISBN: 978-3-030-52482-1
Print ISBN: 978-3-030-52481-4
DOI: https://doi.org/10.1007/978-3-030-52482-1