Categorical Computer Science
Some topics for students'projects
by Dominique Duval

These projects are aimed at students in computer science or in mathematics with some experience of programming and some taste for cleanly specified notions.  

If you are interested in other topics for projects related to Category Theory for Computer Science, please contact Dominique.Duval@imag.fr.


Weakest Preconditions as PullBacks
(for Ensimag 3 MathsForFun, M2R Info, Mosig,...)

Context.

In order to reason about the correctness of imperative programs, one may use the Floyd-Hoare logic. In this logic, a statement {P}C{Q} is made of a command C together with two assertions (i.e., formulas in predicate logic) P and Q, where P is called the precondition and Q the postcondition. An assertion is valid when:

if P holds before the execution of C and if this execution terminates, then Q holds afterwards.

For example the statement {X=0}Y:=X+1{Y>0} is valid, as well as {X>=0}Y:=X+1{Y>0}, but {X=0}Y:=X+1{Y=0} is not valid.

The weakest precondition for a command C and an assertion Q is an "optimal" assertion wp(C,Q) such that the statement {wp(C,Q)}C{Q} is valid.

For example when C is Y:=X+1 and Q is Y>0, the weakest precondition is X>=0. Indeed, the statement {X>=0}Y:=X+1{Y>0} is valid, and any valid statement {P}Y:=X+1{Y>0} is such that P => (X>=0).

On the other hand, mathematicians have defined pullbacks in the framework of category theory, as a kind of generalization of the notion of intersection.

Project.

1. Define the notion of weakest precondition in Floyd-Hoare logic and give examples.
2. Define the notion of pullback in category theory and give examples.
3. What is the link between weakest preconditions and pullbacks?

References.

There are many references on weakest preconditions and pullbacks. A reference for point (3) is [BW, section 8.3.5., p. 87-88], which can be understood without reading all the previous pages.

[BW] Michael Barr and Charles Wells. Category Theory. Lecture Notes for ESSLLI (1999). http://folli.loria.fr/cds/1999/library/pdf/barrwells.pdf




Sketches for Databases
(for Ensimag 3 MathsForFun, M2R Info, Mosig,...)

Context.

Classical approaches to database design can be summarized as follows [J]. Modern relational databases are based on the Relational Model (RM), which is based on set theory. Relational Algebra (RA) is a formal language used to manipulate objects of the relational model. The Structured Query Language (SQL) is used to build and manipulate relational databases. A graphical tool for database design is provided by the Unified Modeling Language (UML), mainly its class diagrams. This is quite similar to some graphic standards of the Entity-Relationship (ER) model. On the other hand, [JRW] suggest that the mathematical notion of sketch, with its graphical interface, should be used for database design. They call it the Sketch Data Model.

Project.

1. It is assumed that classical database design is known.
2. What is the Sketch Data Model? Give examples.
3. Compare the UML class diagram design and the Sketch Data Model design on several examples.

References.

[J] Tom Jewett. Database design with UML and SQL. Introductory database class at California State University Long Beach, Department of Computer Engineering and Computer Science (2002). http://www.tomjewett.com/dbdesign/

[JRW] M. Johnson, R. Rosebrugh and R. J. Wood. Entity-relationship-attribute designs and sketches. Theory and Applications of Categories 10(2002), 94-112. http://tac.mta.ca/tac/volumes/10/3/10-03.pdf



Towards a categorical semantics for UML 
(for Ensimag 3 MathsForFun, M2R Info, Mosig,...)

Context.

In a modelling language like UML, the syntax of diagrams is well specified while its semantics (or intended meaning) remains intuitive and approximate. On the other hand, there is a mathematical theory based on diagrams, it is called the theory of categories. The issue is about using category theory in order to provide a sound semantics to (parts of) a diagrammatic modelling language.

Project.
  1. Look at the examples in [DW].
  2. Learn a little bit of category theory [BW].
  3. Learn a little bit aboutdiagrammatic logics [Du].
  4. Provide an analysis of [DW] in terms of diagrammatic logic.
References.
  • [BW] Michael Barr and Charles Wells. Category Theory for Computing Science. Third edition, CRM. See also: Category Theory. Lecture Notes for ESSLLI (1999).http://folli.loria.fr/cds/1999/library/pdf/barrwells.pdf
  • [DW] Zinovy Diskin and Uwe Wolter. Generalized Sketches: A Universal Logic for Diagrammatic Modeling in Software Engineering Proc. ACCAT 2007. [pdf]
  • [Du] Dominique Duval. How to combine diagrammatic logics. arXiv:0911.3005 (2009).



Conception et réalisation d'une interface graphique pour la réécriture de l'état d'une mémoire d'ordinateur
(stage d'ingénieur de 2 à 3 mois, par exemple Ricm 2)

projet co-encadré avec Frédéric Prost (LIG)

Contexte.

Les techniques de réécriture ont été introduites pour détailler les pas d'un calcul : par exemple (3-2)+4 se réécrit en 1+4 puis en 5. On parle alors de réécriture de termes. Plus généralement, la mémoire d'un ordinateur peut être représentée sous forme d'un graphe : les points sont les cases mémoire, les flèches sont les pointeurs entre les cases. Chaque modification de l'état de la mémoire, lors d'un calcul, peut être vue comme un pas de réécriture de graphes. La réécriture de termes est un cas particulier, où les graphes sont des arbres. Par contre les structures de données circulaires sont représentées par des graphes qui ne sont pas des arbres. Une bonne modélisation de la réécriture de graphes permettrait, entre autres, de contrôler l'occupation de la mémoire ; il s'agit d'un problème important pour les systèmes embarqués. Ce problème de modélisation est étudié depuis quelques années par R. Echahed et F. Prost (équipe CAPP du LIG) et D. Duval (équipe CASYS du LJK). Notre travail déjà conné lieu à plusieurs publications. Il est considéré par le LJK comme l'un des faits marquants du laboratoire pour l'année 2007. Essentiellement, une règle de réécriture L-->R est formée d'un membre gauche L et d'un membre droit R, et un pas de réécriture utilisant cette règle remplace une instance de L dans un graphe G par une instance de R dans un nouveau graphe H. Plus de détails se trouvent dans les références [Y] et [DEP].

Projet.

Il s'agit de compléter un logiciel graphique modélisant un pas de réécriture, écrit par Elias Yegdjong. Les principaux langages utilisés sont JGraphPro et Caml. Pour le moment, le logiciel fonctionne somme suit : l'utilisateur fournit une règle L-->R et une instance de L dans un graphe G, et le logiciel calcule le nouveau graphe H avec l'instance de R dans H. On souhaite ajouter plusieurs fonctionnalités à ce logiciel.

Déroulement du projet :
1. Comprendre le problème en utilisant le logiciel fourni.
2. Ajouter un module pour vérifier que les données fournies par l'utilisateur sont valides.
3. Ajouter un module qui calcule et propose à l'utilisateur toutes les instances de L dans G.
4. Ecrire une traduction des dessins vers LaTeX.

Logiciels utilisés : JGraphPro, Caml, LaTeX.

Un prolongement possible : inclure un traitement graphique du ramasse-miettes.

References.

[DEP] D. Duval, R. Echahed, F. Prost. Modeling pointer redirection as cyclic term-graph rewriting. ENTCS 176 p. 65-84 (2007).

[Y] E. Yegdjong. Conception et réalisation d'une interface graphique pour la réécriture de l'état d'une mémoire d'ordinateur. Rapport de stage RICM2, Polytech'Grenoble (2008).