Protocol Choice and Iteration
for the Free Cornering
Chad Nester 1Niels Voorneveld 2

1 University of Tartu. kodu.ut.ee/~nester/

2 Cybernetica AS. nvoorneveld.com/

MSFP 2024

Categories:

f↭fg

↭

Objects, morphisms, composition, identities.

1A↭

Symmetric Monoidal Categories:

f ⊗g

↭

σA,B

↭

Tensor product and braiding. Monoid of objects.

Naturality Conditions.

“Resource-Theoretic” interpretation.

Composite processes.

(Single-Object) Double Categories:∗X∗A∗αYB↭∗

Horizontal and vertical edge monoids, cells.

α|β↭

idXαβ↭1A↭↭

Horizontal and vertical composition, identities.

The free cornering ⌜⌞A⌝⌟ of a monoidal category A has (Part 1):
Horizontal edge monoid is (A0 , ⊗, I).
Vertical edge monoid is (A◦• , ⊗, I), as in: (also monoid equations)A ∈ A0A ∈ A0A◦ ∈ A◦•

A• ∈ A◦•U ∈ A◦•I ∈ A◦•W ∈ A◦•U ⊗ W ∈ A◦•

Interpretation: A-valued exchanges. A◦ ⊗ B • ⊗ C • ∈ A◦• is:The free cornering ⌜⌞A⌝⌟ of a monoidal category A has (Part 2):
For each f : A → B in A, a cell:⌜ ⌝⌞f⌟

Subject to equations:↭The free cornering ⌜⌞A⌝⌟ of a monoidal category A has (Part 3):
Corner cells for each object A of A:

Subject to equations:Interpretation: resource-passing.
Transform input (top) to output (bottom) by participating inexchanges (left/right).

Horizontal composition ↭ interaction.

Alternatively, elements of A◦• are protocol types!

Q: Is this a good foundation for interactive programming?

A: Not yet. A◦• is disappointing as a system of protocol types.

Goal: Support for more protocols. Choice. Iteration.

For choice, vertical edge monoid becomes (plus monoid equations):
A ∈ A0A ∈ A0A◦ ∈ A◦•⊕A• ∈ A◦•⊕U ∈ A◦•⊕W ∈ A◦•⊕U + W ∈ A◦•⊕U ∈ A◦•⊕I ∈ A◦•⊕W ∈ A◦•⊕U ⊗ W ∈ A◦•⊕U ∈ A◦•⊕W ∈ A◦•⊕U × W ∈ A◦•⊕

Interpretation:
U + W is the protocol in which the left participant chooses
one of U or W , which then happens.
U × W is the protocol in which the right participant chooses
one of U or W , which then happens.
E.g., (A◦ ⊗ B • ) + (A◦ × B • )For U + W , we require injections:

Moreove, we require that:∀satisfying:and∃!

For U × W we require projections:

Moreove, we require that:∀satisfying:and∃!

Let A have distributive binary coproducts A ⊕ B with injections:

Then we can require cells as in:∀andsatisfying:

Case statements / “sequential choice”.

∃!

For iteration, vertical edge monoid becomes:
A ∈ A0A ∈ A0A◦ ∈ A◦•∗A• ∈ A◦•∗U ∈ A◦•∗W ∈ A◦•∗U ∈ A◦•∗I ∈ A◦•∗U ⊗ W ∈ A◦•∗U ∈ A◦•∗U + W ∈ A◦•∗W ∈ A◦•∗W ∈ A◦•∗

U × W ∈ A◦•∗U ∈ A◦•∗U ∈ A◦•∗U + ∈ A◦•∗

U × ∈ A◦•∗subject to (in addition to monoid equations):
U + = I + (U ⊗ U + )U × = I × (U ⊗ U × )Interpretation: given by the equations.

For U + , we require:

∀and

∃!

satisfying:andFor U × , we require:

∀and

∃!

satisfying:andFor example:

For convenience, given α : (U AA W ) we define:+α+ = α(1: (U +A | 0 ), 1AAW +)π πyielding the unique cell such that:π= 1A |

01 |α

π++=α|α+π

0 |α

1π

A Mealy machine in A is a morphism m : S ⊗ A → B ⊗ S.
This gives a cell:
M=Then M + is the process that m is meant to define:Nice mathematical properties:

Monoidal double category.

Protocol choice a lot like (co)products.

Protocol iteration defines a (co)monad.

There is a naturally occurring model of all this.

Let C be cartesian closed and define S(C) to have:1

Horizontal edge monoid (C0 , ⊗, I)

2

Vertical edge monoid (CC , ◦, 1C ) (only strong endofunctors)

3

ACells α : S(C)(U BW ) are strong natural transformations

αX : U X ⊗ A → W (X ⊗ B)

1

S(C) models ⌜⌞C⌝⌟ (structure-preserving double functor).

2

If C distributive, S(C) models cornering with choice.

3

If C is the category of containers over Set, S(C) models
cornering with iteration.

Furture Work:

Sequential iteration (“Active” iteration).

Term logic. Dynamics. Coherence questions.

Connections to monadic effects. More on S(C).

Questions about double categories. What structure is this?

. . . Implementation?

Some References
Protocol Choice and Iteration for the Free Cornering. Nester,Voorneveld. 2024.
The Logic of Message Passing. Cockett, Pastro. 2009.
Runners for Interleaving Algebraic Effects. Voorneveld. 2022.

String Diagrams for Double Categories and Equipments.
Myers. 2016.
Concurrent Process Histories and Resource Transducers.
Nester. 2023.
Situated Transition Systems. Nester. 2021.