Ajout de l'opérateur triangle, début
This commit is contained in:
parent
5c75b2b701
commit
87358efe42
GPG Key ID:
0220AC4A3D6A328B
@ -33,7 +33,7 @@
|
||||
|
||||
A sort specification is a list of \emph{sort declarations} that are defined with \emph{parameters} with $\Set$ as its codomain.
|
||||
|
||||
We give an example of a classical sort specification for Type Theory. On the right column we give the interpretation of the sort declaration on models.
|
||||
We give an example of a sort specification for Type Theory. On the right column we give the interpretation of the sort declarations as components of the models.
|
||||
|
||||
\vspace{1em}
|
||||
\renewcommand\arraystretch{1.5}
|
||||
@ -44,18 +44,18 @@
|
||||
\end{tabular}
|
||||
\vspace{1em}
|
||||
|
||||
A sort declaration therefore describes the sets that the model contains.
|
||||
A sort specification therefore specifies the differents kinds of sets contained in a model, and how they relate to each other.
|
||||
|
||||
\paragraph{Constructor specification}
|
||||
We can also add constructors to a sort specification to make a complete GAT. Those constructors rather describe elements of the sets contained in the model, previously defined by the sort declaration.
|
||||
We can also add constructors to a sort specification. Those constructors specify elements of the sets contained in the model, previously defined by the sort declaration.
|
||||
For example, for the previous sort specification, one can add the following constructors:
|
||||
|
||||
\vspace{1em}
|
||||
\renewcommand\arraystretch{1.5}
|
||||
\begin{tabular}{p{.37\textwidth}|p{.6\textwidth}}
|
||||
$\operatorname{unit} : (\Gamma : \Con) \to \Ty\;\Gamma$ & In any context $\Gamma \in X_\Con$, an element$\operatorname{unit}\;\Gamma \in X_\Ty(\Gamma)$.\\
|
||||
$\operatorname{unit} : (\Gamma : \Con) \to \Ty\;\Gamma$ & In any context $\Gamma \in X_\Con$, a type $\operatorname{unit}(\Gamma) \in X_\Ty(\Gamma)$.\\
|
||||
|
||||
$\operatorname{tt}: (\Gamma : \Con) \to \Tm\;\Gamma\;(\operatorname{unit}\;\Gamma)$ & In any context $\Gamma \in X_\Con$, an element $\operatorname{tt}\;\Gamma \in X_\Tm(\Gamma,\operatorname{unit}\;\Gamma)$.
|
||||
$\operatorname{tt}: (\Gamma : \Con) \to \Tm\;\Gamma\;(\operatorname{unit}(\Gamma))$ & In any context $\Gamma \in X_\Con$, an element $\operatorname{tt}(\Gamma) \in X_\Tm(\Gamma,\operatorname{unit}(\Gamma))$.
|
||||
\end{tabular}
|
||||
\vspace{1em}
|
||||
|
||||
@ -89,9 +89,9 @@
|
||||
$\dots$
|
||||
\end{tabular}
|
||||
|
||||
This process has not been formally justified, although it has been used like in Phipippo Sestini's thesis.
|
||||
This process is useful when studying GATs, as it allows to restrict a study to GATs with only two sorts without loss of generality. It has been used in Philippo Sestini's thesis, although it has not been formally justified.
|
||||
|
||||
\todo{choose}
|
||||
\todo{Ça veut dire qqch que le \enquote{process} pas été \enquote{justified} ?}
|
||||
|
||||
\begin{quote}
|
||||
Many instances of multi-sorted IITs [IITs are variants of GATs] can be reduced to equivalent two-sorted IITs, via a systematic reduction method originally observed by Zongpu (Szumi) Xie. We are not aware of a formal proof of this construction for arbitrary IITs, but we conjecture that it does apply to all instances of induction-induction and consequently that it shows two-sorted IITs are enough to represent any specifiable IIT.
|
||||
@ -99,7 +99,7 @@
|
||||
|
||||
\paragraph{Goal}
|
||||
|
||||
The goal of my internship was to study and undestrand the relationship between the categories of models of an original GAT and the category of models of the transformed GAT, in order to legitimate this transformation.
|
||||
The goal of my internship was to study and understand the relationship between the categories of models of an original GAT and the category of models of the transformed GAT, in order to legitimate this transformation.
|
||||
|
||||
We constructed a coreflection between those two categories, whose formal definition is given in next section. It consists of an adjunction $F \vdash G$ between the category $\CC$ of the models of the GAT and the category $\BB$ of the models of the two-sortified GAT, where G is full and faithful.
|
||||
|
||||
@ -116,6 +116,34 @@
|
||||
|
||||
\section{Construction of the coreflection}
|
||||
|
||||
\paragraph{Structure of the proof}
|
||||
|
||||
We will only only formalize the transformation for \emph{sort specification} (i.e. lists of sort declaration). We can add constructors on a later step, as described in \autoref{sec:constructors2trans}.
|
||||
|
||||
This proof is a big 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 \inlinetodo{MISSING REF}.
|
||||
|
||||
At the $i$-th recursion step, we will build the following objects :
|
||||
\begin{itemize}
|
||||
\setlength\itemsep{-1ex}
|
||||
\item The category of models of the GAT $\CC_i$
|
||||
\item The category of models of the transformed GAT $\BB_i$
|
||||
\item A functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$ and $R_0^i : \BB_i \to \BB_0$, taking track of the fixed sort specification of the transformed GAT. \inlinetodo{Mal Dit, est-ce nécessaire ?}
|
||||
\item An operator $\tl^i : \BB_i \times \BB_0 \to \BB_i$ along with morphisms $\inj_1^i : X \to X \tl Y$
|
||||
\item A functor $F_i : \BB_i \to \CC_i$
|
||||
\item A functor $G_i : \CC_i \to \BB_i$
|
||||
\item An adjunction between them $F_i \vdash G_i$
|
||||
\item A proof that $F_iG_i \cong \Id_{\CC_i}$ (i.e. $F_i \vdash G_i$ make up a coreflection)
|
||||
\item A proof that $F_i\inj_1$ is an isomorphism
|
||||
\item A proof that
|
||||
\end{itemize}
|
||||
|
||||
We will construct both categories $\CC$ and $\BB$ sort declaration by sort declaration in one big recursive process. At each step, we will build the categories $\CC_i$ and $\BB_i$, the adjunction $F_i \vdash G_i$, and keep some invariants that will be stated in \autoref{sec:hypotheses}.
|
||||
|
||||
At the i-th recursion step, we will build the category $\CC_i$ which is the category of models of the $i$ first sorts of the sort specification. Likewise, $\BB_i$ will be the category of models of the 2-sorted $i$ first sorts of the sort specification.
|
||||
|
||||
The overall recursive construction of the categories and of the adjunctions $F_i \vdash G_i$ is given below.
|
||||
|
||||
|
||||
\subsection{Preliminaries}
|
||||
|
||||
\paragraph{Category of models of the two-sort sort specification}
|
||||
@ -633,6 +661,9 @@
|
||||
|
||||
\todo{(small) Show that it is actually a functor (should be trivial), potentially add a diagram}
|
||||
|
||||
\subsection{Adding 2-transformation of constructors}
|
||||
\label{sec:constructors2trans}
|
||||
\todo{Describe the process}
|
||||
|
||||
\subsection{Overview}
|
||||
|
||||
@ -892,5 +923,6 @@
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
@ -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":6,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":8,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":1,"id":9,"label":{"kind":"normal","label":"H_i\\eta^{FG}_{i-1} \\circ g","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":10,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_0^{i-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":0,"id":11,"label":{"kind":"normal","label":"g","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":12,"label":{"kind":"normal","label":"H_i\\text{HR}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4}],"nodes":[{"id":0,"label":{"isMath":true,"label":"B","pos":[100,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"B","pos":[300,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"A","pos":[678,100],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}(G_{i-1}X \\oplus L_0^{i-1}\\Hbar_\\bullet(G_{i-1}X,(B,g)))","pos":[678,211],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"H_iF_{i-1}G_{i-1}X","pos":[300,211],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"H_iX","pos":[100,211],"zindex":-10000}}],"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":6,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":8,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":1,"id":9,"label":{"kind":"normal","label":"H_i\\eta^{FG}_{i-1} \\circ g","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":10,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_0^{i-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":0,"id":11,"label":{"kind":"normal","label":"g","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":12,"label":{"kind":"normal","label":"H_i\\text{HR}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":4}],"nodes":[{"id":0,"label":{"isMath":true,"label":"B","pos":[100,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"B","pos":[300,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"A","pos":[678,100],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}(G_{i-1}X \\oplus L_0^{i-1}\\Hbar_\\bullet(G_{i-1}X,(B,g)))","pos":[678,211],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"H_iF_{i-1}G_{i-1}X","pos":[300,211],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"H_iX","pos":[100,211],"zindex":-10000}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
@ -49,7 +49,6 @@
|
||||
|
||||
\usepackage[textheight=0.75\paperheight]{geometry}
|
||||
|
||||
\usepackage{csquotes}
|
||||
\usepackage[lighttt]{lmodern}
|
||||
\usetikzlibrary{shapes.geometric,positioning,backgrounds}
|
||||
|
||||
@ -65,8 +64,6 @@
|
||||
\newcommand{\longdash}{\:\textrm{---}\:}
|
||||
\newcommand\hole{\left[\raisebox{-0.25ex}{\scalebox{1.2}{$\cdot$}}\right]}
|
||||
\newcommand\bracket[1]{\!\left[#1\right]}
|
||||
\newcommand{\ssi}{\quad\text{\underline{ssi}}\quad}
|
||||
\newcommand\eng[1]{\textit{\foreignlanguage{english}{#1}}}
|
||||
\newcommand\spacebar{\;|\;}
|
||||
\def\nDownarrow{\not\mspace{1mu}\Downarrow}
|
||||
\let\pprec\preccurlyeq
|
||||
@ -114,8 +111,10 @@
|
||||
\newcommand\FamSet{{\ensuremath{\operatorname{\mathcal{F}am\mathcal{S}et}}}}
|
||||
\newcommand\Hom{{\ensuremath{\operatorname{\mathcal{H}om}}}}
|
||||
\newcommand\this{{\ensuremath{\operatorname{\texttt{this}}}}}
|
||||
\newcommand\Hbar{{\ensuremath{\overline{H}}}}
|
||||
\newcommand\Hbar{{\ensuremath{K}}}
|
||||
\newcommand\dash{{\;\textrm{---}\;}}
|
||||
\renewcommand\enquote[1]{``#1''}
|
||||
\newcommand\tl{{\triangleleft}}
|
||||
|
||||
\DeclareMathOperator{\inj}{inj}
|
||||
\DeclareMathOperator{\id}{id}
|
||||
|
||||
78
Report/synthese.tex
Normal file
78
Report/synthese.tex
Normal file
@ -0,0 +1,78 @@
|
||||
\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}
|
||||
Loading…
x
Reference in New Issue
Block a user