Skip to main content

Saturated Semantics for Coalgebraic Logic Programming

  • Conference paper
Book cover Algebra and Coalgebra in Computer Science (CALCO 2013)

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

Included in the following conference series:

Abstract

A series of recent papers introduces a coalgebraic semantics for logic programming, where the behavior of a goal is represented by a parallel model of computation called coinductive tree. This semantics fails to be compositional, in the sense that the coalgebra formalizing such behavior does not commute with the substitutions that may apply to a goal. We suggest that this is an instance of a more general phenomenon, occurring in the setting of interactive systems (in particular, nominal process calculi), when one tries to model their semantics with coalgebrae on presheaves. In those cases, compositionality can be obtained through saturation. We apply the same approach to logic programming: the resulting semantics is compositional and enjoys an elegant formulation in terms of coalgebrae on presheaves and their right Kan extensions.

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

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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. Adámek, J., Koubek, V.: On the greatest fixed point of a set functor. Theor. Comput. Sci. 150, 57–75 (1995)

    Article  MATH  Google Scholar 

  2. Amato, G., Lipton, J., McGrail, R.: On the algebraic structure of declarative programming languages. Theor. Comput. Sci. 410(46), 4626–4671 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  3. Bonchi, F., Buscemi, M.G., Ciancia, V., Gadducci, F.: A presheaf environment for the explicit fusion calculus. J. Autom. Reason. 49(2), 161–183 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  4. Bonchi, F., Montanari, U.: Coalgebraic symbolic semantics. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 173–190. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  5. Bonchi, F., Montanari, U.: Reactive systems (semi-)saturated semantics and coalgebras on presheaves. Theor. Comput. Sci. 410(41), 4044–4066 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  6. Bruni, R., Montanari, U., Rossi, F.: An interactive semantics of logic programming. Theory and Practice of Logic Programming 1(6), 647–690 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  7. Corradini, A., Große-Rhode, M., Heckel, R.: A coalgebraic presentation of structured transition systems. Theor. Comput. Sci. 260(1-2), 27–55 (2001)

    Article  MATH  Google Scholar 

  8. Corradini, A., Heckel, R., Montanari, U.: From SOS specifications to structured coalgebras: How to make bisimulation a congruence. ENTCS 19, 118–141 (1999)

    MathSciNet  Google Scholar 

  9. Corradini, A., Montanari, U.: An algebraic semantics for structured transition systems and its application to logic programs. Theor. Comput. Sci. 103(1), 51–106 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  10. Dwork, C., Kanellakis, P.C., Mitchell, J.C.: On the sequential nature of unification. The Journal of Logic Programming 1(1), 35–50 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  11. Fiore, M.P., Moggi, E., Sangiorgi, D.: A fully abstract model for the π-calculus. Inf. Comput. 179(1), 76–117 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  12. Fiore, M.P., Staton, S.: A congruence rule format for name-passing process calculi from mathematical structural operational semantics. In: LICS, pp. 49–58. IEEE (2006)

    Google Scholar 

  13. Goguen, J.A.: What is unification? - a categorical view of substitution, equation and solution. In: Resolution of Equations in Algebraic Structures, Volume 1: Algebraic Techniques, pp. 217–261. Academic (1989)

    Google Scholar 

  14. Gupta, G., Costa, V.S.: Optimal implementation of and-or parallel prolog. Future Generation Computer Systems 10(1), 71–92 (1994)

    Article  Google Scholar 

  15. Kinoshita, Y., Power, A.J.: A fibrational semantics for logic programs. In: Herre, H., Dyckhoff, R., Schroeder-Heister, P. (eds.) ELP 1996. LNCS, vol. 1050, Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  16. Komendantskaya, E., McCusker, G., Power, J.: Coalgebraic semantics for parallel derivation strategies in logic programming. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol. 6486, pp. 111–127. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  17. Komendantskaya, E., Power, J.: Coalgebraic derivations in logic programming. In: CSL. LIPIcs, vol. 12, pp. 352–366. Schloss Dagstuhl (2011)

    Google Scholar 

  18. Komendantskaya, E., Power, J.: Coalgebraic semantics for derivations in logic programming. In: Corradini, A., Klin, B., Cîrstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 268–282. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  19. Mac Lane, S.: Categories for the Working Mathematician, 2nd edn. Graduate Texts in Mathematics (September 1998)

    Google Scholar 

  20. Miculan, M.: A categorical model of the fusion calculus. ENTCS 218, 275–293 (2008)

    Google Scholar 

  21. Miculan, M., Yemane, K.: A unifying model of variables and names. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 170–186. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  22. Montanari, U., Sammartino, M.: A network-conscious pi-calculus and its coalgebraic semantics. Submitted to TCS (Festschrift for Glynn Winskel)

    Google Scholar 

  23. Sangiorgi, D.: A theory of bisimulation for the pi-calculus. Acta Inf. 33(1), 69–97 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  24. Staton, S.: Relating coalgebraic notions of bisimulation. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 191–205. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  25. Worrell, J.: Terminal sequences for accessible endofunctors. ENTCS 19, 24–38 (1999)

    MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bonchi, F., Zanasi, F. (2013). Saturated Semantics for Coalgebraic Logic Programming. In: Heckel, R., Milius, S. (eds) Algebra and Coalgebra in Computer Science. CALCO 2013. Lecture Notes in Computer Science, vol 8089. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40206-7_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-40206-7_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-40205-0

  • Online ISBN: 978-3-642-40206-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics