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 [2018/03/29 15:15]
apeiron
fr:research:archives [2021/04/07 12:43] (Version actuelle)
apeiron [Résolvante de Galois]
Ligne 1: Ligne 1:
 Cette page regroupe mes anciens projets de recherche, qu'ils soient terminés ou non. Cette page regroupe mes anciens projets de recherche, qu'ils soient terminés ou non.
  
-====== ​La résolvante ​de Galois ======+====== ​Théorèmes de Gödel ====== 
 + 
 +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ématiques,​ et 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]]. 
 + 
 +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écursives,​ théorème de Gödel, thé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. 
 + 
 +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]]. 
 + 
 +====== Résolvante ​de Galois ====== 
 + 
 +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]].
  
 ===== Versions ===== ===== Versions =====
Ligne 36: Ligne 49:
 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$. 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$.
  
-====== Réalisabilité classique ====== 
- 
-Durant ma deuxième année de master Logique Mathématique et Fondements de l'​Informatique en 2011, je profitais de ma présence à l'​Université Paris-Diderot pour faire mon stage auprès du professeur émérite Jean-Louis Krivine. Il m'​avait impressionné par sa démarche tentant d'​associer un contenu calculatoire à tous les résultats mathématiques,​ et il m'a fait travailler sur son article traitant de réalisabilité classique. 
- 
-====== Projets de thèse ====== 
- 
-===== Système T avec opérateurs de contrôle===== 
- 
-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. 
- 
-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. 
- 
-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. 
- 
-===== Contenu algorithmique des stratégies du lambda-calcul ===== 
- 
-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. 
- 
-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 : 
-$$\begin{array}{r|l@{}c@{}r@{}rcl@{}c@{}r@{}rc} 
-\text{appel par nom} 
-&{} \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 \\ 
-\hline 
-\text{appel par valeur} 
-&{} \mu &​{}\ \star\ &{} (t_1)t_2 \ \star\ &{} \pi &{} \succ &{} \mu, t_1 &​{}\ \star\ &{} t_2 \ \star\ &{} \mathunderscore,​\pi \\ 
-&{} \mu, t &​{}\ \star\ &{} v \ \star\ &{} \mathunderscore,​\pi &{} \succ &{} \mu, \mathunderscore &​{}\ \star\ &{} t \ \star\ &{} v, \pi \\ 
-&{} \mu, \mathunderscore &​{}\ \star\ &{} \lambda x.t \ \star\ &{} v,\pi &{} \succ &{} \mu &​{}\ \star\ &{} t[v/x] \ \star\ &{} \pi \\ 
-\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}$$ 
- 
-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. 
- 
-Voici {{ :​fr:​research:​lema.pdf |la dernière version}}.