    Course module   NWIIMC036  Category   MA (Master)  Language of instruction   English  Offered by   Radboud University; Faculty of Science; Informatica en Informatiekunde;  Lecturer(s)     Previous     Next 2 

 
 Academic year   2023   Period   KW3KW4  (29/01/2024 to 31/08/2024) 
 Starting block   KW3  
 Course mode   fulltime  
 Remarks     Registration using OSIRIS   Yes  Course open to students from other faculties   Yes  Preregistration   No  Waiting list   No  Placement procedure    
     
After successful completion of the course, the participants are able to:
• work with basic notions in category theory, such as functors, natural transformations, (co)limits
• recognise the role of monads in computation
• model streams and various types of automata as coalgebras
• formulate induction and coinduction categorically, and apply these as proof and definition principles for streams and automata
• apply the general coalgebraic definitions of behavior and equivalence to concrete system types


In this course, you will learn how to use category theory and coalgebra to study the foundational structure underlying several core concepts in computer science, such as statebased systems and automata and the behaviour of programs and programming languages. Category theory is an abstract mathematical language which organises and unifies numerous concepts in computer science and logic. For instance, it underlies the functional programming language Haskell, allows us to formulate datatypes such as streams and trees, and it provides a clear distinction between specification and implementation. The language of category theory has become standard throughout theoretical computer science.
The theory of coalgebras uses category theory to provide an elegant and very general notion of statebased system, such as automata and finitestate machines. Statebased systems are used widely to model, e.g., digital hardware, software programs, network protocols, distributed systems, programming language semantics, and in program correctness and verification.
In coalgebra, a system is viewed as a black box where knowledge of the system's state can only be obtained by observing the external behaviour. The type of observations and transitions in the external behaviour is specified by the system type. The theory of universal coalgebra provides general definitions of observable behaviour and bisimilarity that can be instantiated for concrete system types, as well as a powerful and fascinating reasoning principle called coinduction (a notion that is dual to the well known induction principle). The principle of coinduction has led to new, efficient algorithms for, e.g., language equivalence of nondeterministic automata.
This course develops the basics of category theory, with a strong emphasis on their use in coalgebra. We will see how various types of systems can be modelled as coalgebras, and how coinduction can be applied to them. These systems include basic datatypes, such as infinite streams and trees, and many types of automata (deterministic, nondeterministic, probabilistic, ...). Next, a number of fundamental notions such as language equivalence of automata, bisimilarity of processes and determinisation of nondeterministic automata, will be treated coalgebraically. You will learn how to combine coinduction and induction to derive effective specification and reasoning techniques for automata, and how these lead to concrete algorithms. The coalgebraic framework will then be used to obtain generalisations of these constructions to other types of systems. Besides coalgebra, we will also discuss the role of category theory, and specifically monads, in functional programming; in particular, this will include probabilistic computation.
The study of computer science at this level of abstraction is valuable in itself, and strengthens the foundation for numerous more concrete skills: e.g. specification, implementation, programming language design, functional programming, and perhaps most prominently abstraction and identification of relevant structure. Coalgebra is a rather recent field of research, existing for a mere two decades, and it is attracting an enthusiastic community. Being relatively young, it still has many elementary and exciting research questions to offer.
Instructional Modes
 Lecture
 Tutorial
 Selfstudy


  The course is selfcontained with respect to category theory: no prior knowledge of category theory or algebra is assumed. We assume that you are well acquainted with basic notions in (discrete) mathematics and propositional logic, and have some familiarity with basic automata theory. These are typically taught in introductory courses at a computer science programme, for example, in the following bachelor CS courses at Radboud University: Languages and Automata, Mathematical Structures, Logic and Applications. 

The final grade is based on:
• weekly homework assignments (h),
• final exam (t)
Homework qualifies as a potential bonus for the final grade, which is t + h/10, provided that t >= 5 (the final grade is t itself if t < 5).

 


   Required materialsHandoutsThe course material will consist of handouts and research papers on coalgebra.
All material will be made available electronically via the course website, or distributed during the course. 


Recommended materialsArticlesB. Jacobs and J.J.M.M. Rutten. An introduction to (co)algebra and (co)induction. In D. Sangiorgi and J.J.M.M. Rutten, editors, Advanced Topics in Bisimulation and Coinduction, Cambridge University Press, 2012. 
 ArticlesJ.J.M.M. Rutten. A tutorial on coinductive stream calculus and signal flow graphs.. Theoret. Comput. Sci., 343(3):443  481, 2005. 
 ArticlesJ.J.M.M. Rutten. Universal coalgebra: a theory of systems. Theoret. Comput. Sci., 249(1):3  80, 2000. 
 ArticlesJ.J.M.M. Rutten. Automata and coinduction (an exercise in coalgebra). Proceedings of CONCUR '98, D. Sangiorigi and R. de Simone (eds.), LNCS 1466, Springer, 1998, pp. 194218. 
 BookB. Jacobs, Introduction to Coalgebra. Towards Mathematics of States and Observations. Cambridge Univ. Press, 2016 


Instructional modesTestsFinal gradeTest weight   1 
Test type   Exam 
Opportunities   Block KW4, Block KW4 
RemarkSee detailed description under Test Information


  
 
 