Coalgebras for binary methods : properties of bisimulations and invariants

Hendrik Tews

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2001)

  • Volume: 35, Issue: 1, page 83-111
  • ISSN: 0988-3754

Abstract

top
Coalgebras for endofunctors 𝒞 → 𝒞 can be used to model classes of object-oriented languages. However, binary methods do not fit directly into this approach. This paper proposes an extension of the coalgebraic framework, namely the use of extended polynomial functors 𝒞 o p × 𝒞 → 𝒞 . This extension allows the incorporation of binary methods into coalgebraic class specifications. The paper also discusses how to define bisimulation and invariants for coalgebras of extended polynomial functors and proves many standard results.

How to cite

top

Tews, Hendrik. "Coalgebras for binary methods : properties of bisimulations and invariants." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 35.1 (2001): 83-111. <http://eudml.org/doc/92656>.

@article{Tews2001,
abstract = {Coalgebras for endofunctors $\{\mathcal \{C\}\}\rightarrow \{\mathcal \{C\}\}$ can be used to model classes of object-oriented languages. However, binary methods do not fit directly into this approach. This paper proposes an extension of the coalgebraic framework, namely the use of extended polynomial functors $\{\mathcal \{C\}\}^\{op\} \times \{\mathcal \{C\}\}\rightarrow \{\mathcal \{C\}\}$. This extension allows the incorporation of binary methods into coalgebraic class specifications. The paper also discusses how to define bisimulation and invariants for coalgebras of extended polynomial functors and proves many standard results.},
author = {Tews, Hendrik},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},
keywords = {binary method; coalgebra; bisimulation; invariant; object-orientation; coalgebras for endofunctors; object-oriented languages},
language = {eng},
number = {1},
pages = {83-111},
publisher = {EDP-Sciences},
title = {Coalgebras for binary methods : properties of bisimulations and invariants},
url = {http://eudml.org/doc/92656},
volume = {35},
year = {2001},
}

TY - JOUR
AU - Tews, Hendrik
TI - Coalgebras for binary methods : properties of bisimulations and invariants
JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY - 2001
PB - EDP-Sciences
VL - 35
IS - 1
SP - 83
EP - 111
AB - Coalgebras for endofunctors ${\mathcal {C}}\rightarrow {\mathcal {C}}$ can be used to model classes of object-oriented languages. However, binary methods do not fit directly into this approach. This paper proposes an extension of the coalgebraic framework, namely the use of extended polynomial functors ${\mathcal {C}}^{op} \times {\mathcal {C}}\rightarrow {\mathcal {C}}$. This extension allows the incorporation of binary methods into coalgebraic class specifications. The paper also discusses how to define bisimulation and invariants for coalgebras of extended polynomial functors and proves many standard results.
LA - eng
KW - binary method; coalgebra; bisimulation; invariant; object-orientation; coalgebras for endofunctors; object-oriented languages
UR - http://eudml.org/doc/92656
ER -

References

top
  1. [1] P. Aczel and P.F. Mendler, A final coalgebra theorem, in Proc. of the Conference on Category Theory and Computer Science, edited by D.H. Pitt, D.E. Rydeheard, P. Dybjer, A.M. Pitts and A. Poigné. Springer, Lecture Notes in Comput. Sci. 389 (1989) 357-365. MR1031572
  2. [2] H.P. Barendregt, Lambda calculi with types, edited by S. Abramsky, D.M. Gabbay and T.S.E. Maibaum. Oxford Science Publications, Handb. Log. Comput. Sci. 2 (1992). Zbl0816.03007MR1381697
  3. [3] K. Bruce, L. Cardelli and G. Castagna, The Hopkins Object Group, edited by G.T. Leavens and B. Pierce, On binary methods. Theory and Practice of Object Systems 1 (1995) 221-242. 
  4. [4] C. Cîrstea, A coalgebraic equational approach to specifying observational structures, in Coalgebraic Methods in Computer Science ’99, edited by B. Jacobs and J. Rutten. Elsevier, Amsterdam, Electron. Notes Theor. Comput. Sci. 19 (1999). Zbl1002.68095
  5. [5] J. Goguen and G. Malcolm, A hidden agenda. Theoret. Comput. Sci. 245 (2000) 55-101. Zbl0946.68070MR1784537
  6. [6] J. Gosling, B. Joy and G. Steele, The Java Language Specification. Addison-Wesley (1996). Zbl0865.68001
  7. [7] R. Hennicker and A. Kurz, ( Ω , Ξ ) –Logic: On the algebraic extension of coalgebraic specifications, in Coalgebraic Methods in Computer Science ’99, edited by B. Jacobs and J. Rutten. Elsevier, Electron. Notes Theor. Comput. Sci. 19 (1999) 195-212. Zbl0918.68064
  8. [8] U. Hensel, Definition and Proof Principles for Data and Processes, Ph.D. Thesis. University of Dresden, Germany (1999). 
  9. [9] U. Hensel, M. Huisman, B. Jacobs and H. Tews, Reasoning about classes in object–oriented languages: Logical models and tools, in European Symposium on Programming, edited by Ch. Hankin. Springer, Berlin, Lecture Notes in Comput. Sci. 1381 (1998) 105-121. 
  10. [10] C. Hermida and B. Jacobs, Structural induction and coinduction in a fibrational setting. Inform. and Comput. (1998) 107-152. Zbl0941.18006MR1641597
  11. [11] B. Jacobs, Objects and classes, co-algebraically, in Object-Orientation with Parallelism and Peristence, edited by B. Freitag, C.B. Jones, C. Lengauer and H.-J. Schek. Kluwer Acad. Publ. (1996) 83-103. 
  12. [12] B. Jacobs, Invariants, bisimulations and the correctness of coalgebraic refinements, in Algebraic Methodology and Software Technology, edited by M. Johnson. Springer, Berlin, Lecture Notes in Comput. Sci. 1349 (1997) 276-291. 
  13. [13] B. Jacobs, Categorical Logic and Type Theory. North Holland, Elsevier, Stud. Logic Found. Math. 141 (1999). Zbl0911.03001MR1674451
  14. [14] B. Jacobs and J. Rutten, A tutorial on (co)algebras and (co)induction. EATCS Bull. 62 (1997) 222-259. Zbl0880.68070
  15. [15] Y. Kawahara and M. Mori, A small final coalgebra theorem. Theoret. Comput. Sci. 233 (2000) 129-145. Zbl0952.68101MR1732181
  16. [16] X. Leroy, D. Doligez, J. Garrigue, D. Rémy and J. Vouillon, The Objective Caml system, release 3.01, March 2001. Available at URL http://caml.inria.fr/ocaml/htmlman/. 
  17. [17] B. Meyer, Eiffel: The Language. Prentice Hall (1992). Zbl0779.68013
  18. [18] R. Milner, Communication and Concurrency. Prentice Hall (1989). Zbl0683.68008
  19. [19] S. Owre, S. Rajan, J.M. Rushby, N. Shankar and M. Srivas, PVS: Combining specification, proof checking, and model checking, in Computer Aided Verification, edited by R. Alur and T.A. Henzinger. Springer, Berlin, Lecture Notes in Comput. Sci. 1102 (1996) 411-414. 
  20. [20] E. Poll and J. Zwanenburg, From algebras and coalgebras to dialgebras, in Coalgebraic Methods in Computer Science ’01, edited by A. Corradini, M. Lenisa and U. Montanari. Elsevier, Amsterdam, Electron. Notes Theor. Comput. Sci. 44 (2001). Zbl1260.18004
  21. [21] H. Reichel, Behavioural validity of conditional equations in abstract data types, in Contributions to General Algebra 3. Teubne, (1985); in Proc. of the Vienna Conference (June 21-24, 1984). Zbl0616.68020MR815137
  22. [22] H. Reichel, An approach to object semantics based on terminal co-algebras. Math. Structure Comput. Sci. 5 (1995) 129-152. Zbl0854.18006MR1368919
  23. [23] G. Roşu, Hidden Logic, Ph.D. Thesis. University of California at San Diego (2000). 
  24. [24] J. Rothe, H. Tews and B. Jacobs, The coalgebraic class specification language CCSL. J. Universal Comput. Sci. 7 (2001) 175-193. Zbl0970.68104MR1829826
  25. [25] J.J.M.M. Rutten, Universal coalgebra: A theory of systems. Theoret. Comput. Sci. 249 (2000) 3-80. Zbl0951.68038MR1791953
  26. [26] B. Stroustrup, The C++ Programming Language: Third Edition. Addison-Wesley Publishing Co., Reading, Mass. (1997). Zbl0609.68011
  27. [27] H. Tews, Coalgebras for binary methods, in Coalgebraic Methods in Computer Science ’00, edited by H. Reichel. Elsevier, Amsterdam, Electron. Notes Theor. Comput. Sci. 33 (2000). Zbl0966.68049

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.