17.01.16 - 22.01.16, Seminar 16031

Well Quasi-Orders in Computer Science

Diese Seminarbeschreibung wurde vor dem Seminar auf unseren Webseiten veröffentlicht und bei der Einladung zum Seminar verwendet.


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.)