Identities in modular arithmetic from reversible coherence operations

TL;DR

This paper explores how structural isomorphisms in categorical models of reversible logic encode non-trivial identities in modular arithmetic, revealing computational content often overlooked in coherence theorems.

Contribution

It demonstrates that categorical coherence isomorphisms in reversible computation models encode significant modular arithmetic identities, challenging the common practice of treating them as trivial.

Findings

Structural isomorphisms manipulate modulo classes of natural numbers.

Coherence properties correspond to infinite families of modular identities.

Proving these identities without categorical coherence theory is difficult.

Abstract

This paper investigates some issues arising in categorical models of reversible logic and computation. Our claim is that the structural (coherence) isomorphisms of these categorical models, although generally overlooked, have decidedly non-trivial computational content. The theory of categorical coherence is based around reversible structural operations (canonical isomorphisms) that allow for transformations between related, but distinct, mathematical structures. A number of coherence theorems are commonly used to treat these transformations as though they are identity maps, from which point onwards they play no part in computational models. We simply wish to point out that doing so overlooks some significant computational content. We give a single example (taken from an uncountably infinite set of similar examples, and based on structures used in models of reversible logic and computation) of a category whose structural isomorphisms manipulate modulo classes of natural numbers. We demonstrate that the coherence properties that usually allow us to ignore these structural isomorphisms in fact correspond to countably infinite families of non-trivial identities in modular arithmetic. Further, proving the correctness of these equalities without recourse to the theory of categorical coherence appears to be a hard task.