The next meeting of the MAX team seminar will be on Tuesday, May 24. The meeting is dedicated to the Computer Mathematics research group. We will welcome Marc Mezzarobba (LIX) for his talk on Asymptotic Expansions with Error Bounds for Solutions of Linear Recurrences.
Abstract: When a sequence (u(n)) of real or complex numbers satisfies a linear recurrence relation with polynomial coefficients, it is usually routine to determine its asymptotic behavior for large n. Well-known algorithms and readily available implementations are often able, given a recurrence satisfied by (u(n)) and some additional information on the particular solution, to compute an explicit asymptotic expansion
u(n) = a0(n) + a1(n) + · · · + ar − 1(n) + O(b(n)), n → ∞
up to any desired order r. If, however, one wishes to prove an inequality satisfied by u(n) for all n, a big-Oh error term is not sufficient and an explicit error bound on the difference between the sequence and its asymptotic approximation is required. In this talk, I will present a practical algorithm for computing such bounds, under the assumption that the generating series of the sequence (u(n)) is solution of a differential equation with regular (Fuchsian) dominant singularities. I will show how it can be used to verify the positivity of a certain explicit sequence, which T. Yu and J. Chen recently proved to imply uniqueness of the surface of genus one in ℝ³ of minimal bending energy when the isoperimetric ratio is prescribed. Based on joint work with Ruiwen Dong and Stephen Melczer
La prochaine séance du séminaire de combinatoire du plateau de Saclay aura lieu ce lundi 23 mai à 15h en salle Philippe Flajolet du LIX. Nous aurons le plaisir d’écouter Anna Vanden Wyngaerd (IRIF, Université Paris Cité) nous parler de « From Delta to Theta conjectures: a survey ».
Résumé : In 2015, Haglund Remmel and Wilson proposed two conjectural combinatorial interpretations of a certain symmetric function involving a certain Delta operator, which acts diagonally on the MacDonald polynomials. These formulas generalise the shuffle conjecture (Haglund, Haimal, Loehr, Remmel, Ulyanov 2002), now theorem (Carlsson, Mellit 2018). In this talk, we will first discuss some of the motivation and history of these famous problems. Then, we will talk about our new symmetric function operator Theta and their role in the proof of one of the Delta conjectures and the formulation of a possible unified Delta conjecture. (Based on joint works with Michele D’Adderio, Alessandro Iraci, Yvan Le Borgne, Marino Romero)
Le programme du séminaire est disponible sur la page https://galac.lri.fr/fr/pages/combi-seminar.html
For the next Proofs & Algorithms seminar on Monday 23rd of May at 14h00, we, at PARTOUT, are very happy to welcome Willem Heijltjes from University of Bath.
Abstract: I will present the Functional Machine Calculus (FMC), a simple model of higher-order computation with “reader/writer” effects: state, input/output, probabilities, and non-determinism. The main result is to extend two fundamental properties of the lambda-calculus to these effects: reduction in the FMC is confluent, and a system of simple types confers strong normalization.
The premise is to view the lambda-calculus as an instruction language for a simple stack machine, in the standard way of the Krivine machine, where application is “push” and abstraction is “pop”. The FMC then consists of two independent generalizations, that are natural from the perspective of the machine.
The first generalization, “locations”, is to allow multiple stacks (or streams) on the machine, each indicated by a “location”. Application and abstraction are parameterized in these locations, to give push and pop actions on the relevant stack. Then input streams, output streams, and memory cells are straightforwardly modelled by distinct locations.
The second generalization, “sequencing”, introduces sequential composition, following the perspective of terms as sequences of machine instructions, as well as a unit, the empty sequence. This is known from Hasegawa’s kappa- calculus and from concatenative programming languages, and enables the encoding of reduction strategies, including call-by-value lambda-calculus, and for the given effects, Moggi’s metalanguage, Levy’s call-by-push-value, and Haskell Arrows.
Reduction in the FMC is confluent, which is possible because encoded effect operations reduce algebraically, rather than operationally. It can be simply typed to confer strong normalization, and because effectful operations are fully typed, it has a semantics as a Cartesian closed category. Unlike in the monadic setting, reader/writer effects in the FMC combine seemlessly.
The list of next seminars can be found at: https://www.lix.polytechnique.fr/proofs-algorithms/seminar/
The calendar of seminars can be found at: https://www.lix.polytechnique.fr/proofs-algorithms/seminar/calendar.ics
For a new seminar of the proofs and algorithms pole of LIX, we are happy to welcome Joël Ouaknine (Max Planck Institute for Software Systems, Saarbrücken, Germany), invited by the AlCo team.
Abstract: The Skolem Problem asks how to determine algorithmically whether a given linear recurrence sequence (such as the Fibonacci numbers) has a zero. It is a central question in dynamical systems and number theory, and has many connections to other branches of mathematics and computer science. Unfortunately, its decidability has been open for nearly a century! In this talk, I will present a survey of what is known on the Skolem Problem and related questions, including recent and ongoing developments.
Modern applications, such as social networking systems and e-commerce platforms are centered around using large-scale databases for storing and retrieving data. In the presence of concurrent accesses, databases trade off isolation for performance. The weaker the isolation level, the more behaviors a database is allowed to exhibit and it is up to the developer to ensure that their application can tolerate those behaviors. However, these weak behaviors only occur rarely in practice and outside the control of the application, making it difficult for developers to check the robustness of their code against weak isolation levels.
In this talk I will present a framework for formalizing database isolation levels and algorithmic methods for checking whether a database conforms to a certain isolation level or that an application satisfies its intended specification when run under a given isolation level.