Différences

Ci-dessous, les différences entre deux révisions de la page.

Lien vers cette vue comparative

Les deux révisions précédentes Révision précédente
Prochaine révision
Révision précédente
fr:research:archives [2017/03/22 16:29]
apeiron [Contenu algorithmique des stratégies du lambda-calcul]
fr:research:archives [2021/04/07 12:43] (Version actuelle)
apeiron [Résolvante de Galois]
Ligne 1: Ligne 1:
-Cette page regroupe mes projets de recherche ​commencés mais laissés en sommeil avant d'être terminés.+Cette page regroupe mes anciens ​projets de recherche, qu'ils soient ​terminés ​ou non.
  
-====== ​Système T avec opérateurs ​de contrôle======+====== ​Théorèmes ​de Gödel ​======
  
-Un des buts est d'étendre le lambda-calcul afin d'​étendre la correspondance de Curry-HowardLa réalisabilité classique ​de Krivine ainsi que le $\lambda \mu$-calcul ​de Parigot sont des avancées indépendantes dans cette direction. D'​autres tentatives (par NakanoSato ou Kameyama par exemple) insistent sur l'​aspect non-déterminisme ​de ces opérateurs ​de contrôlePour forcer le déterminisme,​ il faut forcer la stratégie d'​évaluation,​ ce que nous faisons avec un lambda-calcul monadique où seules les valeurs (variables ou abstractions) peuvent être argument ​d'une réduction.+Comme j'étais alors en [[https://​fr.wikipedia.org/​wiki/​Crise_des_fondements|quête des fondements]] ​de la connaissance mon projet ​de licence porta sur la logique mathématiqueset particulièrement les théorèmes ​de Gödel : [[https://​fr.wikipedia.org/​wiki/​Th%C3%A9or%C3%A8me_de_compl%C3%A9tude_de_G%C3%B6del|théorème ​de complétude]] et les deux [[https://​fr.wikipedia.org/​wiki/​Th%C3%A9or%C3%A8mes_d%27incompl%C3%A9tude_de_G%C3%B6del|théorèmes ​d'incomplétude]].
  
-Afin d'​inclure les entiers et la récurrence,​ c'​est ​le système T de Gödel et non le lambda-calcul qui sera utilisé comme base. Nous obtenons donc un système T par valeur, que nous traduisons vers un système T << ​nommé ​>> ​avec des $\mathtt{let}$puis vers le système T habituel. En montrant la compatibilité ​de notre traduction avec la réduction habituellenous obtenons ​la normalisation forte de notre système ​de calcul en la dérivant ​de celle du système T.+Le travail était fait en collaboration avec le professeur Martin Andler ​de l'​Université Versailles Saint-Quentin en Yvelines et basée sur les deux tomes de l'​ouvrage ​<< ​Logique mathématique ​>> ​de René Cori et Daniel Lascar : 
 +  - Calcul propositionnel,​ algèbres de Boole, calcul ​des prédicats 
 +  - Fonctions récursivesthéorème ​de Gödelthéorie des ensembles 
 +Et j'ai eu la satisfaction ​de présenter mon exposé à René Cori, maître ​de conférences à l'​Université Paris Diderot, qui m'a suggéré ensuite ​de faire le master LMFI : Logique Mathématique et Fondements de l'​Informatique.
  
-L'​idée aurait été ensuite d'ajouter ​à notre système ​de calcul des opérateurs ​de contrôle comme $\mathtt{callcc}$$\mathtt{catch}$ ou $\mathtt{throw}$,​ mais le départ ​de Tristan Crolard mit le projet en sommeil. Voici ma {{ :fr:​research:​tc3.pdf ​|dernière version}} ​de travail.+Ce travail m'a introduit ​à la calculabilité,​ aux structures du premier ordre utilisées dans les ASMs de Gurevich et donc dans mes travaux sur les modèles ​de calcul [[fr:​research:​models-computation#​algorithmes_sequentiels|séquentiels]] et [[fr:​research:​models-computation#​algorithmes_paralleles|parallèles]]ainsi qu'aux systèmes ​de preuve qui m'ont servi pour mes travaux sur lse [[fr:​research:​models-computation#​automates_cellulaires|preuves ​de correction]].
  
-====== ​Contenu algorithmique des stratégies du lambda-calcul ​======+====== ​Résolvante de Galois ​======
  
-Les EMAs ont été développées notamment par Serge Grigorieff ​et Pierre Valarcher dans [[https://​arxiv.org/​abs/1001.2160|leur article]]. L'​idée est que certes les Abstract State Machines de Gurevich peuvent simuler étape par étape toutes les machines usuelles((En tout cas, les machines dont le calcul est séquentiel,​ comme les machines de Turing ou les RAMs.)), mais que simulation n'est pas identification. Ainsi, Serge Grigorieff et Pierre Valarcher montrent que des classes naturelles d'EMAs peuvent être littéralement identifiées à ces machines, ce qui fait des EMAs un modèle mathématique unificateur.+Ce travail sur la théorie de Galois m'a intéressé pour comprendre pourquoi les équations polynomiales de degré quelconque ne sont pas toujours résolubles, ​et m'a donné les base pour comprendre certains concepts comme [[https://​arxiv.org/​pdf/1011.0014.pdf|la théorie de Galois des algorithmes]].
  
-Dans cette optique, j'ai cherché à formaliser sous forme de machines abstraites les différentes stratégies d'évaluation contextuelle utilisées pour le lambda-calcul. Le terme à évaluer n'​est ​donc qu'une entréeet c'​est ​la stratégie ​d'évaluation elle-même qui est vue comme un algorithmeLes différentes stratégies étudiées sont l'​appel par nom, l'appel par besoin ​et l'appel par valeurqui sont respectivement implémentées ​par la machine ​de Krivine ​et deux machines créées ​pour l'occasion ​+===== Versions ===== 
-$$\begin{array}{r|l@{}c@{}r@{}rcl@{}c@{}r@{}rc} + 
-\text{appel ​par nom} +Voici {{ :​fr:​research:​galois-draft.pdf |notre brouillon}} s'attardant davantage sur l'histoire des mathématiques. 
-&​{} ​\mu &{}\ \star\ &{} (t_1)t_2 \ \star\ &{} \pi &{} \succ &{} \mu\mathunderscore &​{}\ \star\ &{} t_1 \ \star\ &{} t_2,\pi \\ + 
-&{} \mu\mathunderscore &​{}\ \star\ &{} \lambda x.t_1 \ \star\ &{} t_2,\pi &{} \succ &{} \mu &​{}\ \star\ &{} t_1[t_2/x] \ \star\ &{} \pi \\ +Voici {{ :​fr:​research:​galois-conf.pdf |une synthèse }} mieux rédigée et focalisée sur la caractérisation du groupe de Galois. 
-\hline + 
-\text{appel ​par valeur} +===== Le projet ===== 
-&​{} ​\mu &{}\ \star\ &{} (t_1)t_2 \ \star\ &{} \pi &{\succ &{} \mu, t_1 &​{}\ \star\ &{} t_2 \ \star\ &{} \mathunderscore,​\pi \\ + 
-&{} \mu, t &​{}\ \star\ ​ &​{} ​\star\ &{} \mathunderscore,​\pi &{} \succ &{} \mu, \mathunderscore &​{}\ \star\ &{} t \ \star\ &{} v, \pi \\ +Ce que nous appelons aujourd'hui la << théorie de Galois >> ​est l'étude des extensions de corps commutatifs par des << groupes de Galois >>, c'​est ​à dire les ensembles ​d'automorphismes d'une extension laissant invariant le corps de base. Cette théorie s'est avérée fertile pour beaucoup de domaines((Théorie des équations algébriques,​ théorie algébrique des nombres, théorie des corps, théorie de Galois inverse, théorie de Galois différentielle,​ géométrie algébrique,​ cryptographie,​ etc.))mais le degré d'​abstraction actuel cache l'extrême simplicité de la théorie initiale. 
-&{} \mu, \mathunderscore &​{}\ \star\ &{} \lambda ​x.t \ \star\ &{} v,\pi &{} \succ &{} \mu &​{}\ \star\ &{} t[v/x] \ \star\ &{} \pi \\ + 
-\hline +Mon camarade Raoul Martin ​et moi avons fait notre projet de première année de master en 2009-2010 sous la direction du professeur Vincent Cossart à l'Université Versailles Saint-Quentin en Yvelinesen étudiant directement le [[http://​www.bibnum.education.fr/​mathematiques/​algebre/​memoire-sur-les-conditions-de-resolubilite-des-equations-par-radicaux|manuscrit de Galois]]. Le but était double : d'une part en formaliser les résultats avec des notations modernes tout en s'en tenant à la fascinante simplicité ​de la preuve initiale. D'​autre part, à cause de la mort tragique de Galois son manuscrit est resté inachevé, donc nous avons dû reconstruire les preuves manquantes selon les outils disponibles ​et en essayant de garder l'​esprit de la preuve initiale. Notre rapport a été suffisamment apprécié ​pour que nous soyons invités à parler durant les Journées Mathématiques des 20 ans de l'UVSQ((Davantage d'​informations peuvent être trouvées sur [[http://​lmv.math.cnrs.fr/​conferences-et-colloques/​journees-mathematiques-des-20-ans/​article/​programme-des-conferences|le site dédié]].)). 
-\text{appel par besoin} + 
-&{} \mu &​{}\ \star\ &​{} ​(t_1)t_2 \ \star\ &{} \pi &{} \succ &​{}\mu,​ \mathunderscore &​{}\ \star\ &{} t_1 \ \star\ &{} t_2,\pi \\ +===== Contexte historique ===== 
-&{} \mu, \mathunderscore &​{}\ ​\star\ &{} v \ \star\ &{} t, \pi &{} \succ &{} \mu, v &{}\ \star\ &{} t \ \star\ &{} \mathunderscore,​\pi \\ + 
-&{} \mu, \lambda ​x.t &{}\star\ &{} v \ \star\ &{} \mathunderscore,​\pi &{\succ &{} \mu &​{}\ \star\ &{} t[v/x] \ \star\ &{} \pi \\+Le problème initial est de chercher à exprimer les racines d'un polynôme ​$P$ à coefficients dans un corps $K$ (par exemple ​$\mathbb{Q}l'​ensemble des rationnels) ​par une combinaison de fonctions élémentaires\footnote{Additionsoutractionmultiplicationdivision et les racines carrées, cubiques, etc.et des coefficients du polynômeSi cela est possible l'​équation $P(x) = 0$ sera dite << résoluble ​par radicaux >>. Par exemple : 
 +$$\begin{array}{r@{}l
 +ax^2 + bx + c = 0  &{}\Leftrightarrow (+ b/2a)^2 = (b^2 - 4ac)/(2a)^2\\ 
 + &{}\Leftrightarrow ​\frac{- b \pm \sqrt{b^2 - 4ac}}{2a}\\
 \end{array}$$ \end{array}$$
  
-Nous prouvons que nos machines sont correctesc'est à dire que si un terme est évalué avec une stratégie jusqu'à une valeur finale ​en $n$ substitutions, alors la  ​machine ne contenant ​que ce terme((C'est à dire que l'​antipile ​$\mu$ et la pile $\pisont vides.)) fait des transitions jusqu'​à ​arriver à la même valeur en ayant fait exactement ​$n$ substitutions puis s'​arrêtePuis nous traduisons ces machines sous forme d'EMA, et discutons des généralisations possibles.+Ainsiune équation polynomiale du second degré est toujours résoluble par radicaux, comme l'a montré Al-Khwârizmî au IXème siècle. Au XVIème siècle, Tartaglia, Cardano et Ferrari généralisèrent ce résultat aux degrés $3$ et $4$. La question des degrés supérieurs ​est restée ouverte jusqu'à ce qu'​Abel [[https://​www.google.fr/​url?​sa=t&​rct=j&​q=&​esrc=s&​source=web&​cd=1&​cad=rja&​uact=8&​ved=0ahUKEwjwoNDRgujSAhXMtxQKHeijAfQQFggeMAA&​url=http%3A%2F%2Fwww.abelprize.no%2Fc54178%2Fbinfil%2Fdownload.php%3Ftid%3D53608&​usg=AFQjCNHh2O36wuv7UrqbLRoztNpSzD6QRA&​sig2=K-GJihBINYTh9KWApMgitQ|prouve]] ​que tous l'​équation de degré $5$ n'est pas toujours résoluble par radicaux. De façon indépendante,​ Galois a montré dans son manuscrit un résultat plus général : une équation polynomiale est résoluble par radicaux si et seulement si son groupe de Galois est résoluble. 
 + 
 +===== Esquisse de la preuve ===== 
 + 
 +Notre travail a consisté ​à construire le groupe de Galois ​en utilisant les outils de Galois. 
 + 
 +Soit $n \ge 2$ le degré du polynôme, et $x_1,​\dots,​x_n$ ses racines. Soit $E = \{x_1,​\dots,​x_n\}$. Nous montrons tout d'​abord qu'il existe une application $\varphi : E^n \rightarrow K[x_1, \dots, x_n]$ telle que si $(y_1, \dots, y_n)$ et $(z_1, \dots, z_n)$ sont des n-uplets distincts de $E^n$, alors $\varphi(y_1,​ \dots, y_n) \neq \varphi(z_1,​ \dots, z_n)$. L'​application $\varphi$ est appelée ​la résolvante de Galois. Nous prouvons ​que $V = \varphi(x_1, \dots, x_n)$ est un élément primitif, c'est à dire que $K[V]$ est un corps et que $K[x_1, ​\dots, x_n] = K[V]$. En particulier,​ pour tout $1 \le i \le n$ nous avons qu'il existe une fonction rationnelle $f_i$ telle que $x_i = f_i(V)$. 
 + 
 +Soit $Q$ le polynôme minimal de $V$ sur $K$, et $V = V_1, \dots, V_mses racinesNous prouvons d'une part que pour chacune de ces racines, $V_k = \varphi(f_1(V_k), \dots, f_n(V_k))$, et d'​autre part qu'à $k$ fixé, $(f_1(V_k), \dots, f_n(V_k))$ est une permutation des racines de $P$. Donc, pour chaque $V_k$ il existe une permutation $\sigma \in S_n$ telle que $V_k = \varphi(f_{\sigma(1)}(V),​ \dots, f_{\sigma(n)}(V))$. Nous définissons donc le groupe de Galois par : 
 +$$Gal(P,​\varphi) = \{\sigma \in S_n\ |\ Q\left(\varphi(f_{\sigma(1)}(V),​ \dots, f_{\sigma(n)}(V))\right) = 0\}$$ 
 + 
 +Nous montrons, ​d'une part que le groupe de Galois est bien un groupe, et d'​autre part qu'il est le plus grand groupe vérifiant que pour tout $F \in K[X_1, \dots, X_n]$, si $F(x_1, \dots, x_n) = 0$ alors $F(x_{\sigma(1)},​ \dots, x_{\sigma(n)}) = 0$. Ainsi, $Gal(P,​\varphi)$ ne dépend que de $P$. C'est bien le groupe de Galois associé à l'​extension où l'on a ajouté les racines de $P$.
  
-Voici {{ :​fr:​research:​lema.pdf |la dernière version}}.