agreg issueshttps://gitlab.crans.org/alopez/agreg/-/issues2017-12-15T08:14:31+01:00https://gitlab.crans.org/alopez/agreg/-/issues/4Lambda Calcul2017-12-15T08:14:31+01:00Aliaume LopezLambda CalculIl faut effectuer les tâches suivantes
* [ ] Mettre en "deux pages coupées" pour que le format soit un poil plus uniforme
* [ ] Ajouter le `.tex` au git et pas seulement le pdf ...
* [ ] Compléter la preuve de contextualisation de l...Il faut effectuer les tâches suivantes
* [ ] Mettre en "deux pages coupées" pour que le format soit un poil plus uniforme
* [ ] Ajouter le `.tex` au git et pas seulement le pdf ...
* [ ] Compléter la preuve de contextualisation de la béta-réduction
* [ ] Ajouter des exemples pertinents (non triviaux)
Voilà, j'ai assigné Gaëtan parce qu'il a déjà commencé à faire çaGaetan Doueneau-tabotGaetan Doueneau-tabothttps://gitlab.crans.org/alopez/agreg/-/issues/3Organisation des développements2017-12-11T20:32:48+01:00Aliaume LopezOrganisation des développementsIl faut ré-organiser la manière dont on gère les développements de maths (qui sont bien plus nombreux qu'en informatique).
* [ ] Donner des numéros explicites à base de `D101 ... D199` pour l'algèbre et de manière similaire pour l'anal...Il faut ré-organiser la manière dont on gère les développements de maths (qui sont bien plus nombreux qu'en informatique).
* [ ] Donner des numéros explicites à base de `D101 ... D199` pour l'algèbre et de manière similaire pour l'analyse
* [ ] Fusionner les listes de développements avec Émilie
* [ ] Faire un système de références de bouquins un peu plus pertinent
* [ ] Construire une réelle base de données
L'objectif est à terme de pouvoir
1. Lister les développements possibles pour une leçon, et observer qui veut les proposer
2. Lister pour un développement la liste des leçons possibles (et par qui)
3. Lister pour une _référence_ les développements qui sont possibles
4. Lister toutes les références utilisées ... C'est quand même pratiquehttps://gitlab.crans.org/alopez/agreg/-/issues/2Rédiger proprement l'algorithme CYK2017-12-11T20:05:39+01:00Aliaume LopezRédiger proprement l'algorithme CYK* [x] Définir proprement la grammaire intersectée
* [ ] Prouver la première inclusion proprement
* [ ] Prouver la deuxième inclusion proprement
* [ ] Rappeler la mise en forme normale de Chomsky
* [ ] Rappeler l'algorithme qui test...* [x] Définir proprement la grammaire intersectée
* [ ] Prouver la première inclusion proprement
* [ ] Prouver la deuxième inclusion proprement
* [ ] Rappeler la mise en forme normale de Chomsky
* [ ] Rappeler l'algorithme qui teste la vacuité
* [ ] Démontrer la correction de CYK avec le théorèmeBoudyBoudyhttps://gitlab.crans.org/alopez/agreg/-/issues/1Formaliser la preuve des traces2017-12-14T19:24:50+01:00Aliaume LopezFormaliser la preuve des tracesLa preuve est pour le moment encore au stade `informel`. Il faut regarder précisément les constantes, et prouver formellement (comme dans boustrophédon) l'injectivité de la fonction.
* [ ] Donner une définition précise de la trace
* [ ...La preuve est pour le moment encore au stade `informel`. Il faut regarder précisément les constantes, et prouver formellement (comme dans boustrophédon) l'injectivité de la fonction.
* [ ] Donner une définition précise de la trace
* [ ] Faire proprement le lemme de `panache`
* [x] Montrer effectivement l'injectivité (en utilisant les idées du pdf dans le dossier ressources)
/estimate 0d 3hAliaume LopezAliaume Lopez