Beyond Monads and Biproducts: A Uniform Interpretation of Parallelism in Intuitionistic Logic

TL;DR

This paper introduces a minimal, unified framework for modeling parallelism and algebraic effects in intuitionistic logic without relying on monads or biproducts, using novel semantics based on magmas and set-theoretic constructions.

Contribution

It proposes two lambda calculi extending intuitionistic logic and provides a new set-theoretic interpretation for disjunction, enabling models without coproducts.

Findings

Sound and adequate models for the calculi are constructed.

A novel set-theoretic interpretation of disjunction is developed.

The framework offers a lightweight alternative to monads and biproducts.

Abstract

Traditional approaches to modelling parallelism and algebraic structure in lambda calculi often rely on monads$\unicode{x2013}$as in Moggi's framework$\unicode{x2013}$or on rich categorical structures such as biproducts$\unicode{x2013}$as used in certain models of linear logic. In this work, we propose a minimal alternative that captures both parallelism and weighted parallelism (linear combinations) within the setting of intuitionistic propositional logic, without resorting to monads or assuming the existence of biproducts. We introduce two lambda calculi: a parallel lambda calculus and an algebraic lambda calculus, both extending full propositional intuitionistic logic. Their semantics are given in two categories: ${\mathbf{Mag}_{\mathbf{Set}}}$, whose objects are magmas and arrows are functions in $\mathbf{Set}$; and ${\mathbf{AMag}^{\mathcal{S}}_{\mathbf{Set}}}$, whose objects are action magmas. The key technical challenge addressed is the interpretation of disjunction in the presence of parallel and algebraic operators. Since the usual coproduct structure is unavailable in our minimal setting, we propose a novel set-theoretic interpretation based on the union of the disjoint union and the Cartesian product. This allows for the construction of sound and adequate models for both calculi. Our results offer a unified and structurally lightweight framework for modelling parallelism and algebraic effects in intuitionistic logic, opening the way to alternatives beyond the traditional monadic or linear logic approaches.