FCT2017

Quicksort, proposed by Hoare in 1961, is a venerable sorting algorithm - it has been thoroughly analyzed, it is taught in basic algorithms classes, and it is routinely used in practice. Can there be anything new about Quicksort today? Dual-pivot quicksort refers to variants of classical quicksort where in the partitioning step two pivots are used to split the input into three segments. Algorithms of this type had been studied by Sedgewick (1975) and by Hennequin (1991), with no further consequences. They received new attention starting from 2009, when a dual-pivot algorithm due to Yaroslavskiy, Bentley, and Bloch replaced the well-engineered quicksort algorithm in Oracle's Java 7 runtime library. An analysis of a variant of this algorithm by Nebel and Wild from 2012, where the two pivots are chosen randomly, showed there are about \(1.9n \ln n\) comparisons on average for \(n\) input numbers. (Other works ensued. Standard quicksort has \(2n \ln n\) expected comparisons. It should be noted that on modern computers parameters other than the comparison count will determine the running time.) In the center of the analysis is the partitioning procedure. Given two pivots, it splits the input keys in "small" (smaller than small pivot), "medium" (between the two pivots), "large" (larger than large pivot). We identify a partitioning strategy with the minimum average number of key comparisons in the case where the pivots are chosen from a random sample. The strategy keeps count of how many large and small elements were seen before and prefers the corresponding pivot. The comparison count is closely related to a "random walk" on the integers which keeps track of the difference of large and small elements seen so far. An alternative way of understanding what is going on is a Pólya urn with three colors. For the fine analysis it is essential to understand the expected number of times this random walk hits zero. The expected number of comparisons can be determined exactly and as a formula up to lower terms: It is \(1.8n \ln n + 2.38..n + 1.675 \ln n + O(1)\). Extensions to larger numbers of pivots will be discussed.

Mathematics was developed as a strong research instrument with fully verifiable argumentations. We call any consistent and sufficiently powerful formal theory that enables to algorithmically verify for any given text whether it is a proof or not algorithmically verifiable mathematics (AV-mathematics for short). We say that a decision problem $L \subseteq \Sigma^\ast$ is almost everywhere solvable if for all but finitely many inputs $x \in \Sigma^\ast$ one can prove either “$x \in L$” or “$x \not\in L$” in AV-mathematics.

First, we formalize Rice's theorem on unprovability, claiming that each nontrivial semantic problem about programs is not almost everywhere solvable in AV-mathematics. Using this, we show that there are infinitely many algorithms (programs that are provably algorithms) for which there do not exist proofs that they work in polynomial time or that they do not work in polynomial time. We can prove the same also for linear time or any time-constructible function.

Note that, if $\textsf{P}\ne \textsf{NP}$ is provable in AV-mathematics, then for each algorithm $A$ it is provable that “$A$ does not solve SATISFIABILITY or $A$ does not work in polynomial time”. Interestingly, there exist algorithms for which it is neither provable that they do not work in polynomial time, nor that they do not solve SATISFIABILITY. Moreover, there is an algorithm solving SATISFIABILITY for which one cannot prove in AV-mathematics that it does not work in polynomial time.

Furthermore, we show that $\textsf{P}=\textsf{NP}$ implies the existence of algorithms $X$ for which the true claim “$X$ solves SATISFIABILITY in polynomial time” is not provable in AV-mathematics. Analogously, if the multiplication of two decimal numbers is solvable in linear time, one cannot decide in AV-mathematics for infinitely many algorithms $X$ whether “$X$ solves multiplication in linear time”.

Based on joint work with Félix Baschenis, Olivier Gauwin and Gabriele Puppis.

Jean-Éric Pin is currently director of research appointed by the CNRS (Centre National de la Recherche Scientifique) and working at IRIF (Institut de Recherche en Informatique Fondamentale), a Joint Research Unit supported by CNRS and University Paris Diderot. He is a leading scientist in the algebraic theory of automata and languages in connection with logic, topology, and combinatorics, but his research has also been influential in other areas. He wrote a number of articles in semigroup theory, most of them motivated by problems issued from automata theory. He is the author of two reference books in automata theory: Varieties of Formal Languages and the monograph Infinite Words, co-authored with D. Perrin. He is also a fellow of the EATCS.

Zoltán Ésik published 2 books as an author, 32 books as editor and over 250 scientific papers in journals, chapters and conferences. It was of course impossible to survey such an impressive list of results and in this lecture, I will only focus on a very small portion of Zoltán's scientific work. The first topic will be a result from 1998, obtained by Zoltán jointly with Imre Simon, in which he solved an old conjecture about the shuffle operation. The second topic will be his algebraic study of various fragments of logic on words. Finally I will briefly describe the results of a new article by Zoltán, Jorge Almeida and myself on commutative languages.