78 lines
3.9 KiB
TeX
78 lines
3.9 KiB
TeX
\documentclass[11pt]{article}
|
|
|
|
\usepackage[francais]{babel}
|
|
\usepackage{csquotes}
|
|
\usepackage{xcolor}
|
|
|
|
% \setlength{\parskip}{0.3\baselineskip}
|
|
|
|
\newcommand\question[1]{\textbf{\textcolor{orange}{#1}}}
|
|
%\newcommand\question[1]{}
|
|
|
|
\begin{document}
|
|
|
|
\title{Sémantique catégorique de la réduction des GATs en GATs à deux sortes}
|
|
|
|
\author{Samy Avrillon, encadré par Ambroise Lafont\\
|
|
\small Équipe PARTOUT, Laboratoire d'Informatique de l'École Polytechnique (LIX)}
|
|
|
|
\maketitle
|
|
|
|
\pagestyle{empty} %
|
|
\thispagestyle{empty}
|
|
|
|
|
|
\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.
|
|
|
|
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 ?}
|
|
|
|
\subsection*{La contribution proposée}
|
|
|
|
Durant ce stage, j'ai apporté une formalisation sémantique de la transformation. J'ai décrit formellement la transformation de modèles du GAT original en modèle du GAT transformé, mais également la transformation réciproque. J'ai également prouvé certaines propriétés de cette transformation.
|
|
|
|
\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}.}
|
|
|
|
\subsection*{Les arguments en faveur de sa validité}
|
|
|
|
La preuve a été faite avec la sémantique en essayant de généraliser les objets utilisés au maximum.
|
|
|
|
Cette preuve valide la conjecture établie par 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 ?}
|
|
|
|
\end{document} |