Abstract
Fiore and Hur [10] recently introduced a conservative extension of universal algebra and equational logic from first to second order. Second-order universal algebra and second-order equational logic respectively provide a model theory and a formal deductive system for languages with variable binding and parameterised metavariables. This work completes the foundations of the subject from the viewpoint of categorical algebra. Specifically, the paper introduces the notion of second-order algebraic theory and develops its basic 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. Our development includes a mathematical definition of syntactic translation between second-order equational presentations. This gives the first formalisation of notions such as encodings and transforms in the context of languages with variable binding.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aczel, P.: A general Church-Rosser theorem. Typescript (1978)
Aczel, P.: Frege structures and the notion of proposition, truth and set. In: The Kleene Symposium, pp. 31–59 (1980)
Birkhoff, G.: On the structure of abstract algebras. P. Camb. Philos. Soc. 31, 433–454 (1935)
Burstall, R.: Proving properties of programs by structural induction. The Computer Journal 12(1), 41–48 (1969)
Church, A.: An unsolvable problem of elementary number theory. Am. J. Math. 58, 354–363 (1936)
Church, A.: A formulation of the simple theory of types. J. Symbolic Logic 5, 56–68 (1940)
Cohn, P.: Universal Algebra. Mathematics and its Applications, vol. 6. Springer, Heidelberg (1981)
Fiore, M.: Second-order and dependently-sorted abstract syntax. In: LICS 2008, pp. 57–68 (2008)
Fiore, M., Hur, C.-K.: Term equational systems and logics. In: MFPS XXIV. LNCS, vol. 218, pp. 171–192. Springer, Heidelberg (2008)
Fiore, M., Hur, C.-K.: Second-order equational logic. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 320–335. Springer, Heidelberg (2010)
Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: LICS 1999, pp. 193–202 (1999)
Fujiwara, T.: On mappings between algebraic systems. Osaka Math. J. 11, 153–172 (1959)
Fujiwara, T.: On mappings between algebraic systems, II. Osaka Math. J. 12, 253–268 (1960)
Goguen, J., Thatcher, J., Wagner, E.: An initial algebra approach to the specification, correctness and implementation of abstract data types. In: Current Trends in Programming Methodology, vol. IV, pp. 80–149. Prentice-Hall, Englewood Cliffs (1978)
Hyland, M., Power, J.: The category theoretic understanding of universal algebra: Lawvere theories and monads. ENTCS 172, 437–458 (2007)
Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Computational Problems in Abstract Algebra, pp. 263–297 (1970)
Linton, F.: Some aspects of equational theories. In: Proc. Conf. on Categorical Algebra at La Jolla, pp. 84–95 (1966)
Lawvere, F.W.: Functorial Semantics of Algebraic Theories and Some Algebraic Problems in the context of Functorial Semantics of Algebraic Theories. Republished in: Reprints in TAC (5), pp. 1–121 (2004)
McCarthy, J.: Towards a mathematical science of computation. In: IFIP Congress 1962. North-Holland, Amsterdam (1963)
Plotkin, G.: Binding algebras: A step from universal algebra to type theory. Invited talk at RTA 1998 (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fiore, M., Mahmoud, O. (2010). Second-Order Algebraic Theories. In: Hliněný, P., Kučera, A. (eds) Mathematical Foundations of Computer Science 2010. MFCS 2010. Lecture Notes in Computer Science, vol 6281. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15155-2_33
Download citation
DOI: https://doi.org/10.1007/978-3-642-15155-2_33
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15154-5
Online ISBN: 978-3-642-15155-2
eBook Packages: Computer ScienceComputer Science (R0)