Complexity doctrines
Michael Barr, James R. Otto · 1995
We characterize various complexity classes as the images in set$\sp2,$ set$\sp{V},$ and set$\sp3$ of categories initial in various complexity doctrines. (A doctrine consists of the models of a theory of theories.) We so characterize the linear time, P space, linear space, P time, and Kalmar elementary functions as well as the linear time hierarchy relations. (Our machine model is multi-tape Turing machines with constant number of tapes.) These doctrines extend, using comprehensions, the first order doctrines GM and JB. We show, using dependent product diagrams, how to so extend the higher order doctrine LCC. However, using Church numerals, we show that the resulting LCC comprehensions do not provide enough control over higher order types to characterize complexity classes. We also show how to use sketches and orthogonality for almost equational specification.