Multicategorical Semantics for Untyped Effects

TL;DR

This paper develops a categorical semantics framework for untyped effectful computations using Freyd operads and PROPs, addressing the challenge of substitution in effectful languages.

Contribution

It introduces Freyd operads and a novel categorical construction to model untyped effectful computations, enabling soundness and completeness proofs.

Findings

Constructed a Freyd-multicategorical setting for substitution

Proved the representability and adjointness of the construction

Interpreted untyped lambda calculus with effects in this framework

Abstract

Completeness proofs in categorical semantics usually proceed by building a syntactic category whose composition is given by substitution. For untyped effectful Call-by-Value languages, this runs into a basic obstacle: there is no canonical notion of simultaneous substitution of computations, since evaluation order is semantically meaningful. We address this by taking single computation substitutions, that is, binding steps, as primitive, and representing computation substitution by finite sequential lists composed by concatenation. We formalize this idea in a one-object Freyd-multicategorical setting. We introduce Freyd operads, separating a cartesian operad of values from a symmetric Ren-cartesian preoperad of computations, connected by a Freyd functor, and from any Freyd operad we construct a corresponding Freyd PROP of substitutions. We prove that this construction is representable and, in the strict one-object setting, left adjoint to restriction to codomain 1. Using the induced term model, we interpret untyped computational lambda-calculus with procedures and higher-order functions in weakly closed Freyd operads, and prove soundness, initiality, and completeness. This yields a categorical semantics tailored to untyped effectful computation and broad enough to encompass realizability-oriented models such as monadic combinatory algebras.