Adjoint logic and behavioral types

My goal with this entry is to outline a plan of attack on how to think about these subjects. Not only is this a vast area of inquiry, it’s connections with what are supposed to be my main area of inquiry (agent-based social simulation for democratic economic planning) is somewhat sketchy. The thoughts in this entry are linked by sketchy leaps and connected by skimmed threads.

One connection is between the actor model of computation and agent-based modeling. This leads to the idea that one should build an agent-based social simulation framework on the actor model of computation. This was explicitly recommended by HASH.ai, although this project appears to have been abandoned by the company. The potential benefit is the proven ability of the actor model of computation to support large-scale communtication technology, as exemplified by WhatsApp being written in Erlang. However, Signal was not written with Erlang or Akka whereas a cofounder of Signal was a founder at Whatsapp.

Another connection is how to model “institutions” in agent-based social simulations. Ghorbani draws on Ostrom’s “institutional grammar” (IG) [@ghorbani:2022:institutional]. This reminded me of the role of channels in session types and I wondered if the notion of behavioral types could be used as a more formal language for institutions. But Frega’s social ontology imagines a “layer” of interactions between individual actors and more formal institutions, inspired by Dewey. Can these relations be considered as layers in an adjoint logic? The IG distinguishes between strategies, norms and rules in a “compositional” way by adding additional structures to a base layer. The “modes” of this analysis are ADIBCO. For example, norms (ADIC) are strategies (AIC) with an additional “deontic” component. This addtional deontic “logic” changes the range of behaviors available to the agents while still maintaining something from the strategy layer. This broad analogy between adjoint logic and institutional grammar may only be suggestive, but there is something temptingly tasty there.

Annother connection is from interesting hints from Peirce in the potential importance of a “system of logics” connected by modality, where these logics are distinguished by differences in their substructural rules. Peirce suggested that the mode of possibility could be distinguished as a logic without the law of contradiction, and the mode of necessity as a logic without excluded middle. Peirce elevates the concepts firstness/secondness/thirdness from phenomenological categories (i.e. at the level of firstness) to the modal relations possibility/actuality/necessity. But Peirce also considered a variety of multi-modal systems in his development of the gamma graphs, and these writings probably contain all sorts of interesting ideas.

I need to better understand the relationship (if any) between the adjunctions connecting substructural logic and those that connect classical, intuitionistic and paraconsistent logics. The latter, more Peircean, system is worked out in great detail for propositional logic by Aryal (as an undergraduate at Tufts!) in the paper (Intuitionistic logic, dual intuitionistic logic, and modality)[https://arxiv.org/html/2411.07363v2], where intuitionistic and dual intuitionistic logics are related to the modal logic S4.

Both adjoint logic and Peirce’s system have been related to the actor model of computation. More specifically, multiparty session types (a particular model of behavioral types) have been developed for the actor model by Simon Fowler. Multiparty session types use linear or affine logic to model interaction/communication protocols between multiple parties. More concrete implementations of the actor model with multi-party session types (such as Maty by Fowler and Hu) exist. The links between these concrete implementations and the more abstract “adjoint logic” perspective by Pruiksma and Pfenning are not entirely clear, since the latter is more of a mathematical model. Like multi-party session types, Pruiksma’s generalization of adjoint logic aims to generalize binary session types, but this extension may be more powerful as it includes patterns such as multicast, replicable services and cancellation.

A recent paper by Pfenning’s group at Carnegie Mellon on Grits, a new language that implements adjoint logic in a channel-based message-passing concurrent language [@francalanza:2026:grits]. This reminds me that it makes sense to consider the broader category of “message-passing” rather than committing to either the actor model or the channel model. It’s not intuitively clear that agent-based models are best implemented in actor models rather than channel models. I also shouldn’t naively assume that the “message passing” interpretation of adjoint logic implies the actor model. Fowler’s works showing that channel and actor based extensions of the lambda calculus are inter-convertable [@fowler:2017:actors]. However, since the actor model is more restrictive in it’s communications pattern, the translation from actors to channels is easier than visa-versa. Intuitively, it seems easier to implement privacy-protecting protocols in the actor model since the channel model almost assumes broadcast. On the other hand, the anonymous processes in the channel model are somewhat insulated from whatever action the message produces. A quick search didn’t reveal too much prior work on this distinction. Also note that Fowler wonders about combining behavioral types with actors in 2017, and writes about their proposed solution in 2024.

It could also be that the focus on actors or channels should be understood in a more broad semiotic system framework. Symbols can be shared between actors through channels, but this requires a certain materialization of the symbol. Traditional logic tends to ignore this materiality (die, strawman, die) but a semiotic focus should always include this material dimension. The networks that connect actors can be a “public” environment accessible to many potential observers to “private” communication lines within a machine boundary that could be very difficult to eavesdrop. It’s easy to keep this in mind for embedded robots, and the “robot frame” should be used as the base case for understanding an “actor”. There is an essential difficulty in recognizing a message as a message that is elided in the actor model, which in some ways presumes a “well-ordered” mailbox that seems far from the robot problem of making sense of an environment.

In looking for the

Links to Peirce’s modal system are a bit more indirect. Carl Hewitt, who developed the actor model, went on to stress the need to use paraconsistent logic to model the messiness of the real world (what he called inconsitency robustness) in what he called “organizational computing”. Some of his later papers try to develop a “strongly typed” actor model. Hewitt’s notion of “large-scale organizational computing” seems like it could be usable in devloping software to support citizens’ assemblies.

Hewitt’s work preceeds session types and is not related to the linear/affine logic of session types. His work on commitment [@hewitt:2006:what] seems to fit within the broader notion of behavioral types as coordination between parties, as commitments are governed by contracts that are inherently incomplete and subject to revision. Hewitt does not seem to distinguish between physical commitments and the contracts that represent them.

Hewitt argues that social commitments are inconsistent and should be analyzed by paraconsistent logic, although this claim is not well developed.

Social commitments are analyzed in terms of permissions, obligations, prohibitions, dispensations, and delegations in [Kagal and Finin 2004] where meta-policies are used to attempt to remove some inconsistencies.

Social commitments seem very similar to the institutional modelling approach developed by Ghorbani [@ghorbani:2022:institutional]. The Gemini AI summary highlights “commitments, conventions and institutions” in Ostrom’s work that parallels Frega’s ontology. Note the strong resemblance to Poinsot’s natural, conventional, stipulated analysis of signs developed by JB Murphy . Perhaps conventions correspond to the “interaction” layer from Frega’s social ontology? Institutional grammar was developed by Ostrom in 1995 wheras Hewitt’s reference to social commitments is from 2004. There is clearly some overlap between the “commitments and conventions” line of research in multi-agent systems due to Jennings [@jennings:1993:commitment] and the institutional grammar approach being applied in agent-based modeling. Probably worth reading Ostrom’s institutional grammar work at some point.

So what would I need to learn enough about this area to move it from intellectual curiousity to useful tool? But this can’t be the only metric. It would have to compete with potentially more fruitful areas in developing the path between Kessler and Citizens’ Nexus. While I still believe that agent-based social simulations lie upon this path, there are a (large|infinite) number of other projects that I could work on.

The notion of a “system of modes” is developed in modal homotopy type theory, where relatively elaborate modal systems are used to characterize “physical systems”. Although I’ve known about this for a long time, I’ve never made the time to really study it in depth. The relative complexity of the system is a major barrier, as it seems to require a non-trivial understanding of topos theory, dependent types, and homotopy theory.

Enter behavioral types. The most concrete development of behavioral types is session types. Binary session types use linear logic as a type theory for communication channels. Again, I have not studies these systems in depth, but my intuition is that these combine a “cartesian” logical system of data types and a “linear” logical system of session types, connected by a modality.

Pavlovic develops this cartesian/monoidal logic in his book “Programs as Diagrams”. I read the first few chapters of this book