Functional Operational Semantics and its Denotational Dual
Daniele Turi · Digital Academic REpository of VU University Amsterdam (Vrije Universiteit Amsterdam) · 1996
The notion of `functorial operational semantics' introduced in this thesis is a categorical formulation (and generalization) of `well-behaved' structural operational semantics based on labelled transition systems.This notion has several desirable properties (such as congruence of the associated strong bisimilarity, and existence of a dual denotational semantics) and it subsumes existing, concrete schemes (such as GSOS) for guaranteeing such good behaviour { at least in the case of languages extending `basic process algebra'.All this is achieved via use of the category theory of monads and comonads.The thesis also contains a coalgebraic treatment of the theory of non-well-founded sets which simpli es and improves some aspects of Peter Aczel's original presentation.Non-well-founded sets have played an important rôle in the development of the whole thesis: by working within Jan Rutten and Jaco de Bakker's project `non-wellfounded sets and programming languages semantics', I have had the opportunity of distilling the mathematical foundations for the main contribution of the thesis, the introduction of the functorial approach to operational semantics.Most of the research presented here has been conducted at the CWI, in Amsterdam.I can hardly imagine a better place to work on a thesis: the serene atmosphere, the international contacts, the superb library, the ecient organization, and the building itself, with quiet, balanced rooms, have made of this institute an ideal place for conducting pure research.Jaco de Bakker's department at the CWI is part of EuroFOCS, the European institute in the logical foundations of computer science.This has oered me the opportunity of spending six, most pro table months at LFCS, Edinburgh, visiting Gordon Plotkin, one of whose many contributions to the theory of computer science has been the introduction of the structural approach to operational semantics.When, in the early 80's, it was introduced, the novelty of structural operational semantics was that of bringing the mathematics of (structural) induction in the operational description of the behaviour of programming languages, providing a powerful formal tool for reasoning about programs.The present functorial approach can be seen as one step further in that direction: based on a suitable interplay between inductive and (dual) coinductive principles, it provides a mathematical de nition and treatment of `well-behaved' structural operational semantics.The contact with Gordon Plotkin has been crucial both for this thesis and for my general development.Particularly vivid in my memory is the image of a beautiful February of two years ago, when, during some discussions with him, the blackboard vii looked like self-drawing; the last picture he drew, with \algebras over coalgebras", has been decisive for formulating the notion of functorial operational semantics.The development of this notion, in Edinburgh, has been in uenced by exciting discussions with Marcelo Fiore and Alex Simpson.More generally, Marcelo has been precious for my whole research activity.Conceived, for the functorial part, in Edinburgh, this thesis has been written in Amsterdam.Thanks to very frequent reviewing sessions with my supervisors, Jaco de Bakker, Bart Jacobs, and Jan Rutten, the writing has rapidly converged to its nal form, in a natural and serene rhythm.Jaco, one of the pioneers of the mathematical approach to the semantics of programming languages which inspires this thesis, has granted me the room to develop the mathematics I felt most suitable, free from any prejudice.Almost without realizing it, I have written a much more thorough thesis than I had imagined, thanks to his gentle, but steady in uence.Jan, who brought me to the CWI, has collaborated to the development of coalgebraic methods in semantics which has been the basis for the research presented here.Bart, with his secure knowledge of category theory, has been a constant source of suggestions, corrections, and improvements.His limpid mind has always been available for discussions.Like Jan, he has shown great interest in and has collaborated to the foundational work on coalgebras.The last step in the preparation of this thesis, the refereeing process, is due to Andy Pitts, who has been very sympathetic to the problems tackled and the methods used in this thesis.In this preface, I have used many expressions plundered from his precise summarizing words.The `palaestra' for my early scienti c development has been the `Amsterdam Concurrency Group' led by Jaco and including Marcello Bonsangue, Frank de Boer, Franck van Breugel, Arie de Bruin, Joost Kok, Erik de Vink, and Herbert Wiklicky.Nostalgically, I remember the rst three-sessions talk I gave there, a promising winter of four years ago.Marcello \kamergeno(o)t" Bonsangue, together with Franck room-mate in the beloved M335, has shared these early developments and my growing interest in category theory.He is one of the extraordinarily many Italians who, from Catuscia Palamidessi on, have been at the CWI over the years.One of the persons who are most `responsible' for this Italian `colonization' is Krzysztof Apt; he was also the supervisor of my \tesi di laurea" for the University of Pisa, in my `prehistorical' time at the CWI.Also at LFCS I have been surrounded by Italians or Italian speakers.One of them, Pietro `everywhere' Di Gianantonio, has also been my colleague at the CWI and in the European SCIENCE project `Mathematical Structures in Semantics of Concurrency'.This project has been an important forum for discussions to me; apart from the CWI, the sites involved have been the university of Koblenz (Lutz Priese), Mannheim (Mila Majster-Cederbaum), Pisa (Ugo Montanari), and Udine (Furio Honsell), and the IRISA-INRIA of Rennes, where, in particular, I have had fruitful contacts with Eric Badouel and Philippe Darondeau.At the CWI, I have enjoyed discussions with Fer-Jan de Vries, Tim Fernando, and Femke van Raamsdonk, the ecient secretarial support by Mieke Brun e and Marja Hegt, the technical support by the Computer Help Information Desk, and the outstanding library service.My visit to Edinburgh has been arranged thanks to George Cleland and Monika Lekuse's help