Coalgebras for modelling observable behaviour of programs
William Steingartner
,Valerie Novitzká
Journal of Applied Mathematics and Computational Mechanics |
Download Full Text |
COALGEBRAS FOR MODELLING OBSERVABLE BEHAVIOUR OF PROGRAMS
William Steingartner, Valerie Novitzká
Faculty of Electrical Engineering and
Informatics, Technical University of Košice
Slovakia
e-mail: william.steingartner@tuke.sk, valerie.novitzka@tuke.sk
Received: 31 March 2017; accepted: 15 May 2017
Abstract. A useful tool for modelling behaviour in theoretical computer science is the concept of coalgebras. Coalgebras enable one to model execution of programs step by step using categorical structures and polynomial endofunctors. In our paper, we start with a short introduction of basic notions and we use this method for modelling structural operational semantics of a simple imperative language.
MSC 2010: 16T15, 18A22, 18C50
Keywords: category, coalgebra, observable behaviour, polynomial endofunctor, semantics
1. Introduction
The development of computers has contributed to the investigation of dynamical features in formal structures. The dynamics involve a state of affairs which can be possibly observed and modified [1]. We can consider a computer state as a combined content of all memory cells. A user can observe only a part of this state, e.g. on display and he can modify this state by typing and executing commands. As a reaction, the computer displays certain behaviour [2]. The aim of programming is to force the computer to execute some actions and to generate desired behaviour. This behaviour can be positive, e.g. expected behaviour; or negative, e.g. side effects that must be excluded from the system. To describe the behaviour of a computer system is a non-trivial matter. But some formal descriptions of such complex systems are needed when we wish to reason formally about their behaviour. This reasoning is needed to achieve the correctness or security of these systems [3].
The basic idea of behavioural theory is to determine a relation between internal states and their observable properties. The internal states are often hidden. Computer scientists have introduced many formal structures to capture the state-based dynamics, e.g. automata, transition systems, Petri nets, etc. In [4] the notion of behaviour in algebraic specifications was firstly introduced.
Coalgebras are a very important part of theoretical computer science. Their main rôle is in modelling the generated behaviour of running programs [5]. This is the behaviour that can be observed on the outside of a machine, for instance on the screen. Coalgebra is a study of states and their operations and properties. The set of states is usually seen as a black box, to which we have limited access [6]. A relation between what is actually inside and what can be observed externally is the foundation of the theory of coalgebras [7].
In this paper we introduce basic concepts and constructions of coalgebras. We start with the notion of signature, category of states and construction of a polynomial endofunctor, which is determined by a corresponding signature. Then we introduce the notion of coalgebra and illustrate it on a simple example of a bank account. The main part of our paper consists of the coalgebraic definition of structural operational semantics of a simple imperative language together with an example how the semantics of a program can be modelled by coalgebra.
2. Basic notions
Program execution can be considered as a mapping from input values to output ones. Giving some input values, the execution causes changes of internal state, i.e. computer memory, and we can observe the behaviour of a program only by its output values. There are also programs changing the internal state of a computer, that do not produce outputs, e.g. the programs running infinitely, sleeping processes in operating systems which wake up and work only in the case when some event occurs. An observer cannot see any changes of internal states because they are hidden [8]. Therefore, it is important to model the behaviour of programs before their implementation, and one of the appropriate methods is to use special categorical structures called coalgebras.
The starting notion in the coalgebraic approach is a signature used in the theory of algebraic specifications [9]. A signature Σ consists of types, e.g. and operation symbols of the form . In a signature we distinguish:
· constructor operation symbols defined inductively. They tell us how to generate (algebraic) data elements;
· destructor operation symbols, also called observers or transition functions defined coinductively. They tell us what we can observe about our data elements;
· derived operations that can be defined inductively or coinductively.
If we define a derived operation inductively, we can define the value of f on all constructors. In a coinductive definition of derived operation f we can define the values of all destructors on each outcome [10, 11].
The next step is to define a basic category as a state space. A category is a mathematical structure consisting of a class of objects, e.g. and a class of morphisms of the form between them [12, 13]. Every object has its identity morphism and morphisms are composable. Because the objects of a category can be arbitrary structures, categories are useful in computer science, where we often use more complex data structures not expressible by sets. In the coalgebraic approach, the objects are states and morphisms are the operations that change states, obviously destructor operations from the corresponding signature.
The basic category of states for a coalgebra has to satisfy several properties. First, this category has to have terminal object to indicate abnormal ending of execution. Second, it needs to have finite products, coproducts and exponentials [14] for constructing polynomial endofunctors introduced below. Third, to model the infinite execution of a program, it needs to have a colimit for any cocone consisting of an infinite sequence of states, i.e. for infinite composition of morphisms [15].
Execution of a program is modelled by a polynomial endofunctor. In the following text we introduce this concept. A functor from a category to a category is a morphism defined as a pair of functions:
and |
which are functorial, i.e. they preserve identities and composition. For a morphism in its image is a morphism in :
|
(1) |
A special functor is endofunctor over a category . In the coalgebraic approach, polynomial endofunctors are widely used. They are constructed by using constants, identities, products, coproducts and exponentials over a state space [16]. A polynomial endofunctor is determined by the corresponding signature, especially by its destructor operations [17]. The syntax of a polynomial endofunctor can be described by the following inference rule:
|
, |
(2) |
where stands for a state space and is a set of constants. The product expresses a change of state from X together with some observable input or output value from Y. The coproduct expresses either a change of state or some observable value, possibly an undefined end of execution [18]. For instance, when an execution of a program can crash, we define this possibility by polynomial endofunctor . Exponential objects express functions from to . In summary, a polynomial endofunctor models the steps of execution and it captures the kind of behaviour that can be observed.
We use the category of sets as a basic category for coalgebras. This category has sets as objects and functions as morphisms. Therefore, we introduce the concept of polynomial endofunctors for this category. Polynomial endofunctors must be defined for objects and also for morphisms.
Consider the category and its objects and . The product is defined by
|
. |
(3) |
The product operation which assigns its cartesian product to a pair of objects can be also applied for morphisms. Let and be morphisms, then we can define a function by
|
. |
(4) |
The coproduct operation is defined by
|
(5) |
|
|
|
|
The first members of pairs, and serve to force the union to be disjoint. The coproduct can also be applied for morphisms, e.g. for and we can define the coproduct of morphisms such that for
|
|
|
Now we have defined polynomial endofunctors for objects and morphisms in the category and we can introduce the concept of coalgebras.
Let be a polynomial endofunctor determined by its corresponding signature. An F-coalgebra, also called coalgebra of type is a pair
|
(7) |
where X stands for a state space and is a structure map
|
(8) |
where is a finite tuple of destructors
|
(9) |
The structure map acts as a destructor, it decomposes elements into their constituent parts. Depending of the definition of it provides the next state possibly with observable values. In other words, a coalgebra investigates states, operations on them. It uses destructor operations returning elements of data structures. The essence of the coalgebraic behavioural theory is the tension between what is actually inside and what can be observed externally [19].
At the end of this section, we show a simple example of how bank account can be modelled by coalgebra.
Example 1. Assume a program of bank account with the following fragment of signature:
We present only destructor operation symbols of a bank account that are important for constructing coalgebra. We assign the following representations to types and operations:
- the type we represent as the set of real numbers ;
- the type we represent as a set of lists of values in the form
|
, |
(10) |
where . Double colon denotes the operation append which extends a list by appending element at the end, e.g. a state is obtained by an operation .
To the operation we assign the function
|
(11) |
that for a state returns the actual balance attribute of this state, i.e. a sum of all values on an account; and to the operation we assign the following function
|
, |
(12) |
that for a state x and input value r returns a new state – it appends the new amount at the end of list.
The basic category consists of states as objects and destructors and as morphisms. Each state is a finite list of real numbers representing the history of an account.
Now we construct polynomial endofunctor using currying on as
|
. |
(13) |
|
|
|
The structure map of coalgebra is a tuple of destructors :
|
. |
(14) |
A bank account with these functions is an F-coalgebra
.
It holds
|
(15) |
where the maps and stand for obvious projections defined to a product.
This coalgebra models a correct bank account which records in the state the history of all deposited sums and returns the total balance on the account when the function is applied.
Let the state space be the set of finite strings over reals and let the symbol denote the sum of all reals in . Then the functions in coalgebra are defined as follows:
|
(16) |
where a double colon denotes the operation append which appends an object at the end of the list .
3. Structural operational semantics as coalgebra
Structural operational semantics is a very popular semantic method and it is also called small-steps semantics. It describes a meaning of a program in elementary steps which can be considered as transitions between memory states [20]. A state is considered as an abstraction of memory. and each change of some value stored in memory is considered as a change of state. This change of state is described by a transition relation [21, 22].
It is useful to use the concepts of the category theory for modelling structural operational semantics. Categories provide a powerful tool for expressing and modelling the program execution. If we consider memory states as category objects, then execution steps (states’ changes) are morphisms between states.
3.1. Simple imperative language Jane
For our aims, we define a simple language Jane which consists of all traditional van Dijkstra’s constructs (D-Charts) for imperative languages and we formulate principles of structural operational semantics in a category. The category serves here as an abstract model of computer memory with possible states, i.e. it can be considered as a state space. Our approach can also be extended for blocks, declarations and user input but here we concerned only with basic imperative features of language.
We introduce for Jane the following well-known syntactic domains:
|
digit strings |
|
variables’ names |
|
arithmetic expressions |
|
Boolean expressions |
|
statements |
The Jane language contains the following statements: assignment, empty statement (considered also as an empty sequence of statements), sequences of statements, conditional statement and prefix logical cycle statement:
Semantics of arithmetic and Boolean expressions are formulated in [23].
Each variable in a program is stored in computer memory. A variable is considered as a container for some value. In our language we consider only implicit types of variables - integer numbers. Here the transient data are Boolean values, but they are never stored as stable values in memory.
We assume that each variable occurring in a program is implicitly allocated and we do not consider the variables’ declarations. A value of allocated variable can be assigned and modified inducing a change of state.
3.2. Signature for states and their representation
States we define as an abstract data type. Its signature consists of types and operation symbols on the type :
The operation symbols have the following intuitive meaning: creates the initial state of a program and returns a variable value in a given state.
Now we assign the representation to the signature . We assign to the type the set of integers together with the undefined value :
|
(17) |
The type is represented by a countable set of variables’ names . The type is represented by a set of states . Every particular state is defined as a function
|
|
(18) |
Each state expresses one moment of program execution, roughly speaking a snapshot. Then any state is expressed as a sequence
|
(19) |
of ordered tuples where is the name of variable with its actual value
The first two operations in signature we define as follows. The operation creates the initial state of a program with no variable defined by
|
(20) |
where represents an empty position and an empty value. The operation returns the value of a selected variable and is defined as follows:
|
(21) |
Such defined states we consider as category objects in our model. We also consider a special state expressing the undefined state
|
(22) |
3.3. Operational semantics of Jane and category of states
In this section we sketch how to construct a categorical model based on structural operational semantics. The most important feature of this semantic method is the detailed description of a program execution in small steps.
We construct a model of structural operational semantics as a transition system, which models program behaviour on a state space [24]. The execution of a statement is defined by inference rules which are listed in [24, 25].
A step of execution with a possible change of state is in structural operational semantics expressed as a transition . This transition is a relation between an input state and an output state . Any change of state is done as one-step action [23]. On the other hand, if a statement is not executed in one step, then the transition is expressed as follows:
|
(23) |
where is a sub-statement of that still should be executed. In both cases the transition rules express one action during the program execution.
A categorical model, the category we construct as follows. We consider:
· category objects as states from , and
· category morphisms as transitions.
The change of state we define by the following function from signature:
|
(24) |
|
|
|
|
For a statement the function is defined as follows:
So any morphism in the category of states can be considered as a function A morphism is a unique morphism which sends any state to the undefined state :
|
(25) |
|
|
|
|
and it represents the situation when an error occurs during the program execution and the program cannot continue its execution. Because from any object in a category, there exists only one morphism into the undefined state, it is an object which has a property of terminal object in the category.
3.4. Coalgebra for Jane as a transition system
An F-coalgebra, also called coalgebra of type F or F-system, is a pair where is a state space of the coalgebra and is the structure map of the coalgebra on (8):
This structure map acts as a destructor operation. It takes an element of the F-coalgebra and decomposes the elements into their constituent parts. This is a common feature of coalgebras, and this point of view is dual to the point of view that algebras are objects together with combinatory principles [26-28].
An endofunctor on the category of states
|
(26) |
for coalgebra is of the type where stands for a singleton of an undefined value and is a placeholder for a state space.
In our case, a state space is the set of category objects and is a singleton set containing only an undefined state. The endofunctor on the category of states is defined as follows:
|
(27) |
|
|
|
|
This endofunctor sends objects to objects:
|
(28) |
and morphisms to morphisms:
|
(29) |
Applying the functor on statements in program, we get steps of its execution.
Example 2. We show a simple example of defining structural operational semantics of a program written in Jane.
We consider the simple program with input values and that would be sorted according the descending order. Namely if , and should switch their values.
We show the solution for both possible cases, when the Boolean expression in the conditional statement evaluates to and then to .
Let the program contains only one statement :
and let the input states be:
a) ; and
b) .
In the case a) when the condition evaluates to ,
|
, |
(30) |
we have the following sequence of states:
|
(31) |
The sequence of states during the program execution is depicted in Figure 1.
Fig. 1. States during the program execution - case a
In the case b) the condition evaluates to ,
|
, |
(32) |
the execution of program is evaluated as follows:
|
(33) |
|
|
|
|
so the initial state is unchanged (Fig. 2).
Fig. 2. An unchanged state - case b
In our program, the variables and store the observable values. The variable is an auxiliary variable and it is not observable for a program user.
4. Conclusion
In this short contribution, we presented the main ideas of the coalgebraic approach of the behavioural theory and the process of defining coalgebra for observing the behaviour of programs and program systems. The main part of our paper is the coalgebra for the Jane simple imperative language, constructed as transition system in the sense of structural operational semantics. Such modelled semantics are easy to comprehend and it gives illustrative information about execution steps for programs.
We would like to extend this approach for language with declarations, input/output statements and procedures.
Our next goal is to investigate bisimilarity, the relation between states that look to be the same and to formulate coinductive proofs of behaviour.
Acknowledgment
This work has been supported by Grant No. 002TUKE-4/2017: Innovative didactic methods of education process at university and their importance in increasing education mastership of teachers and development of students competences.
References
[1] Novitzká V., Mihályi D., Steingartner W., Coalgebraic behaviour of algebraic programs, Analele Universitatii din Oradea, Proc. 8th International Conference on Engineering of Modern Electric Systems,University of Oradea, Romania 2007, 9, 60-64.
[2] Rutten J., Universal Coalgebra: A Theory of Systems, Technical Report CS-R9652, CWI, Amsterdam 1996.
[3] Jacobs B., Introduction to Coalgebra, Towards Mathematics of States and Observations, Version 2.0, 2012.
[4] Reichel H., Behavioural equivalence - a unifying concept for initial and final specifications, 3rd Hungarian Computer Science Conference, Akadémia kiadó, 3, 1981.
[5] Gumm P., Elements of the General Theory of Coalgebras, Notes of Lecture given at LUATCS’99: Logic, Universal Algebra, Theoretical Computer Science, Johanesburg 1999.
[6] Jacobs B., Objects and Classes, Co-Algebraically, [In:] Object Orientation with Prallelism and Persistence, Volume 370 of the series The Kluwer International Series in Engneering and Computer Science, Springer US, 1996, 83-103.
[7] Jacobs B., Rutten J., A tutorial on (co)algebras and (co)induction, Bulletin of the European Association for Theoretical Computer Science 1997, 62, 222-259.
[8] Slodičák V., Macko P., Some New Approaches in Functional Programming Using Algebras and Coalgebras, [In:] Electronic Notes in Theoretical Computer Science 2011, 279, 3, 41-62.
[9] Ehrig H., Mahr B., Fundamentals of Algebraic Specification 1: Equations and Initial Semantics, EATCS Monographs on Theoretical Computer Science, 1985.
[10] 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, 38-99.
[11] Chin W., A brief introduction to coalgebra representation theory, [In:] J. Bergen, S. Catoiu, W. Chin (eds.), Hopf Algebras, Marcel Dekker Inc., USA, 2004, 109-133.
[12] Brandenburg M., Einführung in die Kategorientheorie, Springer Spektrum 2016.
[13] Walters R.F.C., Categories and Computer Science, Cambridge University Press, New York 1992.
[14] Awodey S., Category Theory, Carnegie Mellon University, 2005.
[15] Escardó M.H., Streicher T., Induction and recursion on the partial real line with applications to real PCF, Theoretical Computer Science 1999, 210, 1, 121-157.
[16] Goldblatt R., A calculus of terms for coalgebras of polynomial functors, Electr. Notes of Theroretical Computer Science 2001, 14, 1.
[17] Kock J., Notes on polynomial endofunctors, Universitat Autonoma de Barcelona, 2007.
[18] Deák A., Mihályi D., Jakab F., Exception modeling in the category, Proc. ICETA, IEEE, New York 2016, 49-53.
[19] Crole R.L., Lectures on (co)induction and (co)algebras, Dept. Mathematics and Computer Science, University Leicester 2006.
[20] Fernández M., Programming Languages and Operational Semantics: A Concise Overview, Springer, 2014.
[21] Nygaard M., Transition Systems, University of Aarhus, 2004.
[22] Ivaniga T., Ovseník Ľ., Turán J., Experimental Model of Passive Optical Network Technical University of Košice. ICCC 2015: 16th International Carpathian Control Conference, May 27-30, 2015, Szilvásvárad, Hungary, 186-189.
[23] Steingartner W., Novitzká V., Categorical model of structural operational semantics of imperative language, J. Informational and Organizational Sciences 2016, 40, 2.
[24] Plotkin G.D., The origins of structural operational semantics, J. of Logic and Algebraic Programming 2004, 60-61, 3-15.
[25] Sculthorpe N., Torrini P., Mosses P.D., A modular structural operational semantics for delimited continuations, Proc. Workshop in Continuations, London 2015, 63-80.
[26] Hughes J., A Study of Categories of Algebras and Coalgebras, Ph.D. Thesis, Carnegie Mellon University, Pittsburgh PA 2001.
[27] Adámek J., Milius S., Moss L.S., Initial algebras and terminal coalgebras, 2010 (unpublished).
[28] Herceg Đ., Radaković D., Extensibility of an Interpreted Language Using Plugin Libraries, Numerical Analysis and Applied Mathematics ICNAAM 2011, AIP Conf. Proc. 2011, 1389, 837-840.