Dagstuhl Seminar 16031
Well Quasi-Orders in Computer Science
( Jan 17 – Jan 22, 2016 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/16031
Organizers
- Jean Goubault-Larrecq (ENS - Cachan, FR)
- Monika Seisenberger (Swansea University, GB)
- Victor Selivanov (A. P. Ershov Institute - Novosibirsk, RU)
- Andreas Weiermann (Ghent University, BE)
Contact
- Susanne Bach-Bernhard (for administrative matters)
Impacts
- Noetherian Quasi-Polish Spaces : article - de Brecht, Matthew; Pauly, Arno - 2016. - 11 pp..
- Well-Quasi Orders in Computation, Logic, Language and Reasoning : A Unifying Concept of Proof Theory, Automata Theory, Formal Languages and Descriptive Set Theory - Schuster, Peter M.; Seisenberger, Monika; Weiermann, Andreas - Berlin : Springer, 2020. - X, 391 S. - (Trends in logic ; 53). ISBN: 978-3-030-30228-3 / 3-030-30228-8.
Schedule
Computer science, being a huge and complex conglomerate of theoretical disciplines, technological advances and social methodologies, strongly needs unifying concepts and techniques. In particular, relevant mathematical concepts and theories are required. The notion of well quasi-order (wqo) was discovered independently by several mathematicians in the 1950s and quickly evolved to a very deep theory with many applications and remarkable theorems. Soon afterwards, well and better quasi-orders started to appear more and more frequently in different parts of theoretical computer science such as automata theory, term rewriting, verification of infinite-state systems, computation with infinite data, and others. Accordingly, more and more researchers from different fields of computer science use notions and methods of wqo theory. It seems to be the right time to have a broad discussion on how to speed up this process and to better understand the role of well quasi-orders in theoretical computer science. During this seminar, we hope to intensify the knowledge transfer between mathematicians and computer scientists, between the experienced and young researchers, and between the different communities within computer science in order to foster research in this domain.
Logic and proofs. Well quasi-orders, originally introduced in algebra, soon played an important role in proof theory: Higman's Lemma and Kruskal's Theorem are examples of theorems that are not provable in Peano Arithmetic. Determining the proof-theoretic strength of these (types of) theorems, as well as classifying them in terms of Reverse Mathematics, constituted an important endeavor. The concept of a wqo naturally extends to the more complex concept of a better quasi-order (bqo) which deals with infinite structures. Again, the proof theoretic strength of theorems on bqos has been/must be investigated, and the theorems themselves can be used for more sophisticated termination problems. One of the open challenges is the strength of Fraïssé's order type conjecture. Non-constructive proofs of this type of theorems (on wqos) include proofs using the so-called minimal-bad-sequence argument. Investigating its strength and also its computational content, via Friedman's A-translation or Gödel's Dialectica Interpretation, has led to interesting results. To optimize these techniques so that realistic programs can be extracted from these classical proofs, using bar recursion, update recursion, selection functions, etc., is still ongoing work.
Automata and formal languages. Well quasi-orders have many-fold connections to automata theory and formal language theory. In particular, there are nice characterizations of regular and context-free languages in terms of well quasi-orders, some lower levels of the concatenation hierarchies admit characterizations in terms of the subword relation and its relatives. On the topological level, it is known that the Wadge reducibility (or the reducibility by functions on omega-words computable by finite automata) is a well quasi-order on the class of omega-regular finite partitions of the Cantor space. Using some variants of Kruskal’s Theorem, Selivanov was able to completely characterize the corresponding partial order, obtaining thus a complete extension of the Wagner hierarchy from sets of finite partitions. The mentioned relationships between wqo theory and formal languages are currently not well systematized, and many natural questions remain open. Further insights in this topic seem quite interesting for the development of this field.
Topological issues. An important task in computing with infinite data is to distinguish between computable and non-computable functions and, in the last case, to measure their degree of non-computability. Usually, the cause of non-computability is a lack of continuity, so that a somewhat easier and more fundamental task consists in understanding the degree of discontinuity of functions. This is achieved by defining appropriate hierarchies and reducibility relations. In classical descriptive set theory, along with the well-known hierarchies, Wadge introduced and studied an important reducibility relation on subsets of the Baire space. As shown by van Engelen et al., von Stein, Weihrauch and Hertling, this reducibility of subsets of topological spaces can be generalized in various ways to reducibilities of functions on a topological space. The degrees of discontinuity of several important computational problems have been classified this way. The transfer from sets to functions requires some notions and results of wqo theory in order to define and study the hierarchies and reducibilities that arise in this way. Many problems of this direction are still open and we hope to make steps toward solving some of them during this seminar.
Verification and termination problems. Wqos made their debut in computer science when Don Knuth suggested that Kruskal's Theorem might find an application in proving termination of programs. This was achieved a few years later by Nachum Dershowitz, and the advent of recursive path orderings. Today, it is probably the area of software verification instead that provides the largest number of applications of wqos in computer science. The decidability of coverability for well-structured transition systems (WSTS) crucially relies on the very properties of well quasi-orders. WSTSs include Petri nets and their extensions, and more generally affine nets. They also include lossy channel systems, weak memory models, various process algebras, data nets, certain abstractions of timed Petri nets, and certain parametrized transition systems. The verification of new classes of transition systems prompts for new classes of wqos. In addition to this, understanding the computational complexity of the resulting verification algorithms requires a finer analysis of minimal-bad-sequence arguments, and their relation to hierarchies of recursive functions (Hardy, fast growing, etc.)
Computer Science, being a huge and complex conglomerate of theoretical disciplines, technological advances and social methodologies, strongly needs unifying concepts and techniques. In particular, relevant mathematical concepts and theories are required. The notion of well quasi-order (or almost-full relation, if transitivity is not required -- a notion preferred by some authors) was discovered independently by several mathematicians in the 1950-s and quickly evolved to a deep theory with many applications and remarkable results. Soon afterwards, well and better quasi-orders started to appear more and more frequently in different parts of theoretical computer science such as automata theory, term rewriting, verification of infinite-state systems, computations with infinite data, and others. Accordingly, an increasing number of researchers from different fields of computer science use notions and methods of Wqo-Theory. Therefore, it seemed to be the right time to have a broad discussion on how to speedup this process and to better understand the role of well quasi-orders in theoretical computer science.
Topics of the seminar
During this seminar we concentrated on the following four topics:
- Logic and proofs
- Automata and formal languages
- Topological issues
- Verification and termination problems
Well quasi-orders, originally introduced in algebra, soon played an important role in proof theory: Higman's Lemma and Kruskal's Theorem are examples of theorems that are not provable in Peano Arithmetic. Determining the proof-theoretic strength of these (types of) theorems, as well as classifying them in terms of Reverse Mathematics, constituted an important endeavor. The concept of a WQO naturally extends to the more complex concept of a better quasi-order (BQO) which deals with infinite structures. Again, the proof theoretic strength of theorems on BQOs has been/must be investigated, and the theorems themselves can be used for more sophisticated termination problems. One of the open challenges is the strength of Fraïssé's order type conjecture. Non-constructive proofs of this type of theorems (on WQOs) include proofs using the so-called minimal-bad-sequence argument. Investigating their strengths and also their computational content, via Friedman's A-translation or Gödel's Dialectica Interpretation, has led to interesting results. To optimize these techniques so that realistic programs can be extracted from these classical proofs, using bar recursion, update recursion, selection functions, etc., is ongoing work.
Automata and formal languages
Well quasi-orders have many-fold connections to automata theory and formal language theory. In particular, there are nice characterizations of regular and context-free languages in terms of well quasi-orders, some lower levels of the concatenation hierarchies admit characterizations in terms of the subword relation and its relatives. Such characterizations sometimes help in getting new results, say on decidability of some levels of the concatenation hierarchy (Glasser, Schmitz, Selivanov). The same applies to omega-languages, though in this case the relationships are less investigated.
On the topological level, it is known that Wadge reducibility (or reducibility by functions on omega-words computable by finite automata) are well quasi-orders on the class of omega-regular finite partitions of the Cantor space. Using some variants of the Kruskal theorem on quasi-orderings of labeled trees, Selivanov was able to completely characterize the corresponding partial order, obtaining thus a complete extension of the Wagner hierarchy from sets of finite partitions.
The mentioned relationships between Wqo-theory and formal languages are currently not well systematized, and many natural questions remain open. Further insights in this topic is essential for the development of this field.
Topological issues
An important task in computing with infinite data is to distinguish between computable and non-computable functions and, in the latter case, to measure the degree of non-computability. Usually, functions are non-computable since they are not even continuous, hence a somewhat easier and more principal task is in fact to understand the degree of discontinuity of functions. This is achieved by defining appropriate hierarchies and reducibility relations.
In classical descriptive set theory, along with the well-known hierarchies, Wadge introduced and studied an important reducibility relation on subsets of the Baire space. As shown by van Engelen et al, von Stein, Weihrauch and Hertling, this reducibility of subsets of topological spaces can be generalized in various ways to a reducibility of functions on a topological space. In this way, the degrees of discontinuity of several important computational problems were classified. The transfer from sets to functions requires some notions and results of Wqo-theory in order to define and study hierarchies and reducibilities arising in this way.
Verification and termination problems
WQOs made their debut in computer science when Don Knuth suggested that Kruskal's Theorem might find an application in proving termination of programs. This was achieved a few years later by Nachum Dershowitz and the advent of recursive path orderings. Today, it is probably the area of software verification that provides the largest number of applications of WQOs in computer science. The decidability of coverability for well-structured transition systems (WSTS) crucially relies on the very properties of well quasi-orders. WSTS include Petri nets and their extensions, and more generally affine nets. They also include lossy channel systems, weak memory models, various process algebras, data nets, certain abstractions of timed Petri nets, and certain parametrized transition systems. The verification of new classes of transition systems prompts for new classes of WQOs. In addition to this, understanding the computational complexity of the resulting verification algorithms requires a finer analysis of minimal-bad-sequence arguments and their relation to hierarchies of recursive functions (Hardy, fast growing, etc.)
Report
One of the central purposes of the proposed seminar was to bring together researchers from Wqo-theory and those from the related areas of computer science who actively apply notions and techniques of Wqo-theory. We wanted thus to encourage more interaction between the different communities, leading finally to a significant development of the mentioned fields. Overall, the seminar was very stimulating. The initial concerns that the four topics of the seminar might remain separate was quickly brushed off, as verification talks relied on concepts from logic (e.g., maximal order types), topological issues resonated with verification (e.g., Noetherian spaces), and all participated actively in vivid sessions of setting up and discussing open questions.
To facilitate the interaction, each of the four topics of the seminar started with one or two introductory talks. In the topic Logic and Proofs, Diana Schmidt gave the first talk of the seminar "Ordinal notations, the maximal ordertypes of Kruskal's Theorem and a tale of two cultures", where she summarized work that started 40 years ago, but is still of interest to date. Andreas Weiermann complemented the introduction by addressing open problems concerning the so-called phase transitions (a topic which was then further elaborated by Lev Gordeev) in proof theory and the calculation of maximal ordertypes. A number of contributions focused on the formalization of Kruskal type theorems possibly including the extraction of computational content, leading to various practical exchange sessions in the evenings (see also next paragraph). The topic was continued on Tuesday by Alberto Marcone who gave a survey on WQOs and BQOs in Reverse Mathematics, followed various talks and discussions on open questions around better quasi-orderings. Another highlight of the second day were two contributions on the Graph Minor Theorem: Chun-Hung Liu reported on his recent proof of a conjecture by Robertson involving topological minors, and Michael Rathjen looked at the Graph Minor Theorem to determine its proof theoretic strength. Of the further contributions we want to specifically mention Julia Knight who made the connection between WQOs and Hahn-Fields.
The topic Verification was addressed by Philippe Schnoebelen in "Well quasi-orderings and program verification" on Monday afternoon, with a gentle introduction to the field of well-structured transition systems (WSTS). Although this was an introductory talk, he took the opportunity to introduce the class of priority channel systems as an example, whose decidability results rely on a form of well quasi-ordering with gap embedding. Such orderings require very high maximal order types, and led to the open question of giving a formula, or even lower and upper bounds, for those maximal order types. This has direct consequences on the complexity of verification. Alain Finkel proceeded to give another talk on the verification of WSTS, "Decidability results on infinitely branching WSTS, which completed the introduction given by Philippe Schnoebelen, and quickly proceeded to explore the challenges of verifying WSTS that are infinitely branching. He explained that deciding termination, coverability, and boundedness could be done through computations that involve a so-called completion of the WSTS, generalizing the well-known Karp-Miller construction for Petri nets -- some of these problems turn out to be decidable, some others not. Crucially, in the decidable cases, even if the WSTS is infinitely branching, its completion is always finitely branching. Maurice Pouzet made the observation that the key result used there, that every downwards closed set of a WQO is a union of finitely many ideals, is due to Kabil and himself in 1992, and that this was still true for the more general class of FAC (finite antichain) orders. FAC orders were the subject of the next presentation, by Mirna Dzamonja, entitled "On the width of FAC orders". She started from the fact that, while height, length and width of well quasi-orders are important notions, width generalizes to all FAC orders, and that we can compute the width of FAC orders defined from FAC constituents. One consequence is that for every ordinal alpha, there is a WQO of width exactly alpha. The main open question is to be able to compute the width of a finite product of FAC orders. The width of the product of two ordinals is known, but is given by a complex formula. Mirna Dzamonja gave some new results on the question, in particular for some three-way products.
The final two Monday contributions were concerned with very different questions, namely mechanized proofs of Higman's Lemma, one of the core results in well quasi-order theory. Christian Sternagel described a proof of Higman's Lemma by so-called open induction, a concept akin to Scott induction in domain theory, as one of the participants noticed. The proof is a considerably simplified version of a proof of the same kind given by Alfons Geser. Open induction was again the subject of Thomas Powell's talk "Open induction and the Dialectica interpretation" on Friday morning. Helmut Schwichtenberg concluded the afternoon of Monday, just before a rump session dedicated to open questions. He gave a talk "on the computational content of Higman's Lemma", stressing that different constructive proofs of the same theorem yield programs -- by the Curry-Howard correspondence -- that behave differently in practice. This resonated with the last morning talk of the same day, "An axiom-free Coq proof of Kruskal's Theorem", by Dominique Larchey-Wendling, on a recent constructive proof of the much more complex Kruskal theorem, inspired from and generalizing a proof due to Wim Veldman.
Other verification-oriented talks were given by Mizuhito Ogawa on Thursday morning, "Notes on regularity and WQOs, and well-structured pushdown systems", which gave new decidability results for coverability on extended forms of transition systems, through the use of so-called P-automata. In the evening, Roland Meyer explained how one can encode certain depth-bounded, breadth-bounded, and name-bounded processes of the pi-calculus into well-structured transition systems, and obtain decidability results through acceleration techniques, akin (again) to the Karp-Miller technique already mentioned above. Sylvain Schmitz provided us with a glimpse of the new complexity classes that had to be invented in recent years to characterize the complexity of the standard decidable problems for classical WSTS. These are classes of very high complexity: Ackermannian, hyper-Ackermannian, and others. This was a talk that unified the concerns of verification with the logical view, based on maximal ordertypes, and introduced by Andreas Weiermann and others.This provided a natural link with the last talk in the verification strand, "Trace universality for VASS", given by Simon Halfon, who explained what the problem was, that it relied on the fact that all bad sequences of finite subsets of d-tuples of natural numbers are finite, that it is Ackermann-complete for d=1, and he then proceeded to explain what was known in the cases dgeq 2, on which he is working.
The topic Topological Issues was introduced by Victor Selivanov in "Well quasi-orders and Descriptive Set Theory" on Tuesday afternoon, and by Jean Goubault-Larrecq in "A Gentle Introduction to Noetherian Spaces" on Wednesday morning. Selivanov gave a short survey of the relationships between Wqo-Theory and Descriptive Set Theory, as well as a discussion of several interesting open questions in this field. Even the definition and basics of BQOs are related to Descriptive Set Theory, as was demonstrated in the talks by Alberto Marcone and Yann Pequignot on Tuesday. Other connections were given by Raphael Carroy on Tuesday (discussing some WQOs on continuous functions), by Oleg Kudinov on Wednesday (discussing joint results with Selivanov on definability issues for some popular WQOs) and by Peter Hertling on Friday (giving an overview of results about Weihrauch reducibilities). Goubault-Larrecq introduced an important topological extension of the notion of WQO which motivates several interesting open questions. Some of these questions were addressed in the subsequent Wednesday talks by Matthew de Brecht and Arno Pauly. Both mentioned directions in the topic Topological Issues look very prospective and deserve additional attention.
The topic Automata and Formal Languages was surveyed by Mizuhito Ogawa on Thursday morning who summarized several interesting facts relating WQOs to popular classes of languages and omega-languages on words and trees (cf. also the topic Verification). Automata and Formal Languages were also addressed on Tuesday by Selivanov who related WQOs to his extension of the Wagner hierarchy from the case of sets to the case of k-partitions. Another related talk was given on Thursday by Willem Fouché who discussed some applications of Ramsey theory to unavoidable regularities in words. Although Automata and Formal Languages turned out slightly underrepresented at this seminar, the relationship between Wqo-Theory and Formal Languages seems quite important and deserves further investigation which we hope to include in a future seminar.
Creative Commons BY 3.0 Unported license
Jean Goubault-Larrecq and Monika Seisenberger and Victor Selivanov and Andreas Weiermann
- Lev D. Beklemishev (Steklov Institute - Moscow, RU) [dblp]
- Andreas R. Blass (University of Michigan - Ann Arbor, US) [dblp]
- Raphael Carroy (University of Torino, IT) [dblp]
- Raphael Chane-Yack-Fa (University of Sherbrooke, CA) [dblp]
- Matthew de Brecht (NICT - Osaka, JP) [dblp]
- Dick De Jongh (University of Amsterdam, NL) [dblp]
- Mirna Dzamonja (University of East Anglia - Norwich, GB) [dblp]
- Alain Finkel (ENS - Cachan, FR) [dblp]
- Thomas E. Forster (University of Cambridge, GB) [dblp]
- Willem L. Fouché (UNISA - Pretoria, ZA) [dblp]
- Christian Glasser (Universität Würzburg, DE) [dblp]
- Lev Gordeev (Universität Tübingen, DE) [dblp]
- Jean Goubault-Larrecq (ENS - Cachan, FR) [dblp]
- Simon Halfon (ENS - Cachan, FR) [dblp]
- Peter Hertling (Universität der Bundeswehr - München, DE) [dblp]
- Takayuki Kihara (University of California - Berkeley, US) [dblp]
- Julia Knight (University of Notre Dame, US) [dblp]
- Oleg V. Kudinov (Sobolev Institute of Mathematics - Novosibirsk, RU) [dblp]
- Dominique Larchey-Wendling (LORIA - Nancy, FR) [dblp]
- Chun-Hung Liu (Princeton University, US) [dblp]
- Alberto Marcone (University of Udine, IT) [dblp]
- Roland Meyer (TU Kaiserslautern, DE) [dblp]
- Kenji Miyamoto (LMU München, DE) [dblp]
- Mizuhito Ogawa (JAIST - Ishikawa, JP) [dblp]
- Arno Pauly (University of Brussels, BE) [dblp]
- Yann Pequignot (Universität Wien, AT) [dblp]
- Maurice Pouzet (University Claude Bernard - Lyon, FR) [dblp]
- Thomas Powell (Universität Innsbruck, AT) [dblp]
- Michael Rathjen (University of Leeds, GB) [dblp]
- Diana Schmidt (Heilbronn, DE) [dblp]
- Heinz Schmitz (Hochschule Trier, DE) [dblp]
- Sylvain Schmitz (ENS - Cachan, FR) [dblp]
- Philippe Schnoebelen (ENS - Cachan, FR) [dblp]
- Peter M. Schuster (University of Verona, IT) [dblp]
- Helmut Schwichtenberg (LMU München, DE) [dblp]
- Luc Segoufin (INRIA SENS-Cachan, FR) [dblp]
- Monika Seisenberger (Swansea University, GB) [dblp]
- Victor Selivanov (A. P. Ershov Institute - Novosibirsk, RU) [dblp]
- Dieter Spreen (Universität Siegen, DE) [dblp]
- Christian Sternagel (Universität Innsbruck, AT) [dblp]
- Bill Wadge (University of Victoria, CA) [dblp]
- Andreas Weiermann (Ghent University, BE) [dblp]
- Klaus Weihrauch (FernUniversität in Hagen, DE) [dblp]
- Daniel Wessel (University of Trento, IT) [dblp]
Classification
- data structures / algorithms / complexity
- semantics / formal methods
- verification / logic
Keywords
- Well quasi-order
- noetherian space
- better quasi-order
- verification
- termination
- logic
- hierarchy
- reducibility
- topological complexity
- well-structured transition systems
- infinite state machines
