Commit 45b6ca61 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

k

parent 20dbb785
......@@ -86,6 +86,8 @@
\end{mdframed}}
\newcommand\indcond[1]{(see Cond. \ref{#1})}
\newcommand{\VTyp}{\mcal{V}al_{T}}
\title{Interpr\'etation des types positifs}
\author{Guillaume Genestier}
\date{Mai 2019}
......@@ -101,42 +103,45 @@
\section{Accessibilit\'e}
\begin{defi}[Constructeur de type]
On note \[CTyp=\enscond{F\in\FTyp}{F\text{ n'est pas la t\^ete du membre gauche d'une r\`egle.}}\].
On note \[CTyp=\enscond{F\in\FTyp}{F\text{ n'est pas la t\^ete du membre gauche d'une r\`egle.}}\]
\end{defi}
\begin{nots}
On note \[\VTyp=\enscond{C\,\bar t}{C\in\CTyp, \valabs{\bar t}=\arity(C), \text{pour tout }i, t_i\in\SN}\]
\end{nots}
\begin{defi}[Ordre sur les types]
On se donne $\FTyp'\subseteq\FTyp$ tel que $\CTyp\subseteq\FTyp'$ et $\succ$ un pr\'e-ordre bien fond\'e sur les symboles de $\FTyp'$.
\end{defi}
\begin{defi}[Statut]
On munit chaque $F\in\FTyp'$ d'arit\'e $k$ d'un tuple d'entiers inf\'erieurs \`a $k$ : $(i_1,\dots,i_n)$.
\end{defi}
\begin{defi}[Ordre sur les types construits]
Soit $F\in\FTyp'$ de statut $(i_1,\dots,i_n)$ et $F'\in\FTyp'$ de statut $(j_1,\dots,j_{n'})$.
On a $F\,\bar t\>F'\,\bar u$ si l'une des 2 conditions suivantes sont v\'erifi\'ees :
On a $F\,\bar t\>F'\,\bar u$ si l'une des 3 conditions suivantes sont v\'erifi\'ees :
\begin{itemize}
\item $F\succ F'$,
\item $F\approx F'$ et $(t_{i_1},\dots,t_{i_n})\unrhd_{lex}(u_{j_1},\dots,u_{j_{n'}})$.
\item $F\approx F'$ et $(t_{i_1},\dots,t_{i_{\min(n,n')}})\rhd_{lex}(u_{j_1},\dots,u_{j_{\min(n,n')}})$,
\item $F\approx F'$, $(t_{i_1},\dots,t_{i_{\min(n,n')}})=(u_{j_1},\dots,u_{j_{\min(n,n')}})$ et si $F\in\CTyp$ alors $F'\in\CTyp$.
\end{itemize}
Remarquons que l'ordre strict est d\'efini comme l'ordre large, sauf que $\rhd$ remplace $\unrhd$ dans la derni\`ere condition.
Remarquons que l'ordre strict est d\'efini comme l'ordre large, sauf que ``$F\in\FTyp'\setminus\CTyp$ et $F'\in\CTyp$'' remplace ``si $F\in\CTyp$ alors $F'\in\CTyp$'' dans la derni\`ere condition.
\end{defi}
\remark{Si pour chaque classe d’équivalence pour $\approx$,
il existe un entier $n$ tel que les $st(C)$ sont de taille inférieure à $n$,
alors $>$ est bien fondé.}
\todo{On aimerait utiliser ce que l'on d\'efinit un peu plus tard dans cette d\'efinition, que ce soit $\rhd_{acc}$ pour pouvoir g\'erer un constructeur de type $\Pi(f:Nat\impli Ord).(\Pi(n:Nat).T\,(f\,n))\impli T\,(lim\,n)$, ou SCT pour ne pas se restreindre \`a un ordre lexicographique. (Attention ici, la pr\'esence de = sur la diagonale des boucles idempotentes ne suffit pas dans le cas o\`u l'on d\'esire un inf\'erieur large).}
\todo{On aimerait utiliser ce que l'on d\'efinit un peu plus tard dans cette d\'efinition, que ce soit $\rhd_{acc}$ pour pouvoir g\'erer un constructeur de type $(f:Nat\impli Ord)\impli((n:Nat)\impli T\,(f\,n))\impli T\,(lim\,n)$, ou SCT pour ne pas se restreindre \`a un ordre lexicographique. (Attention ici, la pr\'esence de = sur la diagonale des boucles idempotentes ne suffit pas dans le cas o\`u l'on d\'esire un inf\'erieur large).}
\begin{defi}[Types gel\'es]
Pour $F\in\FTyp'$, $\bar t$ des termes tels que $\valabs{\bar t}=\arity(F)$, on d\'efinit les deux grammaires :
\begin{align*}
T_{\<F\bar l}&::=\Pi(x:U_{<F\bar l}).T_{\<F\bar l}\,\mid\,F'\,u_1,\dots,u_{\arity(F')}&\text{where }F'\,\bar u\<F\,\bar l\\
T_{<F\bar l}&::=\Pi(x:U_{\<F\bar l}).T_{<F\bar l}\,\mid\,F'\,u_1,\dots,u_{\arity(F')}&\text{where }F'\,\bar u<F\,\bar l\\
T_{\<F\bar t}&::=\Pi(x:U_{<F\bar t}).T_{\<F\bar t}\,\mid\,F'\,u_1,\dots,u_{\arity(F')}&\text{o\`u }F'\,\bar u\<F\,\bar t\\
T_{<F\bar t}&::=\Pi(x:U_{\<F\bar l}).T_{<F\bar l}\,\mid\,F'\,u_1,\dots,u_{\arity(F')}&\text{o\`u }F'\,\bar u<F\,\bar t\\
\end{align*}
On note ces 2 ensembles $\Froz_{\<F\bar l}$ et $\Froz_{<F\bar l}$ respectivement.
On note ces 2 ensembles $\Froz_{\<F\bar t}$ et $\Froz_{<F\bar t}$ respectivement.
\end{defi}
\remark{Ici, on a d\'efini la positivit\'e non-stricte,
......@@ -153,7 +158,7 @@ on a $\valabs{l}=\arity(F)$ et $r\in\Froz_{\<F\bar l}$.
\todo{Supprimer la restriction interdisant les constructeurs de types d\'efinis.}
\remark{La pleine application de $C$ est impos\'ee par typage, ce n'\'etait pas utilde de la remettre ici.}
\remark{La pleine application de $C$ est impos\'ee par typage, ce n'\'etait pas utile de la remettre ici.}
\begin{defi}[Position accessible]
Soit $f\in\CObj$, tel que $\tau(f)=\Pi\overline{(x:T)}.C\,t_1\dots t_{\arity(C)}$, on a :
......@@ -164,6 +169,54 @@ on a $\valabs{l}=\arity(F)$ et $r\in\Froz_{\<F\bar l}$.
\section{Interpr\'etations}
Soit $\chi : \Part{\Lm}\setminus\emptyset\to\Lm$ une fonction de choix.
On laisse sous-entendu que tout d\'epend de $\chi$.
On discutera ensuite l'indiff\'erence \`a cette fonction.
\begin{defi}[Interpr\'etations de $\Type$ et des types]
Dans cette d\'efinition, $\alpha$ est un ordinal, $\mu$ est un ordinal limite, $X\in\VTyp\cup\ens{\bot}$ et $Y\in\VTyp$.
\begin{align*}
\interp{\Type}^0_\bot =& \emptyset\\
\interp{\Type}^{\alpha+1}_X =&
\interp{\Type}^\alpha_X\cup
\enscond{A\in\NTyp}{\text{pour tout }U, A\rew U \text{ implique }U\in\interp{\Type}^\alpha_X}\\
&\cup
\enscond{(x:A)\impli B}{A\in\interp{\Type}^\alpha_X\text{ et pour tout }a\in\interp{A}, \subst{B}{x}{a}\in\interp{\Type}^\alpha_X}\\
\interp{\Type}^\mu_X =&
\bigcup_{\alpha<\mu}\interp{\Type}^\alpha_X\\
\interp{\Type}^0_Y =&
\bigcup_{X<Y}\overline{\interp{\Type}_X}\cup\enscond{C\,\bar t\in\VTyp}{C\,\bar t\approx Y}\\
\omit\rlap{$\overline{\interp{\Type}_X}$ est le point fixe de la suite croissante $\paren{\interp{\Type}^\alpha_X}_\alpha$}
\end{align*}
Soit $C\,\bar t\in\VTyp$ avec $C\in\CTyp$.
On d\'efinit alors $\bar C=\enscond{C'\in\CTyp}{C'\approx C}=(C_1,\dots,C_n)$, o\`u l'on omet la conversion entre ensemble et tuple pour des questions de lisibilit\'e.
On d\'efinit alors :
\[
\deffonc{K_{C\bar t}}{\Part{\Lm}^n}{\Part{\Lm}^n}{(X_i)_{i\<n}}
{\paren
{\enscond{t\in\SN}
{\begin{array}{l}
\text{si }t\reww c\,v_1\dots v_m\text{ avec }c\in\CObj\\
\text{alors}
\left\{
\begin{array}{l}
\tau(c)=\overline{(x:T)}\impli (C_i\,\bar s)\\
m\>\arity(c)\\
\text{pour tout }j\in\Acc(c), v_j\in R_{C\bar t}(T_j,(X_k))\\
\end{array}
\right.\\
\end{array}
}
}_i
}
\]
avec $R_{C\bar t}(T,(X_k))=
\left\{
\begin{array}{ll}
X_i& \text{s'il y a des }\bar l\text{ tels que }T=C_i\,\bar l\\
\end{array}
\right.
\end{defi}
\end{document}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment