Modification du document pour rendu. Inclusion de la synthèse dans le document
This commit is contained in:
parent
0cdf37e75a
commit
1d0860712e
GPG Key ID:
0220AC4A3D6A328B
@ -12,6 +12,12 @@
|
||||
\hypersetup{pdftitle={Categorical semantics of the reduction of GATs to two-sorted GATs}}
|
||||
\author{Samy Avrillon, supervised by
|
||||
\\[1ex] Ambroise Lafont (LIX, Palaiseau, France)}
|
||||
\date{}
|
||||
|
||||
|
||||
\fancyhead[L]{M2 internship report}
|
||||
\fancyhead[R]{Categorical semantics of the 2-sortification of GATs}
|
||||
\fancyfoot[L]{Samy Avrillon}
|
||||
|
||||
\begin{document}
|
||||
\doparttoc
|
||||
@ -19,6 +25,37 @@
|
||||
|
||||
\hsep
|
||||
|
||||
\subsection*{General Context}
|
||||
|
||||
Generalized Algebraic Theories a.k.a. GATs are synctaxic objects introduced in 1986 by Cartmell \cite{CartmellGATs}. They enable us to describe algebraic structures that we can see as a generalization of Type Theory's inductive types. For example, we can describe the models of some type theory using a GAT.
|
||||
|
||||
A GAT is made of a list of \enquote{sorts} that describes sets, usually followed by a list of \enquote{constructors}.
|
||||
|
||||
\subsection*{Problem Studied}
|
||||
|
||||
There is a process that transforms any GAT into another GAT with only two sorts. This transformation has been used by Filippo Sestini in their PhD, in order to make simpler proofs the scope of their study. However it has not been proven that using this transformation does not reduce the generality of their thesis.
|
||||
|
||||
\subsection*{Proposed Contribution}
|
||||
|
||||
During this internship, my goal was to semantically formalize this transformation. I looked directly at the categories of models without looking at the syntactic aspects of GATs. I only looked at \enquote{sort specification}, i.e. GATs that are juste a list of sort declarations with no constructors. I started with applying the transformation on simple examples in order to identify properties that would prove the transformation to be correct. I did that in a categorical framework. Then, i formally stated those properties and proved them as generically as possible.
|
||||
|
||||
\subsection*{Arguments Supporting Their Validity}
|
||||
|
||||
The overall proof was made semantically and at each step, we tried to generalize objects as much as possible. The ways of constructing the objects is based on published papers \cite{Altenkirch2018} \cite{Fiore2008}.
|
||||
|
||||
My contribution also proves the conjecture stated in Sestini's PhD.
|
||||
|
||||
\subsection*{Summary and Future Work}
|
||||
|
||||
We formalised semantically this transformation, enabling us to be more general and to avoid the syntactical aspects of GATs.
|
||||
This transformation has been proven, so that studying only GATs with two sorts can be done without loosing generality.
|
||||
|
||||
A next step could be to add term constructors to our formalization. We could describe their transformation and adapt the properties we stated for sort specification to them.
|
||||
|
||||
We could also try to further generalize GATs using this transformation. We could for example try to describe sorts that are mutually included one into the other. There is work in studying them, and looking at how the transformation affects them in order to discover new properties.
|
||||
|
||||
\hsep
|
||||
|
||||
\setcounter{tocdepth}{2}
|
||||
\tableofcontents
|
||||
|
||||
@ -115,7 +152,7 @@
|
||||
\section{Examples}
|
||||
\label{sec:Examples}
|
||||
|
||||
Before making the formal proof, we will study our construction on three examples, in order to ease understanding of the formal proof.
|
||||
Before making the formal proof, we will study our construction on two examples, in order to ease understanding of the formal proof.
|
||||
|
||||
\paragraph{Structure of the proof}
|
||||
The formal proof will be an induction on the number of sorts taken into account. At each step, we will add a new sort declaration, represented by a functor $H_i$ described later (\autoref{sec:constructingCategory}).
|
||||
@ -131,7 +168,7 @@
|
||||
\item A proof that $F_iG_i \cong \Id_{\CC_i}$ (i.e. $F_i \vdash G_i$ make up a coreflection)
|
||||
\end{itemize}
|
||||
|
||||
We will now present those objects on three specific examples in order to help getting an understanding of the logic behind the formal proof.
|
||||
We will now present those objects on two specific examples in order to help getting an understanding of the logic behind the formal proof.
|
||||
|
||||
\subsection{The empty sort specification}
|
||||
|
||||
@ -424,8 +461,6 @@
|
||||
With this functor, every element of $X_\UU$ is reached by some constructor. And therefore, every object of $X_\El$ points to a sort that is reached by some constructor.
|
||||
\end{remark}
|
||||
|
||||
\todo{Parler des morphismes ? Est-ce nécessaire ?}
|
||||
|
||||
\paragraph{Constructing $F_i$}
|
||||
|
||||
We will now create an object $Y = F_i X$ of $\CC_3$ from an object $X$ of $\BB_3$.
|
||||
@ -493,8 +528,8 @@
|
||||
|
||||
And therefore $F_3G_3 \cong \Id_{\CC_3}$.
|
||||
|
||||
\subsection{Another sort specification}
|
||||
\todo{L'exemple, ou sinon remplacer toutes les occurences de «trois» par «deux»}
|
||||
% \subsection{Another sort specification}
|
||||
% \todo{L'exemple, ou sinon remplacer toutes les occurences de «trois» par «deux»}
|
||||
|
||||
\section{Constructing the coreflection}
|
||||
\label{sec:proofSection}
|
||||
@ -736,14 +771,7 @@
|
||||
W(g,h) := \left(g \tl^{i-1} K_{H_iF_{i-1}}(g,h)\right)
|
||||
\]
|
||||
|
||||
It is indeed a morphism of $\BB_{i}$ as it makes the following diagram commute.
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM WghMorphismOfBi.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/WghMorphismOfBi.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
We verify that it is indeed a morphism of $\BB_{i}$ in appendix \ref{apx:wdefsound}
|
||||
|
||||
\subsubsection{E definition}
|
||||
|
||||
@ -823,13 +851,7 @@
|
||||
\inj_1^i := \inj_1^{i-1} : R_{i-1}^i X \to R_{i-1}^i (X \tl^i Y) = R_{i-1}^i X \tl^{i-1} Y
|
||||
\]
|
||||
|
||||
It is a morphism of $\BB_i$ as it makes the following diagram commute:
|
||||
\begin{center}
|
||||
% YADE DIAGRAM TlInj1MorphismOfBi.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/TlInj1MorphismOfBi.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
We check that $\inj_1^i$ is a morphism of $\BB_i$ in appendix \ref{apx:inj1morphism}.
|
||||
|
||||
The second injector is defined as
|
||||
\[
|
||||
@ -847,14 +869,7 @@
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
We define $\{g ; h\}_i = \{R_{i-1}^i g ; h\}_{i-1}$. This is a morphism of $\BB_i$ as it makes the following diagram commute:
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM TlUniversalMorphismIsOfBi.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/TlUniversalMorphismIsOfBi.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
We define $\{g ; h\}_i = \{R_{i-1}^i g ; h\}_{i-1}$. We check that this is a morphism of $\BB_i$ in appendix \ref{apx:universalpropertymorphismIsMorphism}.
|
||||
|
||||
And this morphism $\{g;h\}_i$ is such that the universal property for it is exactly the same as the one of $\{R_{i-1}^i g, h\}$.
|
||||
|
||||
@ -866,7 +881,6 @@
|
||||
\[
|
||||
g\tl^ih := R_{i-1}^ig \tl^{i-1} h
|
||||
\]
|
||||
\todo{Même question d'homogénéité}
|
||||
|
||||
This is indeed a morphism of $\BB_i$ as it makes the following diagram commute:
|
||||
|
||||
@ -1051,11 +1065,11 @@
|
||||
|
||||
This definition is redundant with that of the last paragraph, but it has the advantage of directly creating the functor $\Gamma_i$ that are used to create the functors $H_i$ and all the rest of the proof.
|
||||
|
||||
\subsection{Non-recursive definitions}
|
||||
|
||||
\subsubsection{Redefinition of $\BB_i$}
|
||||
\subsubsection{Redefinition of $G_i$ and $F_i$}
|
||||
\subsubsection{Non-direct base category}
|
||||
% \subsection{Non-recursive definitions}
|
||||
%
|
||||
% \subsubsection{Redefinition of $\BB_i$}
|
||||
% \subsubsection{Redefinition of $G_i$ and $F_i$}
|
||||
% \subsubsection{Non-direct base category}
|
||||
|
||||
\section{Summary}
|
||||
|
||||
@ -1072,6 +1086,7 @@
|
||||
\renewcommand{\section}[2]{}%
|
||||
\printbibliography
|
||||
\endgroup
|
||||
\label{LastReportPage}
|
||||
|
||||
\newpage
|
||||
\addappheadtotoc
|
||||
@ -1079,6 +1094,43 @@
|
||||
\addtocontents{toc}{\protect\setcounter{tocdepth}{-1}}
|
||||
\appendixpage
|
||||
|
||||
\section{Soundness of definitions}
|
||||
|
||||
\subsection{$W(g,h)$ morphism of $\BB_i$}
|
||||
\label{apx:wdefsound}
|
||||
|
||||
The morphism $W(g,h) = g \tl_{i-1} K_{H_iF_{i-1}}(g,h)$ is a morphism of $\BB_i$ as it makes the following diagram commute:
|
||||
\begin{center}
|
||||
% YADE DIAGRAM WghMorphismOfBi.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/WghMorphismOfBi.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
\subsection{$\inj_1^i$ morphism of $\BB_i$}
|
||||
\label{apx:inj1morphism}
|
||||
|
||||
The morphism $\inj_1^i := \inj_1^{i-1}$ is a morphism of $\BB_i$ as it makes the following diagram commute:
|
||||
\begin{center}
|
||||
% YADE DIAGRAM TlInj1MorphismOfBi.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/TlInj1MorphismOfBi.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
\subsection{$\{g,h\}_i$ morphism of $\BB_i$}
|
||||
\label{apx:universalpropertymorphismIsMorphism}ç
|
||||
|
||||
$\{g,h\}_i := \{R_{i-1}^ig,h\}_{i-1}$ is a morphism of $\BB_i$ as it makes the following diagram commute:
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM TlUniversalMorphismIsOfBi.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/TlUniversalMorphismIsOfBi.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
|
||||
\section{$W \dashv E$ adjunction}
|
||||
\label{apx:adjunction}
|
||||
|
||||
@ -1325,3 +1377,4 @@
|
||||
\todo{Show that those are the same functors as those defined recursively. Prove the adjunction/reflection infinitely ?}
|
||||
|
||||
\end{document}
|
||||
|
||||
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"kind":"normal","label":"R_0^i\\inj_1^i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":5,"label":{"kind":"normal","label":"R_0^i\\{g,h\\}","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":6,"label":{"kind":"normal","label":"R_0^ig","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":7,"label":{"kind":"normal","label":"g","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":8,"label":{"kind":"normal","label":"\\inj_2^i","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1}],"nodes":[{"id":0,"label":{"isMath":true,"label":"R_0^iX","pos":[100,94],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"R_0^i(X \\tl^i Y)","pos":[300,94],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^iZ","pos":[300,318],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"Y","pos":[500,94],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"kind":"normal","label":"R_0^i\\inj_1^i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":5,"label":{"kind":"normal","label":"R_0^i\\{g,h\\}","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":6,"label":{"kind":"normal","label":"R_0^ig","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":7,"label":{"kind":"normal","label":"g","style":{"alignment":"left","bend":-0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":8,"label":{"kind":"normal","label":"\\inj_2^i","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1}],"nodes":[{"id":0,"label":{"isMath":true,"label":"R_0^iX","pos":[100,94],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"R_0^i(X \\tl^i Y)","pos":[300,94],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^iZ","pos":[300,176],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"Y","pos":[500,94],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
@ -46,7 +46,7 @@
|
||||
\usepackage[backend=biber,style=numeric]{biblatex}
|
||||
\usepackage{hyperref}
|
||||
|
||||
\usepackage[textheight=0.75\paperheight]{geometry}
|
||||
\usepackage[textheight=0.75\paperheight,a4paper,margin=2cm]{geometry}
|
||||
|
||||
\usepackage[lighttt]{lmodern}
|
||||
\usetikzlibrary{shapes.geometric,positioning,backgrounds}
|
||||
@ -184,4 +184,11 @@
|
||||
}
|
||||
\makeatother
|
||||
|
||||
\usepackage{fancyhdr}
|
||||
\makeatletter
|
||||
\makeatother
|
||||
\fancyfoot[C]{}
|
||||
\fancyfoot[R]{\textbf{\thepage / \pageref{LastReportPage}}}
|
||||
\pagestyle{fancy}
|
||||
|
||||
\addbibresource{Bilibibio.bib}
|
||||
@ -1,56 +0,0 @@
|
||||
% !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}
|
||||
Loading…
x
Reference in New Issue
Block a user