Dagstuhl Seminar 13311
Duality in Computer Science
( Jul 28 – Aug 02, 2013 )
Permalink
Organizers
- Mai Gehrke (University of Paris VII, FR)
- Jean-Eric Pin (University of Paris VII, FR)
- Victor Selivanov (A. P. Ershov Institute - Novosibirsk, RU)
- Dieter Spreen (Universität Siegen, DE)
Contact
- Andreas Dolzmann (for scientific matters)
- Annette Beyer (for administrative matters)
Duality allows one to move between the two worlds: the world of certain algebras of properties and a spacial world of individuals, thereby leading to a change of perspective that may, and often does, lead to new insights. Dualities have given rise to active research in a number of areas of theoretical computer science. In this seminar we will concentrate on applications of duality in computation, semantics, and formal languages and we want to uncover the commonalities of the applications and of the further duality results developed in these areas.
Duality and computation Consider the area of exact real number computation. Real numbers are abstract infinite objects. Computing machines, on the other hand, can only transform finite objects. However, each real number is uniquely determined by the collection of rational open intervals that contain it, or a certain sub-collection thereof. Rational intervals can be finitely described as a pair of rationals. So, in order to compute with real numbers one has to compute with certain properties, i.e., one no longer works in the space of the reals but in the algebra generated by these properties. In doing so, the open intervals are considered as first-class objects and the concept of point is taken as a derived one. This is exactly the approach of pointless topology which tries to develop analytical concepts in a pointfree way, hereby using constructive logic.
Duality and semantics In logic, dualities have been used for relating syntactic and semantic approaches. Stone's original result is in fact of this type as it shows that clopen subsets of Stone spaces provide complete semantics for classical propositional logic. This base case has been generalized in various directions. There is a general scheme underlying this work: given a logic, construct its Lindenbaum algebra which in these cases is a Boolean algebra with unary operators. Jonsson-Tarski duality relates such algebras to binary relational structures which in the modal case are just Kripke frames. In this setting, a wide spectrum of duality tools are available, e.g. for building finite models, for obtaining interpolation results, for deciding logical equivalence and other issues. For infinitary logics, Stone-type dualities have also played an important role starting with Scott's groundbreaking first model of the lambda-calculus which is a Stone space. Subsequently Abramsky, Zhang and Vickers developed a propositional program logic, the logic of finite observations. More recently work of Jung, Moshier, and others has evolved this link between infinitary and finitary logics in the setting of logics for computation much further.
Duality and formal languages The connection between profinite words and Stone spaces was already discovered by Almeida, but Pippenger was the first to formulate it in terms of Stone duality. Gehrke, Pin and Grigorieff lately systematized and extensively developed this discovery which led to new research efforts in formal language theory. A final goal is a general theory of recognition.
Goals of the seminar The aim of this seminar is to bring together researchers from mathematics, logic and theoretical computer science that share an interest in the fields of computing with infinite data, semantics and for- mal languages, and/or the application of duality results, as well as to foster interaction between them. Some specific questions:
- Explore the use of the link between finitary and infinitary Stone dualities in other settings than semantics;
- Explore the link between complexity theory and semantics provided by the connection via duality theory;
- Identify the relationship between game semantics and dual spaces;
- Explore the link between the profinite semi-groups used in formal language theory and logics given by state-based transition systems or categorical models)
This seminar concentrated on applications of duality in computation, semantics, and formal languages.
Duality and computation
Consider the area of exact real number computation. Real numbers are abstract infinite objects. Computing machines, on the other hand, can only transform finite objects. However, each real number is uniquely determined by the collection of rational open intervals that contain it, or a certain sub-collection thereof. Rational intervals can be finitely described as a pair of rationals. So, in order to compute with real numbers one has to compute with certain properties, i.e., one no longer works in the space of the reals but in the algebra generated by these properties. In doing so, the open intervals are considered as first-class objects and the concept of point is taken as a derived one. This is exactly the approach of pointless topology which tries to develop analytical concepts in a pointfree way, hereby using constructive logic.
Duality and semantics
In logic, dualities have been used for relating syntactic and semantic approaches. Stone's original result is in fact of this type as it shows that clopen subsets of Stone spaces provide complete semantics for classical propositional logic. This base case has been generalized in various directions. There is a general scheme underlying this work: given a logic, construct its Lindenbaum algebra which in these cases is a Boolean algebra with unary operators. Jonsson-Tarski duality relates such algebras to binary relational structures which in the modal case are just Kripke frames. In this setting, a wide spectrum of duality tools are available, e.g. for building finite models, for obtaining interpolation results, for deciding logical equivalence and other issues. For infinitary logics, Stone-type dualities have also played an important role starting with Scott's groundbreaking first model of the lambda-calculus which is a Stone space. Subsequently Abramsky, Zhang and Vickers developed a propositional program logic, the logic of finite observations. More recently work of Jung, Moshier, and others has evolved this link between infinitary and finitary logics in the setting of logics for computation much further.
Duality and formal languages
The connection between profinite words and Stone spaces was already discovered by Almeida, but Pippenger was the first to formulate it in terms of Stone duality. Gehrke, Pin and Grigorieff lately systematized and extensively developed this discovery which led to new research efforts in formal language theory. A final goal is a general theory of recognition.
The seminar brought together researchers from mathematics, logic and theoretical computer science that share an interest in the fields of computing with infinite data, semantics and formal languages, and/or the application of duality results. The researchers came from 12, mostly European, countries, but also from Argentina, Japan, Russia, South Africa, and the United States.
Some of the specific questions that were investigated in talks and discussions:
- Explore the use of the link between finitary and infinitary Stone dualities in other settings than semantics;
- Explore the link between complexity theory and semantics provided by the connection via duality theory;
- Identify the relationship between game semantics and dual spaces;
- Explore the link between the profinite semi-groups used in formal language theory and logics given by state-based transition systems or categorical models)
- Jorge Almeida (University of Porto, PT) [dblp]
- Andrej Bauer (University of Ljubljana, SI) [dblp]
- Veronica Becher (University of Buenos Aires, AR) [dblp]
- Ulrich Berger (Swansea University, GB) [dblp]
- Vasco Brattka (Universität der Bundeswehr - München, DE) [dblp]
- Karin Cvetko-Vah (University of Ljubljana, SI) [dblp]
- Matthew de Brecht (NICT - Osaka, JP) [dblp]
- Hannes Diener (Universität Siegen, DE) [dblp]
- Willem L. Fouché (UNISA - Pretoria, ZA) [dblp]
- Mai Gehrke (University of Paris VII, FR) [dblp]
- Serge Grigorieff (University of Paris VII, FR) [dblp]
- Georges Hansoul (University of Liège, BE) [dblp]
- Reinhold Heckmann (AbsInt - Saarbrücken, DE) [dblp]
- Peter Hertling (Universität der Bundeswehr - München, DE) [dblp]
- Achim Jung (University of Birmingham, GB) [dblp]
- Klaus Keimel (TU Darmstadt, DE) [dblp]
- Andreas Krebs (Universität Tübingen, DE) [dblp]
- Ganna Kudryavtseva (University of Ljubljana, SI) [dblp]
- Hans-Peter Albert Künzi (University of Cape Town, ZA) [dblp]
- Rutger Kuyper (Radboud University Nijmegen, NL) [dblp]
- Jimmie D. Lawson (Louisiana State University - Baton Rouge, US) [dblp]
- Yoshihiro Maruyama (University of Oxford, GB) [dblp]
- Paul-Andre Mellies (University Paris-Diderot, FR) [dblp]
- Luca Motto Ros (Universität Freiburg, DE) [dblp]
- Alessandra Palmigiano (University of Amsterdam, NL) [dblp]
- Arno Pauly (University of Cambridge, GB) [dblp]
- Jean-Eric Pin (University of Paris VII, FR) [dblp]
- Davide Rinaldi (LMU München, DE) [dblp]
- Giuseppe Rosolini (University of Genova, IT) [dblp]
- Antonino Salibra (University of Venezia, IT) [dblp]
- Matthias Schröder (Universität Wien, AT) [dblp]
- Peter M. Schuster (University of Leeds, GB) [dblp]
- Helmut Schwichtenberg (LMU München, DE) [dblp]
- Victor Selivanov (A. P. Ershov Institute - Novosibirsk, RU) [dblp]
- Dieter Spreen (Universität Siegen, DE) [dblp]
- Paul Taylor (Birmingham, GB) [dblp]
- Sebastiaan A. Terwijn (Radboud University Nijmegen, NL) [dblp]
- Sam van Gool (Radboud University Nijmegen, NL) [dblp]
- Lorijn van Rooijen (University of Bordeaux, FR) [dblp]
- Klaus Weihrauch (FernUniversität in Hagen, DE) [dblp]
- Pascal Weil (University of Bordeaux, FR) [dblp]
- Marc Zeitoun (University of Bordeaux, FR) [dblp]
Related Seminars
- Dagstuhl Seminar 15441: Duality in Computer Science (2015-10-25 - 2015-10-30) (Details)
Classification
- data structures / algorithms / complexity
- semantics / formal methods
- verification / logic
Keywords
- Stone-Priestley duality
- point free topology
- infinite computations
- exact real number computation
- computability in analysis
- hierarchies
- reducibility
- topological complexity
- domain theory
- semantics
- recognizability
- profinite topology