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:27]
apeiron [Réalisabilité classique]
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  
-{{ :​fr:​research:​realizability_in_classical_logic.pdf |son article}} traitant de réalisabilité classique. 
- 
-La logique intuitionniste peut être vue comme la logique classique où des règles équivalentes comme le tiers exclu, l'​élimination de la double négation ou la loi de Peirce ne seraient plus toujours autorisées. La correspondance de Curry-Howard permet d'​associer à chaque preuve en logique intuitionniste un programme en lambda-calcul. En cherchant à typer une instruction de contrôle dans un langage dérivant du lambda-calcul,​ l'​informaticien Tim Griffin associa un programme (la commande $\mathtt{callcc}$) à la loi de Peirce. 
- 
-Ainsi, la correspondance de Curry-Howard peut être étendue à la logique classique. Plus formellement,​ étendons le lambda-calcul habituel avec une instruction cc pour << current continuation >> en introduisant des piles e termes clos et des continuations comme termes. Alors il est possible de définir un système de transition, qui est un lambda-calcul avec continuations. 
- 
-Jean-Louis Krivine va plus loin dans ce papier et les autres en associant des programmes aux axiomes de la théorie des ensembles et à l'​axiome du choix, ce qui permet d'​étendre la correspondance à tous les théorèmes prouvés depuis l'​antiquité. Pour un résumé accessible de ses travaux, voir {{ :​fr:​research:​expose_krivine.pdf |l'​exposé de Krivine}} à un colloque de sciences cognitives. 
- 
-Cette approche très constructive stimula mon intérêt pour les modèles de calcul, notamment implémentés sous forme de système de transition comme ce fût le cas durant ma thèse, ainsi que pour la correspondance preuve-programme,​ notamment lors de mon apprentissage de Coq durant mon postdoc. 
- 
- 
-====== 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}}.