Utilisateur : Devevey
Développements
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érences :
A Guide to Algorithm Design: Paradigms, Methods, and Complexity Analysis - Anne Benoît, Yves Robert, Frédéric Vivien
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érences :
Langages formels, Calculabilité et Complexité - Carton
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
Références :
Introduction à l'algorithmique - Thomas H. Cormen, Charles E. Leiserson, Clifford Stein, Ronald Rivest
Développement : Un algorithme de programmation dynamique pour les polynômes d'interpolation de Lagrange
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érences :
Modélisation à l'oral de l'agrégation - Dumas
On peut admettre la démonstration du théorème 2 si trop long.
Se recase (mal) dans la 932.
Références :
Introduction à l'algorithmique - Thomas H. Cormen, Charles E. Leiserson, Clifford Stein, Ronald Rivest
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)
Recasable dans la 916.
Références :
Langages formels, Calculabilité et Complexité - Carton
(p.159 pour la version française du livre)
Références :
Compilers - Aho, Ullman, Lam, Sethi
Références :
Introduction à l'algorithmique - Thomas H. Cormen, Charles E. Leiserson, Clifford Stein, Ronald Rivest
Références :
Introduction à l'algorithmique - Thomas H. Cormen, Charles E. Leiserson, Clifford Stein, Ronald Rivest
Computational complexity - Papadimitriou
Références :
Introduction à l'algorithmique - Thomas H. Cormen, Charles E. Leiserson, Clifford Stein, Ronald Rivest
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
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érences :
Le Langage des machines - Floyd, Beigel
Références :
Mathématiques de l'informatique - Dehornoy
Trop court ?
Références :
The Lambda Calculus. Its Syntax and Semantics - Henk Barendregt
Peut se placer dans les leçons 924 et 918 aussi
Références :
Introduction à la logique - René David, Karim Nour, Christophe Raffalli (DNR)