Perspectives of semantic modeling in categories

Abstract

This paper explores the domain of semantic modeling, emphasizing the thoughtful influence of category theory on imperative programming. We aim to present a formal semantics model by seamlessly integrating categorical concepts. A core focus of this study is clarifying relationships between objects representing the memory states as denotation functions. Extending our exploration, we examine categorical modeling within the context of structural operational semantics. An important aspect is the purposeful use of coalgebras to express program behavior, especially concerning memory configurations. Our methodology involves modeling denotation within categories, considering input/output values and state dynamics. This synthesis leads to a comprehensive and robust semantic framework. Notably, our research concludes with the development of a category tailored for memory configurations, effectively mirroring program transitions. Execution dynamics finds representation through a customized polynomial endofunctor, accommodating a range of transition types. Importantly, our study contributes mathematical rigor to the domain of program semantics, offering practical applications across various IT challenges, including recursive calculations, function relationships, and component program systems. Significantly, this study underscores the enduring relevance of category theory in the dynamic landscape of semantic modeling, offering insights into potential practical applications within programming and related fields.

Introduction

Semantic (formal) modeling plays a crucial rôle in various fields, enabling the representation and understanding of complex information structures. In recent years, an escalating interest has emerged in the investigation of semantic modeling techniques in the domain of the mathematical category theory. Categories serve as fundamental frameworks for organizing and comprehending diverse entities, and the incorporation of semantic modeling can greatly enhance the effectiveness and efficiency of categorical representations and implementing the categories in practice. This paper explores the perspectives of semantic modeling in categories, investigating its potential applications, benefits, and challenges.

Category theory provides a formal basis for engineering modeling, as well as in the disciplines of mathematics and science. The wide possibilities of modeling with the help of category theory are given primarily by the properties of categorical structures – objects as building blocks of categories can express structures of arbitrary complexity. Category theory can be used to formalize mathematics and its concepts as a collection of objects and morphisms (also denoted as arrows), sometimes called morphemics (Mabrok and Ryan 2015). Relationships between objects are expressed by morphisms, and depending on the mathematical properties of the structures, categories provide various specific morphisms like isomorphism and monomorphism, etc. Indeed, much of category theory’s power comes from its recursive ability to treat ever more complicated systems as building blocks in the next level of abstraction (Vickers et al. 2013): thanks to higher-order abstractions, it is possible to express relationships between categories (as functors) or relationships between functors (as natural transformations). In this sense, the key to compositional modeling is developing the mathematics so that putting together smaller models to form bigger ones is an example of composing morphisms in a category and writing software to implement those ideas in a system that is friendly to category theory (Baez et al. 2023). The modeling capabilities and expressive power of the categories are very broad in this regard. The main thing to point out is that categorical methods provide tools for expressing and relating the formal models (Diskin 2001). Recently (mostly in the last two decades), formal methods (system design approaches that employ rigorously defined mathematical models in the development of both software and hardware systems) have played an important role in software engineering. With increasing robustness and complexity and hybridity, it is increasingly necessary to adhere to the design principles of correct and reliable programs and program systems with the necessity of eliminating the maximum number of errors in the process of design, development, and even after the deployment of systems. Indeed, until recently, software engineers may feel that they could live without mathematical models: just build the new software by whatever means available, check and debug it, and keep doing this throughout the software life-cycle (Diskin and Maibaum 2012).

There is a very wide spectrum of formal methods that have successfully played a key role in practice of computer science: model checking, B method, abstract state machines, process calculus, several modeling languages, various semantic methods and approaches, etc. All formal methods are grounded in formal semantics. Semantic methods belong to the frequently used formal methods for determining the meaning of programs written in programming languages, with a primary focus on ensuring program correctness. While these methods provide a rigorous foundation for reasoning about program meaning and behavior, they are not intended to address performance metrics such as computational efficiency or memory usage, which lie beyond their primary scope. Formal semantics abstracts away from the specific architecture on which computation is performed. Its primary role is to model the programs and ensuring their correctness with respect to a given specification. Individual methods are formulated to serve some specific purposes. In the field of language semantics, there are many interesting results and approaches to the semantics of functional languages, also expressed in category theory, but there are few ways of applying category theory to express the meanings of imperative languages and also e.g. domain-specific languages. This fact, as well as the expressive power of categories and their modeling capabilities, inspired us to focus our research on this area and explore the possibilities of category theory in expressing the semantics of programs written in imperative languages. We used a simple abstract language as a basis, which contains the tiny core of all imperative languages (all typical constructs). This language is relatively well known and often used precisely for verifying the properties of real imperative languages, or the construction of compilers, and computational models, determining semantics or applying common methodological procedures in pedagogy.

In this article, we focus on advancing theoretical foundations (rather than empirical optimization) – the mutual symbiosis of formal semantics and category theory. We briefly present our achieved results in the field of semantics of programming languages, which came to light thanks to the power of category theory. We seamlessly integrate category theory into imperative programming, offering a fresh and comprehensive perspective that has not been explored to this extent in previous works. This integration serves as the cornerstone of our research, setting it apart from traditional approaches. In addition, we also present other interesting results that are related to our research and are grounded in category theory. This is preceded by an extensive overview of the use of category theory in various areas of computer science and related fields. We present the most interesting results achieved in this area and explain their relationship with our research.

We note that in this work we do not present all the formulations, definitions, properties and their proofs, as we only present the essential properties of both semantic methods defined by us and their relationship to formal semantic modeling. The reader can find the details necessary for a complete specification of both methods in the works (Steingartner et al. 2017) and Steingartner et al. (2019).

Overall, this paper provides a comprehensive overview of the perspectives of semantic modeling in categories. By studying and adopting the power of semantic modeling, researchers, IT experts, and students can unlock new insights, improve accuracy of expressing and modeling the problems in categories, and enhance various applications across diverse domains. We note that we are of the opinion that embracing the potential of semantic modeling opens doors for researchers, IT experts, and students to uncover novel insights, uphold the precision of categorical modeling process, and enhance the functionality of diverse applications spanning various domains.

The structure of the article is as follows. Section 2 presents the syntax and basic structure of the abstract language Jane that serves as a necessary foundation for formulating our semantic methods. Subsequently, in Section 3, we present an extensive overview of interesting and important results in the field of formal modeling based on category theory, some of which also inspired us in our research or confirmed our research assumptions.

Continuing with the presentation of research results, we present in Section 4 categorical denotational and in Section 5 categorical operational semantics (based on coalgebras), as significant results in the field of formal semantics of imperative languages. No less interesting, some other research results related to categorical modeling (or expression) of various structures, calculations, and systems are presented in Section 6. Finally, Section 7 concludes our article, taking into account some other aspects and possibilities of expanding the research and continuing from the presented results to the others an interesting problems based on semantic modeling in basic and applied research.

Theoretical foundations and sources

Semantics of programming languages (also formal semantics of languages) is one of the basic formal methods in software engineering. Its results are very valuable, especially when revealing hidden defects in programs when it is possible to evaluate the behavior of programs using mathematical methods and thus determine the critical points, or find the correct result of the program calculation.

When deriving and using individual semantic methods, we proceed from the fact that semantic methods for the same area of use (application domain, e.g. for imperative languages) are mutually equivalent. In this direction, there are several well-known semantic methods, for example, natural semantics, which constructs the meaning of a program using derivation trees, operational semantics, in which we derive the meaning using transitive relations for the description of individual steps (similar to when tracing programs), denotational semantics, where the meaning of a program is given using mathematical principles and (above all) the composition of functions on states, axiomatic semantics for partial verification of programs, which derives meaning using a system of logical preconditions and postconditions, or algebraic for the specification of programs and their modeling using heterogeneous algebras. In addition to the above, there are other (more or less well-known) semantic methods designed for some specific use cases. Therefore, the relationship between semantics and abstract syntax, which deals only with the structure of programs, is of decisive importance. Hence, we can define abstract syntax in a relatively simple way – using syntactic domains and the abstract syntax trees. In other words, abstract syntax, primarily encompassing data structure, differs from concrete syntax, which embodies both structure and representation details. The abstract syntax of an implementation comprises the tree structures utilized for representing programs within that implementation. This distinction is crucial as it governs the appearance of programs to the interpreter or compiler. A typical example of the difference between abstract and concrete syntax is a conditional statement – in the theory of programming languages at the level of abstract syntax, a conditional statement is like a two-way branching with mandatory both branches (then/else), while in concrete syntax it depends on the programming language, where notations can differ e.g. multiple decisions (elseif/elif), typically an optional else branch, or the way nested statements are written (grouping them using parentheses, keywords begin/end, or simply indenting a block, etc.).

When conducting research in the field of semantic methods for imperative languages, researchers (conventionally) rely on a very simple language that forms the tiny core of every standard (real) imperative language and contains basic constructs typical for imperative languages – variable assignment, branching, or looping (Nielson and Nielson 2007).

Concrete syntax is a part of the definition of the language. The concrete syntax of a programming language is defined by context-free grammar. It consists of a set of rules (productions) that define the way programs look to the programmer.

The relationship between syntax and the model of computation is given by the semantics of programming languages (Fernández 2014). Semantics describes the processes a computer follows when executing a program in that specific language. This can be shown by describing the relationship between the input and output of a program, or an explanation of how the program will execute on a certain platform, hence creating a model of computation (Slonneger and Kurtz 1995).

This abstract language (sometimes also a model or toy language) is referred to as While (Nielson and Nielson 2007) in a wide range of literature. Many researchers also use other names for this language, e.g. IMP (Roşu et al. 2010). For pedagogical reasons, we chose the name of the language as Jane. In its nature, it is an abstract language that contains standard constructs typical of imperative languages and simple arithmetic and Boolean expressions. Implicitly, the language contains only two types – the type of integers and the type of Boolean values, and we assume that all variables and expressions are implicitly typed.

The Jane (While) language plays a very important role in semantics research because its elements at the abstract level of syntax form the basis of common real programming languages. Undoubtedly, this concept is also successful in pedagogy in the field of formal methods, when students are not distracted by implementation details and can concentrate on the essential features of the language and programs in this language.

In our research and our pedagogical practice, we have successfully used the Jane language in the field of compilers and formal languages (Kollár 2009), in the creation of a compiler from a higher language to the binary code of (in our case) a virtual platform (Steingartner 2021) or for visualization of several semantic methods.

Thanks to the fact that we can ignore typical implementation details and dependencies on a specific platform, it is quite easy to focus on the essential features when creating a compiler, during semantic modeling, or when constructing an abstract machine for verifying the properties of operational semantics.

Even though in this article we deal with the category theory and its use in semantic modeling, we are of the view that it is not necessary for the reader to formulate the theoretical foundations and definitions of the necessary concepts, or proofs of the properties of categories. Hence, we suggest that readers refer to readily accessible literature on category theory for fundamental terms and definitions, e.g. Barr and Wells (1990, 2013); Walters (1992).

Our study underscores the enduring relevance of category theory in the ever-evolving landscape of semantic modeling. By offering insights into potential practical applications within programming and related fields, our research contributes to the field’s continued growth and evolution. We present our research results in the field of category-theoretic semantics of imperative languages. We present these results on the already mentioned Jane language, the basics of which is briefly explained in Section 2.1. Subsequently, we show a brief example of the application of both methods in a common case – the well-known Make chocolate puzzle. A comment on the given puzzle as well as one of the possible solutions are given in Section 2.2.

A brief introduction to the language Jane

Our approach to defining categorical semantics we show on a simple imperative language Jane. It is a non-real programming language based on an imperative paradigm, representing a minimal foundational subset of typical mainstream languages like C or Java. It encompasses fundamental imperative elements, including sequential statements, conditional selection, loops for iteration, and memory variable assignment. To bring Jane language closer to real languages and to semantically demonstrate interaction with the user, we added to the language the constructs for user input and output.

As the definition of this language is commonly referenced in many research works (Nielson and Nielson 2007; Slonneger and Kurtz 1995), we forego a redundant restatement and instead offer a brief introduction, leveraging the foundational concepts inherent in the language definition (Dedera 2014):

• syntax definition using EBNF, inductive definition or derivation rules,

• formal definition of the semantics of a particular language using an appropriate semantic method.

The abstract syntax of the language Jane is defined by the set of rules taking the syntactic elements from the following syntactic domains (or syntax categories) listed in Table 1.

Table 1. Syntactic domains for language Jane

$n\in \mathbf{Num}$	— strings of digits, numerals,
$x\in \mathbf{Var}$	— variables’ names,
$e\in \mathbf{Expr}$	— arithmetic expressions,
$b\in \mathbf{Bexpr}$	— Boolean expressions,
$S\in \mathbf{Statm}$	— statements,
$D\in \mathbf{Decl}$	— declarations.

For each syntactic domain, exactly one production rule given in EBNF is defined:

• the elements in domains for numerals $\mathbf{Num}$ and variables’ names $\mathbf{Var}$ have no internal structure from the semantic point of view, so we do not define rules for them;

• production rule for arithmetic expressions: $$\begin{array}{c}\hfill e::=n|x|e+e|e-e|e\ast e|e\text{div}e|e\text{mod}e,\end{array}$$

• production rule for Boolean expressions: $$\begin{array}{c}\hfill b::=\mathtt{true}|\mathtt{false}|e=e|e\le e|\neg b|b\wedge b|b\vee b,\end{array}$$

• production rule including five (traditional) Dijkstra’s statements (D-diagrams), an unnamed block statement and a user input/output statements: $$\begin{array}{c}\hfill \begin{array}{cc}\hfill S::=& x:=e|\mathtt{skip}|S;S|\mathtt{if}b\mathtt{then}S\mathtt{else}S|\hfill \\ \hfill & \mathtt{while}b\mathtt{do}S|\mathtt{read}x|\mathtt{print}e|\mathtt{begin}D;S\hfill \\ \hfill & \mathtt{end},\hfill \end{array}\end{array}$$

• production rule for the declarations (all variables used in programs must be declared): $$\begin{array}{c}\hfill D::=\mathtt{var}x;D|\epsilon ,\end{array}$$ where $\epsilon$ stands for an empty declaration.

Illustrative code instance for applying semantic methods within categories

Here we demonstrate the use of both of our semantic methods (explained in Sections 4 and 5) on a simple but well-known example (puzzle) Make chocolate (Parlante 2013). The formulation of the exercise is as follows:

This puzzle is popular in various platforms for testing programming skills and knowledge (for instance CodingBat code practice, www.codingbat.com), where the tested person is tasked with completing a code snippet for a specific function, and the system then tests the generated code against random inputs, providing results and feedback. There are many solutions to this problem (more or less effective). Our solution is adapted to the features and capabilities of the Jane language. We chose the following notation for the input parameters:

• x for the number of small chocolates,

• y for the number of big chocolates,

• z for the desired goal.

The source code of the solution in the Jane language is on Listing 1.

Semantic modeling: Related research overview

As W. Lawvere has underscored, the utility of category theory-based modeling extends beyond representing multi-structural aspects of the mathematical universe; a categorical perspective on a single mathematical structure can also yield significant advantages (Diskin and Maibaum 2012). There are several well-established applications of category theory in theoretical computer science; typical examples are programming language semantics and concurrency. Categories are useful mathematical structures for modeling programs and defining their categorical semantics. Categorical semantics of programs is in the literature oriented mostly on functional programming paradigm, for instance, Hyland and Ong (2000) or Milewski (2019), but our approach is for the imperative paradigm modeled by category of states. We defined denotational categorical semantics for imperative languages and extended it for procedures (Steingartner et al. 2017). Another categorical structure we defined for structural operational semantics is coalgebra (Steingartner et al. 2019). We followed the ideas published in the book (Jacobs 2016).

Category theory is a very powerful formal modeling tool. In recent years, many researchers have been concerned with using category theory as a formal basis for modeling various aspects of software engineering, applied computer science, and related fields. In this section, we present some applications of the category theory, in which this apparatus has an irreplaceable role and can rightly be considered a significant contribution to the field of formal modeling in categories.

In Section 3.1, we delve into categorical modeling in the field of systems engineering and some specific areas continuing from it. Next, in Section 3.2 we review some applications of categorical modeling in complex systems (with a focus on multi-agent systems and machine learning). Finally, in Section 3.3 we discuss the use of categorical models in some areas of applied research, where it is shown that the expressive power of category theories serves equally well not only in mathematics and computer science but also in other scientific fields.

Categorical modeling in system engineering

System engineering is the engineering discipline that unifies the functions of a system, its environmental context, and the required engineering disciplines to create and/or operate an elegant system. For a comprehensive understanding, we should refer to Griffin (2010), which defines the four characteristics of an elegant system. System engineering, as a field of research and study, is leading the effort to create strategies to cope with changes in technology and systems complexity in engineering and other fields (Mabrok and Ryan 2015). This discipline is based on several important postulates (7), and principles (8) and posits three hypotheses (Watson 2019). It is accepted that systems consist of two basic structures: components and relationships (between components and with the environment, these are physical and logical relationships). Consequently, the representation of systems using category theory appears to be very suitable and elegant for the needs of formalization and modeling. Mathematical category theory provides the mathematical structure to fully represent a system – all of its components and all of its physical and logical relationships. Since a category may contain smaller categories, then an engineering black box is a category treated as an object within a larger category. When focusing on system specification, the category must contain the correct and complete objects and relationships.

In System Dynamics, dynamical systems are modeled using stock-flow diagrams, which are widely used in economics, epidemiology (for instance to model the spread of disease), etc. Stock-flow diagrams give differential equations describing how the stocks change with time. For users who are not familiar with differential equations, it is easier to understand the graphical representations expressed by diagrams. Authors of the paper (Baez et al. 2023) present their contribution to a new software package StockFlow introduced within the AlgebraicJulia ecosystem, aimed at enhancing the modeling of population dynamics in epidemiology through stock and flow diagrams. These diagrams, commonly used in this field, can now be built and simulated with greater efficiency and flexibility using the StockFlow package. By integrating principles from category theory, particularly the theory of decorated cospans, the package addresses limitations present in existing tools (for instance, in AnyLogic, there was an absence of support for model composition to create larger, stratified models, and for collaborative model construction). The ability to compose models is crucial because realistic models are more complicated and built out of many smaller parts. The key steps in compositional modeling are based on mathematical principles that allow putting together smaller models to create bigger ones (which corresponds to composing morphisms in category) and converting models to systems of differential equations (this is a functor between categories). Finally, writing software that implements the mentioned ideas is a logical step and a practical application of the mentioned principles. The categorical system model presented in Baez et al. (2023) consists of two categories: $\mathbf{Open}(\mathbf{StockFlow})$ and $\mathbf{Open}(\mathbf{Dynam})$. The objects of the category $\mathbf{Open}(\mathbf{StockFlow})$ are finite sets and morphisms are open stock-flow diagrams. The second category is $\mathbf{Open}(\mathbf{Dynam})$, the category of open dynamic systems. The relationship between both categories is expressed by a functor $\varphi$ that turns an open stock-flow diagram into an open dynamic system in the sense of the specification presented in the given work.

A very interesting demonstration of the modeling of the system and its properties was presented at the seminar in the work (Aguinaldo 2020), where the author focused on the option of programming the robot and its model in category theory. RoboCat is a framework consisting of a goal-oriented functional programming environment, a functional interoperable compiler, and the mapping to the Canonical Robot Command Language (CRCL) and robot-specific APIs (Aguinaldo et al. 2022). The non-trivial symmetric monoidal closed category (Mac Lane 1998; Slodičák 2012) was used as the basic categorical structure (its main property is the existence of a tensor product). Moreover, symmetric monoidal closed categories are special categories that have been used for expressing the semantics of linear logic (Ambler 1991; Méhats and Soloviev 2007; Novitzká and Slodičák 2010). The presented RoboCat model consists of three symmetrical monoidal closed categories: category ${\mathcal{C}}_1$ refers to the physical representation of the world (objects are physical objects and arrows are the set of possible statements), category ${\mathcal{C}}_2$ refers to the informational (virtual) resources (objects are physical objects and arrows represent skills needed to complete the desired actions), in addition, in this category it is possible to define sessions that encode semantic equivalences between skills and composition of skills, and category ${\mathcal{C}}_3$ that refers to the category of CRCL commands (objects are separate robot platforms and arrows are fully parameterized CRCL commands). Relationships between categories are expressed by two functors: $F:{\mathcal{C}}_1\to {\mathcal{C}}_2$ is a human-performed task model of developing a model of the physical environment and $G:{\mathcal{C}}_2\to {\mathcal{C}}_3$ maps software objects to robot platforms with preserving the structural properties. The advantage of using category theory in modeling lies in the clear distribution of translation from physical objects to programming language syntax and then to robot command APIs in a given robot program. The categorical model thus provides a system for tracking semantic relationships.

Similarly, the authors of the work (Breiner et al. 2018) come from the idea that category theory is the mathematical theory of abstract processes, and as such it encompasses both physics and computation. This alone makes it a good candidate for foundational work on modern systems, which can thus provide a formal basis and practice of system engineering. The authors begin by formulating the system concept and outlining their diverse requirements and assumptions. Category theory’s primary application in systems engineering lies in serving as a precise technical language for expressing and analyzing models of systems information, spanning from theoretical predictions to raw data. Subsequently, they elaborate on this by creating a functional decomposition that outlines how the system will achieve its objectives. During implementation, they link these functions to the system’s components. Finally, they bring together these components to form a complete system, continuously testing throughout the process, before deploying the system for operational use. The main principle of this modeling is the turning of abstract models into concrete realizations, which is very reminiscent of a logician’s notation of syntax and semantics. In the context of system integration, models primarily serve the purpose of gathering and organizing the vast volume of structured data acquired and examined throughout the integration procedure. This data inherently possesses diverse characteristics, spans multiple scales, and is distributed among numerous models and specialists. Categorical models offer a range of beneficial attributes that facilitate the consolidation of this data. Authors construct the models using several very interesting and important structures such as colimit (which generalizes unions, providing new objects), and in the $\mathcal{C}at$ category (where objects are categories and arrows are functors) these colimits in related semantic contexts can be used to define model integrations. As for heterogeneity, categorical constructions called sheaves (Barr and Wells 1990) have recently been proposed as the canonical data structure for sensor integration (Robinson 2016). Categorically speaking, the sheaf assigns a set to each element of the cover, or else each intentionally specified piece of the complex object (Zafiris 2005). Viewing the models as specialized languages for particular domains (the domain-specific languages), the task at hand involves translating data from one language to another. Such processes tend to be disorderly and improvised; however, categorical frameworks can bring organization to these procedures. The conceptual framework of category theory permits the utilization of a consistent set of techniques across an exceptionally wide array of issues and situations. The conclusion is that the real value of category theory lies in facilitating diverse interactions and precise analysis. It produces graphical and semantic models from existing schemas, helping in dynamic model creation and computational simulations for statistical analysis. Categorical models structure this process, yet tool support remains a challenge, limiting implementation despite category theory’s conceptual efficacy.

The paper (Zafiris 2005) addresses the need for a foundational approach to understanding complex systems in physical and social sciences. It introduces a categorical framework that emphasizes the role of information structure. This framework, based on categorical adjunction, views complex systems as processes of information communication. The proposal advocates for using category theory’s language to model these systems effectively. The core concept involves families of partial information carriers and a sheaf-theoretical perspective. The framework suggests that complex systems can be understood through mappings connecting simpler and complex system structures. The idea of an adjunctive correspondence is crucial, based on categorical colimits over elements of information carrier sets. This approach offers a way to comprehend complex systems by breaking them into partial information carriers and understanding them through functorial information communication.

In Diskin and Maibaum (2012), the authors focus on Model-Driven Engineering (MDE) as a recent trend in software development. As their results show, categorical patterns turn out to be directly applicable to the mathematical modeling of structures appearing in everyday MDE practice: model merging, transformation, synchronization, and other important model management scenarios can be seen as executions of categorical specifications. It turned out that relationships between CT and MDE are more complex and richer than is normally assumed for applied mathematics. Category theory provides a toolbox of design patterns and principles, whose added value goes beyond such typical applications of mathematics to software engineering as formal semantics for a language, or formal analysis and model checking. The authors start from the idea that The foundational principles that support contemporary Software Engineering (SE) could be naturally based on category theory. The gap separating SE and category theory can be bridged, and MDE seems like a perfect fit, in which an abstract view of SE realities and concrete interpretations of categorical abstractions merge: SE $\to$ MDE $\leftarrow$ CT. In their work, the authors highlight the categorical nature that underlies the fundamental concepts of multimodeling and intermodeling and present their results on two examples of categorical arrangement of model management scenarios: a model merge (via colimit) and bidirectional update propagation (BX). The authors formulate their modelware. The modelware universe consists of a series of modelwares – systems of requirement, analysis, and design models, with each consecutive member in the list refining the previous one, and in its turn encompassing several internal refinement chains. The modelware universe then appears as a collection of structured objects and structure-compatible mappings between them, as a categorical phenomenon (Diskin and Maibaum 2012). The model itself is constructed in two levels – the base universe and intermodel relations and queries. The key categorical structures in this approach are the Kleisli categories of heterogeneous models fibered over the Kleisli category of metamodels. As an added value, it turns out that the introduction of CT courses into the SE curriculum, especially in the MDE context, would be the most natural approach to the problem. Basic category theory studies should encourage thinking in terms of arrows, promote diagram-based reasoning, and develop an intuitive sense for distinguishing between well-formed and problematic structures. Introducing these principles, especially within the context of Model-Driven Engineering (MDE), would naturally address the challenge.

A similar approach in categorical modeling is presented by the author in the work (Diskin 2001), where he refers to the Reference Model of Open Distributed Processing (RM-ODP). The author highlights the role of formal modeling in the field of systems and software engineering and provides clear arguments for why category theory is a very suitable formal framework. RM-ODP is a conceptual framework and architectural model used to design and specify complex distributed systems, particularly those involving multiple computers and networked environments (Vallecillo 2000). ODP-systems are necessarily heterogeneous including architectural heterogeneity and semantic heterogeneity in the sense of types of data and behavior. RM-ODP focuses on defining highly diverse structural patterns in an exceedingly abstract and consistent manner, serving as a fundamental basis for structural engineering within the realm of ODP. A comparable overarching objective is shared by category theory, which can be regarded as a discipline and framework for carefully addressing mathematical structure engineering at an abstract level. Hence, the comprehensive approach employed in category theory for specification aligns harmoniously with the broader philosophy that can be discerned within RM-ODP. Consequently, the principles and constructs forged in category theory provide precisely the mathematical underpinnings that RM-ODP requires to establish its conceptual framework. Category theory is considered a meta-mathematical framework where the emphasis is made on relations, manipulations, and transformations of/between mathematical structures, which suits the essence of mathematical modeling for ODP – it follows then that the concepts developed in category theory form just that mathematical framework RM-ODP needs. Therefore, the application of CT to ODP-system specification is both surprising and inherently logical, as the shared goal of managing complex structures effectively has yielded similar outcomes in software engineering and mathematics.

Authors in Mabrok and Ryan (2015) present the category theory as a formal foundation for model-based system engineering. As the starting point, they present a generalized view of the system based on category theory, and they formulate principles of how any system can be considered as a category. The research is focused on System Engineering (SE) which is the discipline focused on researching and studying methods to develop strategies for managing technological advancements and the increasing complexity of systems within engineering and various other domains. Then, a system is defined as a combination of interacting elements organized to achieve one or more stated objectives (Bunge 1979). Because some researchers view the system as an object that can be composed of several parts that have a relationship with each other (Steingartner et al. 2014), a logical conclusion follows up that the system can be modeled (considered) as a category, where the elements and components of the system are category objects and the relationships between the elements and the components are represented (expressed) by the arrows. A system model is a conceptual representation of a system’s various façets, including planning, design, behavior, and data handling. However, mathematical theories are restricted by structural limitations, necessitating a more flexible and abstract framework. This framework should bridge the gap between mathematical logic and real-world system modeling, accommodating the complexities of practical scenarios.

Moreover, authors present olog (which refers to Ontology Log, introduced in Spivak and Kent (2012) by David Spivak), here considered as a category that can be used to model or formalize a given real-world situation. As a great advantage, objects in olog are boxes with English-language phrases and the arrows represent the relationship between the boxes. Commutative diagrams represent facts. Furthermore, olog contains several important elements such as types, aspects, facts, and instances. We note that using phrases/formulas to describe formal elements expressed in the English language is a rather interesting step in the research. As an example, we can also mention the action semantics of programming languages (Mosses 1996), which expresses the meaning of individual elements of the language/programs using English phrases and is a fully formal method. The authors of this study investigated the use of systems engineering language, conceptualizing the design process as a translation of requirements from the problem domain to design parameters and components in the solution domain. This mapping can be described in categorical terms, employing morphisms (functors) to link two categories: the problem category (Pro) and the solution category (Sol). The authors demonstrate that the functor encompasses all mathematical and logical mappings and transformations that connect the problem statements with potential solutions.

Regarding the realm of (semantic) modeling, systems seem to provide a viable foundation for their formal representation. Likewise, akin to previous research, the paper (Kovalyov 2020) addresses the matter of product assembly within the context of model-based system engineering (MBSE). This work (following the trends in Mabrok and Ryan 2015 and Luzeaux 2015) explores the application of category theory, a branch of higher algebra known for its abstract representation using diagrams and arrows, to enhance the formal description and analysis of model-based enterprise (MBE) practices. The framework supports interoperability among different modeling tools, offering a common foundation for representing, generating, and verifying design and production knowledge. In this framework, models are treated as objects within categories, and morphisms represent actions involved in product assembly and design. This approach provides a rigorous and unified way to express complex product structures, processes, and interactions. The paper introduces the concept of a symmetric monoidal category (Mac Lane 1998; Slodičák 2012), which allows the graphical representation of control system state spaces and signal-flow diagrams. Category theory offers potential solutions to direct and inverse assembly problems and presents a coherent methodology for integrating various MBSE techniques. The paper underscores the need for practical implementation in software tools to make these theoretical advancements accessible to industry, with the potential to revolutionize automatic production planning and generative design (a major area for further theoretical and applied research). The integration of category theory into MBSE not only formalizes the representation of products but also holds the promise of optimizing engineering processes and innovation. The approach is exemplified in solid body geometric modeling and discrete-event simulation of production processes.

A very interesting application of categorical modeling not only at the theoretical level is presented in Graves (2013). Both structure and behavior, as they occur in engineering models for manufactured products and biomedicine, can be embedded as axiom sets within a mathematical formalism, called Algos. The Algos language is a two-sorted first-order Horn clause theory based on topos language constructions. In this paper, authors describe how engineering models (as they are constructed for manufactured products and biomedicine), can be embedded as axiom sets within a logic-based formalism called Algos. Algos is based on elementary topos theory and follows the path of topos foundations for mathematics and physics. Embedding an engineering model as an axiom set provides the means to integrate automated reasoning with product development and analysis. The authors assume that the best-known logic-based formalisms are subsets of the first-order logic which only use variables of a single type (a similar approach to Schreiner et al. 2020). This paper employs two instances of engineering modeling to provide illustrative examples. The first scenario pertains to various domains like manufactured products, human anatomy, and molecular biology. It centers on depicting axiomatic descriptions for a category of structures, wherein each adheres to a distinct graph-theoretic configuration of components and their interconnections. The second illustrated case encompasses a model representing the operational dynamics of a vehicular system within its operational context. Algos generates a topos, allowing the utilization of constructs like the description operator without concern for logical soundness. Imposed limits on axiom sets yield decidability results, applicable to molecular biology. These axiom sets, e.g., for amino acid structures, belong to a restricted Algos axiom category. The language structures, alongside their axioms, establish an axiomatic semantics for a broader description logic. The selection of language structures and axioms for Algos was driven by the goal of creating a logic-based framework that scientists and engineers could use interactively with automated theorem proving and proof checking, supporting both system description and specification. In that way, various engineering issues are addressed through logic-based analysis.

Finally, we present one work in which general assumptions for semantic modeling of systems in categories were formulated. The paper (Lippe and Ter Hofstede 1996) introduces a novel (at the time of its publication) conceptual data modeling approach by leveraging category theory principles. This technique extends existing methods and incorporates advanced features like specialization, generalization, and power types. Grounded in several fundamental category theory concepts such as (co)limits, epi- and monomorphisms, it transcends traditional instance categories like topoi ($\tau \acute{o}\pi o\iota$) or Cartesian Closed Categories, accommodating intricate elements such as uncertainty, missing values, and multi-valued relations. Historically, data modeling has evolved from implementation-centric to problem-centric approaches. Conceptual data modeling now aligns with the Conceptualization Principle, focusing on graphical representations to enhance comprehension and facilitate stakeholder communication. The main objective of conceptual data modeling is to precisely outline an application’s data perspective independently of its implementation, streamlining communication with stakeholders. The paper primarily delves into the syntactic aspects of conceptual data models, expressing them as type graphs. These graphs illustrate object types through nodes and their interactions via labelled arrows. The semantics of these type-graphs is established as a collection of models, employing a wide-ranging category theory-based methodology that transcends typical instance categories. Unlike conventional limitations of topoi or Cartesian Closed Categories enhances inclusivity. The inherent simplicity of the category theory constructs used contributes to its accessibility. The presented model shares similarities with object-oriented data models and draws insights from category theory to grasp fundamental concepts in data modeling. Compared to the formalism in this paper, some earlier works (Baclawski et al. 1994) and Tuijn (1994) employed category theory within topoi as instance categories to define standard relational database operations. While this approach employs simpler categories, it holds promise for defining common relational database operations and potentially extending to encompass database updates and schema evolution.

Categorical models for interactive and adaptive systems

In recent years, the integration of machine learning techniques into network engineering data analysis has gained significant attention (e.g. Palša et al. 2022 or Oreški 2023). The paper (Zhao et al. 2023) presents a novel approach that combines machine learning with category theory, aiming to address the growing complexity in this field. By leveraging category theory’s mathematical language, the authors connect diverse machine learning structures, offering a structural perspective that simplifies understanding and management. The paper’s main contribution lies in its implementation of a machine learning representation within the category theory framework, with a focus on slice categories. This innovative concept enhances the understanding of data preprocessing and is exemplified through the application of functors to benchmark datasets, evaluating the accuracy of various machine learning models. This work extends the understanding of how category theory can enhance machine learning methodologies, offering a potential foundation for new methods in network engineering and data analysis. However, it turns out that for the representation of deep learning by a category theory, choosing other concepts can provide a new, simple language for understanding and managing deep learning algorithms.

The paper (Ormandjieva et al. 2015) explores the formal connection and relationship between two distinct areas of knowledge: multiagent systems (MAS) and category theory. More recently, category theory was applied to model MASs, and a categorical model of MASs was stated in Pfalzgraf (2005); Pfalzgraf and Soboll (2008) as the MAS category. The main aim is to provide a categorical structure for defining MAS properties using the inherent framework of category theory. The interaction between category theory and multi-agent systems involves representing agents and their connections using categorical ideas and then using category theory to validate system properties with concrete proofs. The authors present a formal model that applies category theory to MAS, focusing on the connections between agents instead of their representations. This method aligns well with agent-based systems, emphasizing communication among agents as a foundational concept. The study particularly examines Belief-Desire-Intention (BDI) agents, extensively studied by many researchers from both theoretical specification perspective and practical design perspective, including the use of BDI modal logic that extends temporal logics with BDI modalities. We note that BDI logic also has interesting uses in the formal modeling of system behavior, e.g. as an Intrusion Detection System (IDS) (Perháč et al. 2018, 2021; Vokorokos et al. 2009). The category of MAS functions as a model that captures agents’ communication structures, where agents represent entities and connections depict communication links. By utilizing this category, the authors effectively model relationships among agents within a system, identifying direct communication abilities, message delegation, and communication types. The authors emphasize the importance of creating an accurate MAS model using the same category theory-based formal approach. This effort is vital not only for precisely defining MAS properties and conducting formal verification but also for visually summarizing essential aspects of agents and MAS within category theory constructs. The proposed approach establishes MAS properties through concrete proofs, capitalizing on the constructive character of category theory. The process involves explicit constructions based on representations of MAS categories and functors. The paper concludes by demonstrating the practical application of the proposed framework in a real-world scenario by exemplifying the constructive proof approach using the fault-tolerance property.

Some other varied aspects of categorical modeling

In applied research, there is a whole range of implementation of theoretical formal principles in modeling and expressing real systems. One example is the conceptual modeling of phytometric systems. The exploration of the phytometric system of virtual plants has evolved into a complex interdisciplinary project, transitioning from a predominantly computer science-centric approach. During the process of conceptualizing this system, challenges related to requirement elicitation difficulties and inconsistency have emerged. The study (Yi et al. 2018) centres around the computer visual modeling of plant morphology and employs category theory, a formalized mathematical tool, to delve into a comprehensive suite of conceptual modeling methods and tools tailored specifically for the phytometric system, i.e. to develop a conceptual modeling approach specific to the phytometric system of virtual plants. The focus is on addressing challenges related to requirement elicitation, inconsistency, and optimization of plant morphology.

The potential of virtualizing and visualizing plant growth emerges as a potent tool for optimizing plant morphological structure. Category theory, which focuses on relationships among objects while abstracting their internal structures, provides a unified visual representation, effectively concealing heterogeneity among objects. In essence, it allows the representation of complex matters through a unified visual format, consisting of objects and arrows.

In summary, the conceptual modeling process of the phytometric system involves amalgamating atomic systems using the modeling language of category theory. The resulting plant conceptual model comprises first-level subsystems along with the topological relations spanning the second to fourth layers. Through the application of category theory’s modeling approach, the abstraction level of system conceptualization is elevated. This approach empowers system modelers to analyze intricate systems from both global and local perspectives, all while offering a formalized guarantee that fosters knowledge sharing among modelers. This, in turn, streamlines the integration and consolidation of existing cognitive outputs.

Category theory has also found an application in semiotics. For example, the first effort to apply category theory to semiotics was that of Goguen and Harrell (2005) who attempted a formalist treatment of the semiotics of information visualization and user interface design, which they described as algebraic semiotics. The article (Vickers et al. 2013) explores the foundational aspects essential for constructing a formal framework to describe visualization processes. It employs semiotic theories, category theory, and mathematical constructs to establish a comprehensive understanding of visualization concepts. The alignment of information visualization with Peirce and Saussure’s semiotic theory is explored (for basics see, e.g. Yakin and Totu 2014), followed by a formal characterization using category theory.

The Peircean semiotic triad (notation after Sowa 2000) is expanded into a mathematically closed category, incorporating contextual relationships and insights generated during visualization. The article defines and formalizes visualization properties such as literalness, redundancy, sensitivity, generalizability, and chart junk. By introducing the concept of intensionality in visualizations, it enables users with enhanced capabilities. The work transforms intuitive concepts into verifiable theoretical descriptions, offering a reliable foundation for making principled judgments about the visualization process and specific instances. A mathematical diagram is presented to ensure a structured visualization process, potentially facilitated by a tool that validates designs and analyzes their implications. The article identifies key objects and relationships in visualization and outlines future work involving higher-order category theory tools to compare diverse visualizations, especially across different modalities. This article further extends these structures using the tools of category theory to provide a general framework for understanding visualization in practice. This framework encompasses relationships between systems, data collected from those systems, renderings of those data in the form of representations, the reading of those representations to create visualizations, and the use of those visualizations to establish knowledge and understanding of the system under inspection. Finally, this work contributes to a robust theoretical understanding of visualization, laying the groundwork for advancements in theory and practice. In a specific example, authors present their approach: with the category corresponding to the visualization process they use the concepts of category theory to consider its properties. Subsequently, they proceed to demonstrate how conventional intuitions can be refined into more rigorous definitions. For instance, the monomorphism corresponds to sensitivity.

Paper (Bradley et al. 2021) presents a mathematical framework for passing from probability distributions on extensions of given text on input. The framework is based on large language models extending to an enriched category containing semantic information. In other words, the probability distributions on text are modeled as a category enriched over the unit interval (which models probability distributions on text continuations). The whole model is constructed from two categories: the syntactic category where objects are expressions in language. The second is the semantic category, a category of enriched copresheaves. We note that a category of copreshaves is a topos (Barr and Wells 1990). For example, the expression x is identified with the functor $h^x:=hom(x,\text{--})$ which is an example of copresheaf, moreover identified as representable copresheaf. Furthermore, within the framework of enriched categories, the morphisms connecting distinct objects attain the status of discrete entities within a designated category, denoted as the foundational (or base) category. Remarkably, this base category is classified as a symmetric monoidal closed category (Mac Lane 1998; Slodičák 2012), endowing it with the unique capacity for self-enrichment. In short, the authors have introduced a mathematical framework that helps understand the type of grammar-related information that large language models learn and describes where the learned semantic information resides within those models. They have connected this understanding to a concept from category theory, specifically to a category called $\left[0,,,1\right]$-copresheaves. This connection enables us to better grasp where the semantic (meaning-related) knowledge is encoded within the model’s parameters or representations. By studying how certain operations work within this framework, the authors suggest that there are practical applications that could be explored in more detail.

Categorical denotational semantics

As mentioned, category is a very useful mathematical structure for modeling programs and defining their semantics. Therefore, our research focused on the use of categories for defining semantics. We present a formal semantics model that not only leverages categorical concepts but also extends them to clarify relationships between objects representing memory states. This novel approach bridges the gap between abstract category theory and concrete program behavior.

In this section, we briefly present our approach to defining the semantics of programming languages using categorical structures. We show how we can model the denotation of programs written in an imperative language. We construct our model as an integrated categorical model using denotation functions (and partly an operational approach).

Definition of semantics in categories

We worked with imperative and procedural languages, where the essential concept is a state. The state is considered an abstract model of computer memory which is independent from the real architecture and allows one to view the changes in computer memory formally.

In our approach, the essential idea in the semantic modeling of a program is the construction of one category of states for a given program. The denotation of a program is thus a path in a (directed) graph, which is understood in the category as a compound morphism.

We construct the program model as a category of states (i.e. an instance category), where the environment expressing contextual dependencies known from structural semantics is part of the objects of the category, expressed formally (and simplified) using the level of nesting. The dynamics of program execution are described using category morphisms, which serve to represent changes in the program’s states. These morphisms are essentially semantic functions, resembling the traditional denotational approach. One notable benefit of our model is its ability to visually illustrate the program’s execution, enhancing comprehension of the program’s method of execution, including its components.

We define a state s as a function$$s:\mathbf{Var}\times \mathbf{Level}\to \mathbf{Value},$$where $\mathbf{Var}$ is a set of variables, $\mathbf{Level}$ expresses nesting level and $\mathbf{Value}$ is the set of integers containing also the undefined value $\perp$. Each state is then a list of tuples, where $x_i$ is a variable, l is nesting level ($l\in \mathbf{Level}={\mathbf{N}}_0$) and v is a value of variable of the given level:$$s=⟨\left(\left(x_1,,,1\right),,,v_1\right),,,\dots ,,,\left(\left(x_n,,,l\right),,,v_n\right)⟩.$$States are the objects of our model – the category of states. Each variable of a program needs to be declared. With each variable declaration, the variable environment is updated. A declaration $\mathtt{var}x$ is modeled as an endomorfism on a given state s (Fig. 1) and it adds a new tuple to a given state:$$〚\mathtt{var}x〛:s\to s.$$

[See PDF for image]

Fig. 1

The semantics of a declaration as an endomorphism on a state

The most important elements of imperative languages are statements. They perform the actions of the program, in simple terms, that is, they take the values of the variables in the current state and after computations provide new values. If the value of the allocated variable is changed, the memory state updates as well. Therefore, we model state change using functions between states. These functions are the morphisms in the category of states.

The statements are modeled as category morphisms – for a statement S, we have$$〚S〛:s\to s^{\prime }.$$It expresses a change of state induced by the execution of S. In such a way, we defined denotational semantics (Steingartner et al. 2017), where we constructed a category of states and defined statements of a simple imperative language using morphisms. If the semantics of the statement S is not defined (usually in the case of an infinite loop), the resulting state $s^{\prime }$ is an undefined state, $s^{\prime }=s_{\perp }$. Statements are performed sequentially, following the order in which they appear in the program’s source text.

In the case of simple statements (executed in one step) – an assignment statement and empty statement, their semantics is expressed in a very simple way.

The statement for variable assignment $x:=e$ stores the value of the arithmetic expression e in the memory cell allocated for the variable x at the innermost nesting level where this variable was declared. This condition ensures that a local variable (if declared) within the current scope is utilized. We define the semantics of the assignment statement as follows:

1

$$\begin{array}{c}\hfill \begin{array}{cc}& 〚x:=e〛s=\hfill \\ \hfill \\ \hfill & =\left\{\begin{array}{cc}& s\left[\left(\left(x,,,l\right),,,v\right),\mapsto ,\left(\left(x,,,l\right),,,〚,,e,,〛,s\right)\right],\text{for}\left(\left(x,,,l\right),,,v\right)\in s,\hfill \\ \hfill & s_{\perp },\text{otherwise.}\hfill \end{array}\right)\hfill \end{array}\end{array}$$The change of state after a variable assignment is illustrated in Fig. 2.

[See PDF for image]

Fig. 2

An assignment statement in the category of states

[See PDF for image]

Fig. 3

An empty statement in the category of states

An empty statement $\mathtt{skip}$ does not perform any action, i.e. it does not change the state. It is clear that the semantics of this statement is an identity function on the s state (Fig. 3), and its semantics is defined as:$$\begin{array}{c}\hfill 〚\mathtt{skip}〛s=\text{id}(s)=s.\end{array}$$The given representation meets the category definition, where an identical morphism is defined for each object.

[See PDF for image]

Fig. 4

A compound morphism for a sequence of statements

[See PDF for image]

Fig. 5

The path of execution $P_1$

For illustration, in Fig. 4, we show the semantics of compound statement $S_1;S_2$. The semantics of this syntactic pattern is a compound function$$\begin{array}{c}\hfill 〚S_1;S_2〛=〚S_2〛\circ 〚S_1〛\end{array}$$defined for a state s as follows:$$\begin{array}{c}\hfill 〚S_1;S_2〛s=〚S_2〛\left(〚,,S_1,,〛,s\right)\end{array}$$If any of the statements in sequence fails to produce a result for an input state s, i.e. its semantics is not defined, the meaning of the entire sequence of statements is undefined:$$\begin{array}{c}\hfill 〚S_1;S_2〛s=〚S_2〛\left(〚,,S_1,,〛,s\right)=s_{\perp }.\end{array}$$Conditional statement$$\begin{array}{c}\hfill \mathtt{if}b\mathtt{then}{S}_1\mathtt{else}{S}_2\end{array}$$causes the program to branch depending on the value of the Boolean expression b. A conditional statement is a programming construct (a scheme) that allows for different actions to be taken based on whether a specified condition is true or false. We define the semantics of the conditional statement using the semantics of a specific statement intended for execution depending on the value of the condition (analogous to the cond function in classical denotational semantics Nielson and Nielson 2007). The categorical semantics of the loop statement is extensively discussed in Steingartner et al. (2017).

We also consider block structure of Jane language. A block can contain declarations and statements. Block statements can be nested within each other. Executing a block statement$$\begin{array}{c}\hfill \mathtt{begin}D;S\mathtt{end}\end{array}$$is performed through the following steps:

• the nesting level l is incremented; this step is represented by a dummy row in the state table: $$\begin{array}{c}\hfill \left(\left(\mathtt{begin},,,l,+,1\right),,,\perp \right)\end{array}$$

• a local variable environment in terms of operational semantics is formed,

• at nesting level $l+1$ local declarations are elaborated,

• the body S of the block statement is executed,

• at the end of block execution, locally declared variables are forgotten (formally we use the $〚\mathit{del}〛$ operation to model this situation).

Formally:$$\begin{array}{cc}& 〚\mathtt{begin}D;S\mathtt{end}〛s=\hfill \\ \hfill & 〚\mathit{del}〛\circ 〚S〛\circ 〚D〛(s\diamond ⟨\left(\left(\mathtt{begin},,,l+1\right),,,\perp \right)⟩),\hfill \end{array}$$where the keywords $\mathtt{begin}$ and $\mathtt{end}$ serve as fictive variables and del is a function releasing all declaration on the level $l+1$, for $l\in \mathbf{Level}$.

Practical example

As an example, the semantics of the program given in Listing 1 can be presented as a directed path in the category of states (Fig. 5).

The individual states during program execution are the result of the application of the corresponding semantic functions. The semantics of a program is expressed as a composition of semantic functions for individual parts of the program (individual statements and variable declarations), and in a category expressed as a directed graph, this composite function is representable as a path between two vertices – from the initial state ($s_0)$ to the final state (here $s_6$).

A detailed analysis of the use of the categorical semantics method of the given program in the Listing 1 can be observed in the composition of the denotations of individual parts of the program. Lines 1-4 contain declarations of the necessary variables. The declarations do not change the state, they only introduce empty records into the state (with undefined variable values). User input occurs on lines 5-7. Each read command changes the current state, the individual changes are shown in Fig. 6: states $s_1$ for $x=\mathbf{6}$ (small chocolates), $s_2$ for $y=\mathbf{1}$ (big chocolates), $s_3$ for $z=\mathbf{10}$ (expected result).

[See PDF for image]

Fig. 6

Sequence of states $s_0$-$s_3$

On line 8, the logical condition in the conditional statement is first evaluated. For the entered values, this condition is false, therefore the denotation of the conditional statement provides as a result a composite function for the block on lines 11-18 (else branch).

Entering the block on line 11 creates a new level of declarations for this local block, and all new declarations in this block are introduced with this level of declaration (nesting). Introducing a variable by declaring it on line 12 does not change the state of $s_3$.

On line 13, a logical condition is first evaluated, which is true, so the conditional statement continues on line 14 with the then branch, which creates a new state $s_4$ (Fig. 7).

The program continues on line 17, where a new value is assigned to the variable result and a new state $s_5$ is created. The end of the block on line 18 means the release of local declarations with the highest level of declarations, and the program is thus in the final state $s_6$, which is the final state of the entire program (Fig. 8).

[See PDF for image]

Fig. 7

State $s_4$ – change in the local block

[See PDF for image]

Fig. 8

States $s_5$ (before leaving the local block) and $s_6$ (the final state)

Semantic function expressed as a path in directed graph in Fig. 5 represent the semantic function$$\begin{array}{c}\hfill \begin{array}{cc}& \left(〚,,\mathit{del},,〛,\circ ,〚,,result:=z-5\ast calc,,〛,\circ ,〚,,calc:=y,,〛,\circ \right)\hfill \\ \hfill \\ \hfill & \circ 〚\mathtt{var}calc〛\circ 〚\mathtt{read}z〛\circ 〚\mathtt{read}y〛\circ 〚\mathtt{read}x〛\circ \hfill \\ \hfill \\ \hfill & \left(\circ ,〚,,\mathtt{var}result,,〛,,\circ ,,〚,,\mathtt{var}z,,〛,,\circ ,,〚,,\mathtt{var}y,,〛,,\circ ,,〚,,\mathtt{var}x,,〛\right)(s_0)=s_6.\hfill \\ \hfill \end{array}\end{array}$$

Semantics of procedures

After defining the semantics for a basic syntax of the language Jane, we extended the language with procedures to the procedural language and constructed a collection of state categories that are linked using functors for calling the procedure and returning to the calling subroutine. The advantage of our approach is the possibility of multiple procedure calls and the use of recursive calls.

The basic idea is that a procedure is a named block that can be called from different places in the program. We have to declare the procedure before the first call. A procedure declaration encompasses its name, typically along with its parameters, local declarations, and the procedure’s body. During a procedure call, the parameters are substituted with actual arguments, and the procedure’s body is associated with its name, representing a dynamic approach to defining semantics. In this context, we focus on situations involving a single parameter for simplicity.

[See PDF for image]

Fig. 9

Semantics of the procedure call statement

We extend the formal syntax of the language by a new syntactic area of procedure declarations $Dp\in \mathbf{ProcDecl}$ and define the elements of this area by the following production rule:$$\begin{array}{c}\hfill Dp::=\mathtt{proc}p(t):S;\mathtt{return};Dp|\epsilon .\end{array}$$Because we have changed the structure of the block statement, we need to introduce this new form into the production rule for the block and the new statement for procedure calling as well:$$\begin{array}{c}\hfill S::=\dots |\mathtt{begin}D;Dp;S\mathtt{end}|\mathtt{call}p(t).\end{array}$$We represent the semantics of a program with procedures by utilizing a collection of instance categories of states. In doing so, we proceed from the following idea. The declaration of each procedure requires the construction of a separate category of states for that procedure. Its construction is the same as the category for the main program, and it contains as objects the states that may arise during the execution of the procedure. Local declarations and statements in the procedure body are modeled by morphisms in the given category.

We express the relationship between the main program category and the individual categories for the respective procedures using two functors:$$\begin{array}{c}\hfill \begin{array}{c}\hfill C:\mathbf{Statm}\to {\mathcal{C}}_{\mathit{State}}\to {\mathcal{C}}_p,\\ \hfill R:\mathbf{Statm}\to {\mathcal{C}}_p\to {\mathcal{C}}_{\mathit{State}}.\\ \hfill \end{array}\end{array}$$

[See PDF for image]

Fig. 10

Categorical interpretation of recursive calls

The functor C serves as a model for a procedure call. Its definition follows from the following considerations. If the current statement S in the category of states is a calling of the procedure p (here with the argument e), i.e. $\mathtt{call}p(e)$, in state s, then the functor C must perform the following steps:

• update the initial state of the category for the procedure, i.e. transfer the values from state s to the initial state $s_0^p$ of procedure p,

• in state $s_0^p$ add a new line for the procedure parameter,

• increment declaration level (nesting level),

• transfer the value of the argument $〚e〛s$ of the procedure parameter into the table $s_0^p$.

Formally:$$\begin{array}{c}\hfill \begin{array}{c}\hfill C(S)s=\left\{\begin{array}{cc}& s_0^p[⟨(,(,\perp ,,,1,),,,\perp ,)⟩\mapsto s\diamond ⟨(,(,t,,,l,+,1,),,,〚,,e,,〛,s,)⟩],\hfill \\ \hfill & \text{if}S=\mathtt{call}p(e),\hfill \\ \hfill & s_{\perp }^p,\hfill \\ \hfill & \text{otherwise.}\hfill \end{array}\right)\end{array}\end{array}$$The principle of semantic modeling of procedure execution is the same as for the main program. However, at the end of the execution of the procedure block, we must transfer the result to the main category (to the point of the procedure call). We model this using the R functor, which:

• removes from the final state of the procedure (from the sequence in the state) those elements that contain locally declared variables,

• transfers the new values of the global variables to the main (calling) category and creates the state that formally occurs when the procedure is invoked.

Formally:$$\begin{array}{c}\hfill R(S)s^p=\left\{\begin{array}{ccc}& 〚\mathit{del}〛(s^p),\hfill & \hfill \text{if}{s}^p=s_f^p,\\ \hfill & s_{\perp },\hfill & \hfill \text{otherwise}.\end{array}\right)\end{array}$$The structures C and R are functors, so they assign objects to the respective objects and morphisms to morphisms, which we verified in Steingartner et al. (2017).

Formally, the semantics of the procedure call (statement $\mathtt{call}p(e)$) is expressed as follows:$$\begin{array}{c}\hfill 〚\mathtt{call}p(e)〛=R\circ \left(〚,,S_p,,〛,\circ ,C,\left(\mathtt{call},,p,(,e,)\right)\right)\end{array}$$and is depicted in Fig. 9.

The definition of procedure semantics requires an extension of the model by a collection of categories for individual procedures, which are connected to each other by functors. These functors are modeled procedure calls and procedure returns. As an example, we also show how to model recursive computation of the factorial (here for the input value $n=4$) in the “farm” of instance categories. The categorical interpretation of recursive calls is given in Fig. 10.

Final thoughts

Categories allow a graphical representation of program execution, which inspired us to introduce graphical visualization of semantics into the teaching process. Categorical structures are quite difficult for students studying technical sciences because they require a deep knowledge of mathematics. However, it turned out that using visual representation can obviously help to better understand the mathematical structures of higher complexity, even when this visualization is also interactive (using some teaching software). So we tried to visualize the definition of the traditional approach to defining and visualizing semantics. This can contribute valuable insights to the realm of education and technology, similar to those discussed in Radaković and Herceg (2018) where authors focus on the development of a completely extensible dynamic geometry software with metadata.

Our approach to category-defined semantics contributes to the field of program modeling and provides the following advantages.

• Our semantic method provides a denotational approach using mathematical structures other than the standard denotation (sets, unions). When constructing the model and searching for semantics, we apply procedures from category theory. In this way, we avoid some complicated procedures typical of the standard semantic method.

• Thanks to the graphic representation, it is easy to understand. In the teaching, an essential minimum of category theory is presented, which allows us to understand the principles and details of this method.

• Our categorical model (framework) is capable of representing the progression of program execution and possesses significant illustrative potential in visually depicting program execution, namely, in a step-by-step manner.

• The representation of the category as a directed graph creates an excellent basis for the software implementation of the visualization of this method. The software visualization can then be provided as a teaching aid.

• Our methodology introduces mathematical rigor to program semantics. By modeling denotations within categories, considering input/output values, and addressing state dynamics, we offer a robust framework that enhances the theoretical foundations of the field.

Categorical operational semantics

The second semantic method, which we modeled using categories, was structural operational semantics, which provides an overview of the detailed steps of the executed program. Technically, it resembles the tracing over the program. Formally, it describes the program’s detailed behavior. This knowledge is important already in the program preparation phase and for program implementation. The traditional definition of this method defines each step of the program as a transition relation (Jaskelioff et al. 2011; Plotkin 2004) in some form $⟨S,s⟩\Rightarrow \alpha$, where $\alpha$ can stand either for a new state $s^{\prime }$, or the new configuration $⟨S^{\prime },s^{\prime }⟩$ (whether the execution of S has terminated or is not completed). However, in the standard approach, some language constructions are considered irrelevant from the point of view of operational semantics. Therefore, it is not always easy to find the meaning of a program written in a real language in operational semantics.

Our study delves deep into categorical modeling within structural operational semantics. A noteworthy aspect is the innovative use of coalgebras to articulate program behavior, particularly in the realm of memory configurations. This unique approach sets our work apart from standard operational semantics.

Semantic framework

In this section, we present our approach, as detailed in Steingartner et al. (2019), for defining operational semantics as a coalgebra within the category of (memory) configurations. This approach enables us to handle programs written in a modest yet practical imperative language, which includes standard programming constructs like input and output statements as well as declarations. Utilizing coalgebra, as discussed in Jacobs (2016), provides a uniform means to define operational semantics and describe program behavior. The state space within our coalgebra encompasses configurations that emulate real states. In the basic category of coalgebras, morphisms are functions that define individual steps in program execution. To represent execution dynamics, we introduce a customized polynomial endofunctor. This novel concept accommodates a wide range of transition types, providing a versatile tool that can revolutionize the understanding of program transitions. The polynomial endofunctor determines this type of system (Kock 2009). Another advantage of our approach lies in its straightforward implementation and visual representation, as demonstrated using a basic program.

Operational semantics provides a behavior of programs, that is, it considers every detail in program execution. The best categorical structure, which is appropriate for this purpose, is a coalgebra. Coalgebras are a useful tool for modeling the behavior of dynamic systems (Adámek 2005; Jacobs 2016; Trancón et al. 2010). They are defined over a base category whose objects form a state space and whose morphisms are transitions.

A coalgebra is a mathematical structure that extends the concept of algebras by incorporating a set with a comultiplication operation, often utilized to model systems generating data or events over time, while also involving the notion of an endofunctor (Jacobs and Rutten 1997), here over a base category. Every application of this functor expresses one step of program execution.

Since the Jane language includes block statements, potentially featuring local variable declarations, we need to account for the nesting level of a block. This nesting level allows us to establish a variable environment, facilitating the differentiation between local declarations and global ones.

Let $\mathbf{Memory}$ be a set of non-empty memory objects:$$\begin{array}{c}\hfill \mathbf{Memory}=\left\{m,:,\mathbf{Var},\times ,\mathbf{Level},\to ,\mathbf{Value}\right\}.\end{array}$$Each memory configuration m represents one moment of program execution, the actual state (snapshot) of the computer’s memory. The function m is identified by its graph, graph(m) (Schmidt 1986), i.e. a set of tuples, where the first member of the structure is the argument of this function (an ordered pair (x, l)) and the second member is the value of the function:$$\begin{array}{c}\hfill graph(m)=\left\{(,(,x,,,l,),,,v,),,|,,(,x,,,l,),\in ,d,o,m,(,m,),\wedge ,m,(,x,,,l,),=,v\right\}.\end{array}$$Also in this approach for visualizing (displaying) the real memory, we can represent the function m as a table.

Subsequently, we express the representation for the configuration type $\mathit{Config}$. We construct the set of configurations $\mathbf{Config}$ as a Cartesian product

2

$$\begin{array}{c}\hfill \mathbf{Config}=\mathbf{Program}\times \mathbf{Memory}\times \mathbf{Input}\times \mathbf{Output},\end{array}$$where $\mathbf{Program}$ consists of lists of global declarations and statements to be processed and executed. To construct coalgebra for our purposes, we need to construct a base category as a category of configurations. A configuration is a tuple$$config=(〚D_{}^{\ast };S_{}^{\ast }〛,m,i_{}^{\ast },o_{}^{\ast }),$$where $D_{}^{\ast }$ is a finite list of declarations, $S_{}^{\ast }$ is a finite list of statements, m is actual memory, $i_{}^{\ast }$ and $o_{}^{\ast }$ are lists of input and output values, respectively. The morphisms of the base category are the transition operations $〚next〛$ for statements, $〚read〛$ and $〚print〛$ for input and output statements, resp. We note that at the beginning of the program execution, we work with the fact that the list of output values $o_{}^{\ast }$ is empty, $o_{}^{\ast }=\epsilon$.

We start with the operation next. Generally, the interpretation of $〚\mathit{next}〛$ is the following:$$\begin{array}{c}\hfill 〚\mathit{next}〛:\mathbf{Config}\to \mathbf{Config}.\end{array}$$The argument of the function $〚\mathit{next}〛$ is the memory configuration. After applying the function, the result is a new memory configuration, which contains a modified statement sequence – the first member of the sequence was processed and possibly caused changes in the memory. For example, for the assignment statement, the following definition of its semantics is:$$\begin{array}{c}\hfill 〚\mathit{next}〛(〚x:=e;S^{\ast }〛,m,i_{}^{\ast },o_{}^{\ast })=(〚S_{}^{\ast }〛,m^{\prime },i_{}^{\ast },o_{}^{\ast }),\end{array}$$where$$\begin{array}{c}\hfill \begin{array}{c}\hfill m^{\prime }=\left\{\begin{array}{cc}& m\left[(,(,x,,,H,i,g,h,e,s,t,(,m,,,x,),),,,v,)\right)\mapsto \hfill \\ \hfill & \mapsto \left((,(,x,,,H,i,g,h,e,s,t,(,m,,,x,),),,,〚,,e,,〛,m,)\right],\hfill \\ \hfill & \text{if}Defined(m,x),\hfill \\ \hfill & \\ \hfill & m_{\perp },\text{otherwise}.\hfill \end{array}\right)\end{array}\end{array}$$The semantics of the other basic statements of the Jane language is quite simple and is based on the definition of the basic constructs and properties of the semantics (see Steingartner et al. 2019).

Similar to the denotation in categories, here we also assume variable declarations and their introduction into the table of memory states. The semantics of declarations is defined as follows:

We represent each declaration as the following function on memory:$$\begin{array}{c}\hfill 〚\mathtt{var}x〛:\mathbf{Memory}\to \mathbf{Memory}.\end{array}$$For a given memory m, we define a function in the following way:$$\begin{array}{c}\hfill 〚\mathtt{var}x〛m=〚\mathit{alloc}〛(x,m).\end{array}$$This definition conveys the fact that the declaration is executed in a single step. Formally, the semantics of variable declaration is expressed as follows:$$\begin{array}{cc}& 〚\mathit{next}〛(〚\mathtt{var}x;D^{\ast };S^{\ast }〛,m,i_{}^{\ast },o_{}^{\ast })\hfill \\ \hfill & =(〚D^{\ast };S^{\ast }〛,〚\mathtt{var}x〛m,i_{}^{\ast },o_{}^{\ast }).\hfill \end{array}$$The user input statement, $\mathtt{read}x$, is performed in a single step and updates the previously declared variable x with the input value $v^{\prime }$. This action results in a change in the configuration, as indicated by the transition function$$\begin{array}{c}\hfill 〚\mathit{read}〛:\mathbf{Config}\to {\mathbf{Config}}^{\mathbf{Value}}\end{array}$$defined as follows:$$\begin{array}{c}\hfill \begin{array}{cc}& 〚\mathit{read}〛(〚\mathtt{read}x;S^{\ast }〛,m,i_{}^{\ast },o_{}^{\ast })=\hfill \\ \hfill \\ \hfill & =\left\{\begin{array}{ccc}& \lambda v^{\prime }.(〚S^{\ast }〛,m^{\prime },tail(i_{}^{\ast }),o_{}^{\ast }),\hfill & \hfill \text{if}Defined(m,x),\\ \hfill \\ \hfill & (〚S_{}^{\ast }〛,m_{\perp },tail(i_{}^{\ast }),o_{}^{\ast }),\hfill & \hfill \text{otherwise},\end{array}\right)\hfill \end{array}\end{array}$$where$$\begin{array}{c}\hfill m^{\prime }=m[((x,Highest(m,x)),v)\mapsto ((x,Highest(m,x)),v^{\prime })].\end{array}$$This implies that any value stored in the variable x, which was declared at the outermost (highest) nesting level, will be altered (replaced) with the input value $v^{\prime }$.

The statement to provide the observable value to the user $\mathtt{print}e$ is also executed in one step. This statement computes the current value of the arithmetic expression e within the existing memory m and presents the result as an observable (visible) value. The memory remains unchanged, but the configuration changes. The semantics of this statement can be represented by a transition function$$\begin{array}{c}\hfill 〚\mathit{print}〛:\mathbf{Config}\to \mathbf{Value}\times \mathbf{Config}\end{array}$$defined as follows:$$\begin{array}{cc}& 〚\mathit{print}〛(〚\mathtt{print}e;S_{}^{\ast }〛,m,i_{}^{\ast },o_{}^{\ast })\hfill \\ \hfill & =\left(〚,,e,,〛,m,,,(,〚,,S_{}^{\ast },,〛,,,m,,,i_{}^{\ast },,,(〚e〛m;o_{}^{\ast }),)\right).\hfill \end{array}$$To express the possibility of an unsuccessful termination of program execution due to an error (without specifying the resulting state), we introduce an additional function$$\begin{array}{c}\hfill 〚\mathit{abort}〛:\mathbf{Config}\to \mathbf{Config},\end{array}$$which is defined as follows:$$\begin{array}{c}\hfill 〚\mathit{abort}〛(config)=(\epsilon ,m_{\perp },\epsilon ,\epsilon ),\end{array}$$where $\epsilon$ stands for the empty list. This definition ensures that the interrupted program halts in an error configuration that no longer includes any statements requiring further execution.

[See PDF for image]

Fig. 11

Semantics of program $P_2$ in coalgebra

Now that we have the base category that serves as a model for the language Jane, we can proceed to construct a coalgebra modeling the behavior of programs written in Jane. This category consists of

• configurations $config=(〚D_{}^{\ast };S^{\ast }〛,m,i_{}^{\ast },o_{}^{\ast })$ as category objects,

• mappings $〚\mathit{next}〛,〚\mathit{read}〛,〚\mathit{print}〛$ and $〚\mathit{abort}〛$ as category morphisms.

The objects within our category constitute the state space of a coalgebra, and the morphisms represent the transition mappings. Hence, we construct the polynomial endofunctor for this kind of systems$$Q(\mathbf{Config})=1+\mathbf{Config}+O\times \mathbf{Config}+{\mathbf{Config}}^I.$$Here, $I\subseteq \mathbf{Value}$ represents the domain of input values, and $O\subseteq \mathbf{Value}$ signifies the domain of output values during program execution. The operation $+$ in the definition of the functor Q expresses distinct, mutually exclusive results of the functor.

It is easy to verify that such a defined structure is a category.

• An identity morphism is required for each object, but no morphism that defines the operational semantics of the language Jane can be considered an identity. To meet this requirement, we must explicitly define the identity ${\text{id}}_{\mathit{config}}$ for each object. The definition of such a morphism for every object ensures the fulfillment of this property.

• The composition of two morphisms, where the codomain of one morphism is also the domain of the other morphism, is a new morphism in $\mathcal{C}onfig$. This situation occurs when executing a sequence of statements.

• The associativity of morphism composition is evident and straightforward (trivial).

In addition, the category contains a final object – an undefined configuration $confi{g}_{\perp }$.

We can now construct a Q-coalgebra for the language Jane. A coalgebra morphism is formed by four functions:$$\begin{array}{c}\hfill ⟨〚,,\mathit{abort},,〛,,,〚,,\mathit{next},,〛,,,〚,,\mathit{print},,〛,,,〚,,\mathit{read},,〛⟩:\mathbf{Config}\to Q(\mathbf{Config}).\end{array}$$This coalgebra models the execution of a program step by step, thus providing the operational semantics of any program written in the Jane language. We note that thanks to our coalgebra, we are capable of modeling the behavior of programs written in real programming languages that include similar constructs.

Example in practice

In Fig. 11, we depict the semantics of the program for solving the puzzle Make chocolate (Listing 1) from Section 2.2.

At the beginning, we assume the input values for the variables x, y, z as follows: let $x=\mathbf{6}$, $y=\mathbf{1}$, and $z=\mathbf{10}$. These values are in the input value stream, $i_{}^{\ast }=(\mathbf{6},\mathbf{1},\mathbf{10})$, the output value list is empty, $o_{}^{\ast }=\epsilon$.

We add that in this case we also assume (at the global level) the statement $\mathtt{print}result$ at the end of the program.

The initial configuration is$$\begin{array}{c}\hfill confi{g}_0=\left(〚,,S,,〛,,,m_0,,,(\mathbf{6},\mathbf{1},\mathbf{10}),,,\epsilon \right),\end{array}$$where S is a substitution for a compound statement – the entire input program. The initial memory $m_0$ is empty.

First, the declarations on lines 1-4 are processed:$$\begin{array}{c}\hfill \begin{array}{cc}\hfill confi{g}_1& =〚\mathit{next}〛(confi{g}_0)\hfill \\ \hfill & =\left(〚,,\mathtt{var}y;\dots ,,〛,,,m_1,,,(\mathbf{6},\mathbf{1},\mathbf{10}),,,\epsilon \right),\hfill \\ \hfill confi{g}_2& =〚\mathit{next}〛(confi{g}_1)\hfill \\ \hfill & =\left(〚,,\mathtt{var}z;\dots ,,〛,,,m_2,,,(\mathbf{6},\mathbf{1},\mathbf{10}),,,\epsilon \right),\hfill \\ \hfill confi{g}_3& =〚\mathit{next}〛(confi{g}_2)\hfill \\ \hfill & =\left(〚,,\mathtt{var}result;\dots ,,〛,,,m_3,,,(\mathbf{6},\mathbf{1},\mathbf{10}),,,\epsilon \right),\hfill \\ \hfill confi{g}_4& =〚\mathit{next}〛(confi{g}_3)\hfill \\ \hfill & =\left(〚,,\mathtt{read}x;\dots ,,〛,,,m_4,,,(\mathbf{6},\mathbf{1},\mathbf{10}),,,\epsilon \right),\hfill \\ \hfill \end{array}\end{array}$$where $m_1=〚\mathtt{var}x〛m_0$, analogously to the processing of the other declarations, as shown in the Fig. 12.

[See PDF for image]

Fig. 12

Memory configurations during the declarations of variables

Subsequently, in individual steps, the commands on lines 5-7 are executed and formally expressed by the corresponding semantic function $〚\mathit{read}〛$. These statements gradually update the memory contents by assigning values from the input to individual variables (according to the specified specification, Fig. 13) and the list of input values is gradually emptied:$$\begin{array}{c}\hfill \begin{array}{cc}\hfill confi{g}_5& =〚\mathit{read}〛(confi{g}_4)\hfill \\ \hfill & =\left(〚,,\mathtt{read}y;\dots ,,〛,,,m_5,,,(\mathbf{1},\mathbf{10}),,,\epsilon \right),\hfill \\ \hfill confi{g}_6& =〚\mathit{read}〛(confi{g}_5)\hfill \\ \hfill & =\left(〚,,\mathtt{read}z;\dots ,,〛,,,m_6,,,(\mathbf{10}),,,\epsilon \right),\hfill \\ \hfill confi{g}_7& =〚\mathit{read}〛(confi{g}_6)\hfill \\ \hfill & =\left(〚,,S^{\prime };\dots ,,〛,,,m_7,,,\epsilon ,,,\epsilon \right),\hfill \\ \hfill \end{array}\end{array}$$where $S^{\prime }$ stands for the conditional statement beginning at line 8.

[See PDF for image]

Fig. 13

Assigning the values to variables from user’s input

The conditional statement is then executed. The value of the condition on line 8 is false,$$\begin{array}{c}\hfill 〚(z>x+5\ast y)\vee (z\text{mod}>x)〛m_7=\mathbf{false},\end{array}$$so the next configurations follow:$$\begin{array}{c}\hfill \begin{array}{cc}\hfill confi{g}_8& =〚\mathit{next}〛(confi{g}_7)\hfill \\ \hfill & =\left(〚,,\mathtt{begin}\dots ,,〛,,,m_7,,,\epsilon ,,,\epsilon \right),\hfill \\ \hfill \end{array}\end{array}$$which corresponds to continuing in the program in the else branch (line 10) and entering the local block on line 11. The local declaration (line 12) is processed in the block$$\begin{array}{c}\hfill \begin{array}{cc}\hfill confi{g}_9& =〚\mathit{next}〛(confi{g}_8)\hfill \\ \hfill & =\left(〚,,\mathtt{var}calc;\dots ,,〛,,,m_8,,,\epsilon ,,,\epsilon \right).\hfill \\ \hfill \end{array}\end{array}$$After the declaration, the conditional statement follows (line 13):$$\begin{array}{c}\hfill \begin{array}{cc}\hfill confi{g}_{10}& =〚\mathit{next}〛(confi{g}_9)\hfill \\ \hfill & =\left(〚,,S^{\prime \prime };\dots ,,〛,,,m_9,,,\epsilon ,,,\epsilon \right),\hfill \\ \hfill \end{array}\end{array}$$where $S^{\prime \prime }$ is a substitution for the conditional statement on lines 13-16. The condition in the conditional statement is evaluated with values from the memory state $m_9$. Its value is true,$$\begin{array}{c}\hfill 〚z\text{div}5>y〛m_9=\mathbf{true},\end{array}$$so the following configuration has the form (the then branch on line 14)$$\begin{array}{c}\hfill \begin{array}{cc}\hfill confi{g}_{11}& =〚\mathit{next}〛(confi{g}_{10})\hfill \\ \hfill & =\left(〚,,calc:=y;\dots ,,〛,,,m_9,,,\epsilon ,,,\epsilon \right).\hfill \\ \hfill \end{array}\end{array}$$The changes of memory states during the processing the local block are expressed in Fig. 14.

[See PDF for image]

Fig. 14

Memory during the processing of the local block

[See PDF for image]

Fig. 15

Final memory configuration after the program execution

The last step in the local block is to assign a value to the global variable result (line 17)$$\begin{array}{c}\hfill \begin{array}{cc}\hfill confi{g}_{12}& =〚\mathit{next}〛(confi{g}_{11})\hfill \\ \hfill & =\left(〚,,result:=z-5\ast calc;\dots ,,〛,,,m_{10},,,\epsilon ,,,\epsilon \right),\hfill \\ \hfill \end{array}\end{array}$$followed by the termination of the local block and the removal of local declarations (Fig. 15)$$\begin{array}{c}\hfill \begin{array}{cc}\hfill confi{g}_{13}& =〚\mathit{next}〛(confi{g}_{12})\hfill \\ \hfill & =\left(〚,,\mathtt{end};\dots ,,〛,,,m_{11},,,\epsilon ,,,\epsilon \right).\hfill \\ \hfill \end{array}\end{array}$$If we assume that the last line of code at the end of the program at the global level is the print result statement, then the next steps in the calculation are:$$\begin{array}{c}\hfill \begin{array}{cc}\hfill confi{g}_{14}& =〚\mathit{next}〛(confi{g}_{13})\hfill \\ \hfill & =\left(〚,,\mathtt{print}result,,〛,,,m_{12},,,\epsilon ,,,\epsilon \right),\hfill \\ \hfill \\ \hfill confi{g}_{15}& =〚\mathit{print}〛(confi{g}_{14})\hfill \\ \hfill & =\left(\epsilon ,,,m_{12},,,\epsilon ,,,(\mathbf{5})\right).\hfill \\ \hfill \end{array}\end{array}$$

Key takeaways

Our approach to defining the semantics of programming languages, this time using categories and coalgebras, overcomes several shortcomings of the traditional approach. We expressed the operational semantics using a coalgebra over the category of memory configurations.

The presented definition of configurations as memory abstractions makes it possible to work with both statements and declarations simply and uniformly, which is one of the advantages of our approach. Each separate step of program execution is expressed by the application of the polynomial endofunctor Q in the configuration category that characterizes this kind of system. Our coalgebra provides insights into the mechanisms governing the flow of input and output values as they enter and exit the system. Another advantage of our approach is the possibility to graphically illustrate the execution of the individual steps of the program execution and thereby simply visualize the execution of the program, which is more comprehensible for pedagogical purposes and the needs of practice.

The way we constructed the coalgebra and the category above the coalgebra will also serve as a basis for our further research. This way of defining semantics can be further extended, for example by adding other types of values or defining the operational semantics of procedures. This could be the starting point for the definition of coalgebraic semantics for component systems. In this way, we would make it possible to define semantics for advanced and modern programming constructs.

Exploring further insights from our research of semantic modeling findings

Our research extends beyond theory. It offers practical applications to address a multitude of IT challenges, including recursive calculations, function relationships, and component program systems. This bridge between theory and practicality is a distinctive feature of our work. In the previous research, we focused primarily on category-based modeling of imperative programs. Categories as mathematical structures have proven to be a very useful modeling tool: category objects can represent structures of arbitrary complexity, and morphisms between objects express relationships (transitions, derivations, parts of proofs, parts of calculations, etc.).

In this section, we present some other results of our research. In Section 6.1, we present how we integrated one way of modeling recursive calculations using algebraic and coalgebraic structures into the teaching process. In Section 6.2, we model the relations between functions and their derivatives using the codomain functor as a special functor. We present the properties of categorical models of component programs and the relationships between them in Section 6.3.

An insight into modeling of recursion

Recursion plays an essential role in programming. It has an irreplaceable place in computer science curricula (courses such as Data structures and algorithms, Semantics of languages, Advanced programming techniques, and others).

Initial algebra as a special algebra provides a general framework for induction and recursion. The initial algebra $(\mu F,i{n}_F)$ is the least fixed point of the functor F (Lambek and Scott 1986). The existence of this algebra means that to any algebra (A, a) there is exactly one homomorphism from the initial algebra, which is called a catamorphism and denoted by ${(cataa)}_F:\mu F\to A$ (Fokkinga 1992). The structure ${(cata(-))}_F$ acts as an iterator in the computation. Since algebras and coalgebras are dual mathematical structures, the analogous property also applies to coalgebras: the final coalgebra $(\nu F,ou{t}_F)$ is the largest fixed point of the functor F. The existence of this coalgebra means that from any coalgebra $(U,\phi )$ there is exactly one homomorphism to the final coalgebra, which is called an anamorphism and denoted ${(ana\phi )}_F:U\to \nu F$. The structure ${(ana(-))}_F$ acts as a coiterator in the computation. In addition to the listed special morphisms, there is also a hylomorphism. It is a special morphism that expresses the notation of a recursive scheme. It was first defined in the work of Fokkinga and Meijer (1991). Hylomorphism expresses the recursive function $f:U\to FU$, which is the least fixed point of the function composed of $a:FA\to A$ and $\phi :U\to FU$ (Cunha et al. 2006):$$hylo{(a,\phi )}_F=\mu (\lambda f.a\circ Ff\circ \phi ).$$We construct hylomorphism as a composition of anamorphism and catamorphism (Kabanov and Vene 2006):

3

$$\begin{array}{c}\hfill hylo{(a,\phi )}_F={(cataa)}_F\circ {(ana\phi )}_F.\end{array}$$Hylomorphism represents general recursion by creating complex data structures and then processing them (Adámek et al. 2007; Capretta et al. 2006).

In the works (Steingartner and Macko 2011; Steingartner et al. 2012), we presented some more of our ideas and results regarding the construction of hylomorphism and recursive coalgebra.

We note that, for example, factorial calculation can be performed both recursively and iteratively. But the factorial can be calculated in other ways (albeit many times unconventionally), as presented in Ruehr (n.d.). The given material inspired us to explore more deeply the properties of algebraic and categorical structures and the result is the categorical model along with the implementation of the calculation using the functions acting as catamorphism and anamorphism, written in OCaml language (Leroy et al. 2020; OCaml Development Team 2024) which also supports the object approach (Hickey 2008; Minsky et al. 2013).

Function ana has a form listed in Listing 2.

Subsequently, function cata has a form listed in Listing 3.

Hylomorphism, which implements recursive computation, is a composition of anamorphism and catamorphism functions. In Ocaml, the implementation of this function is listed in Listing 4 The calculation principle consists of the fact that the ana function first creates a list, i.e. it behaves like a constructor. Subsequently, the list filled with values is passed to the cata function, which is a deconstructor, and thus sequentially selects the elements it processes – multiplying them in the order in which they are selected from the list. At the output, this composite function will give the correct (expected) result.

We have successfully implemented this method in the form of a separate chapter in the course Data Structures and Algorithms focused on recursion and its properties and formal foundations. Moreover, we presented how we can model recursive calculations in an unconventional, but equally illustrative and interesting way. At the same time, we have also integrated these principles into the course Formal Semantics of Languages, where recursive computations form a pillar of denotational semantics. When searching for the meanings of recursive functions, we can compare, for example, recurrent relations, the construction of a functional (higher-order function) and the derivation of its fixed point, as well as the method we have presented for computing recursive functions using algebraic and coalgebraic structures.

We note that the method of modeling recursion presented by us is intended primarily to help with the illustrativeness and, to a large extent, the elegance of the recursion expression itself, which is often very positively received in various courses where we focus on the basics of programming, algorithm design, or advanced calculations with recursion.

Categorical modeling in differential calculus and integral calculus

Categorical structures have also proven to be an interesting means of modeling some types of calculations in differential and integral calculus. The rigorous foundations of infinitesimal calculus are based on the concept of functions and limits. This insight makes it possible to model relations between sets and functions using categorical structures: objects, morphisms, and functors (Steingartner and Galinec 2013).

Differential calculus provides methods and procedures to find its derivative $f^{\prime }$ for a given function f. In practice, we use a few rules that tell us how to find the derivative of almost any common function.

We presented and constructed a categorical model of the relationship between functions and derivatives in the papers (Steingartner and Galinec 2013; Steingartner and Radaković 2014). In this section, we briefly introduce the basic elements and properties of our model for functions and their derivatives.

To easily express derivations in categories, we use morphism category, which is constructed above the base category. Objects of the morphism category ${\mathcal{C}}^{\to }$ are morphisms from the base category $\mathcal{C}$. Morphisms in the category ${\mathcal{C}}^{\to }$ are pairs of mappings between domains and codomains of morphisms of the category $\mathcal{C}$.

The derivative $f^{\prime }$ of the function f is also a function. The base category, which for our purposes we denote $\mathcal{D}er$, consists of:

• of object classes, which are sets – domains and codomains of functions,

• of the class of morphisms, i.e. functions.

We can reliably verify the fact that in this category an identity (identical function) is defined for each object, functions can be composed, and associativity applies to the composition of functions.

We construct a category of morphisms $\mathcal{D}e{r}^{\to }$ above the base category. This category exists by definition. Its objects are functions (morphisms from the base category), morphisms are pairs displayed between domains and codomains of functions, while we limit ourselves to morphisms that display functions on their derivatives.

The category of morphisms $\mathcal{D}e{r}^{\to }$ is thus defined as follows:

• Category objects are functions and their derivatives: $f,g,f^{\prime },f^{\prime \prime },\dots$

• Morphisms are ordered pairs of mappings between respective domains and codomains: $$(d,c):f\to f^{\prime },$$ where d is the mapping between domains and c between codomains. We simply denote the der morphisms: $$der:f\to f^{\prime }.$$

• For each object f there is an identical morphism that maps the given object to the same object: $${\text{id}}_f:f\to f.$$

• Composition of morphisms is based on properties of composition of functions and derivatives of functions. For two morphisms $de{r}_1:f\to f^{\prime }$ and $de{r}_2:f^{\prime }\to f^{\prime \prime }$ there exists a morphism $$de{r}_2\circ de{r}_1:f\to f^{\prime \prime },$$ which expresses the second derivative of the function f. The second derivative of the function f is the first derivative of the function $f^{\prime }$: ${(f^{\prime })}^{\prime }=f^{\prime \prime }$.

• Composition of morphisms is an associative operation and is defined as follows: $$\left(d,e,r_3,\circ ,d,e,r_2\right)\circ de{r}_1=de{r}_3\circ \left(d,e,r_2,\circ ,d,e,r_1\right).$$

A codomain functor between a base category and a category of morphisms$$Cod:\mathcal{D}e{r}^{\to }\to \mathcal{D}er$$always exists by definition. The functor assigns an object f from the category $\mathcal{D}e{r}^{\to }$ to its codomain cod(f) from the base category $\mathcal{D}er$ and to each morphism $der:f\to f^{\prime }$ from the category $\mathcal{D}e{r}^{\to }$ morphism between the corresponding codomains from the category $\mathcal{D}er$. We model this relationship in Fig. 16.

[See PDF for image]

Fig. 16

A categorical model of the relationship of functions and their derivatives

Concerning similar approaches in categorical modeling for differential calculus, in the work (Wituła et al. 2020) the authors present their way of evaluating integrals using matrix inversion. The authors of the mentioned work state that the theoretical foundations presented and published by them indicate a remarkable similarity or even complete agreement with the considerations presented in our work (Steingartner and Galinec 2013), which refers to the relations between categorical structures and infinitesimal calculus.

Some ideas and assumptions for categorical component modeling

Component programming is sometimes viewed as a (modular) superstructure of object-oriented programming. The main difference between component and object-oriented programming is that in component programming the emphasis is on interfaces and composition, in object-oriented programming on objects and classes.

Our research focuses on the formulation of a formal framework for the specification and modeling of component programming systems. The steps taken so far have led us to consider that, due to the complexity of this problem, it seems logical to construct this framework hierarchically on three levels. At the first level, we deal with interfaces and interactions between components. Interfaces are visible parts of components (Gupta and Tripathi 2011) and can be expressed as algebraic specifications consisting of signatures and axioms, where the signature contains typed ports and operational specifications (Löwe et al. 2005). In addition to expressing the interface using abstract data types, an alternative – abstract behavioral type (abstract behavioral type – ABT) was presented in the work (Arbab 2005). The authors define this type as a higher-level alternative to the abstract data type and propose it as a suitable base model for both components and their composition. An abstract behavioral type defines an abstract behavior as a relationship between sets of temporal data streams without specifying any implementation details.

By the term port we mean a communication element through which a component sends or receives data of a certain type (Bauer et al. 2013). Axioms can usually be written in equational logic or predicate linear logic (Macko et al. 2013). The first layer of a component system can be modeled as a category of interfaces, where objects are representations of interfaces and morphisms are interactions between components. The task of the second layer is to take into account the contracts that form the basis for the successful composition and interaction of components. The composition of two or more components leads to a functional system if all assumptions and guarantees of both components are met (Mantel et al. 2011). A diagram of contracts for the interaction and composition of two components is in Fig. 17.

[See PDF for image]

Fig. 17

Contract diagram between components (reprinted from Steingartner et al. 2014)

[See PDF for image]

Fig. 18

An architecture of the proposed framework for modeling component systems (reprinted from Steingartner et al. 2014)

In the case of composition and interaction, we have two options: to extend the interface specifications with assumptions and guarantees or to express them as formulas in predicate linear logic. Both solutions allow for maintaining a subtyped relationship between assumptions and guarantees. This layer can limit the possible interaction between components to fulfill contracts. Dependencies will be introduced on the third layer. Dependencies can be expressed as predicates in predicate linear logic and modeled in the appropriate category. A schematic of this three-layer architecture is in Fig. 18.

Our idea of expressing how individual layers are connected leads to some functors or natural transformations with appropriate properties. In our research, we focus on examining and illustrating our theoretical results on real component systems. One such true component system appears to be a system composed of microservices. Such a system can help us verify our results and illustrate relevant concepts for students, as well.

Category theory provides two possibilities for modeling systems of basic component programs in this approach. If we are interested in component composition, it is convenient to model component interfaces as category objects. In the case of modeling interactions as category morphisms, we have two options: either we can construct category morphisms as representations expressing the functionalities of interactions, or we can model them as relations that lead to relational categories. The second approach is not trivial and requires a deeper analysis. In the case of modeling the observable behavior of component program systems, it is advisable to use coalgebras, while constructing a polynomial endofunctor for modeling the behavior in individual steps. This endofunctor is constructed over the category of states.

This research is still relevant and our common goal in this research is to prepare a formal system appropriately describing and interpreting the basic principles of component program systems.

Conclusions

In this article, we focused on presenting several important results of our research in the field of semantic methods and semantic modeling. We are aware that while practical metrics like memory usage or efficiency are essential in applied implementations, the primary objective of our research is theoretical: to create a rigorous formal framework. As the main structures for modeling, we chose categories. We proposed formal modeling of denotational semantics of imperative programs with category theory, focusing on the morphisms or relationships between objects (expressing the denotation functions), i.e. as states of memory. Similarly to the previous case, we subsequently focused on research in the field of categorical modeling for structural operational semantics. We proceeded from the properties of the method, which describes the implementation in individual elementary steps. Coalgebras that are not trivial structures have proven to be very suitable for this type of expression of program behavior and dynamics. In describing the denotation in categories, we proceeded from the fact that the state of memory was the basic object for categorical representation. In the modeling of operational semantics, we also took into account the input and output values, which required a change of state for the configuration. The meanings (semantics) of programs in this model, thanks to the coalgebras, resemble the stepping of programs, and thus the representation of the meaning of programs in individual elementary steps. Formally, this is expressed by the function $〚\mathit{next}〛$, which always represents one step of the computation. Subsequently, we proceeded to the construction of the category $\mathcal{C}onfig$, whose objects are configurations and morphisms are transitions. Execution is modeled by a polynomial endofunctor Q which is defined for individual types of transitions depending on the statement to be executed (input, output, interrupt, transition). Finally, we presented and discussed some other results that we achieved in research in the field of semantic modeling of some mathematical and practical IT problems: categorical modeling of recursive calculations and their subsequent implementation (with a focus on teaching support), categorical model of function relationships and their derivatives (categorical modeling in differential calculus), or the formulation of foundations and assumptions for the construction of categorical models of component program systems.

We are not limited in this research, as new challenges and problems appear that need to be solved in the given area and to find a relationship with already existing approaches. The same is true in the broader spectrum of semantic (or formal) modeling using category theory in the wider scientific community. We discussed several significant cases of using category theory for real systems in informatics and related fields (modeling of agent systems and their communication similar to Novotný et al. (2022), use of category theory for modeling in machine learning, model-driven based approach, or modeling of natural processes or other use in the field of applied informatics, etc.). Several real-world examples of similar problems can be found in the cited literature and elsewhere.

In short, we presented a mathematical framework that can rigorously and formally accurately express the dynamics of the execution of programs written in an imperative language and interpret state changes during program execution. Understanding the semantic information resides in graphical representation where the sequence of all states during the program execution provides a path in a directed graph (which is another expression of the category itself! see Barr and Wells 1990) since the category theory provides a framework in which category can be regarded as a directed graph describing the mathematical structure (Zhao et al. 2023) and understanding how categorical operations act on that information leads to many specific real-world situations that can occur in programming which should be explored further.

In summary, our research presents a paradigm shift in the understanding of imperative programming semantics. Our innovative approach, rich in mathematical rigor and practical relevance, not only advances the field but also opens up new avenues for research and application. We hope that this work will have a lasting impact on the dynamic landscape of semantic modeling, reshaping the way we view and use imperative programming concepts.

Author Contributions

The sole author was responsible for the conception, research, writing, and revision of this paper.

Funding

This work was supported by the Aktion Österreich-Slowakei project grant Nr. 2024-05-15-001 “Formalizing and Generating Executable Implementations of Domain-Specific Languages”, and by KEGA project 030TUKE-4/2023 “Application of new principles in the education of IT specialists in the field of formal languages and compilers”, granted by the Cultural and Education Grant Agency of the Slovak Ministry of Education.

Availability of data and material

Not applicable.

Declarations

Conflict of interest

Not applicable.

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

References

Adámek, J. Introduction to coalgebra. Theory Appl Categories [electronic only]; 2005; 14, pp. 157-199.2156194

Adámek, J; Lücke, D; Milius, S. Recursive coalgebras of finitary functors. RAIRO - Theoretical Inf Appl - Inf Théorique Appl; 2007; 41, 4 pp. 447-462.2377973 [DOI: https://dx.doi.org/10.1051/ita:2007028]

Aguinaldo A (2020) Category theory for software modeling and design. Hunter College Applied Mathematics Seminar. https://angelineaguinaldo.com/assets/slides/HCAM_Seminar___Oct_29_2020.pdf. Accessed 12 07 2023

Aguinaldo, A; Pollard, B; Canedo, A; Quiros, G; Regli, W. Robocat: a category theoretic framework for robot interoperability using goal-oriented programming. IEEE Trans Autom Sci Eng; 2022; 19, 3 pp. 2637-2645. [DOI: https://dx.doi.org/10.1109/TASE.2021.3094055]

Ambler S-J (1991) First order linear logic in symmetric monoidal closed categories. PhD thesis, University of Edinburgh

Arbab F (2005) Abstract behavior types: a foundation model for components and their composition. Sci Comput Program 55(1):3–52.https://doi.org/10.1016/j.scico.2004.05.010. Formal methods for components and objects: pragmatic aspects and applications

Baclawski, K; Simovici, D; White, W. A categorical approach to database semantics. Math Struct Comput Sci; 1994; 4, pp. 147-183.1281758 [DOI: https://dx.doi.org/10.1017/S0960129500000426]

Baez, J; Li, X; Libkind, S; Osgood, ND; Patterson, E. Compositional modeling with stock and flow diagrams. Electron Proc Theoretical Comput Sci; 2023; 380, pp. 77-96.4660933 [DOI: https://dx.doi.org/10.4204/eptcs.380.5]

Barr, M; Wells, C. Category theory for computing science; 1990; Prentice Hall:

Barr M, Wells C (2013) Toposes, triples and theories. Grundlehren der mathematischen Wissenschaften. Springer. http://www.cwru.edu/artsci/math/wells/pub/ttt.html

Bauer, S; Hennicker, R; Legay, A. Păsăreanu, CS; Salaün, G. Component interfaces with contracts on ports. FACS 2012: formal aspects of component software; 2013; Springer: pp. 19-35. [DOI: https://dx.doi.org/10.1007/978-3-642-35861-6_2] 7684

Bradley, T-D; Terilla, J; Vlassopoulos, Y. An enriched category theory of language: from syntax to semantics. Matematica; 2021; 1, pp. 551-580.4445934 [DOI: https://dx.doi.org/10.1007/s44007-022-00021-2]

Breiner, S; Subrahmanian, E; Jones, A. Categorical foundations for system engineering; 2018; Cham, Disciplinary convergence in systems engineering research. Springer: pp. 449-463.

Bunge, M. Treatise on basic philosophy: ontology II: a world of systems; 1979; Springer: [DOI: https://dx.doi.org/10.1007/978-94-009-9392-1] 4

Capretta V, Uustalu T, Vene V (2006) Recursive coalgebras from comonads. Inf Comput 204(4):437–468. Seventh workshop on coalgebraic methods in computer science 2004

Cunha, A; Pinto, JS; Proença, J. Butterfield, A; Grelck, C; Huch, F. A framework for point-free program transformation. Implementation and application of functional languages; 2006; Berlin, Heidelberg, Springer: pp. 1-18.

Dedera, L. Počítačové jazyky a ich spracovanie [Computer Languages and Their Processing]; 2014; Liptovský Mikuláš (in Slovak), Academy of the Armed Forces of General Milan Rastislav Štefánik:

Diskin Z (2001) On modeling, mathematics, category theory and rm-odp. In: Open distribute processing: enterprise, computation, knowledge, engineering and realisation, pp 38–54. https://api.semanticscholar.org/CorpusID:15306625

Diskin, Z; Maibaum, T. Category theory and model-driven engineering: from formal semantics to design patterns and beyond. Electron Proc Theoretical Comput Sci; 2012; 93, pp. 1-21. [DOI: https://dx.doi.org/10.4204/eptcs.93.1]

Fernández, M. Programming languages and operational semantics; 2014; A Concise Overview, Springer: [DOI: https://dx.doi.org/10.1007/978-1-4471-6368-8]

Fokkinga MM (1992) Law and order in algorithmics. PhD thesis, University of Twente, Netherlands

Fokkinga M, Meijer E (1991) Program calculation properties of continuous algebras. Automatica

Goguen JA, Harrell DF (2005) Information visualization and semiotic morphisms. In: Multidisciplinary approaches to visual representations and interpretations, pp 83–97. Elsevier

Graves H (2013) Category theory foundation for engineering modelling. http://www.omgwiki.org/MBSE/lib/exe/fetch.php?media=mbse:mathematical_foundation_engineering.pdf

Griffin, MD. How do we fix system engineering?. Paper presented at 61st international astronautical congress; 2010; Prague, Czech Republic: pp. 1-9.

Gupta R, Tripathi A (2011) Dependence analysis of component based software through assumptions. Int J Comput Sci Iss 8

Hickey J (2008) Introduction to objective Caml. s.n., dostupné na. https://www.freetechbooks.com/introduction-to-objective-caml-t698.html. Accessed 11 Dec 2022

Hyland, JME; Ong, C-HL. On Full Abstraction for PCF: I, II, and III. Inf Comput; 2000; 163, 2 pp. 285-408.1808886 [DOI: https://dx.doi.org/10.1006/inco.2000.2917]

Jacobs B (2016) Introduction to coalgebra: towards mathematics of states and observation. Cambridge tracts in theoretical computer science. Cambridge University Press

Jacobs, B; Rutten, J. A tutorial on (Co)Algebras and (Co)Induction. EATCS Bull; 1997; 62, pp. 62-222.

Jaskelioff M, Ghani N, Hutton G (2011) Modularity and implementation of mathematical operational semantics. Electronic notes in theoretical computer science vol 229(no 5), 75–95. Proceedings of the second workshop on Mathematically Structured Functional Programming (MSFP 2008)

Kabanov, J; Vene, V. Uustalu, T. Recursion schemes for dynamic programming. Mathematics of program construction; 2006; Berlin, Heidelberg, Springer: pp. 235-252. [DOI: https://dx.doi.org/10.1007/11783596_15]

Kock J (2009) Notes on polynomial functors. http://mat.uab.es/~kock/cat/polynomial.pdf. Universitat Autònoma de Barcelona, on-line. Accessed 12 July 2023

Kollár J (2009) Prekladače [Compilers]. elfa, s.r.o. (in Slovak)

Kovalyov S (2020) Leveraging category theory in model based enterprise. Adv Syst Sci Appl 20(1):50–65. https://doi.org/10.25728/assa.2020.20.1.781

Lambek, J; Scott, PJ. Introduction to higher order categorical logic; 1986; USA, Cambridge University Press:

Leroy X, Doligez D, Frisch A, Garrigue J, Rémy D, Vouillon J (2020) The OCaml system release 4.10. Version 4.10

Lippe, E; Ter Hofstede, AHM. A category theory approach to conceptual data modeling. RAIRO-Theor Inf Appl; 1996; 30, 1 pp. 31-79.1398858 [DOI: https://dx.doi.org/10.1051/ita/1996300100311]

Löwe, M., König H, Schulz C (2005) Algebraic properties of interfaces. In: Formal methods in software and systems modeling: essays dedicated to Hartmut Ehrig on the occasion of his 60th birthday, pp 190–203. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31847-7_11

Luzeaux, D. Boulanger, F; Krob, D; Morel, G; Roussel, J-C. A formal foundation of systems engineering. Complex systems design & management; 2015; Cham, Springer: pp. 133-148. [DOI: https://dx.doi.org/10.1007/978-3-319-11617-4_10]

Mabrok M, Ryan M (2015) Category theory as a formal mathematical foundation for model-based systems engineering. Appl Math Inf Sci 11:43–51. https://doi.org/10.18576/amis/110106

Mac Lane S (1998) Categories for the working mathematician, 2nd edn. Graduate texts in mathematics, vol 5. Springer

Macko P, Novitzká V, Steingartner W (2013) Interactions between components described in linear logic. In: Electrical engineering and informatics IV: proceedings of the faculty of electrical engineering and informatics of the technical University of Košice, pp 665–668. Faculty of Electrical Engineering and Informatics, Technical University of Košice, Košice, Slovakia

Mantel H, Sands D, Sudbrock H (2011) Assumptions and guarantees for compositional noninterference. In: Proceedings – IEEE computer security foundations symposium, pp 218–232. https://doi.org/10.1109/CSF.2011.22

Méhats, L; Soloviev, S. Coherence in smccs and equivalences on derivations in imll with unit. Ann Pure Appl Logic; 2007; 147, 3 pp. 127-179.2335084 [DOI: https://dx.doi.org/10.1016/j.apal.2007.03.005]

Milewski B (2019) Category theory for programmers

Minsky, Y; Madhavepeddy, A; Hickey, J. Real world OCaml; 2013; O’Reilly:

Mosses PD (1996) Theory and practice of action semantics. BRICS report series, vol. RS9653. University of Aarhus, Aarhus, DK

Nielson, HR; Nielson, F. Semantics with applications: an appetizer (Undergraduate topics in computer science); 2007; Berlin, Heidelberg, Springer: [DOI: https://dx.doi.org/10.1007/978-1-84628-692-6]

Novitzká, V; Slodičák, V. Categorical structures and their application in informatics; 2010; Košice, Equilibria:

Novotný, S; Michalko, M; Perháč, J; Novitzká, V; Jakab, F. Formalization and modeling of communication within multi-agent systems based on transparent intensional logic. Symmetry; 2022; 14, 3 588. [DOI: https://dx.doi.org/10.3390/sym14030588]

OCaml Development Team (2024) The OCaml Language. https://www.ocaml.org. Accessed 14 Jul 2024

Oreški D (2023) Application of machine learning methods for data analytics in social sciences. WSEAS Trans Syst 22:69–72. https://doi.org/10.37394/23202.2023.22.8

Ormandjieva, O; Bentahar, J; Huang, J; Kuang, H. Modelling multi-agent systems with category theory. Proc Comput Sci; 2015; 52, pp. 538-545. [DOI: https://dx.doi.org/10.1016/j.procs.2015.05.031]

Palša J, Ádám N, Hurtuk J, Chovancová E, Madoš B, Chovanec M, Kocan S (2022) Mlmd-a malware-detecting antivirus tool based on the xgboost machine learning algorithm. Appl Sci-Basel 12(13). https://doi.org/10.3390/app12136672

Parlante N (2013) CodingBat – introduction to MakeBricks. https://codingbat.com/doc/practice/makebricks-introduction.html. Accessed 7 November 2022

Perháč, J; Mihályi, D; Maťaš, L. Elimination of network intrusions via a resource oriented bdi architecture. Open Comput Sci; 2018; 8, 1 pp. 173-181. [DOI: https://dx.doi.org/10.1515/comp-2018-0016]

Perháč J, Novitzká V, Steingartner W, Bilanová Z (2021) Formal model of ids based on bdi logic. Mathematics 9(18). https://doi.org/10.3390/math9182290

Pfalzgraf, J. On categorical and logical modelling in multiagent systems. Anticipative Predictive Mod Syst Sci; 2005; 1, pp. 93-98.

Pfalzgraf J, Soboll T (2008) On a general notion of transformation for multiagent systems and its implementation. Electron Commun Eur Assoc Softw Sci Technol 12. https://doi.org/10.14279/TUJ.ECEASST.12.259

Plotkin, G. The origins of structural operational semantics. J Logic Algebraic Program; 2004; 60–61, pp. 3-15.2067227 [DOI: https://dx.doi.org/10.1016/j.jlap.2004.03.009]

Radaković, D; Herceg, Đ. Towards a completely extensible dynamic geometry software with metadata. Comput Lang Syst Struct; 2018; 52, pp. 1-20. [DOI: https://dx.doi.org/10.1016/j.cl.2017.11.001]

Robinson M (2016) Sheaves are the canonical datastructure for sensor integration. arXiv:1603.01446

Roşu G, Şerbănută TF (2010) An overview of the K semantic framework. J Logic Algebraic Program 79(6):397–434. https://doi.org/10.1016/j.jlap.2010.03.012. Membrane computing and programming

Ruehr F (n.d.) The evolution of a haskell programmer. Willamette University, Available at: https://willamette.edu/~fruehr/haskell/evolution.html. Accessed 21 Aug 2023

Schmidt, DA. Denotational semantics: a methodology for language development; 1986; William C, Brown Publishers, USA:

Schreiner, W; Steingartner, W; Novitzká, V. A novel categorical approach to semantics of relational first-order logic. Symmetry; 2020; 12, 10 1584. [DOI: https://dx.doi.org/10.3390/sym12101584]

Slodičák V (2012) Toposes are symmetric monoidal closed categories. Sci Res Inst Math Comput Sci 11(1), 107–116. https://doi.org/10.17512/jamcm.2012.1.11

Slonneger, K; Kurtz, B. Formal syntax and semantics of programming languages: a laboratory Based approach; 1995; 1 Inc, USA, Addison-Wesley Longman Publishing Co.:

Sowa JF (2000) Knowledge representation: logical, philosophical, and computational foundations. Brooks/Cole

Spivak, DI; Kent, RE. Ologs: a categorical framework for knowledge representation. PLoS One; 2012; 7, 1 24274. [DOI: https://dx.doi.org/10.1371/journal.pone.0024274]

Steingartner, W. On some innovations in teaching the formal semantics using software tools. Open Comput Sci; 2021; 11, 1 pp. 2-11. [DOI: https://dx.doi.org/10.1515/comp-2020-0130]

Steingartner, W; Macko, P. New approaches in functional programming using algebras and coalgebras. ETAPS 2011: European joint conferrences on theory and practice of software - workshop on generative technologies; 2011; Saarbrücken, Germany, Universität des Saarlandes: pp. 13-23.

Steingartner, W; Radaković, D. Categorical structures as expressing tool for differential calculus. Central Eur J Comput Sci; 2014; 4, 3 pp. 96-106. [DOI: https://dx.doi.org/10.2478/s13537-014-0220-7]

Steingartner, W; Macko, P; Novitzká, V. Some new approaches in functional programming based on categories. Lect Notes Comput Sci; 2012; 7241, pp. 517-532. [DOI: https://dx.doi.org/10.1007/978-3-642-32096-5_11]

Steingartner W, Galinec D (2013) The rôle of categorical structures in infinitesimal calculus. J Appl Math Comput Mech 12(1):107–119. https://doi.org/10.17512/jamcm.2013.1.11

Steingartner W, Novitzká V, Bačíková M, Korečko S (2017) New approach to categorical semantics for procedural languages. Comput Inf 36(6)

Steingartner W, Novitzká V, Benčková M, Prazňák P (2014) Considerations and ideas in component programming - towards to formal specification. In: Proceedings of the Central European Conference on Information and Intelligent Systems (CECIIS), (ed) Hunjak T, Lovrenčić S, Tomičić I. Faculty of Organization and Informatics, University of Zagreb, Varaždin, Croatia, pp 332–339

Steingartner W, Novitzká V, Schreiner W (2019) Coalgebraic operational semantics for an imperative language. Comput Inf 38(5)

Trancón y Widemann B, Hauhs M, (2010) Scientific modelling with coalgebra-algebra homomorphisms. Electron Notes Theoretical Comput Sci 264:105–123

Tuijn C (1994) Data modeling from a categorical perspective. PhD thesis, University of Antwerp, Antwerp, Belgium

Vallecillo A (2000) RM-ODP : the ISO reference model for open distributed processing. https://api.semanticscholar.org/CorpusID:7293221

Vickers, P; Faith, J; Rossiter, N. Understanding visualization: a formal approach using category theory and semiotics. IEEE Trans Visual Comput Graph; 2013; 19, pp. 1048-61. [DOI: https://dx.doi.org/10.1109/TVCG.2012.294]

Vokorokos L, Baláž A, Chovanec M (2009) Distributed detection system of security intrusions based on partially ordered events and patterns. In: Rudas IJ, Fodor J, Kacprzyk J (eds) Towards intelligent engineering and information technology, pp 389–403. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03737-5_28

Walters, RFC. Categories and computer science; 1992; Cambridge computer science texts, Cambridge University Press: [DOI: https://dx.doi.org/10.1017/CBO9780511608872]

Watson MD (2019) Engineering elegant systems: systems in mathematical categories. Seminar at Wright State University. https://www.nasa.gov/sites/default/files/atoms/files/system_engineering_research_consortium_category_theory_022619.pdf. System Engineering Research Consortium Category Theory Introduction. Accessed 28 05 2021

Wituła R, Słota D, Matlak J, Chmielowska A, Różański M (2020) Matrix methods in evaluation of integrals. J Appl Math Comput Mech 19(1):103–112. https://doi.org/10.17512/jamcm.2020.1.09

Yakin HSM, Totu A (2014) The semiotic perspectives of peirce and saussure: a brief comparative study. Procedia - Soc Behav Sci 155:4–8. https://doi.org/10.1016/j.sbspro.2014.10.247. The international conference on communication and media 2014 (i-COME’14) – communication, empowerment and governance: the 21st century enigma

Yi W, Gerasimov IV, Kuzmin SA, He H (2018) A category theory approach to phytometric system conceptual modeling. In: 2018 IEEE conference of Russian young researchers in electrical and electronic engineering (EIConRus), pp 391–393.https://doi.org/10.1109/EIConRus.2018.8317114

Zafiris, E. Complex systems from the perspective of category theory: I. functioning of the adjunction concept. Axiomathes; 2005; 15, 1 pp. 147-158. [DOI: https://dx.doi.org/10.1007/s10516-005-3790-0]

Zhao H, Chen Y, Fu X (2023) Comparison of machine learning based on category theory. J Web Eng 22(1), 41–54. https://doi.org/10.13052/jwe1540-9589.2213