Différences
Ci-dessous, les différences entre deux révisions de la page.
| Les deux révisions précédentes Révision précédente Prochaine révision | Révision précédente Prochaine révision Les deux révisions suivantes | ||
|
fr:research:archives [2017/03/22 16:29] apeiron [Contenu algorithmique des stratégies du lambda-calcul] |
fr:research:archives [2021/04/06 14:15] apeiron [Théorèmes d'incomplétude de Gödel] |
||
|---|---|---|---|
| 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-Howard. La 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 Nakano, Sato ou Kameyama par exemple) insistent sur l'aspect non-déterminisme de ces opérateurs de contrôle. Pour 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. | + | ====== Résolvante de Galois ====== |
| - | 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 habituelle, nous obtenons la normalisation forte de notre système de calcul en la dérivant de celle du système T. | + | ===== Versions ===== |
| - | 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. | + | Voici {{ :fr:research:galois-draft.pdf |notre brouillon}} s'attardant davantage sur l'histoire des mathématiques. |
| - | ====== Contenu algorithmique des stratégies du lambda-calcul ====== | + | Voici {{ :fr:research:galois-conf.pdf |une synthèse }} mieux rédigée et focalisée sur la caractérisation du groupe 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. | + | ===== Le projet ===== |
| - | 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ée, et c'est la stratégie d'évaluation elle-même qui est vue comme un algorithme. Les différentes stratégies étudiées sont l'appel par nom, l'appel par besoin et l'appel par valeur, qui sont respectivement implémentées par la machine de Krivine et deux machines créées pour l'occasion : | + | 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. |
| - | $$\begin{array}{r|l@{}c@{}r@{}rcl@{}c@{}r@{}rc} | + | |
| - | \text{appel par nom} | + | 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 Yvelines, en é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é]].)). |
| - | &{} \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 \\ | + | ===== Contexte historique ===== |
| - | \hline | + | |
| - | \text{appel par valeur} | + | 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{Addition, soutraction, multiplication, division et les racines carrées, cubiques, etc.} et des coefficients du polynôme. Si cela est possible l'équation $P(x) = 0$ sera dite << résoluble par radicaux >>. Par exemple : |
| - | &{} \mu &{}\ \star\ &{} (t_1)t_2 \ \star\ &{} \pi &{} \succ &{} \mu, t_1 &{}\ \star\ &{} t_2 \ \star\ &{} \mathunderscore,\pi \\ | + | $$\begin{array}{r@{}l} |
| - | &{} \mu, t &{}\ \star\ &{} v \ \star\ &{} \mathunderscore,\pi &{} \succ &{} \mu, \mathunderscore &{}\ \star\ &{} t \ \star\ &{} v, \pi \\ | + | ax^2 + bx + c = 0 &{}\Leftrightarrow (x + b/2a)^2 = (b^2 - 4ac)/(2a)^2\\ |
| - | &{} \mu, \mathunderscore &{}\ \star\ &{} \lambda x.t \ \star\ &{} v,\pi &{} \succ &{} \mu &{}\ \star\ &{} t[v/x] \ \star\ &{} \pi \\ | + | &{}\Leftrightarrow x = \frac{- b \pm \sqrt{b^2 - 4ac}}{2a}\\ |
| - | \hline | + | |
| - | \text{appel par besoin} | + | |
| - | &{} \mu &{}\ \star\ &{} (t_1)t_2 \ \star\ &{} \pi &{} \succ &{}\mu, \mathunderscore &{}\ \star\ &{} t_1 \ \star\ &{} t_2,\pi \\ | + | |
| - | &{} \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 \\ | + | |
| \end{array}$$ | \end{array}$$ | ||
| - | Nous prouvons que nos machines sont correctes, c'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 $\pi$ sont vides.)) fait des transitions jusqu'à arriver à la même valeur en ayant fait exactement $n$ substitutions puis s'arrête. Puis nous traduisons ces machines sous forme d'EMA, et discutons des généralisations possibles. | + | Ainsi, une é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_m$ ses racines. Nous 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}}. | ||