Mysaa/M2Internship
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Modification de la synthèse selon les commentaires

Browse Source
This commit is contained in:
Samy Avrillon 2024-08-16 02:05:34 +02:00
parent 86dd4ec900
commit fa2353c84c
Signed by: Mysaa
GPG Key ID: 0220AC4A3D6A328B
1 changed files with 12 additions and 34 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

46
Report/synthese.tex
View File

@ -1,3 +1,4 @@
% !TeX spellcheck = fr_FR
\documentclass[11pt]{article}
\usepackage[francais]{babel}
@ -24,55 +25,32 @@
\subsection*{Le contexte général}
Les théories algébriques généralisées (ou GAT) sont des objects syntaxiques introduits en 1986 par Cartmell qui permettent la description d'objects algébriques, comme une généralisation des types inductifs de théorie des types.
Les théories algébriques généralisées (ou GAT) sont des objects syntaxiques introduits en 1986 par Cartmell qui permettent la description de structures algébriques, que l'on peut voir comme une généralisation des types inductifs de la théorie des types. Par exemple, on peut décrire les modèles d'une théorie des types à l'aide d'un GAT.
Un GAT est constitué d'une liste de \enquote{sortes} décrivant les ensembles, généralement suivie d'une liste de \enquote{constructeurs}.
\question{De quoi s'agit-il ?}
\question{D'où vient-il ?}
\question{Quels sont les travaux déjà accomplis dans ce domaine dans le monde ?}
\subsection*{Le problème étudié}
Il existe un processus qui permet de transformer n'importe quel GAT en un GAT avec seulement deux sortes. Cette transformation a été utilisée par Philippo Sestini dans sa thèse, afin de restreindre son sujet d'étude. Cependant, il n'a pas été prouvé que cette transformation ne réduisait pas la généralité de sa thèse.
\question{Quelle est la question que vous avez abordée ?}
\question{Pourquoi est-elle importante, à quoi cela sert-il d'y répondre ?}
\question{Est-ce un nouveau problème ?}
\question{Si oui, pourquoi êtes-vous le premier chercheur de l'univers à l'avoir posée ?}
\question{Si non, pourquoi pensiez-vous pouvoir apporter une contribution originale ?}
Il existe un processus qui permet de transformer n'importe quel GAT en un GAT avec seulement deux sortes. Cette transformation a notamment été exploitée par Filippo Sestini dans sa thèse, afin de restreindre son sujet d'étude. Cependant, il n'a pas été prouvé que cette transformation ne réduisait pas la généralité de sa thèse.
\subsection*{La contribution proposée}
Durant ce stage, j'ai recherché à formaliser sémantiquement cette transformation. J'ai commencé par l'appliquer à des exemples, trouver des propriétés sur ces exemple, pour ensuite formaliser dans la théorie des catégorie la transformation, et prouver formellement les propriétés que j'avais remarquées sur les exemples.
\question{Qu'avez vous proposé comme solution à cette question ?
Attention, pas de technique, seulement les grandes idées !
Soignez particulièrement la description de la démarche \emph{scientifique}.}
Durant ce stage, j'ai chercher à formaliser sémantiquement cette transformation. C'est à dire que je me suis intéressé directement aux catégories des modèles sans m'attacher à l'aspect syntaxique des GATs. Je me suis restreint à l'étude des \enquote{spécification de sortes}, c'est à dire aux GATs constitués uniquement d'une liste de sortes, sans constructeurs. J'ai commencé par appliquer la transformation sur des exemples simples, afin d'identifier des propriétés qui la justifient, le tout dans un cadre catégorique. Ensuite, j'ai énoncé et prouvé formellement ces propriétés dans leur plus grande généralité.
\subsection*{Les arguments en faveur de sa validité}
La preuve a été faite sémantiquement en essayant à chaque étape de généraliser les objets utilisés au maximum. Les constructions des objets sont basées sur des papiers déjà publiés, qui sont cités dans ce rapport.
La preuve a été faite sémantiquement en essayant à chaque étape de généraliser les objets utilisés au maximum. Les constructions des objets sont basées sur des papiers déjà publiés, qui sont cités dans ce rapport.
La construction proposées et les propriétés établies prouvent également la conjecture établie par Philippo Sestini dans sa thèse.
La construction proposées et les propriétés établies prouvent également la conjecture établie par Philippo Sestini dans sa thèse.
\question{Qu'est-ce qui montre que cette solution est une bonne solution ?}
\question{Des expériences, des corollaires ?}
\question{Commentez la \emph{robustesse} de votre proposition :
comment la validité de la solution dépend-elle des hypothèses de travail ?}
\subsection*{Le bilan et les perspectives}
Nous avons formalisé la transformation sémantiquement, ce qui permet de gagner en généralité.
Cette tranformation a été prouvée, et permet notamment de restreindre une étude aux seuls GATs à deux sortes.
Cette transformation met en correspondanc de façon intéressante les \enquote{déclarations de sortes} et les \enquote{constructeurs}, ce qui permetterai évenuellement de les recouper dans une même notion.
Nous avons également de quoi réfléchir à une généralisation des GATs qui décriraient par exemple des types mutuellement inductif, mais aussi d'autres objets plus \enquote{exotiques}. Il y a du travail à les étudier, et à observer l'effet de la transformation sur ces objets.
\question{Et après ? En quoi votre approche est-elle générale ?}
\question{Qu'est-ce que votre contribution a apporté au domaine ?}
\question{Que faudrait-il faire maintenant ?}
\question{Quelle est la bonne \emph{prochaine} question ?}
Nous avons formalisé la transformation sémantiquement, ce qui permet de gagner en généralité et de s'abstraire de l'aspect syntaxique des GATs.
Cette tranformation a été prouvée, et permet notamment de justifier une restriction d'une étude aux seuls GATs à deux sortes.
Une prochaine étape serait de rajouter les constructeurs de termes à notre formalisation, en décrivant leur transformation et en adaptant les propriétés prouvées pour le cas des spécifications de sortes.
Nous avons également de quoi réfléchir à une généralisation des GATs qui décriraient par exemple des sortes définies l'une mutuellement contenue dans l'autre, et d'autres sortes plus \enquote{exotiques}. Il y a du travail à les étudier, et à observer l'effet de la transformation sur ces objets.
\end{document}