Symmetric Monoidal Sketches

Martin Hyland and John Power

To appear at the 2nd International Conference on Principles and Practice of Declarative Programming (PPDP 2000), Montreal, Canada, September 20-22, 2000

Abstract

We introduce and develop the notion of symmetric monoidal sketch. Every symmetric monoidal sketch generates a generic model. If the sketch is commutative and single-sorted, the generic model can be characterised as a free structure on 1, and the construction sending a small symmetric monoidal category to the category of models of the sketch in it can be seen as a right adjoint. We investigate specific cases generated by the Eckmann-Hilton argument, which allows a simple characterisation of the constructions. This accounts for the various categories of wiring currently being investigated in modelling concurrency, as well as providing a basis for understanding the axiomatically generated categories in axiomatic domain theory and in presheaf models of concurrency.