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.