Hostname: page-component-cc8bf7c57-fxdwj Total loading time: 0 Render date: 2024-12-11T23:02:45.341Z Has data issue: false hasContentIssue false
  • English
  • Français

Coalgebraic description of generalised binary methods†

Published online by Cambridge University Press:  01 August 2007

FURIO HONSELL ,
MARINA LENISA  and
REKHA REDAMALLA
FURIO HONSELL
Affiliation:
Dipartimento di Matematica e Informatica, Università di Udine, Via delle Scienze 206, 33100 Udine, Italy
MARINA LENISA
Affiliation:
Dipartimento di Matematica e Informatica, Università di Udine, Via delle Scienze 206, 33100 Udine, Italy
REKHA REDAMALLA
Affiliation:
Dipartimento di Matematica e Informatica, Università di Udine, Via delle Scienze 206, 33100 Udine, Italy B.M. Birla Science Centre, Adarsh Nagar, Hyderabad, 500 063 A.P., India
Get access Rights & Permissions [Opens in a new window]

Abstract

We extend the coalgebraic account of specification and refinement of objects and classes in object-oriented programming given by Reichel and Jacobs to (generalised) binary methods. These are methods that take more than one parameter of a class type. Class types include products, sums and powerset type constructors. To allow for class constructors, we model classes as bialgebras. We study and compare two solutions for modelling generalised binary methods, which use purely covariant functors.

In the first solution, which applies when we already have a class implementation, we reduce the behaviour of a generalised binary method to that of a bunch of unary methods. These are obtained by freezing the types of the extra class parameters to constant types. If all parameter types are finitary, the bisimilarity equivalence induced on objects by this model yields the greatest congruence with respect to method application.

In the second solution, we treat binary methods as graphs instead of functions, thus turning contravariant occurrences in the functor into covariant ones.

We show the existence of final coalgebras in both cases.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 17 , Issue 4 , August 2007 , pp. 647 - 673
Copyright
Copyright © Cambridge University Press 2007

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Abramsky, S. and Ong, L. (1993) Full Abstraction in the Lazy Lambda Calculus. Information and Computation 105 (2)159–267.CrossRefGoogle Scholar
Aczel, P. (1988) Non-wellfounded sets, CSLI Lecture Notes 14Google Scholar
Aczel, P. and Mendler, N. (1989) A Final Coalgebra Theorem. In: Pitt, D. H. et al. . (eds.) Proc. category theory and computer science. Springer-Verlag Lecture Notes in Computer Science 389 357–365.CrossRefGoogle Scholar
van den Berg, J., Huisman, M., Jacobs, B. and Poll, E. (1999) A type-theoretic memory model for verification of sequential Java programs. In: Bert et al. . (eds.) WADT'99. Springer-Verlag Lecture Notes in Computer Science 1827 1–21.Google Scholar
Bruce, K. B., Cardelli, L., Castagna, G., Eifrig, J., Smith, S. F., Trifonov, V., Leavens, G. T. and Pierce, B. C. (1995) On Binary Methods. TAPOS 1 (3)221–242.Google Scholar
Cancila, D., Honsell, F. and Lenisa, M. (2006) Some Properties and Some Problems on Set Functors. CMCS'06. Electronic Notes in Theoretical Computer Science (to appear).CrossRefGoogle Scholar
Corradini, A., Heckel, R. and Montanari, U. (2002) Compositional SOS and beyond: A coalgebraic view of open systems. Theoretical Computer Science 280 163–192.CrossRefGoogle Scholar
Cirstea, C. (2000) Integrating observations and computations in the specification of state-based, dynamical systems, Ph.D. thesis, University of Oxford.Google Scholar
Forti, M. and Honsell, F. (1983) Set-theory with free construction principles. Ann. Scuola Norm. Sup. Pisa, Cl. Sci. (4) 10 493–522.Google Scholar
Goguen, J. and Malcolm, G. (2000) A Hidden Agenda. Theoretical Computer Science 245 55–101.CrossRefGoogle Scholar
Hennicker, R. and Kurz, A. (1999) (Ω, Ξ)-Logic: On the algebraic extension of coalgebraic specifications. CMCS'1999. Electronic Notes in Theoretical Computer Science 19CrossRefGoogle Scholar
Hermida, C. and Jacobs, B. (1998) Structural induction and coinduction in a fibrational setting. Information and Computation 145 (2)107–152.CrossRefGoogle Scholar
Honsell, F. and Lenisa, M. (1995) Final Semantics for Untyped Lambda Calculus. In: Dezani, M. et al. . (eds.) TLCA'95. Springer-Verlag Lecture Notes in Computer Science 902 249–265.CrossRefGoogle Scholar
Honsell, F. and Lenisa, M. (1999) Coinductive Characterizations of Applicative Structures. Mathematical Structures in Computer Science 9 403–435.CrossRefGoogle Scholar
Honsell, F., Lenisa, M. and Redamalla, R. (2004) Coalgebraic Semantics and Observational Equivalences of an Imperative Class-based OO-Language. In: Honsell, F. et al. . (eds.) COMETA'03. Electronic Notes in Theoretical Computer Science 104 163–180.CrossRefGoogle Scholar
Huisman, M. (2001) Reasoning about Java programs in Higher-order logic using PVS and Isabelle, Ph.D. thesis, University of Nijmegen, The Netherlands.Google Scholar
Jacobs, B. (1996) Objects and Classes, co-algebraically. In: Freitag, B. et al. . (eds.) Object-Orientation with Parallelism and Book Persistence, Kluwer Academic Publishers 83–103.CrossRefGoogle Scholar
Jacobs, B. (1996a) Inheritance and cofree constructions. In: Cointe, P. (ed.) ECOOP'96. Springer-Verlag Lecture Notes in Computer Science 1098 210–231.CrossRefGoogle Scholar
Jacobs, B. (1997) Behaviour-refinement of object-oriented specifications with coinductive correctness proofs. In: Bidoit, M. et al. . (eds.) TAPSOFT'97. Springer-Verlag Lecture Notes in Computer Science 1214 787–802.CrossRefGoogle Scholar
Jacobs, B. and Rutten, J. (1996) A tutorial on (co)algebras and (co)induction. Bulletin of the EATCS 62 222–259.Google Scholar
Lenisa, M. (1996) Final Semantics for a Higher Order Concurrent Language. In: Kirchner, H. et al. . (eds.) CAAP'96. Springer-Verlag Lecture Notes in Computer Science 1059 102–118.CrossRefGoogle Scholar
Poll, E. and Zwanenburg, J. (2001) From algebras and coalgebras to dialgebras. In: Corradini, A., Lenisa, M. and Montanari, U. (eds.) CMCS'01. Electronic Notes in Theoretical Computer Science 44CrossRefGoogle Scholar
Reichel, H. (1995) An approach to object semantics based on terminal co-algebras. Mathematical Structures in Computer Science 5 129–152.CrossRefGoogle Scholar
Rosu, G. and Goguen, J. (2000) Hidden Congruent Deduction. FTP'98. Springer-Verlag Lecture Notes in Artificial Intelligence 1761 252–267.Google Scholar
Rothe, J., Tews, H. and Jacobs, B. (2001) The Coalgebraic Class Specification Language CCSL. Journal of Universal Computer Science 7 175–193.Google Scholar
Tews, H. (2002) Coalgebraic Methods for Object-Oriented Specifications, Ph.D. thesis, Dresden University of technology, 2002.Google Scholar
Turi, D. and Plotkin, G. (1997) Towards a mathematical operational semantics. 12th LICS, IEEE, Computer Science Press 280–291.Google Scholar