Functorial Semantics of Second-Order Algebraic Theories

MaRDI QIDQ6248241zbMATH OpenFDO

Authors Marcelo P. Fiore, Ola Mahmoud

Publication date 19 January 2014

Abstract: 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 $MoMlaw$ 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.

This page was built for publication: Functorial Semantics of Second-Order Algebraic Theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6248241)