Finite proofs capture compact quantitative equational theories categorically
Compact Quantitative Equational Theories as Monad Restrictions
Logic in Computer Science
Summary
Mathematical proofs in a certain kind of algebra can sometimes be infinitely long because they use rules that allow endless steps. The authors study which theories can be proven using only finite-length proofs, calling these compact. They show that being compact is the same as a special way to limit a mathematical construction called a monad. This gives a new perspective connecting logic and category theory.
What this means in practice
- •For programming language designers: Determine when program properties can be fully verified using finite proof techniques via categorical methods.
- •For formal verification engineers: Use monad restriction concepts to identify finitely checkable properties in quantitative systems and reduce verification complexity.
A theory result. No direct application yet.
Authors
Matteo Mio, Colin Riba
Abstract
Proofs in quantitative algebra are, generally, infinite objects due to the presence of infinitary rules in the deductive apparatus. A quantitative equational theory is called compact if all its consequences are derivable by means of finite proofs, that is, proofs not using any instances of the infinitary rules. This definition is purely logical. In this work we give an equivalent, but categorical, characterisation based on the notion of monad restriction.