Reversible Computation : 14th International Conference, RC 2022, Urbino, Italy, July 5–6, 2022, Proceedings

This book constitutes the refereed proceedings of the 14th International Conference on Reversible Computation, RC 2022, which was held in Urbino, Italy, during July 5-6, 2021. The 10 full papers and 6 short papers included in this book were carefully reviewed and selected from 20 submissions. They were organized in topical sections named: Reversible and Quantum Circuits; Applications of quantum Computing; Foundations and Applications. Preface Organization Contents Reversible and Quantum Circuits Reversible Computation in Integrated Photonics 1 Introduction 2 Building Blocks 3 Properties 4 Synthesis in Case w=2u 5 Comparison with Quantum Computation 6 A Finite Library 7 Conclusion References Optimization of Quantum Boolean Circuits by Relative-Phase Toffoli Gates 1 Introduction 2 Preliminary 2.1 Quantum Boolean Circuits 2.2 T Gates and S Gates 2.3 Relative-Phase Toffoli Gates (RTOFs) 3 Optimization By Using RTOFs 3.1 Phase Functions 3.2 Erasing Relative Phases 4 Conclusion References Constructing All Qutrit Controlled Clifford+T gates in Clifford+T 1 Introduction 2 Preliminaries 2.1 The Clifford+T gate set 2.2 Controlled Unitaries 3 Adding Controls to Clifford+T Gates 3.1 Permutation Gates with Two Controls 3.2 Permutation Gates with Any Number of Controls 3.3 Building Multiple-Controlled Clifford+T gates 3.4 The Main Theorem 4 Building Trit Permutation Gates in Clifford+T 5 Conclusion References Fast Control for Reversible Processors 1 Introduction 2 The Control Mechanism in PISA and BobISA 2.1 Procedure Calls 3 Making the Control Step More Efficient 3.1 Optimising Jumps 3.2 Making Fall Through More Efficient 4 Gate-Level Realisation 4.1 Making DR Explicit 5 Summary and Discussion 5.1 Future Work References Designing a Reversible Stack Machine 1 Introduction 2 Stack-based Architecture Design 3 Reversible Arithmetic 4 Reversible Control Flow 5 Encoding and Executing Instructions 6 Current Progress and Future Work References Applications of Quantum Computing Directed Graph Encoding in Quantum Computing Supporting Edge-Failures 1 Introduction 2 Preliminaries 2.1 Quantum Computing 2.2 Graph Theory 2.3 Quantum Random Walks 3 Unitary Matrix of an Eulerian Multigraph 3.1 From a Graph to Its Line 3.2 Construction of the Unitary Matrix 4 Embedding Multigraphs into Eulerian Ones 5 The Quantum Circuit: With and Without Projections 6 Edges/Nodes Failures 7 Comparisons and Examples 7.1 Continuous Time Walk from ch6minello2019can 7.2 Discrete Time Walk from ch6QuantumWalksDistributions 7.3 Our Method 7.4 Random Thoughts on Random Walks 8 Conclusions References Reordering Decision Diagrams for Quantum Computing Is Harder Than You Might Think 1 Introduction 2 Background 2.1 Quantum Computing 2.2 Decision Diagrams 3 Reordering Decision Diagrams 4 Challenges in Reordering Decision Diagrams for Quantum Computing 4.1 Floating-Point Accuracy 4.2 Node Collisions 4.3 Normalization 5 Case Study 6 Conclusions References Foundations and Applications Certifying Algorithms and Relevant Properties of Reversible Primitive Permutations with Lean 1 Introduction 2 Reversible Primitive Permutations (RPP) 2.1 The Functions |inv f| and |f| are each other inverse 2.2 How |rpp| differs from original RPP 3 RPP Algorithms Central to Our Proofs 4 Proving in Lean that RPP is PRF-complete 4.1 Primitive Recursive Functions |primrec| of mathlib 4.2 The Main Point of the Proof 5 Conclusion and Developments References Algeo: An Algebraic Approach to Reversibility 1 Introduction 2 Algeo by Example 3 Syntax and Semantics 3.1 Type System 3.2 Axiomatic Semantics 3.3 Justification of the Semantics 3.4 Derived Equations and Evaluation 3.5 Relation to Linear Algebra 4 Applications 5 Related Work 6 Conclusion and Future Work References Concurrencies in Reversible Concurrent Calculi 1 Introduction: Reversibility, Concurrency–Interplays 2 Finite and Reversible Process Calculi 2.1 Finite, Forward-Only CCS 2.2 CCSK: A ``Keyed'' Reversible Concurrent Calculus 3 A New Causal Semantics for CCSK 3.1 Proved Labeled Transition System for CCSK 3.2 Diamonds and Squares: Concurrency in Action 3.3 Causal Consistency 4 Structural Congruence, Universality and Other Criteria 5 Conclusion and Perspectives References The -Calculus 1 Introduction 2 Examples 3 Definition 4 Semantics 5 Discussion and Future Work References Formal Translation from Reversing Petri Nets to Coloured Petri Nets 1 Introduction 2 Definition of Reversing Petri Nets 3 Transformation and Software 4 Conclusions A Explanations of Individual Elements of a Coloured Perti Net Based on Low-Level Reversing Petri Net References Reversibility in Erlang: Imperative Constructs 1 Introduction 2 Background 3 Reversible Erlang with Imperative Primitives 3.1 Semantics of Imperative Features 3.2 Properties 4 CauDEr with Imperative Primitives 5 Conclusion, Related and Future Work References A Reversible Debugger for Imperative Parallel Programs with Contracts 1 Introduction 2 Reversible Runtime for Parallel Programs 3 Reversible Debugging with Contract Annotations 4 Reversible Debugger with Contracts 5 Concluding Remarks References Towards Causal-Consistent Reversibility of Imperative Concurrent Programs 1 Introduction 2 Backtracking Reversibility 2.1 Proposed Relaxations of Backtracking 3 Towards Causal-Consistent Reversibility 3.1 Data Race and Causal Independence 4 Conclusion and Future Work A Causally Independent Interleavings B Local Variables References Optimizing Reversible Programs 1 Introduction 2 The Compiler rc3 3 Optimizations 3.1 Procedure Inlining 3.2 Local Common-Subexpression Elimination 3.3 Constant Propagation and Folding 3.4 Dead-Code Elimination 4 Example 5 Conclusions and Outlook References Author Index