Table of Contents
Aspects Algorithmiques de la Théorie des Beaux préordres / Algorithmic Aspects of WQO Theory (24h, 3 ECTS)Où, quand ? / Where, when?: The course takes place on Thursdays in the morning slot (from 08h45 to 11h45), building Sophie Germain room 1014. Poly / Lecture notes: can be found at this link Algorithmic Aspects of WQO Theory. Prérequis / Prequisites: Elementary notions from logic (ordinals, ..), from complexity, and from recursion theory. Intervenants / Lecturers: Jean GoubaultLarrecq goubault@lsv.fr (LSV, ENS ParisSaclay, Université ParisSaclay) Ph. Schnoebelen, phs@lsv.fr (LSV, ENS ParisSaclay, Université ParisSaclay & CNRS) Responsable / In charge: Jean GoubaultLarrecq goubault@lsv.fr (LSV, ENS ParisSaclay, Université ParisSaclay)
Final Exam (Nov 26th)The final exam is a homework problem to be returned (to J. GoubaultLarrecq and Ph. Schnoebelen) no later than Saturday Dec. 5th at 09h00 AM. Answers in French are accepted. Handwritten answers are accepted but make sure that your scan is highly readable: don't use lined paper and write very carefully. A version with solutions is now available. Motivations & AbstractWellquasiorderings, or WQOs, play a fundamental role in important results in several areas of computer science : formal language theory, rewriting, program verification, algorithmic graph theory, automated deduction, etc. and they are still intensively used nowadays (see e.g. Separability via PiecewiseTestable Languages by GoubaultLarrecq & Schmitz, or OrdinalRecursive Complexity by Schmitz & Schnoebelen). The objective of this course is to teach the basic notions of WQO Theory, motivated and illustrated by algorithmic applications in various areas. Outline of the course1. 17 Sep. 2020 (J. GoubaultLarrecq): Introduction. Definition, a few characterizations of wqos. A library of well quasiordered data types: announcement, and proofs for the simplest cases. All the other cases will be seen in further lectures. Our first wqo: Dickson's Lemma. Application to coverability of WSTS, and of Petri nets in particular. The slides. Exercises for next time: 1.1, 1.2, 1.3, 1.22, 1.13, 1.14. 2. 24 Sep. 2020: Petri nets continued. Dickson's original application. Our second operation on wqos: Higman's Lemma. Applications: lossy channel systems. The slides. Exercises for next time: 1.6, 1.9, 1.29. 3. 01 Oct. 2020: Multisets, finite sets, Rado's counterexample. Van der Meyden's algorithm for satisfiability of disjunctive queries on indefinite databases. A quick word on parameterized complexity. Kruskal's theorem. Application to the termination of rewriting systems. The slides. Exercises for next time: 1.15, 1.5, 1.7, 1.8, 1.10, 1.11, 1.12. (Do not attempt to do the final subquestion of 1.8. Otherwise, look at the 2018 homework assignment and midterm exam, section 2, for inspiration.) 4. 08 Oct. 2020: beware! online session (click here). Beyond trees: graph minors, and the Robertson and Seymour theorem (no proof). Applications to algorithmic graph theory. Beyond wqos: bqos, Noetherian spaces. Ideals and irreducible (downwards)closed subsets. The slides.
The homework assignment for this year (beware: new version 2 of Oct. 9th, 11.27am), to be turned it by October 22nd, 2020, to Jean GoubaultLarrecq or to Philippe Schnoebelen. And here is a possible solution.
5. 15 Oct. 2020 (Ph. Schnoebelen): Lossy channel systems and decidability (Sections 1.9 and 3.1). See also this paper. NB: Students interested in Presburger arithmetic will learn a lot by reading this recent survival guide. 6. 22 Oct. 2020: Lossy counters are hard (Section 3): existence of Büchi runs is undecidable, reachability is Ackermannhard (see slides used Nov 12th.) * take note: 29 Oct. 2020: No class (midterm break). 7. 12 Nov. 2020: Complexity Upper Bounds for WSTS (Section 2): Normed wqos and controlled bad sequences. The Length Function Theorem for polynomials nwqos. (see slides used Nov 12th). NB: The FastGrowing Complexity Hierarchy is described in this recent article.
8. 19 Nov. 2020: Computing with ideals. Revisions before the exam. (see slides used Nov 19th.) * 26 Nov. 2020: Was planned to be the final written exam. Because of recent sanitary restrictions, this will be replaced by some athome exam with dates to be fixed.
EvaluationThe evaluation is in two parts : a homework assignment serving as midterm exam, and a final 2h45hour written exam on 19 Nov, from 9h to 11h45. Documents & computers are not allowed. Here are last year's homework assignment and last year's final exam. Versions with solutions are available on request.
M2 InternshipsHere are listed the internship projects that are in direct linked to the topic of MPRI course 291. M2 students interested in one of these projects should contact the listed adviser.
