The semantics of programs written in some languages is concerned with the interpretation in various types of models. Denotational semantics expresses the meaning of programs by functions from syntactical domains to semantic domains which can be non-trivial mathematical structures. On the other hand, structural operational semantics describes the program behaviour in the form of states' changes caused by the execution of elementary steps. We present in this paper categorical representation of denotational semantics in category of states as objects and semantic functions as morphisms. We present also categorical representation of structural operational semantics in category as a transition system where states are objects and morphisms are elementary transitions. We also sketch how to de ne endofunctor on the category of states and how to construct a Q-coalgebra of the functor.
Introduction Copyright © by the paper's authors. Copying permitted for private and academic purposes.
Operational semantics expresses each step of program execution in detail using transition relations. It provides not only a meaning of a program but also its observable behaviour. This method requires medial knowledge of mathematics and it is more understandable for practical programmers. Structural operational semantics was formulated by Gordon Plotkin in [Plo81] and the main ideas and motivations are explained in [Plo04].
In the last decades the categorical structures have become useful for modeling the meanings of programs. Categories are mathematical structures that consist of objects and morphisms between them. They enable to work with more complex structures as the sets are and their properties can be represented also graphically. There are several publications concerning with categorical denotational semantics, e.g. in [Ste15b]; they are based on a category where the category objects, the semantic domains, represent the types of data structures and category morphisms are operations. Such models are suitable primarily for functional programming languages.
When we are interested in behaviour of programs, operational semantics seems to be the most adequate method. The useful categorical structures for operational semantics are coalgebras. They enable to generate observable behaviour of a running program step by step [Plo04, Tur97]. A coalgebra can be considered as a study of states and operations on them. The states form a state space that is hidden from an observer. A relation between what is actually inside and what can be observed externally is the foundation of coalgebras [Jac97]. Coalgebras are constructed using polynomial endofunctors over a category of states. In [Abo14] is elaborated coalgebraic semantics for imperative languages with non-determinism and other e ects. The author constructs a monad over state space for the e ects of a language and the behaviour of a program is obtained by the composition of a polynomial endofunctor and a monad.
By contrast to the works in the area of denotational semantics and operational semantics mentioned above, we attempt to de ne them so that they are both intelligible and demonstrative for students of computer science and also for practical software engineers. The aim of our paper is to present principles of denotational and operational semantics in terms of categories as simple as it is possible without loss of exactness. We de ne a simple imperative language J ane with basic statements. In the case of denotational semantics we construct a category of states, where the objects are states and morphisms are statements. For operational semantics we construct also a category of states where the objects are states but morphisms are transition functions. We model behaviour of programs as an appropriate endofunctor over this category as a coalgebra. In the both cases we use the categories which objects are sets and we discuss the properties of them to be legal categories. The advantage of our approach is that it provides precise graphically illustrated denotational and operational semantics without need of deeper knowledge of mathematics and therefore it is suitable for teaching.
The e ectiveness of categories is in their expressive power. Categorical models are highly illustrative and their graphical representations are very good readable and understandable. The e ectiveness of coalgebras we showed in [Ste16] where we presented construction of coalgebra for concrete programming problem taught on SLGeometry tool. Then the next step could be a construction of an appropriate transition system as category of states. Moreover, categorical semantic methods are suitable also for e-Learning education process. They can be easily implemented and integrated into standard e-Learning tools such as LMS Moodle. 2
Language J ane In our paper we use a simple language J ane. This language consists of traditional syntactic constructions of imperative languages, namely arithmetic and Boolean expressions and statements. For this language the well-known syntactic domains are introduced: n ∈ Num - digit strings x ∈ Var - variable names e ∈ Aexpr - arithmetic expressions b ∈ Bexpr - Boolean expressions
S ∈ Statm - statements
Five Dijkstra's elementary statements that are elements of the syntactic domain Statm, S ∈ Statm, are considered: assignment, empty statement, sequence of statements, conditional statement and cycle statement:
S ∶∶= x ∶= e S skip S S; S S if b then S else S S while b do S: The semantics of arithmetic and Boolean expressions was formulated in [Ste15a]. For preservation of simplicity, here we do not consider blocks, input statement and declarations.
The states as memory abstraction A program in J ane is a sequence of the statements. Execution of a program causes a change of some memory cells. Every snapshot of a memory during program execution can be abstracted as a state where program variables have assigned some values. Execution of a statement can modify some values of program variables, i.e. a state is changed. A meaning of a program is then the change of an initial state before program execution to a nal state after program execution. Therefore state is a basic concept in the de nition of formal semantics of imperative languages.
We de ne the semantic domain State as an abstract data type with the following signature: State = types ∶ opns ∶
State; V ar; V alue init ∶→ State get ∶ V ar; State → V alue V ar and V alue are type names for program variables and values, respectively. The operation speci cations have the following intuitive meaning: • init merely creates the initial state of a program; • get returns a variable value in a given state.
Now we assign the representation to the signature of states integer numbers together with the unde ned value :
We assign to the type V ar a countable set Var of variable names. Our representation of an element of type State has to express a variable name and its value.
We assign to the type State the set State of states. Every state s ∈ State is represented as a function Each state s expresses one moment of program execution. We express a state s as a sequence: of ordered tuples where x is the name of a variable with its actual value v.
We de ne representations of operation speci cations from the signature de ned by
JinitK = s0; (3) creates the initial state s0 of a program possibly with input values of variables. Its role is to create a new sequence of state at the beginning of program execution.
The operation JgetK returns the value of a variable and is de ned by
State as follows. The operation JinitK
JgetK(x; ⟨: : : ; (x; vi); : : : ; (z; vk); : : :⟩) = vi; from the de nition of state.
States de ned above will be category objects in our model. We also consider a special state expressing the unde ned state.
Value = Z ∪ {} : s ∶ Var → Value: s = ⟨(x; v1) ; : : : ; (z; vn)⟩
(x; v) ; s = ⟨(; )⟩
JskipK • semantic functions as category morphisms.
JskipKs = s: JS1; S2K = JS2K ○ JS1K Statements execute program actions, i.e. they get values from the actual state and possibly provide new values. A state is changed if a value of a program variable is modi ed. We model the change of states as the semantic function JSK between states, where S is a statement:
JSK ∶ s → s′; where s and s′ are states. This function is partially de ned, because the resulting state s′ can be unde ned. To be a semantic function a morphism in CState, we extend JSK to total function using a special object of unde ned state s:
JSK ∶ s → s if a statement S has unde ned meaning in its input state s.
Category CState has to satisfy the following axioms from the de nition of categories [Bar90]: • each object has identity morphism; • for two composable morphisms there exists a morphism that is their composition.
A morphism is CState is an application of the semantic function JSK. As we see bellow, the role of identity morphism plays the semantic function applied on the empty statement. The second axiom is satis ed in the case of sequence of statements. Therefore we can state that CState is a category.
We follow with the de nition of the semantic function JSK for J ane statements. Assignment statement x ∶= e assigns a value of an arithmetic expression e in a state s to the variable x.
The semantic function for assignment statement is de ned as follows:
s [(x; v) ↦ (x; JeKs)] ; Jx ∶= eKs = s ; for (x; v) ∈ s; otherwise and it is illustrated in Figure 1.
The empty statement skip does not do anything, i.e. it does not change the state. Clearly, the semantic function applied on the empty statement is the identity morphism on a state s (Figure 2) and it is de ned by: A sequence of statements S1; S2 is executed one by one and can be modeled as a composition of morphisms (Figure 3) (6) (7) (8) (9) (10) s
JS1K If a state s′ is unde ned, i.e. s′ = s, then the execution of the whole sequence of statements provides unde ned state:
JS1; S2Ks = JS2K (JS1K) s:
JSKs = s:
(11)
(
Conditional statement
if b then S1 else S2 causes branching of execution depending on the value of a Boolean expression. The semantic function for conditional statement is de ned as:
⎧⎪⎪ JS1Ks; if JbKs = true; Jif b then S1 else S2Ks = ⎪⎨ JS2Ks; if JbKs = false; (13)
⎪⎪⎪⎩ s; otherwise: It is interesting that the path of a program can follow either to the state JS1Ks or to the state JS2Ks, i.e. deterministically and the branching is unseen in CState as it is illustrated in Figure 4. The result state s′ can be either JS1Ks or JS2Ks, but only one of them.
Now we consider cycle statement
while b do S Its execution also depends on the value of Boolean expression b. If JbKs evaluates to true in an actual state s, the body S of a cycle is executed, then again b is evaluated in a possibly modi ed state. If JbKs evaluates to false, execution of cycle statement is nished and we obtain the result state.
The traditional denotational semantics of a cycle statement is de ned by using xpoint operator. This approach is obvious if the categorical model is a category of types. Existence of the least xed point ensures that while statement nishes, in the other case the execution of while statement is in nite, i.e. the denotational semantics of this statement is not de ned. This approach is discussed in detail in [Nie07, Sch97]. In general, the computational categorical models have continuous lattices as objects and continuous functions as morphisms [Sto77]. Such models require some structure on endomorphisms [Esc07].
In our approach we use categorical model with states as objects and functions as morphisms. The domains (states) are sets, not lattices; therefore we use another concept for handling in nite cycles. The execution of a while statement is a path of morphisms, i.e. a composition of morphisms. This path can be either nite or in nite and we need some construction in our category to solve both cases. The useful construct is the colimit of a diagram. Consider a diagram D consisting of the composition of morphisms This composition of morphisms is a composition of semantic functions applied on while statement with actual states. This in nite composition is a morphism
D ∶ s0 → s1 → s2 → : : : si → si+1 → : : :
(
fi∞+1 fi∞ s0 f0∞
f1∞ s1
f2∞ s2 . . . si
si+1 . . . Because the objects in CState are sets, such colimits always exist. 5
Example of categorical denotational semantics We present in this section a short example. We show how to nd a semantics of program, that calculates integer division and modulo. Let the program S0 be the following: and let the input state be s0 = [x ↦ 17; y ↦ 5]. We assume in variable x a divident, and in variable y a divisor. We introduce the following substitutions in our program: A meaning of the program S in an input state s0 is given as follows:
JS1; S2Ks0 = JS2K (JS1Ks0) = JS2Ks1 = JS2K (Jx ∶= x − yK (Jz ∶= z + 1Ks1)) = JS2K (Jx ∶= x − yKs2) = JS2Ks3 = JS2K (Jx ∶= x − yK (Jz ∶= z + 1Ks3)) = JS2K (Jx ∶= x − yKs4) = JS2Ks5 = JS2K (Jx ∶= x − yK (Jz ∶= z + 1Ks5)) = JS2K (Jx ∶= x − yKs6) = JS2Ks7 = id(s7) = s7 Particular states during the program execution are listed in Figure 6.
Expected results are: a quotient is after the execution stored in the variable z and remainder in variable x.
We can observe that program is expressed as a compound function consisting of more morphisms which form together a path in category. The compound function is constructed as follows:
JSK = JskipK ○ Jx ∶= x − yK ○ Jz ∶= z + 1K ○ Jx ∶= x − yK ○ Jz ∶= z + 1K ○ Jx ∶= x − yK ○ Jz ∶= z + 1K ○ Jz ∶= 0K:
(
A model of structural operational semantics is a transition system which models program behaviour on a state space [Jon03, Plo04]. The change of state is de ned for particular statements by inference rules.
A transition is a relation between input state s and output state s′. A change of state is done as one-step action [Rad13]. If a statement is not being executed in one step, then a transition can be written as:
⟨S; s⟩ ⇒ s′ ⟨S; s⟩ ⇒ ⟨S′; s′⟩ : In both cases a transition rule expresses one action during the program execution. The inference rules for J ane in structural operational semantics are the following [Nie07]: ⟨x ∶= e; s⟩ ⇒ s[x ↦ JeKs]
(1os) ⟨skip; s⟩ ⇒ s
(2os) ⟨S1; s⟩ ⇒ ⟨S1′; s′⟩ 1 ⟨S1; S2; s⟩ ⇒ ⟨S1′; S2; s′⟩ (3os)
⟨S1; s⟩ ⇒ s′ 2 ⟨S1; S2; s⟩ ⇒ ⟨S2; s′⟩ (3os)
JbKs = true ⟨if b then S1 else S2; s⟩ ⇒ ⟨S1; s⟩ (4torsue)
JbKs = false ⟨if b then S1 else S2; s⟩ ⇒ ⟨S2; s⟩ (4foaslse) The inference rule for pre x cycle uses semantic equivalence: ⟨while b do S; s⟩ ⇒ ⟨if b then (S; while b do S) else skip; s⟩ (5os) In these inference rules, JeK and JbK are semantic functions, which assign to any syntactic well-formed expressions their meanings - an integer value, a Boolean value, resp. The result of the functions JeK and JbK, where e stands for an arithmetic expression and b stands for a Boolean expression, depend on an actual state JeK ∶ State → Value;
JbK ∶ State → {false; true} : Function produces transient data, that are consumed during the program execution and their values are never stored into memory - they are used only for a ecting the control ow in a program.
A categorical structure that models observable behaviour of programs is a coalgebra. It is constructed over a base category of states using a polynomial endofunctor. A base category DState consists of • objects that are states from State; and • morphisms that are transitions.
The objects of DState are the same as for the category CState constructed for categorical denotational semantics but these two categories di er in morphisms. Because we need transitions as morphisms, we de ne the transition function next: that return for a statement S next ∶ Statm → (State → State);
nextJSK ∶ State → State tshtaetenmexetntsstainteJobatnaeinbeyd: from the execution of the rst step of a statement JSK. We de ne this function for ⎧⎪ s′ = s [x ↦ JeK] if S = x ∶= e; ⎪⎪⎪⎪⎪ s if S = skip ⎪⎪⎪⎪⎪ or S = while b do S and JbKs = false; nextJSK(s) = ⎪⎪⎪⎪⎪⎨⎪ nneexxttJJSS12′;K(Ss2′K)(s′) iiff SS == SS11;; SS22 aanndd ⟨⟨SS11;; SS22;; ss⟩⟩ ⇒⇒ ⟨⟨SS12′;; sS′2⟩;;s′⟩ ; (17) ⎪⎪⎪⎪⎪⎪⎪⎪⎪ nneexxttJJSS12KK((ss)) iiff SS == iiff bb tthheenn SS11 eellssee SS22 aanndd JJbbKKss == ftarlusee;; ⎪⎪⎪⎪⎪⎩⎪⎪⎪ anbeoxrttJ(Ss;)while b do SK(s) iofthSer=wwihsei:le b do S and JbKs = true; From this de nition follows that any morphism in the category of states DState can be considered as an application of function nextJSK for a given statement.
Now we construct the polynomial endofunctor
Q ∶ DState → DState that to any statement S and an object s assigns the next state or unde ned state. The name polynomial [Koc12] indicates the polynomial form of a functor constructed using products and coproducts. For our purposes we de ne a functor where State is a state space. We de ne this functor for objects and morphisms in DState as follows:
Q(State) = 1 + State Q(s) = Q(nextJSK) = s + nextJSKs abort + next S
J K abort ∶ s ⇢ s where abort is a unique morphism which sends any state to the unde ned state s: 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 unde ned state, it is an object which has a property of terminal object 1 in the category.
A Q-coalgebra, also called coalgebra of type Q or Q-system, is a pair (State; nextJSK), where State is a state space of the coalgebra and nextJSK is the structure map of the coalgebra on State:
nextJSK ∶ State → Q(State): This structure map acts as a destructor. It takes an element of the Q-coalgebra and decomposes the element into its 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 [Hug01]. 7
Example of categorical operational semantics We present in this section a short example of nding a meaning of a program in categorical operational semantics. We continue with the same program as in Section 5 - we show how to nd a semantics of program, that calculates integer division and modulo. The code of program S0 is: (18) and let the input state be again s0 = [x ↦ 17; y ↦ 5]. We assume in variable x a divident, and in variable y a divisor. We follow the substitutions in our program from Section 5: z ∶= 0; while (y ≤ x) do (z ∶= z + 1; x ∶= x − y); S1 = z ∶= 0
S2 = while (y ≤ x) do (z ∶= z + 1; x ∶= x − y)
Here the coalgebra state space is the set of category objects Ob(CState) = State and 1 = {s} is a singleton set containing only an unde ned state. The endofunctor on category of states is de ned as follows: and it sends objects s ∈ State to objects: and morphisms to morphisms:
Q(State) = 1 + State;
Q(s) = s + nextJSKs; Q(nextJSK) = abort + next S
J K
s0 = ⟨(x; 17); (y; 5)⟩ s1 = ⟨(x; 17); (y; 5); (z; 0)⟩ Jy ≤ xKs1 = true s2 = ⟨(x; 17); (y; 5); (z; 1)⟩ s3 = ⟨(x; 12); (y; 5); (z; 1)⟩ Jy ≤ xKs3 = true s4 = ⟨(x; 12); (y; 5); (z; 2)⟩ s5 = ⟨(x; 7); (y; 5); (z; 2)⟩ Jy ≤ xKs5 = true s6 = ⟨(x; 7); (y; 5); (z; 3)⟩ s7 = ⟨(x; 2); (y; 5); (z; 3)⟩ Jy ≤ xKs7 = false Expected results are: a quotient is after the execution stored in the variable z and remainder in the variable x. ◻ 8
Conclusion We presented in our paper a new approach how to de ne denotational semantics and operational one in terms of categories. In both cases a state is a basic concept. A state represents a snapshot of a memory that can be changed during the program execution. In denotational approach category objects are states and morphisms are functions on states. We discussed also how to solve the situation of in nite sequence of states using colimits of diagrams. In the operational semantics the category objects are also states but the morphisms are transitions, i.e. elementary actions representing detailed steps of execution. The behaviour of a program is obtained by polynomial endofunctor and structure map of coalgebra.
Very high illustrative power of categories is very fruitful for innovative didactic methods used in education process of young software engineers and IT experts.
We want to extend our approach by introducing and modeling also user inputs and outputs, blocks, variable declarations and procedures and then to construct denotational and operational semantics for real programming language in categorical terms by following our ideas in [Ste17].
Acknowledgements 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. [Esc07]
Escardo, M.H.: Recursion and Induction on the Real Line, In: Proceedings for the Second Imperial College Department of Computing Workshop on Theory and Formal Methods, M ller Centre, Cambridge, 11-14 September 1994. [Hug01] Hughes J.: A Study of Categories of Algebras and Coalgebras, Ph.D. thesis, Carnegie Mellon University,
Pittsburgh PA, USA, 2001. [Jac97] Jacobs, B., Rutten, J.: A Tutorial on (Co)Algebras and (Co)Induction, EATCS Bulletin Vol. 62, 1997, pp. 222-259. [Jac05] Jacobs, B.: Introduction to coalgebra. Towards Mathematics of States and Observations (draft) (2005). [Jas11]
Jaskelio , M., Ghani, N., Hutton, G.: Modularity and Implementation of Mathematical Operational Semantics, Electronic Notes in Theoretical Computer Science, Vol. 229, No. 5, 2011, pp. 75{95, Proceedings of the Second Workshop on Mathematically Structured Functional Programming, MSFP 2008. [Jay91] Jay, B.: Fixpoint And Loop Constructions As Colimits, Lecture Notes In Mathematics, Vol. 1488, pp.
187-192, 1991. [Nie07] [Per15] [Plo81] [Plo04]
Perhac, J., Mihalyi, D.: Intrusion Detection System Behavior as Resource-Oriented Formula, Acta Electrotechnica et Informatica, Vol. 15, No. 3, Technical University of Kosice, Slovakia, 2015. Plotkin, G. D.: A Structural Approach to Operational Semantics, Technical Report DAIMI FN-19, University of Aarhus, 1981. [Rad13] Radakovic, D., Herceg, D.: A Platform for Development of Mathematical Games on Silverlight, Acta
Didactica Napocensia, Vol. 6, No. 1, Babes-Bolyai University, pp. 77-90, 2013. [Sch97] Schmidt, D.: Denotational Semantics. A methodology for language development, 1997. [Slo11]
Slodicak, V., Macko, P.: Some New Approaches in Functional Programming Using Algebras and Coalgebras, Electronic Notes on Theoretical Computer Science, Vol. 279, No. 3, 2011, pp. 41{62. [Ste15a] Steingartner, W., Novitzka, V.: A new approach to operational semantics by categories, Proceedings of the 26th Central European Conference on Information and Intelligent Systems, CECIIS 2015, Varazdin, University of Zagreb, 2015.