28. Juli – 02. August 2013, Dagstuhl Seminar 13311
Duality in Computer Science
1 / 2 >
Auskunft zu diesem Dagstuhl Seminar erteilt
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)
Creative Commons BY 3.0 Unported license
Mai Gehrke and Jean-Eric Pin and Victor Selivanov and Dieter Spreen
Related Dagstuhl Seminar
- 15441: "Duality in Computer Science" (2015)
- Data Structures / Algorithms / Complexity
- Semantics / Formal Methods
- Verification / Logic
- Stone-Priestley duality
- Point free topology
- Infinite computations
- Exact real number computation
- Computability in analysis
- Topological complexity
- Domain theory
- Profinite topology