Utilisateur : Meven
Développements
Références :
Compilers - Aho, Ullman, Lam, Sethi
Développement : Algorithme de type principal
Il faut pas mal adapter la version du bouquin.
Références :
Lambda Calculus With Types - H. Barendregt
Développement : Tri fusion
Références :
Introduction à l'algorithmique - Thomas H. Cormen, Charles E. Leiserson, Clifford Stein, Ronald Rivest
Développement : Décidabilité de l'arithmétique de Presburger
Références :
Langages formels, Calculabilité et Complexité - Carton
Développement : Théorème de compacité du calcul propositionnel
Le Queffelec pour la première partie, le reste je n'ai pas de source…
Références :
Topologie - Queffelec
Pas trouvé de référence papier pour la preuve par compacité.
Références :
Développement : Complexité amortie des tableaux dynamiques
Références :
Introduction à l'algorithmique - Thomas H. Cormen, Charles E. Leiserson, Clifford Stein, Ronald Rivest
Développement : Algorithme de Bellman-Ford
Références :
Introduction à l'algorithmique - Thomas H. Cormen, Charles E. Leiserson, Clifford Stein, Ronald Rivest
Développement : Preuve de la factorielle en logique de Hoare
Références :
The formal semantics of programming langages - Winskel
Développement : Théorème de Rice
$L_{\in}$ est indécidable, puis théorème de Rice en corollaire
Références :
Langages formels, Calculabilité et Complexité - Carton
Développement : Exemples de réduction polynomiale
3-SAT $\leq_P$ CLIQUE et 3-SAT $\leq_P$ SUBSET-SUM
Références :
Introduction à l'algorithmique - Thomas H. Cormen, Charles E. Leiserson, Clifford Stein, Ronald Rivest
Développement : Théorie des ordres denses
Démonstration par l'élimination des quantificateurs.
Références :
Introduction à la logique - René David, Karim Nour, Christophe Raffalli (DNR)
Développement : Problème du voyageur de commerce euclidien
Avec la 2-approx polynomiale dans le cas euclidien.
Références :
Introduction à l'algorithmique - Thomas H. Cormen, Charles E. Leiserson, Clifford Stein, Ronald Rivest
Développement : Intégrale de Dirichlet et séries de Fourier
Le Faraut calcule l'intégrale du sinus cardinal, mais pas par holomorphie… Et je n'ai pas réussi à trouver de référence pour ça.
Références :
Calcul Intégral - Faraut
Développement : Sémantique dénotationelle de PCF
La référence en ligne http://www.cl.cam.ac.uk/~gw104/dens.pdf est mieux que le Mitchell pour préparer le développement.
Références :
Foundations for Programming Languages - John C. Mitchell
Développement : Méthode de Newton pour les polyômes
Références :
Exercices pour l'agrégation - Analyse 2 - Chambert-Loir
Développement : Sémantique opérationnelle de constructions non séquentielles
Références :
Semantics with Applications: An Appetizer - H. R. Nielson, F. Nielson
Développement : Théorème de Savitch
Références :
Introduction to the theory of computation - Sipser
Langages formels, Calculabilité et Complexité - Carton
Développement : Décomposition Polaire C infini difféomorphisme
Le caractère $C^\infty$ de la décomposition est fait dans Calcul Différentiel, mais de manière très elliptique. Le reste est plus développé dans (par exemple) le H2G2.
Références :
Histoires hédonistes de groupes et géométries, Tome 1 - Caldero, Germoni
Calcul différentiel - Gonnord, Tosel
Développement : Complexité moyenne du tri rapide
L'étude est un peu subtile, et le lemme important et qu'en partant de permutations équiprobables, on arrive après la phase de division du tableau à des permutations des tableaux restant à trier qui sont encore équiprobables, ce qui est rarement bien fait dans les livres d'algorithmique…
Références :
Eléments d'algorithmique - Beauquier, Berstel et Chrétienne
Développement : Tri par tas
En faisant la correction de manière complètement formelle, on atteint relativement les 15 min.
Références :
Introduction à l'algorithmique - Thomas H. Cormen, Charles E. Leiserson, Clifford Stein, Ronald Rivest
Développement : La fonction d'Ackermann n'est pas récursive primitive
Références :
Logique mathématique Tome 2 - René Cori, Daniel Lascar
Développement : Calcul de la distance d'édition
Références :
Algorithms on string - Crochemore, Hancart et Lecroq