Premonoidal multicategories (Student project)
The following is a proposal for a student project at the masters or undergraduate level.
Cartesian multicategories—coloured Lawvere theories—provide a categorical semantics for algebraic expressions in typed universal algebra. However, cartesian multicategories make two assumptions that are unreasonable in a programming context: firstly, that all expressions are pure and with no global effects, which is false for programs modifying global state; and secondly, that all processes may be copied or discarded without changing the meaning of the program, which is false for a simple coin flip or a non-halting program.
Dropping these two assumptions, we obtain copy-discard premonoidal multicategories, a variation on the concept of Freyd multicategory studied by Staton and Levy. However, the same syntax we were using for cartesian multicategories—algebraic expressions—stops working. A first proposal of a syntax for copy-discard premonoidal multicategories can be extracted from the work of Staton and Levy, but it is inefficient: e.g., associativity of composition is not transparent in that syntax.
Research proposal. To construct the free copy-discard premonoidal multicategory over a signature represented by a multiquiver, using a simple type theory of program expressions that may function in a similar fashion to the algebraic syntax of Lawvere theories.
References.