2014/01/19 by Fiore, Marcelo, Mahmoud, Ola
#Category Theory (math.CT) #FOS: Computer and information sciences #FOS: Mathematics #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.1401.4697
The purpose of this work is to complete the algebraic foundations of second-order languages from the viewpoint of categorical algebra as developed by Lawvere. To this end, this paper introduces the notion of second-order algebraic theory and develops its basic theory. A crucial role in the definition is played by the second-order theory of equality \M, representing the most elementary operators and equations present in every second-order language. The category \M can be described abstractly via the universal property of being the free cartesian category on an exponentiable object. Thereby, in the tradition of categorical algebra, a second-order algebraic theory consists of a cartesian category \Mlaw and a strict cartesian identity-on-objects functor \M → \Mlaw that preserves the universal exponentiable object of \Mlaw. Lawvere's functorial semantics for algebraic theories can then be generalised to the second-order setting. To verify the correctness of our theory, two categorical equivalences are established: at the syntactic level, that of second-order equational presentations and second-order algebraic theories; at the semantic level, that of second-order algebras and second-order functorial models.