SpringerLink
Log in

Second-Order Equational Logic (Extended Abstract)

  • Conference paper
Computer Science Logic (CSL 2010)

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

Included in the following conference series:

Abstract

We extend universal algebra and its equational logic from first to second order as follows.

  1. 1

    We consider second-order equational presentations as specified by identities between second-order terms, with both variables and parameterised metavariables over signatures of variable-binding operators.

  2. 1

    We develop an algebraic model theory for second-order equational presentations, generalising the semantics of (first-order) algebraic theories and of (untyped and simply-typed) lambda calculi.

  3. 1

    We introduce a deductive system, Second-Order Equational Logic, for reasoning about the equality of second-order terms. Our development is novel in that this equational logic is synthesised from the model theory. Hence it is necessarily sound.

  4. 1

    Second-Order Equational Logic is shown to be a conservative extension of Birkhoff’s (First-Order) Equational Logic.

  5. 1

    Two completeness results are established: the semantic completeness of equational derivability, and the derivability completeness of (bidirectional) Second-Order Term Rewriting.

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

Access this chapter

Log in via an institution
Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now
Chapter
EUR 29.95
Price includes VAT (Germany)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 42.79
Price includes VAT (Germany)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 53.49
Price includes VAT (Germany)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** 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.

Similar content being viewed by others

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. Baader, F., Nipkow, T.: Term Rewriting and All That. CUP (1998)

    Google Scholar 

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

    Article  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  6. Clouston, R., Pitts, A.: Nominal equational logic. ENTCS 172, 223–257 (2007)

    MathSciNet  Google Scholar 

  7. Fiore, M.: Algebraic meta-theories and synthesis of equational logics. Research Programme (2009)

    Google Scholar 

  8. Fiore, M.: Semantic analysis of normalisation by evaluation for typed lambda calculus. In: PPDP 2002, pp. 26–37 (2002)

    Google Scholar 

  9. Fiore, M.: Mathematical models of computational and combinatorial structures. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 25–46. Springer, Heidelberg (2005)

    Google Scholar 

  10. Fiore, M.: A mathematical theory of substitution and its applications to syntax and semantics. In: Invited tutorial for the Workshop on Mathematical Theories of Abstraction, Substitution and Naming in Computer Science, ICMS (2007)

    Google Scholar 

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

    Google Scholar 

  12. Fiore, M., Hur, C.-K.: On the construction of free algebras for equational systems. Theor. Comput. Sci. 410, 1704–1729 (2008)

    Article  MathSciNet  Google Scholar 

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

    Google Scholar 

  14. Fiore, M., Mahmoud, O.: Second-order algebraic theories. In: Hlineny, P. (ed.) MFCS 2010. LNCS, vol. 6281, pp. 368–380. Springer, Heidelberg (2010)

    Google Scholar 

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

    Google Scholar 

  16. Goguen, J., Meseguer, J.: Completeness of many-sorted equational logic. Houston J. Math. 11, 307–334 (1985)

    MATH  MathSciNet  Google Scholar 

  17. Hamana, M.: Term rewriting with variable binding: An initial algebra approach. In: PPDP 2003, pp. 148–159 (2003)

    Google Scholar 

  18. Hamana, M.: Free Σ-monoids: A higher-order syntax with metavariables. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol. 3302, pp. 348–363. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  19. Hur, C.-K.: Categorical Equational Systems: Algebraic Models and Equational Reasoning. PhD thesis, Computer Laboratory, University of Cambridge (2010)

    Google Scholar 

  20. Janelidze, G., Kelly, G.: A note on actions of a monoidal category. TAC 9(4), 61–91 (2001)

    MATH  MathSciNet  Google Scholar 

  21. Klop, J.: Combinatory Reduction Systems. PhD thesis, Mathematical Centre Tracts 127, CWI, Amsterdam (1980)

    Google Scholar 

  22. Klop, J., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems: introduction and survey. Theor. Comput. Sci. 121, 279–308 (1993)

    Article  MATH  Google Scholar 

  23. Lawvere, F.: Functorial semantics of algebraic theories. Republished in: Reprints in TAC (5), 1–121 (2004)

    Google Scholar 

  24. Gabbay, M.J., Mathijssen, A.: Nominal (universal) algebra: Equational logic with names and binding. J. Logic Computation 19(6), 1455–1508 (2009)

    Article  MATH  MathSciNet  Google Scholar 

  25. Pigozzi, D., Salibra, A.: The abstract variable-binding calculus. Studia Logica 55, 129–179 (1995)

    Article  MATH  MathSciNet  Google Scholar 

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

    Google Scholar 

  27. Sun, Y.: A Framework for Binding Operators. PhD thesis, LFCS, The University of Edinburgh (1992)

    Google Scholar 

  28. Sun, Y.: An algebraic generalization of Frege structures — binding algebras. Theor. Comput. Sci. 211, 189–232 (1999)

    Article  MATH  Google Scholar 

  29. van Raamsdonk, F.: Higher-order rewriting. In: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55, pp. 588–667 (2003)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Laboratory, University of Cambridge,  

    Marcelo Fiore

  2. Laboratoire PPS, Université Paris 7,  

    Chung-Kil Hur

Authors
  1. Marcelo Fiore
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Chung-Kil Hur
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computer Laboratory, University of Cambridge, J.J. Thomson Avenue, CB3 0FD, Cambridge, UK

    Anuj Dawar

  2. Formal Methods in Systems Engineering, Vienna University of Technology, Favoritenstr. 9-11, 1040, Vienna, Austria

    Helmut Veith

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fiore, M., Hur, CK. (2010). Second-Order Equational Logic (Extended Abstract) . In: Dawar, A., Veith, H. (eds) Computer Science Logic. CSL 2010. Lecture Notes in Computer Science, vol 6247. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15205-4_26

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-15205-4_26

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-15204-7

  • Online ISBN: 978-3-642-15205-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation