Table of Contents
Fetching ...

A Compositional Account of Generalized Reversible Computing

Clémence Chanavat, Priyaa Varshinee Srinivasan

TL;DR

The paper addresses how to compose generalized reversible computing by connecting physical processes and computational transformations in a probabilistic, category-theoretic setting. It introduces partitioned sets, subdistribution matrices, and the aggregation functor $\mathsf{Q}$ to relate physical and computational levels via Kleisli categories of the subdistribution monad. The work defines physical, computational, and non-computational entropies and proves a fundamental theorem that physical reversibility (non-entropy-ejection) corresponds to conditional computational reversibility under $\mathsf{Q}$, within resource theories. The mathematical backend using monads and monoidal structures supports a modular, compositional framework with broad links to Landauer's principle and generalized reversible computing.

Abstract

We develop a compositional framework for generalized reversible computing using copy-discard categories and resource theories. We introduce partitioned matrices between partitioned sets as subdistribution matrices which preserve the equivalence relation of its domain. We model computational and physical transformations as subdistribution matrices over the category of sets and partitioned matrices on partitioned sets, respectively. We show that the interactions between the physical and computational transformations are governed by an aggregation functor whose functoriality and monoidality we deduce from general principles of the formal theory of monads. We study the associated copy-discard structures, in particular, general conditions for determinism and partial invertibility. We then define several notions of entropies that we use to state and prove the fundamental theorem of generalized reversible computing.

A Compositional Account of Generalized Reversible Computing

TL;DR

The paper addresses how to compose generalized reversible computing by connecting physical processes and computational transformations in a probabilistic, category-theoretic setting. It introduces partitioned sets, subdistribution matrices, and the aggregation functor to relate physical and computational levels via Kleisli categories of the subdistribution monad. The work defines physical, computational, and non-computational entropies and proves a fundamental theorem that physical reversibility (non-entropy-ejection) corresponds to conditional computational reversibility under , within resource theories. The mathematical backend using monads and monoidal structures supports a modular, compositional framework with broad links to Landauer's principle and generalized reversible computing.

Abstract

We develop a compositional framework for generalized reversible computing using copy-discard categories and resource theories. We introduce partitioned matrices between partitioned sets as subdistribution matrices which preserve the equivalence relation of its domain. We model computational and physical transformations as subdistribution matrices over the category of sets and partitioned matrices on partitioned sets, respectively. We show that the interactions between the physical and computational transformations are governed by an aggregation functor whose functoriality and monoidality we deduce from general principles of the formal theory of monads. We study the associated copy-discard structures, in particular, general conditions for determinism and partial invertibility. We then define several notions of entropies that we use to state and prove the fundamental theorem of generalized reversible computing.

Paper Structure

This paper contains 18 sections, 44 theorems, 97 equations, 1 figure.

Key Result

Corollary 1

The construction sending a partitioned matrix $M$ to its aggregated matrix $\mathsf{Q} M$ defines a strong monoidal functor

Figures (1)

  • Figure 1: Schematic for functor of resource theories

Theorems & Definitions (98)

  • Corollary
  • Theorem
  • Lemma 2.4
  • proof
  • Lemma 2.6
  • proof
  • Lemma 2.7
  • proof
  • Lemma 2.8
  • proof
  • ...and 88 more