Some properties of coalgebras and their rôle in computer science

• BibTex
• RIS
• APA
• Harvard
• IEEE
• MLA
• Vancouver
• Chicago

@article{Steingartner_2016,
   doi = {10.17512/jamcm.2016.4.16},
   url = {https://doi.org/10.17512/jamcm.2016.4.16},
   year = 2016,
   publisher = {The Publishing Office of Czestochowa University of Technology},
   volume = {15},
   number = {4},
   pages = {145--156},
   author = {William Steingartner and  Davorka Radaković and  František Valkošák and  Pavol Macko},
   title = {Some properties of coalgebras and their rôle in computer science},
   journal = {Journal of Applied Mathematics and Computational Mechanics}
}

TY  - JOUR
DO  - 10.17512/jamcm.2016.4.16
UR  - https://doi.org/10.17512/jamcm.2016.4.16
TI  - Some properties of coalgebras and their rôle in computer science
T2  - Journal of Applied Mathematics and Computational Mechanics
JA  - J Appl Math Comput Mech
AU  - Steingartner, William
AU  - Radaković, Davorka
AU  - Valkošák, František
AU  - Macko, Pavol
PY  - 2016
PB  - The Publishing Office of Czestochowa University of Technology
SP  - 145
EP  - 156
IS  - 4
VL  - 15
SN  - 2299-9965
SN  - 2353-0588
ER  - 

Steingartner, W., Radaković, D., Valkošák, F., & Macko, P. (2016). Some properties of coalgebras and their rôle in computer science. Journal of Applied Mathematics and Computational Mechanics, 15(4), 145-156. doi:10.17512/jamcm.2016.4.16

Steingartner, W., Radaković, D., Valkošák, F. & Macko, P., 2016. Some properties of coalgebras and their rôle in computer science. Journal of Applied Mathematics and Computational Mechanics, 15(4), pp.145-156. Available at: https://doi.org/10.17512/jamcm.2016.4.16

[1]W. Steingartner, D. Radaković, F. Valkošák and P. Macko, "Some properties of coalgebras and their rôle in computer science," Journal of Applied Mathematics and Computational Mechanics, vol. 15, no. 4, pp. 145-156, 2016.

Steingartner, William, Davorka Radaković, František Valkošák, and Pavol Macko. "Some properties of coalgebras and their rôle in computer science." Journal of Applied Mathematics and Computational Mechanics 15.4 (2016): 145-156. CrossRef. Web.

1. Steingartner W, Radaković D, Valkošák F, Macko P. Some properties of coalgebras and their rôle in computer science. Journal of Applied Mathematics and Computational Mechanics. The Publishing Office of Czestochowa University of Technology; 2016;15(4):145-156. Available from: https://doi.org/10.17512/jamcm.2016.4.16

Steingartner, William, Davorka Radaković, František Valkošák, and Pavol Macko. "Some properties of coalgebras and their rôle in computer science." Journal of Applied Mathematics and Computational Mechanics 15, no. 4 (2016): 145-156. doi:10.17512/jamcm.2016.4.16

SOME PROPERTIES OF COALGEBRAS AND THEIR RÔLE IN COMPUTER SCIENCE

William Steingartner ¹, Davorka Radaković ², František Valkošák ¹, Pavol Macko ¹

¹ Department of Computers and Informatics, Faculty of Electrical Engineering and Informatics
Technical University of Košice
Košice, Slovak Republic
² Department of Mathematics and Informatics, Faculty of Sciences, University of Novi Sad
Novi Sad, Serbia
william.steingartner@tuke.sk, davorkar@dmi.uns.ac.rs, frantisek.valkosak@student.tuke.sk pavol.macko@gmail.com
Received: 31 July 2016; accepted: 10 November 2016

Abstract. This paper introduces basic theoretical knowledge of coalgebras in computer science. Coalgebras are, specifically in category theory, structures defined according to an endofunctor. For both algebra and coalgebra, a functor is a convenient and general way of defining a signature. We present practical usage of the coalgebras in an example. We observe a behavior of a simple Sequencer developed in SLGeometry framework. We model its behavior with the simple program written in Python, and we describe its behavior within coalgebra of endofunctor. The computation of the values stored in internal states is performed coinductively. Our approach can be used in the teaching process of formal methods for young software engineers.

Keywords: coalgebra, functor, induction, internal state of program, observable behavior of program, SLGeometry software

1. Introduction

Induction is a well-known mathematical proof method which is also used in computer science. The frequent usage of induction in computer science is with well-founded sets [1]. With these sets, we are able to define elements by constructors in finite steps. Induction is represented by notions like initial algebras and finality. Coinduction is dual notion to induction. It is also a proof method, which serves to gain some observations on structures and is used with non-well-founded sets or with infinite streams. Coalgebras are a very important part of theoretical computer science. Their main rôle is in describing the generated behavior of running programs [2, 3]. It is the behavior that can be observed from the outside of a machine - for instance on the screen. Typically, we model many problems by mathematical programs which seek to maximize or minimize some objective which is a function of the decisions [4, 5]. Coalgebra is an abstract notion of observable behavior. It is a study of states and their operations and properties. The set of states is usually seen as a black box, to which one has limited access [6]. A relation between what is actually inside and what can be observed externally is the foundation of the theory of coalgebras [3].

The main goal of this article is to introduce the purpose of coalgebras in computer science and to introduce basic principles of coinductive computation.

The paper is organized as follows: Section 2 gives us basic notions of functor, algebra, coalgebra and category theory. The application of coinduction on Sequencer example is presented in Section 3. Experiment about Sequencer’s behavior, check- ing of the results and description of Sequencer’s behavior is introduced in Section 4. Finally, some conclusions are closing our article.

2. Basic concepts

In this section we briefly introduce some basic concepts that we use further.

Category theory is the algebra of functions. A category is an abstract structure: a collection of objects, together with a collection of arrows between them. Precisely, a category C is a mathematical structure that consists of a set of objects, e.g. and a set of morphisms or arrows of the form between them [7, 8].

For any given object there is designated identity morphism . For two morphisms and , there is designated composite morphism .

The objects of category can be arbitrary structures, therefore categories are useful in computer science, where we often use more complex structures not expressible by sets. Morphisms between categories are called functors, e.g. a functor from a category C into a category D is considered as a structure-preserving mapping (identities, morphisms and composition) between categories [9, 10].

Let be a functor. An algebra of the functor is according to [11] a tuple where:

· is the carrier-set of the algebra;

· the function is the algebra structure.

Dually, an F-coalgebra or F-system is a pair consisting of a set and a function [12, 13]. The set is called the carrier of the system, also called the set of states; the function is called the F-transition structure (or dynamics) of the system. When no explicit reference to the functor (i.e., the type of the system) is needed, we shall simply speak of system and transition structure. Moreover, when no explicit reference to the transition structure is needed, we shall often use instead of .

Coalgebras are dual notion to algebras. We show a difference between them in an example. What is the main difference between an algebra and a coalgebra ? Essentially, the difference is between construction and observation. An algebra consists of a carrier-set with a function going into this carrier . It tells us how to construct elements in . Coalgebra consists of a state space with a function going out of , in an opposite direction. In this case we do not know how to form elements in , but we only have operations acting on , which may give us some information about [9].

According to [13, 14], the main differences between the theory of universal algebra and universal coalgebra is shown in Table 1.

Table 1

Comparision of universal algebra and coalgebra

3. Coalgebras and SLGeometry

In this section we introduce SLGeometry framework with its UI controls. In [15] we demonstrated the use of triggers and their propagation from one component to another as children’s mathematical game to calculate arithmetic sum. We present how this game can be described in a formal way, as well as how it could be used for teaching coalgebras at the faculty level.

3.1. SLGeometry

SLGeometry is an extensible dynamic geometry framework, which is now implemented as a Universal Windows Application on the .NET Framework [15-18]. It consists of an expression parser and an extensible functional language (Engine) at its core, and a graphical surface (GeoCanvas). The main purpose of the Engine is to maintain a set of expressions, stored in named variables, which represent the elements of geometric drawings.

Geometric shapes and visual controls are displayed by GeoCanvas as a response to user interaction. Geometric drawings are designated by expressions, built from atomic values, lists and functions applied to parameters. A dynamic of a system is evident with each change of a particular variable, then a recursive recalculation of all dependent variables is triggered. Since the variables are bound to graphical objects and user controls on the screen, the user can change a variable by interacting with the bound object. After that, all dependent objects are recalculated and their corresponding graphical objects on the GeoCanvas are updated.

The main aim of the SLGeometry framework is to improve the development of teaching materials and games using it as a foundation for experiments. The motivation for developing custom UI controls was found on GeoGebraTube (now on [19] with more than 450.000 of free and interactive materials) where many teaching materials and games could be found. The representation of each of these controls is given with a single variable and all controls have properties which determine the control’s appearance and behavior.

In [15] we proposed UI controls with a sequential behavior Sequencer and Scorekeeper to demonstrate how to calculate the arithmetic sum of numbers from 1 to 9. A Sequencer is a counter which cycles through an interval of integer values and it behaves like modulo. The interval in the Sequencer can be assigned. An UI control Scorekeeper keeps added points when it is triggered. The user clicks on a PushButton which then triggers the Sequencer and it's Done property triggers the Scorekeeper. To achieve this flow, the given controllers has to be connected to each other by the user. If the Sequencer is denoted with variable s, PushButton with p and Scorekeeper with k, the connection is given in Table 2.

Table 2

Daisy chaining via triggers

3.2. Formal description of Sequencer

We use the given example of controllers to demonstrate the modulo as an example of sequential behavior that is attractive for the students. It propagates coinductive computation and coalgebras in an interesting way. In this case, we use the interval of naturals from 0 to 8, so Sequencer properties Min and Max are changed to 0 and 8, respectively. This represents the congruence class of the modulo 9, denoted as for the presentation of coinduction with this example. Whenever the PushButton is pushed, the Sequencer increments the value by .

We use derived function , which sends its input value to the congruence class of the modulo :

In our case the value of a is 9, i.e. :

The value of the Scorekeeper is computed as follows:

,

(1)

where stands for index and for quotient value for modulo calculation.

We define a state for any as follows:

(2)

A state is defined as a tuple of two values:

· value is a number of how many times the PushButton has been pushed;

· is a sum of all values given by Sequencer from to and kept by the Scorekeeper.

The states we enclose into the state space . We define destructor operations over the state space as follows:

where is a set of naturals. An operation returns the actual sum stored in a state; it is an operation that represents the behavior of the Sequencer. The operation is triggered by the PushButton and it autoincrements the index of state. The last operation generates a new state. The new state appears after pushing the button and the value of the index is incremented by . This could be expressed in a formal way for a state as follows:

We enclose functions and into the coalgebraic specification as follows:

Operations:

Assertions:

Creation:

We define the coalgebra structure as follows:

.

The appropriate endofunctor for the coalgebra is

.

By observing the output values of the Sequencer we can formulate the following proposition.

Proposition 1: Let be a state with and (according to (2)) and let be a value for modulo calculation.

If the following congruence

,

holds, then in the state with and the corresponding values are the same:

i.e.

Proof: The proof is done by induction.

(1) In the case , for any state let index be some value , . It holds, that . Then for the state holds that and (according to (2)).

Thus, the property for holds trivially.

(2) Now we consider, that for some an induction hypothesis

holds and we prove the property for .

We present for what holds. Let and . According to the formal definition (2) at the state with the index it holds that

Since,

(by definition)

and

(reflexivity of congruence by modulo k),

by addition of congruence then we have

, i.e. .

The proof can also follow the following idea: for any , the sequential state values are:

.

We denote a modulo (or remainder) operator simply , where be a quotient. Let be a value

,

(3)

which is alternatively

and .

Adding value 1 to both sides of (3) we get

which follows to

.

Then we can express state values as follows:

(4) .

From induction hypothesis it follows that state values and are equal,

,

if for given .

Now we consider the following congruence for :

.

Then we can express state values according (4) for as follows:

,

which means that state values and are equal,

,

if for given .

Hence, we formulate the following corollaries.

Corollary 1: First occurrence of value and such that , defined in Proposition 1 is at index with value .

Corollary 2: The given tuples appear after each a steps.

4. Experiment and results

In this section we present an example of the Sequencer’s behavior. We follow the presented example in [15]: we model it in a formal way and then we show its behavior by a simple program written in the Python programming language. Finally, we compare the results when the quotient is changed.

At the beginning, the Scorekeeper is in the initial state and its sum value is , i.e. . After the PushButton is pushed, the next state is generated and its value is previous index value incremented by . So after the PushButton is pushed ten times, the sequence of ten new states appear according to the following formula:

, where in our example.

The list of states then looks like:

4.1. Simulation of Sequencer’s behavior

To check the Proposal in practice, we also demonstrated the Sequencer’s behavior by a simple program in the Python programming language. The source code is listed in Table 3.

Table 3

Python listing of Sequencer’s behavior

We conducted an experiment for different values of (see line 13 in Table 3). Tables 4 and 5 show the concrete computed values for and (as in SLGeometry), for simplicity in the first 30 states. In both cases we can see the values as they are generated by the Sequencer. The property in Proposition 1, which we proved, can also be observed on the output values.

Table 4

Values for a = 5

Table 5

Values for a = 9

Comparing the results of the Sequencer in Table 4 (a = 5) and in Table 5 (a = 9) we can see the following:

– state values in which have the same values for index i and index i+1;

– the first occurrence of values and such that , defined in Proposition 1 is at index with value in accordance with the Corollary 1;

– and these given tuples appear after each a steps in accordance with the Corollary 2.

5. Conclusion

The main goal of this article was to bring a closer view on coalgebras in computer science. We introduced some example and practical examples of coalgebras and coinductive computation of state values. The example used with SLGeometry represents a very interesting way of using coalgebras and coinduction. We want to extend our approach with the coinduction and bisimulation method when observing the output states of a running system.

Acknowledgement

This work was supported by Grant No. FEI-2015-18: Coalgebraic models of component systems.

&

This work is the impact of the projects implementation: Center of Information and Communication Technologies for Knowledge Systems (ITMS project code: 26220120020 and Development of the Center of Information and Communication Technologies for Knowledge Systems (ITMS project code: 26220120030) supported by the Research Development Operational Program funded by the ERDF.

&

This work is a result of an international cooperation under the CEEPUS network No. CIII-HU-0019-11-1516.

References

[1] Aczel P., Non-well-founded sets, Center for the Study of Language and Information, Stanford 1941.

[2] Adámek J., Milius S., Moss L.S., Initial algebras and terminal coalgebras: a survey, 2010.

[3] Jacobs B., Rutten J., An introduction to (co)algebras and (co)induction, [in:] D. Sangiorgi, J. Rutten (eds.), Advanced topics in bisimulation and coinduction, 2011 (This chapter is a modest update of the 1997 BEATCS old tutorial paper).

[4] Novitzká V., Slodičák V., On applying stochastic problems in higher-order theories, Acta Electrotechnica et Informatica 2007, 7, 3.

[5] Ristić S., Aleksić S., Čeliković M., Luković I., Generic and standard database constraint meta-models, Comput. Sci. Inf. Syst. 2014, 11(2), 679-696.

[6] Jacobs B., Introduction to Coalgebra. Towards Mathematics of States and Observations, Version 2.0, 2012.

[7] Walters R.F.C., Categories and Computer Science, Cambridge University Press, New York 1992.

[8] Brandenburg M., Einführung in die Kategorientheorie. Mit ausführlichen Erklärungen und zahlreichen Beispielen, Springer-Verlag, Berlin-Heidelberg, Springer Spektrum, 2016.

[9] Barr, M., Wells, C., Category Theory for Computing Science, Prentice Hall International, 1990.

[10] Blute R., Scott P., Category theory for linear logicians, [in:] T. Erhard, J.-Y. Girard, P. Ruet (eds.), Linear Logic in Computer Science, London Mathematical Society Lecture Note Series, Cambridge Univ. Press, 2004.

[11] Geuvers H., Representing Streams in Second Order Logic (Coinduction and Coalgebra in Second Order Logic), Seminar Representing Streams, Lorentz Centre, Leiden Dec 14 2012, ISBN 3-540-66463-7.

[12] Vene V., Categorical Programming with Inductive and Coinductive Types, Tartu University Press, Tartu 2000.

[13] Rutten J.J.M.M., Fundamental study - universal coalgebra: a theory of systems, Theoretical Computer Science 2000, 249, 3-80.

[14] Jacobs B., Rutten J., Tutorial on (Co)Algebras and (Co)Induction, EATCS 1999, 222-259.

[15] Radaković D., Herceg Đ., A platform for development of mathematical games on silverlight, Acta Didactica Napocensia 2013, 6(1), 77-90.

[16] Radaković D., Herceg Dj, The Extensibility of an Interpreted Language Using Plugin Libraries, AIP Proceedings, Numerical Analysis and Applied Mathematics ICNAAM 2011: International Conference on Numerical Analysis and Applied Mathematics 2011, 1389, 837-840.

[17] Herceg Đ., Radaković D., Herceg D., Generalizing the Extensibility of a Dynamic GeometrySoftware, AIP Proceedings, Numerical Analysis and Applied Mathematics ICNAAM 2012: International Conference of Numerical Analysis and Applied Mathematics 2012, 1479, 482-485.

[18] Radaković D., Herceg Dj, The Use of WPF for Development of Interactive Geometry Software, Acta Universitatis Matthiae Belii, Series Mathematics 2010, 16, 65-79.

[19] GeoGebra: Featured Materials, https://www.geogebra.org/materials/