Structures de données persistantes

Xavier Leroy

Collège de France, chaire Sciences du logiciel, 2022-2023

Résumé

L'efficacité d'un logiciel dépend beaucoup de la manière dont il organise les données qu'il manipule en structures algorithmiquement efficaces. La plupart des structures de données connues aujourd'hui sont transientes : les mises à jour de la structure s'effectuent par modification en place, rendant inaccessible l'état de la structure avant modification. Au contraire, les structures de données persistantes conservent l'historique complet des données : tout se passe comme si une mise à jour recréait une nouvelle structure, indépendante de la structure précédente ; cela peut se réaliser de manière efficace en temps et en espace mémoire à condition d'utiliser des algorithmes ingénieux. Ces structures de données persistantes efficaces jouent un rôle crucial pour la programmation purement fonctionnelle, où les programmes prennent la forme de définitions mathématiques sur lesquelles on peut raisonner de manière équationnelle. Le cours présentere les principales structures de données persistantes connues aujourd'hui, certaines implémentées de manière purement fonctionnelle et d'autres à l'aide de modifications impératives cachées, et décrit les principes généraux qui guident la conception de ces structures persistantes ainsi que leur analyse de complexité.

Cours

Les enregistrement vidéo sont disponibles sur le site du Collège de France.

1. Rien ne se perd, tout se crée : introduction aux structures de données persistantes.
2. Arbres équilibrés + copie de branches = dictionnaires persistants.
3. Concilier amortissement et persistance : de l'importance de la paresse.
4. Comment rendre persistante une structure impérative ?.
5. Systèmes de numération et types non réguliers.
6. De la dérivation formelle à la navigation dans une structure : contextes, zippers, index.
7. À la recherche du vecteur perdu : limites théoriques et conclusions.

Séminaire

Certains exposés étaient en français, d'autres en anglais. Les enregistrements vidéo et les présentations sont disponibles sur le site du Collège de France.

1. Tobias Nipkow: Verification of Functional Data Structures: Correctness and Complexity.
2. Jean-Christophe Filliâtre: Structures de données semi-persistantes.
3. KC Sivaramakrishnan: Mergeable Replicated Data Types.
4. Arthur Charguéraud: Comment allier persistance et performance.
5. Pierre-Etienne Meunier: Une algèbre de modifications, ou : le contrôle de versions pour tous.