Condition/Decision Duality and the Internal Logic of Extensive Restriction Categories

TL;DR

This paper explores how extensive restriction categories model the dual nature of predicates in flowchart languages, revealing an internal logic that connects decisions with algebraic structures like De Morgan quasilattices and Boolean algebras.

Contribution

It introduces the concept that decisions in extensive restriction categories capture the condition/decision duality and establish an internal logic linking to weak Kleene and classical propositional logic.

Findings

Decisions form a De Morgan quasilattice related to weak Kleene logic.

Total decisions correspond to classical Boolean algebras.

Decisions as partial isomorphisms enable reversible logic models.

Abstract

In flowchart languages, predicates play an interesting double role. In the textual representation, they are often presented as conditions, i.e., expressions which are easily combined with other conditions (often via Boolean combinators) to form new conditions, though they only play a supporting role in aiding branching statements choose a branch to follow. On the other hand, in the graphical representation they are typically presented as decisions, intrinsically capable of directing control flow yet mostly oblivious to Boolean combination. While categorical treatments of flowchart languages are abundant, none of them provide a treatment of this dual nature of predicates. In the present paper, we argue that extensive restriction categories are precisely categories that capture such a condition/decision duality, by means of morphisms which, coincidentally, are also called decisions. Further, we show that having these categorical decisions amounts to having an internal logic: Analogous to how subobjects of an object in a topos form a Heyting algebra, we show that decisions on an object in an extensive restriction category form a De Morgan quasilattice, the algebraic structure associated with the (three-valued) weak Kleene logic $\mathbf{K}^w_3$. Full classical propositional logic can be recovered by restricting to total decisions, yielding extensive categories in the usual sense, and confirming (from a different direction) a result from effectus theory that predicates on objects in extensive categories form Boolean algebras. As an application, since (categorical) decisions are partial isomorphisms, this approach provides naturally reversible models of classical propositional logic and weak Kleene logic.