[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

A Coalgebraic Perspective on Logical Interpretations

  • Published:
Studia Logica Aims and scope Submit manuscript

Abstract

In Computer Science stepwise refinement of algebraic specifications is a well-known formal methodology for rigorous program development. This paper illustrates how techniques from Algebraic Logic, in particular that of interpretation, understood as a multifunction that preserves and reflects logical consequence, capture a number of relevant transformations in the context of software design, reuse, and adaptation, difficult to deal with in classical approaches. Examples include data encapsulation and the decomposition of operations into atomic transactions. But if interpretations open such a new research avenue in program refinement, (conceptual) tools are needed to reason about them. In this line, the paper’s main contribution is a study of the correspondence between logical interpretations and morphisms of a particular kind of coalgebras. This opens way to the use of coalgebraic constructions, such as simulation and bisimulation, in the study of interpretations between (abstract) logics.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Abadi, M., and L. Cardelli, A Theory of Objects. Springer-Verlag, 1996.

  2. Adamek J.: An introduction to coalgebra. Theory and Applications of Categories 14(8), 157–199 (2005)

    Google Scholar 

  3. Barbosa, L. S., J. N. Oliveira, and A. M. Silva, Calculating invariants as coreflexive bisimulations. In J. Meseguer and G. Rosu, (eds.), Algebraic Methodology and Software Technology, 12th International Conference, AMAST 2008, Urbana, IL, USA, July 28-31, 2008, Proceedings Springer Lect. Notes Comp. Sci. (5140), 2008, pp. 83–99.

  4. Batory D., J. N. Sarvela, A. Rauschmayer: Scaling step-wise refinement. IEEE Trans. in Sofware Engineering 30(6), 355–371 (2004)

    Article  Google Scholar 

  5. Bird R., and O. Moor, The Algebra of Programming. Series in Computer Science. Prentice-Hall International, 1997.

  6. Blok, W., and D. Pigozzi, Algebraizable logics. Memoirs of the American Mathematical Society (396). Amer. Math. Soc., Providence, 1989.

  7. Blok, W., and D. Pigozzi, Abstract algebraic logic and the deduction theorem, 2001. Available from http://www.math.iastate.edu/dpigozzi/papers/aaldedth.pdf.

  8. Blok W., J. Rebagliato: Algebraic semantics for deductive systems. Studia Logica 74(1-2), 153–180 (2003)

    Article  Google Scholar 

  9. Caleiro, C., and R. Gonçalves, Equipollent logical systems. In Logica Universalis, Birkhäuser, Basel, 2005, pp. 99–111.

  10. Carnielli W. A., M.E. Coniglio, I. M.L. D’Ottaviano: New dimensions on translations between logics. Logica Universalis 3(1), 1–18 (2009)

    Article  Google Scholar 

  11. Czelakowski, J., Protoalgebraic Logics. Trends in logic, Studia Logica Library, Kluwer Academic Publishers, 2001.

  12. Czelakowski, J., and D. Pigozzi, Amalgamation and interpolation in abstract algebraic logic. In X. Caicedo and C. H. Montenegro, (eds.), Models, Algebras, and Proofs, Lecture Notes in Pure and Applied Mathematics (vol. 203), 1998, pp. 187–265.

  13. Descalço, L., A. Madeira, and M. A. Martins, Applying abstract algebraic logic to classic automata theory: an exercise. In F. Ferreira, Guerra H., and E. Mayordomo, (eds.), Programs, Proofs and Processes; Computability in Europe Cie 2010, 2010, pp. 146–157.

  14. Feitosa, H. A., Traduções Conservativas. PhD thesis, Universidade Federal de Campinas, Instituto de Filosofia e Ciências Humanas, 1997.

  15. Feitosa H. A., I. M. L. D’Ottaviano: Conservative translations. Ann. Pure Appl. Logic 108(1-3), 205–227 (2001)

    Article  Google Scholar 

  16. Font J. M., and R. Jansana, A general Algebraic Semantics for Sentential Logics, 2nd edition, volume 7. Lecture Notes in Logic, 2009.

  17. Freyd, P. J., and A. Ščedrov, Categories, Allegories, volume 39 of Mathematical Library. North-Holland, 1990.

  18. Glivenko V.: Sur quelques points de la logique de M. Brouwer. Bulletins de la classe des sciences 15(5), 183–188 (1929)

    Google Scholar 

  19. Gödel, K., An interpretation of the intuitionistic proposicional calculus (1933). In S. Feferman et alii, (eds.), Collected works of Kurt Gödel (vol. I), Oxford: Oxford University Press, 1986, pp. 301–303.

  20. Hermida C., B. Jacobs: Structural induction and coinduction in a fibrational setting. Information and Computation 145, 105–121 (1998)

    Article  Google Scholar 

  21. Kock A.: Strong functors and monoidal monads. Archiv für Mathematik 23, 113–120 (1972)

    Article  Google Scholar 

  22. Kolmogorov, A. N., On the principle of excluded middle (1925). In J. Hei-Jenoort, (ed.), From Frege to Gddotödel: a source book in mathematical logic 1879-1931, Cambridge: Harvard University Press, 1977, pp. 414–437.

  23. Lucanu, D., E. Goriac, G. Caltais, and G. Rosu, Circ: A behavioral verification tool based on circular coinduction. In Algebra and Coalgebra in Computer Science, Third International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. Proceedings, Springer Lect. Notes Comp. Sci. (5728), 2009, pp. 433–442.

  24. Maddux R. D.: The origin of relation algebras in the development and axiomatization of the calculus of relations. Studia Logica 50(3-4), 42–455 (1991)

    Article  Google Scholar 

  25. Martin C.E., S.A. Curtis, I. Rewitzky: Modelling angelic and demonic nondeterminism with multirelations. Sci. Comput. Program 65(2), 140–158 (2007)

    Article  Google Scholar 

  26. Martins M. A.: Behavioral institutions and refinements in generalized hidden logics. Journal of Universal Computer Science 12(8), 1020–1049 (2006)

    Google Scholar 

  27. Martins M.A.: Closure properties for the class of behavioral models. Theor. Comput. Sci. 379(1-2), 53–83 (2007)

    Article  Google Scholar 

  28. Martins M.A.: On the behavioral equivalence between k-data structures. The Computer Journal 51(2), 181–191 (2008)

    Article  Google Scholar 

  29. Martins, M. A., A. Madeira, and L. S. Barbosa, Refinement by interpretation. In Dang Van Hung and P. Krishnan, (eds.), 7th IEEE International Conference on Software Engineering and Formal Methods (SEFM’09), IEEE Computer Society Press, 2009, pp. 250–259.

  30. Martins, M. A., A. Madeira, and L. S. Barbosa, Refinement by interpretation in a general setting. In J. Derrick, E. Boiten, and S. Reeves, (eds.), Proc. Refinement Workshop 2009, Electr. Notes Theor. Comput. Sci. (256), Elsevier, 2009, pp. 105–121.

  31. Martins M.A., D. Pigozzi: Behavioural reasoning for conditional equations. Math. Struct. Comput. Sci. 17(5), 1075–1113 (2007)

    Article  Google Scholar 

  32. Meinke, K., and J. V. Tucker, Universal algebra. In Handbook of logic in computer science, Vol. 1, volume 1 of Handb. Log. Comput. Sci., Oxford Univ. Press, New York, 1992, pp. 189–411.

  33. Meng , Sun , L.S. Barbosa: Components as coalgebras: The refinement dimension. Theor. Comp. Sci. 351, 276–294 (2005)

    Article  Google Scholar 

  34. Michel Bidoit, M., and R. Hennicker, Proving behavioral refinements of colspecifications. In Essays Dedicated to Joseph A. Goguen, 2006, pp. 333–354.

  35. Mossakowski T., R. Diaconescu, A. Tarlecki: What is a logic translation?. Logica Universalis 3(1), 95–124 (2009)

    Article  Google Scholar 

  36. Mossakowski T., A.Haxthausen D. Sannella, A. Tarlecki: CASL: The common algebraic specification language: Semantics and proof theory. Computing and Informatics 22, 285–321 (2003)

    Google Scholar 

  37. Palmigiano, A., Abstract logics as dialgebras. Electr. Notes Theor. Comput. Sci. 65(1), 2002.

  38. Park, D., Concurrency and automata on infinite sequences. Springer Lect. Notes Comp. Sci. (104), 1981, pp. 561–572.

  39. Poll, E., and J. Zwanenburg, From algebras and coalgebras to dialgebras. In H. Reichel, (ed.), Coalgebraic Methods in Computer Science (CMCS’2001), number 44 in ENTCS. Elsevier, 2001.

  40. Pratt, V., Origins of the calculus of binary relations. In Proc. IEEE Symp. on Logic in Computer Science, Santa Cruz, CA,USAIEEE, 1992, pp. 248–254.

  41. Prawitz, D., and P.-E. Malmnäs, A survey of some connections between classical, intuitionistic and minimal logic. In Contributions to Mathematical Logic: Proc. Logic Colloq. (Hannover 1966), North-Holland, 1968, pp. 215–229.

  42. Robinson E. P.: Variations on algebra: monadicity and generalisations of equational theories. Formal Aspects of Computing 13, 308–326 (2002)

    Article  Google Scholar 

  43. Rutten, J., Universal coalgebra: A theory of systems. Theoretical Computer Science 249(1):3–80, 2000. (Revised version of CWI Techn. Rep. CS-R9652, 1996).

  44. Sannella D., A. Tarlecki: Towards Formal Development of Programs from Algebraic Specifications: Implementations Revisited. Acta Informatica 25(3), 233–281 (1988)

    Article  Google Scholar 

  45. Sannella D., A. Tarlecki: Essential concepts of algebraic specification and program development. Formal Aspects of Computing 9(3), 229–269 (1997)

    Article  Google Scholar 

  46. Da Silva, J., I. D’Ottaviano, and A. M. Sette, Translations between logics. In Models, algebras, and proofs: Selected papers of the X Latin American Symposium on Mathematical Logic, (Bogotá, 1995), Lect. Notes Pure Appl. Math. (203), 1968, pp. 435–448.

  47. Tarlecki, A., Abstract specification theory: An overwiew. In M. Broy, and M. Pizka, (eds.), Models, Algebras, and Logics of Engineering Software, NATO Science Series, Computer and Systems Sciences, VOL 191, IOS Press, 2003, pp. 43–79.

  48. Tarski A.: On the calculus of relations. The Journal of Symbolic Logic 6(3), 73–89 (1941)

    Article  Google Scholar 

  49. Wirsing, M., Algebraic specification. In J. van Leeuwen, (ed.), Handbook of Theoretical Computer Science (volume B), Elsevier - MIT Press, 1990, pp. 673–788.

  50. Wójcicki, R., Theory of logical caculi. Basic theory of consequence operations. Synthese Library, 199. Kluwer Academic Publishers., 1988.

Download references

Author information

Authors and Affiliations

  1. CIDMA, Dep. Mathematics, Universidade de Aveiro, Aveiro, Portugal

    M. A. Martins

  2. Critical Software, MAP-i Doctoral Programme, Aveiro, Portugal

    A. Madeira

  3. HASLab \ INESC TEC, Universidade do Minho, Braga, Portugal

    L. S. Barbosa

Authors
  1. M. A. Martins
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. A. Madeira
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. L. S. Barbosa
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to M. A. Martins.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Martins, M.A., Madeira, A. & Barbosa, L.S. A Coalgebraic Perspective on Logical Interpretations. Stud Logica 101, 783–825 (2013). https://doi.org/10.1007/s11225-013-9498-z

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11225-013-9498-z

Keywords

Search

Navigation