% !TeX spellcheck = fr_FR
\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 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}.
	
	\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 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 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 construction proposées et les propriétés établies prouvent également la conjecture établie par Philippo Sestini dans sa thèse.
	
	
	\subsection*{Le bilan et les perspectives}
	
	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}