Skip to main content
SpringerLink
Log in

Second-Order Algebraic Theories

(Extended Abstract)

  • Conference paper
Book cover Mathematical Foundations of Computer Science 2010 (MFCS 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6281))

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aczel, P.: A general Church-Rosser theorem. Typescript (1978)

    Google Scholar 

  2. Aczel, P.: Frege structures and the notion of proposition, truth and set. In: The Kleene Symposium, pp. 31–59 (1980)

    Google Scholar 

  3. Birkhoff, G.: On the structure of abstract algebras. P. Camb. Philos. Soc. 31, 433–454 (1935)

    Article  Google Scholar 

  4. Burstall, R.: Proving properties of programs by structural induction. The Computer Journal 12(1), 41–48 (1969)

    MATH  Google Scholar 

  5. Church, A.: An unsolvable problem of elementary number theory. Am. J. Math. 58, 354–363 (1936)

    Article  MathSciNet  Google Scholar 

  6. Church, A.: A formulation of the simple theory of types. J. Symbolic Logic 5, 56–68 (1940)

    Article  MATH  MathSciNet  Google Scholar 

  7. Cohn, P.: Universal Algebra. Mathematics and its Applications, vol. 6. Springer, Heidelberg (1981)

    MATH  Google Scholar 

  8. Fiore, M.: Second-order and dependently-sorted abstract syntax. In: LICS 2008, pp. 57–68 (2008)

    Google Scholar 

  9. Fiore, M., Hur, C.-K.: Term equational systems and logics. In: MFPS XXIV. LNCS, vol. 218, pp. 171–192. Springer, Heidelberg (2008)

    Google Scholar 

  10. 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)

    Google Scholar 

  11. Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: LICS 1999, pp. 193–202 (1999)

    Google Scholar 

  12. Fujiwara, T.: On mappings between algebraic systems. Osaka Math. J. 11, 153–172 (1959)

    MATH  MathSciNet  Google Scholar 

  13. Fujiwara, T.: On mappings between algebraic systems, II. Osaka Math. J. 12, 253–268 (1960)

    MATH  MathSciNet  Google Scholar 

  14. 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)

    Google Scholar 

  15. Hyland, M., Power, J.: The category theoretic understanding of universal algebra: Lawvere theories and monads. ENTCS 172, 437–458 (2007)

    MathSciNet  Google Scholar 

  16. Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Computational Problems in Abstract Algebra, pp. 263–297 (1970)

    Google Scholar 

  17. Linton, F.: Some aspects of equational theories. In: Proc. Conf. on Categorical Algebra at La Jolla, pp. 84–95 (1966)

    Google Scholar 

  18. 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)

    Google Scholar 

  19. McCarthy, J.: Towards a mathematical science of computation. In: IFIP Congress 1962. North-Holland, Amsterdam (1963)

    Google Scholar 

  20. Plotkin, G.: Binding algebras: A step from universal algebra to type theory. Invited talk at RTA 1998 (1998)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Laboratory, University of Cambridge,  

    Marcelo Fiore & Ola Mahmoud

Authors
  1. Marcelo Fiore
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ola Mahmoud
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Falculty of Informatics, Masaryk University, Botanicka 68a, 602 00, Brno, Czech Republic

    Petr Hliněný

  2. Faculty of Informatics, Masaryk University, Botanicka 68a, 602 00, Brno, Czech Republic

    Antonín Kučera

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation