Total and Partial Computation in Categorical Quantum Foundations

TL;DR

This paper establishes a fundamental categorical equivalence between effectuses for total computation and FinPACs with effects for partial computation, advancing the mathematical understanding of quantum effect logic.

Contribution

It introduces FinPACs with effects and proves their categorical equivalence with effectuses, linking total and partial quantum computation models.

Findings

Kleisli category of the lift monad on an effectus is a FinPAC with effects

The construction of FinPACs with effects from effectuses is always possible

State-and-effect triangles over FinPACs with effects are developed

Abstract

This paper uncovers the fundamental relationship between total and partial computation in the form of an equivalence of certain categories. This equivalence involves on the one hand effectuses, which are categories for total computation, introduced by Jacobs for the study of quantum/effect logic. On the other hand, it involves what we call FinPACs with effects; they are finitely partially additive categories equipped with effect algebra structures, serving as categories for partial computation. It turns out that the Kleisli category of the lift monad (-)+1 on an effectus is always a FinPAC with effects, and this construction gives rise to the equivalence. Additionally, state-and-effect triangles over FinPACs with effects are presented.