Data refinement in a categorical setting: enrichment in a non-symmetric monoidal biclosed category
John Power – 1 April 2020
In 1990, Tony Hoare and He Jifeng wrote a paper called "Data refinement in a categorical setting." Sir Tony is a particularly influential computer engineer, and data refinement is a critical, practical aspect of computer science. They proposed specific category theoretic constructs as a body of theory in support of data refinement, unaware of a relevant, unifying category theoretic body of work but stating explicitly that surely such a body of category theory exists. In fact, without realising it, they proposed specific instances of finitary V-monads on V, equivalently Lawvere V-theories, where V is the category of small locally ordered categories with the Gray tensor product.At the time, Max Kelly had studied the situation for symmetric V, and the extant theory for bicategories did not include their examples. So Bob Gordon and I extended Max's work and more in order to provide the theory. In this talk, I plan simply to explain informally what happened as best I recall it, thus providing a solid computer science motivation for the study of categories enriched in non-symmetric monoidal biclosed categories.
Back