Abstract
Colimits are a powerful tool for the combination of objects in a category. In the context of modeling and specification, they are used in the institution-independent semantics (1) of instantiations of parameterised specifications (e.g. in the specification language CASL), and (2) of combinations of networks of specifications (in the OMG standardised language DOL).
The problem of using colimits as the semantics of certain language constructs is that they are defined only up to isomorphism. However, the semantics of a complex specification in these languages is given by a signature and a class of models over that signature – not by an isomorphism class of signatures. This is particularly relevant when a specification with colimit semantics is further translated or refined. The user needs to know the symbols of a signature for writing a correct refinement.
Therefore, we study how to usefully choose one representative of the isomorphism class of all colimits of a given diagram. We develop criteria that colimit selections should meet. We work over arbitrary inclusive categories, but start the study how the criteria can be met with \(\mathbb Set\)-like categories, which are often used as signature categories for institutions.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
When we use the term specification, our theory applies equally to ontologies and models, provided these have a formal semantics as theories of some institution.
- 2.
That is, with the same objects as \(\mathbf {C}\).
- 3.
For inclusive categories for which the symbol functor uniquely lifts colimits, solving colimit selection for \(\mathbb Set\) already suffices. However, the inclusive categories studied in Sect. 4.3 typically do not enjoy this property.
- 4.
It is straightforward but not essential here to make the notion of sentence precise.
- 5.
CASL has a mechanism of “compound identifiers” that ensures name-clash-freeness in multiple instantiations of parametrised specifications, such as List[List[Elem]], see [16], p.47f. and p.224f.
- 6.
Note that this construction extends to institutions, yielding Grothendieck institutions, see [5].
- 7.
In some languages, # is used instead of/. But this has the disadvantage that, when used as an IRL, the fragment following the # is not transmitted to servers.
References
Baumeister, H., Cerioli, M., Haxthausen, A., Mossakowski, T., Mosses, P.D., Sannella, D., Tarlecki, A.: CASL Semantics. In: Mosses, P.D. (ed.) CASL Reference Manual, Part III. LNCS, vol. 2960. Springer, London (2004). Edited by Sannella, D., Tarlecki, A
Borceux, F.: Handbook of Categorical Algebra I - III. Cambridge University Press, Cambridge (1994)
Căzănescu, V.E., Rosu, G.: Weak inclusion systems. Math. Struct. Comput. Sci. 7(2), 195–206 (1997)
Codescu, M., Mossakowski, T.: Heterogeneous colimits. In: Boulanger, F., Gaston, C., Schobbens, P.-Y. (ed.) MoVaH 2008 Workshop. IEEE Press (2008)
Diaconescu, R.: Institution-Independent Model Theory. Birkhäuser, Basel (2008)
Diaconescu, R., Goguen, J.A., Stefaneas, P.: Logical support for modularisation. In: 2nd Workshop on Logical Environments, pp. 83–130. CUP, New York (1993)
Goguen, J.A.: A categorical manifesto. Math. Struct. Comput. Sci. 1, 49–67 (1991)
Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specification and programming. J. ACM 39, 95–146 (1992)
W3C SEmantic Web Deployment Working Group. Best practice recipes for publishing RDF vocabularies. W3C Working Group Note, 28 August 2008. http://www.w3.org/TR/2008/NOTE-swbp-vocab-pub-20080828/
Kutz, O., Bateman, J., Mossakowski, T., Neuhaus, F., Bhatt, M.: E pluribus unum - formalisation, use-cases, and computational support for conceptual blending. In: Besold, T.R., Schorlemmer, M., Smaill, A. (eds.) Computational Creativity Research: Towards Creative Machines. Atlantis Thinking Machines, vol. 7, pp. 167–196. Atlantis Press (2015)
Mossakowski, T.: Colimits of order-sorted specifications. In: Presicce, F.P. (ed.) WADT 1997. LNCS, vol. 1376, pp. 316–332. Springer, Heidelberg (1998). https://doi.org/10.1007/3-540-64299-4_42
Mossakowski, T.: Specifications in an arbitrary institution with symbols. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol. 1827, pp. 252–270. Springer, Heidelberg (2000). https://doi.org/10.1007/978-3-540-44616-3_15
Mossakowski, T., Maeder, C., Lüttich, K.: The heterogeneous tool set, Hets. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 519–522. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71209-1_40
Mossakowski, T., Kutz, O., Codescu, M., Lange, C.: The distributed ontology, modeling and specification language. In: Del Vescovo, C., Hahmann, T., Pearce, D., Walther, D. (eds) WoMo 2013, CEUR-WS Online Proceedings, vol. 1081 (2013)
Mossakowski, T., Tarlecki, A.: Heterogeneous logical environments for distributed specifications. In: Corradini, A., Montanari, U. (eds.) WADT 2008. LNCS, vol. 5486, pp. 266–289. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03429-9_18
Mosses, P.D. (ed.): Casl Reference Manual. LNCS, vol. 2960. Springer, Heidelberg (2004). https://doi.org/10.1007/b96103
Object Management Group: The distributed ontology, modeling, and specification language (DOL) 2015. OMG draft standard: http://www.omg.org/spec/DOL/
Rabe, F.: How to Identify, Translate, and Combine Logics? J. Logic Comput. (2014). https://doi.org/10.1093/logcom/exu079
Sannella, D., Tarlecki, A.: Specifications in an arbitrary institution. Inf. Comput. 76, 165–210 (1988)
Schröder, L., Mossakowski, T.: Hascasl: integrated higher-order specification and program development. Theor. Comput. Sci. 410(12–13), 1217–1260 (2009)
Schultz, P., Spivak, D.I., Vasilakopoulou, C., Wisnesky, R.: Algebraic databases. CoRR, abs/1602.03501 (2016)
Smith, D.R.: Composition by colimit and formal software development. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation. LNCS, vol. 4060, pp. 317–332. Springer, Heidelberg (2006). https://doi.org/10.1007/11780274_17
Tarlecki, A., Burstall, R.M., Goguen, J.A.: Some fundamental algebraic tools for the semantics of computation: Part 3: indexed categories. Theor. Comput. Sci. 91(2), 239–264 (1991)
Williamson, K.E., Healy, M., Barker, R.A.: Industrial applications of software synthesis via category theory-case studies using specware. Autom. Softw. Eng. 8(1), 7–30 (2001)
Zimmermann, A., Krötzsch, M., Euzenat, J., Hitzler, P.: Formalizing ontology alignment and its operations with category theory. In: Proceedings of FOIS-2006, pp. 277–288 (2006)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 IFIP International Federation for Information Processing
About this paper
Cite this paper
Mossakowski, T., Rabe, F., Codescu, M. (2017). Canonical Selection of Colimits. In: James, P., Roggenbach, M. (eds) Recent Trends in Algebraic Development Techniques. WADT 2016. Lecture Notes in Computer Science(), vol 10644. Springer, Cham. https://doi.org/10.1007/978-3-319-72044-9_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-72044-9_12
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-72043-2
Online ISBN: 978-3-319-72044-9
eBook Packages: Computer ScienceComputer Science (R0)
