pith. sign in

arxiv: 2605.21337 · v1 · pith:KFIQZLFOnew · submitted 2026-05-20 · 💻 cs.PL · math.CT

Multicategorical Semantics for Untyped Effects

Ariel Grunfeld , Liron Cohen This is my paper

Pith reviewed 2026-05-21 03:16 UTC · model grok-4.3

classification 💻 cs.PL math.CT
keywords Freyd operadscategorical semanticsuntyped lambda calculuseffectful computationsubstitutionsoundnesscompletenessFreyd PROP
0
0 comments X

The pith

Freyd operads interpret untyped effectful lambda calculus with soundness and completeness

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper tackles the obstacle that simultaneous substitution of computations lacks a canonical form in untyped effectful call-by-value languages, because evaluation order carries semantic weight. It treats single computation substitutions as the basic building blocks and represents them via finite sequential lists joined by concatenation. This idea is encoded in a one-object Freyd-multicategorical framework by introducing Freyd operads that keep a cartesian operad of values separate from a symmetric Ren-cartesian preoperad of computations, linked by a Freyd functor. From any such operad the authors build a corresponding Freyd PROP of substitutions and prove the construction is representable and left adjoint in the strict one-object case. The resulting term model then supplies an interpretation of the untyped computational lambda-calculus with procedures and higher-order functions inside weakly closed Freyd operads, together with proofs of soundness, initiality, and completeness.

Core claim

Freyd operads are defined as a cartesian operad of values, a symmetric Ren-cartesian preoperad of computations, and a Freyd functor between them. Any Freyd operad induces a Freyd PROP of substitutions that is representable and, in the strict one-object setting, left adjoint to restriction to codomain 1. The induced term model interprets the untyped computational lambda-calculus with procedures and higher-order functions in weakly closed Freyd operads, establishing soundness, initiality, and completeness. The resulting semantics applies to untyped effectful computation and includes realizability-oriented models such as monadic combinatory algebras.

What carries the argument

Freyd operads consisting of a cartesian operad of values, a symmetric Ren-cartesian preoperad of computations connected by a Freyd functor, together with the induced Freyd PROP of substitutions

If this is right

  • The untyped computational lambda-calculus with procedures and higher-order functions receives a sound interpretation in weakly closed Freyd operads.
  • Initiality and completeness hold for the induced term model.
  • The semantics covers realizability-oriented models such as monadic combinatory algebras.
  • Sequential single substitutions suffice to capture the semantic importance of evaluation order.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same single-substitution technique could be adapted to typed effectful calculi by enriching the value operad with types.
  • Concrete instances of weakly closed Freyd operads built from known monads would supply explicit models against which completeness can be checked directly.
  • The left-adjoint property may link this construction to other universal properties in the theory of operads and PROPs.

Load-bearing premise

The construction from any Freyd operad to the corresponding Freyd PROP of substitutions is representable and, in the strict one-object setting, left adjoint to restriction to codomain 1.

What would settle it

A concrete Freyd operad in which the substitution PROP construction fails to be representable or in which the term-model interpretation of the computational lambda-calculus fails to be complete.

Figures

Figures reproduced from arXiv: 2605.21337 by Ariel Grunfeld, Liron Cohen.

Figure 1
Figure 1. Figure 1: Syntax and well-formedness rules for λml∗. up to α equivalence. All substitutions are capture avoiding, and we freely rename bound variables to avoid capture. The syntax of λml∗ is given in the top part of [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Equational theory of λml∗. structure via a functor J : V → C that embeds pure maps as central morphisms. Throughout, a natural number n is read as a context of n variables. A morphism m → n should be read as an n-tuple of effectful bindings that may use m variables as input. With this convention, addition m + n represents context concatenation, and whiskering by k on the left or right extends a morphism wi… view at source ↗
Figure 3
Figure 3. Figure 3: Rules for the equivalence relation on pre-substitutions. [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 3 minor

Summary. The paper claims to address the obstacle of defining simultaneous substitution for computations in untyped effectful Call-by-Value languages (where evaluation order is semantically meaningful) by taking single computation substitutions as primitive and representing them via finite sequential lists composed by concatenation. It introduces Freyd operads (separating a cartesian operad of values from a symmetric Ren-cartesian preoperad of computations via a Freyd functor), constructs a corresponding Freyd PROP of substitutions from any Freyd operad, proves that this construction is representable and (in the strict one-object setting) left adjoint to restriction to codomain 1, and uses the induced term model to interpret the untyped computational lambda-calculus with procedures and higher-order functions in weakly closed Freyd operads while proving soundness, initiality, and completeness. This yields a categorical semantics broad enough to include realizability-oriented models such as monadic combinatory algebras.

Significance. If the central claims hold, the work supplies a multicategorical semantics tailored to untyped effectful computation, directly tackling the lack of a canonical notion of simultaneous substitution. The explicit use of finite sequential lists for substitutions and the adjointness result in the strict one-object case provide a concrete, falsifiable foundation for the term model. The framework's ability to encompass realizability models is a notable strength that extends its applicability beyond standard monadic or Freyd-category approaches.

major comments (1)
  1. [§4.1] §4.1: The explicit construction of the Freyd PROP of substitutions via finite sequential lists for single substitutions is load-bearing for the induced term model used in the soundness and completeness proofs; the representability claim should be verified to confirm that the concatenation operation preserves the required Freyd functoriality without introducing implicit choices of evaluation order.
minor comments (3)
  1. [Abstract] Abstract and §2: The term 'Ren-cartesian preoperad' appears without an immediate definition or forward reference; adding a one-sentence gloss or citation to the multicategory literature would improve readability for readers outside the immediate subfield.
  2. [§5.2] §5.2: The statement of the initiality theorem could explicitly note how the weakly closed structure interacts with procedure bindings to avoid any appearance of circularity in the untyped higher-order case.
  3. Notation throughout: The use of sequential lists for substitutions is clear in the main text, but a small table summarizing the composition rules (concatenation vs. standard substitution) in an early section would aid comparison with classical syntactic categories.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript and for the constructive comment. We respond to the major comment below.

read point-by-point responses

  1. Referee: [§4.1] §4.1: The explicit construction of the Freyd PROP of substitutions via finite sequential lists for single substitutions is load-bearing for the induced term model used in the soundness and completeness proofs; the representability claim should be verified to confirm that the concatenation operation preserves the required Freyd functoriality without introducing implicit choices of evaluation order.

    Authors: We appreciate the referee drawing attention to this foundational aspect of the construction. In the explicit definition of the Freyd PROP of substitutions (Section 4.1), morphisms are finite ordered lists of computations, with composition given by list concatenation. The representability proof establishes that this yields a well-defined Freyd PROP by verifying that concatenation is associative and unital and that it commutes appropriately with the Freyd functor from the cartesian operad of values. Because the lists are strictly ordered sequences, the evaluation order is recorded explicitly by the list structure itself; no additional choice of order is introduced by the concatenation operation. The symmetric Ren-cartesian structure on the computation preoperad ensures functoriality is preserved by construction. To address the request for explicit verification, we will add a short clarifying paragraph immediately after the definition of the PROP in the revised version. revision: partial

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained via explicit constructions and proofs

full rationale

The paper defines Freyd operads by separating a cartesian operad of values from a symmetric Ren-cartesian preoperad of computations connected by a Freyd functor. It then gives an explicit construction of the corresponding Freyd PROP of substitutions using finite sequential lists for single substitutions composed by concatenation. Representability and left-adjointness (in the strict one-object case) are proven as mathematical properties of this construction. The induced term model is used to interpret the untyped computational lambda-calculus and establish soundness, initiality, and completeness in weakly closed Freyd operads. These steps rely on standard categorical definitions and independent proofs rather than any reduction to fitted parameters, self-definitional loops, or load-bearing self-citations. The approach remains self-contained against external benchmarks with no circular steps identified.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

Relies on background from category theory and prior work on Freyd categories for effects; introduces new structures without independent evidence beyond the proofs claimed.

axioms (1)
  • standard math Standard properties of Freyd categories and multicategorical composition
    Invoked as background for separating values and computations in effectful settings.
invented entities (1)
  • Freyd operad no independent evidence
    purpose: To connect cartesian operad of values with symmetric preoperad of computations for untyped effects
    Newly defined structure whose properties are proved in the paper.

pith-pipeline@v0.9.0 · 5738 in / 1134 out tokens · 36343 ms · 2026-05-21T03:16:37.240075+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

28 extracted references · 28 canonical work pages

  1. [1]

    Sobocinski and F

    Bonchi, F., P. Sobocinski and F. Zanasi,Lawvere Categories as Composed PROPs, in:International Workshop on Coalgebraic Methods in Computer Science, pages 11–32, Springer (2016)

    work page 2016

  2. [2]

    Burroni, A.,Higher Dimensional Word Problem, in:International Conference on Category Theory and Computer Science, pages 94–105, Springer (1991)

    work page 1991

  3. [3]

    Cockett, J.,Categories and Computability, Lecture notes available at http://pages. cpsc. ucalgary. ca/robin (2010)

    work page 2010

  4. [4]

    Cockett, J. R. B. and P. J. Hofstra,Introduction to Turing Categories, Annals of pure and applied logic156, pages 183–209 (2008)

    work page 2008

  5. [5]

    Grunfeld, D

    Cohen, L., A. Grunfeld, D. Kirst and ´E. Miquey,From Partial to Monadic: Combinatory Algebra with Effects, in:FSCD 2025-10th International Conference on Formal Structures for Computation and Deduction(2025)

    work page 2025

  6. [6]

    Grunfeld, D

    Cohen, L., A. Grunfeld, D. Kirst and ´E. Miquey,Syntactic Effectful Realizability in Higher-Order Logic, 2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) pages 16–30 (2025)

    work page 2025

  7. [7]

    Miquey and R

    Cohen, L., ´E. Miquey and R. Tate,Evidenced Frames: A Unifying Framework Broadening Realizability Models, in:2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–13 (2021)

    work page 2021

  8. [8]

    De’Liguoro, U. and R. Treglia,The Untyped Computationalλ-Calculus and its Intersection Type Discipline, Theoretical Computer Science846, pages 141–159 (2020)

    work page 2020

  9. [9]

    F¨ uhrmann, C.,Direct Models of the Computational Lambda-Calculus, Electronic Notes in Theoretical Computer Science 20, pages 245–292 (1999)

    work page 1999

  10. [10]

    Hermida, C.,Representable Multicategories, Advances in Mathematics151, pages 164–225 (2000)

    work page 2000

  11. [11]

    Hoshino, N.,Linear realizability, in:International Workshop on Computer Science Logic, pages 420–434, Springer (2007)

    work page 2007

  12. [12]

    Lafont, Y.,Towards an Algebraic Theory of Boolean Circuits, Journal of Pure and Applied Algebra184, pages 257–310 (2003)

    work page 2003

  13. [13]

    W.,Functorial Semantics of Algebraic Theories, Proceedings of the National Academy of Sciences50, pages 869–872 (1963)

    Lawvere, F. W.,Functorial Semantics of Algebraic Theories, Proceedings of the National Academy of Sciences50, pages 869–872 (1963)

    work page 1963

  14. [14]

    Leinster, T.,Higher Operads, Higher Categories, 298, Cambridge University Press (2004)

    work page 2004

  15. [15]

    Power and H

    Levy, P., J. Power and H. Thielecke,Modelling Environments in Call-by-Value Programming Languages, Information and computation185, pages 182–210 (2003)

    work page 2003

  16. [16]

    B.,Call-by-Push-Value: A Subsuming Paradigm, in:International Conference on Typed Lambda Calculi and Applications, pages 228–243, Springer (1999)

    Levy, P. B.,Call-by-Push-Value: A Subsuming Paradigm, in:International Conference on Typed Lambda Calculi and Applications, pages 228–243, Springer (1999)

    work page 1999

  17. [17]

    Moggi, E.,Notions of Computation and Monads, Information and computation93, pages 55–92 (1991)

    work page 1991

  18. [18]

    Moggi, E.et al.,Computational Lambda-Calculus and Monads, in:Fourth Annual Symposium on Logic in Computer Science, pages 14–23 (1989)

    work page 1989

  19. [19]

    Pirashvili, T.,On theP ROPCorresponding to Bialgebras, Cahiers de topologie et g´ eom´ etrie diff´ erentielle cat´ egoriques 43, pages 221–239 (2002)

    work page 2002

  20. [20]

    Pitts, A. M.,Evaluation Logic, in:IV Higher Order Workshop, Banff 1990: Proceedings of the IV Higher Order Workshop, Banff, Alberta, Canada 10–14 September 1990, pages 162–189, Springer (1991)

    work page 1990

  21. [21]

    M.,Categorical logic, Handbook of Logic in Computer Science, Volume 5

    Pitts, A. M.,Categorical logic, Handbook of Logic in Computer Science, Volume 5. Algebraic and Logical Structures (S. Abramsky, DM Gabbay, and TSE Maibaum, eds.)(2001)

    work page 2001

  22. [22]

    Power, J. and E. Robinson,Premonoidal Categories and Notions of Computation, Mathematical structures in computer science7, pages 453–468 (1997)

    work page 1997

  23. [23]

    Rajesh, N.,Universal Algebra and Effectful Computation, arXiv preprint arXiv:2504.10314 (2025)

    work page arXiv 2025

  24. [24]

    Sabry, A. and P. Wadler,A Reflection on Call-by-Value, ACM transactions on programming languages and systems (TOPLAS)19, pages 916–941 (1997)

    work page 1997

  25. [25]

    16 Cohen, Grunfeld

    Staton, S.,Freyd categories are Enriched Lawvere Theories, Electronic Notes in Theoretical Computer Science303, pages 197–206 (2014). 16 Cohen, Grunfeld

    work page 2014

  26. [26]

    Staton, S. and P. B. Levy,Universal Properties of Impure Programming Languages, ACM SIGPLAN Notices48, pages 179–192 (2013)

    work page 2013

  27. [27]

    Tomita, H.,Realizability Without Symmetry, in:29th EACSL Annual Conference on Computer Science Logic (CSL 2021), pages 38–1, Schloss Dagstuhl–Leibniz-Zentrum f¨ ur Informatik (2021)

    work page 2021

  28. [28]

    17 Cohen, Grunfeld A Appendix A.1 Category of Substitutions Proof

    Yamada, R.,Effectful Toposes and Their Lawvere-Tierney Topologies, arXiv preprint arXiv:2602.23086 (2026). 17 Cohen, Grunfeld A Appendix A.1 Category of Substitutions Proof. Proposition 3.14 (i) Morphismsm→nare equivalence classes of pre-substitutionsPreSub C (m⇒n) modulo the sym- metric rules of Fig. 3. Because the relation is a congruence (rules apply i...

    work page arXiv 2026