Profil de Devevey

Développement :
Théorie des matroïdes et une application
Remarque :
La preuve est légèrement modifiée par rapport à celle du livre pour utiliser un invariant de boucle, ce qui permet le recasage dans la leçon 927 et rend la preuve plus formelle.
Référence :
- A Guide to Algorithm Design: Paradigms, Methods, and Complexity Analysis, Anne Benoît, Yves Robert, Frédéric Vivien
Fichier :
- ThMatroïdes.pdf

Développement :
Théorème de Rice
Remarque :
On prouve le théorème de Rice, et on rajoute à la fin un contre-exemple pour bien faire sentir ce que le théorème dit réellement : les propriétés doivent concerner le langage lui-même, pas la machine de Turing ni la manière dont elle exécute les calculs.
Recasable avec 4* dans la leçon 913.
Référence :
- Langages formels, Calculabilité et Complexité, Carton
Fichier :
- ThmRice.pdf

Développement :
Complexité moyenne du tri rapide
Remarque :
L'algorithme présenté dans le Beauquier n'est pas le tri rapide de base, c'est pour ça qu'on se base sur celui présenté dans le Cormen et qu'on adapte la preuve du Beauquier pour calculer la complexité en moyenne du tri rapide.
Références :
- Eléments d'algorithmique, Beauquier, Berstel et Chrétienne
- Introduction à l'algorithmique, Thomas H. Cormen, Charles E. Leiserson, Clifford Stein, Ronald Rivest
Fichier :
- TriRapide.pdf

Développement :
Tri par tas
Référence :
- Introduction à l'algorithmique, Thomas H. Cormen, Charles E. Leiserson, Clifford Stein, Ronald Rivest
Fichier :
- TriParTasv2.pdf

Développement :
Un algorithme de programmation dynamique pour les polynômes d'interpolation de Lagrange
Remarque :
La preuve de la relation de récurrence sert aussi de preuve de correction de l'algorithme, ce qui justifie le recasage dans la leçon 927, car les preuves de correction des algorithmes dynamiques sont particulières : elles interviennent avant même l'écriture de l'algorithme, car cette preuve revient à prouver la relation de récurrence sur laquelle repose l'algorithme.
Référence :
- Modélisation à l'oral de l'agrégation , Dumas
Fichier :
- Lagrange.pdf

Développement :
Hachage parfait
Remarque :
On peut admettre la démonstration du théorème 2 si trop long.
Se recase (mal) dans la 932.
Référence :
- Introduction à l'algorithmique, Thomas H. Cormen, Charles E. Leiserson, Clifford Stein, Ronald Rivest
Fichier :
- HachageParfait.pdf

Développement :
Décidabilité de l'arithmétique de Presburger
Remarque :
La récurrence est mal posée dans le Carton, il faut l'expliciter un peu mieux.
Les définitions sont mieux posées dans le DNR.
Références :
- Langages formels, Calculabilité et Complexité, Carton
- Introduction à la logique, René David, Karim Nour, Christophe Raffalli (DNR)
Fichier :
- Presburgerv2.pdf

Développement :
Les fonctions récursives sont lambda-définissables
Remarque :
On prouve uniquement que les fonctions primitives récursives sont lamda-définissables.
Il faut faire attention aux livres, une partie de la preuve de chaque livre est fausse/trop compliquée, et il faut mélanger les deux preuves pour que ça marche. Aussi, il y a pas mal de typos
Références :
- Classical Recursion Theory, Piergiorgio Odifreddi
- Logique et fondements de l'informatique, Rougemont, Lassaigne
Fichier :
- RecPrimenLambdaCalc.pdf

Développement :
Algorithme d'Earley
Remarque :
Le plus simple est d'expliquer l'algorithme au fur et à mesure qu'on l'écrit, car il peut être assez difficile à comprendre au premier abord.
Référence :
- Le Langage des machines, Floyd, Beigel
Fichier :
- Earleyv2.pdf

Développement :
Confluence du lambda-Calcul
Remarque :
Trop court ?
Référence :
- The Lambda Calculus. Its Syntax and Semantics, Henk Barendregt
Fichier :
- Confluence.pdf

Développement :
Théorie des ordres denses
Remarque :
Peut se placer dans les leçons 924 et 918 aussi
Référence :
- Introduction à la logique, René David, Karim Nour, Christophe Raffalli (DNR)
Fichier :
- Ordre dense.pdf