Commit 879a88f2 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Début débug interp

parent 14ae17f7
This diff is collapsed.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Interprétations}
\begin{defi}[Termes neutres]
Un terme est \emph{neutre} s'il est de la forme :
\begin{center}
\begin{tabular}{rlr}
$B$ & $::=(\lm (x:A).\,T)\,U_0\dots U_m$&$m\>0$\\
$b$ & $::=(\lm (x:A).\,t)\,u_0\dots u_m\mid x\,t_1\dots t_m\mid f\,t_1\dots t_n$&$m\>0$, $f\in\FObj\setminus\CObj$ et $n\>\arity(f)$\\
\end{tabular}
\end{center}
en fonction de s'il s'agit d'une famille ou d'un objet.
On note $\NTyp$ l'ensemble des \emph{familles neutres} et $\NObj$ celui des \emph{objets neutres}.
\end{defi}
\begin{coro}[Forme des types habités]
Chaque famille habitée est un produit, un type neutre ou une constante de type pleinement appliquée.
\end{coro}
\begin{proof}
Les abstractions et les symboles de la signature partiellement appliqués habitent dans des produits
et aucun produit n'est convertible avec une sorte.
D'après le \indlem{lem-Stratification} ces familles ne peuvent donc pas être habitées.
\end{proof}
\begin{nots}
On note
\[\mbb{F}_{inh}=\NTyp\cup\enscond{t\in\mbb{F}}{t\text{ est un produit ou une constante de type pleinement appliquée}}\]
\end{nots}
\begin{defi}[Interprétation des constructeurs de type]
Ici $\approx$ est la relation d'équivalence induite par $\preced$ et $\sim$ celle induite par $\<$.
\begin{itemize}
\item Soit $C$ une constante de type et $\bar l$ une suite de termes telle que $\valabs{\bar l}=\arity(C)$.
On définit la fonction
\[
\deffonc
{K_{C\bar l}}
{\Part{\Lambda}}
{\Part{\Lambda}}
{X}
{\enscond{t\in\SN(\rew\cup\surterm_{acc})}
{\begin{array}{l}
\text{si }t\reww c\,v_1\dots v_m\text{}
\left\{\begin{matrix}
c\in\CObj\\
m\>\arity(c)\\
\tau(c)=\Pi\overline{(x:T)}.(C'\,\bar s)\\
C'\approx C\\
\end{matrix}\right.\\
\text{alors pour tout }j\in\Acc(c),v_j\in R_{C\bar l}(T_j,X)\\
\end{array}}
}
\]
\[
\text{avec }
R_{C\bar l}(T,X)=
\left\{
\begin{array}{ll}
X &\text{ si } T\sim C\,\bar l\\
\multicolumn{2}{l}{\enscond{t\in\Lambda}
{\text{pour tout }u\in R_{C\bar l}(T_1,X), t\,u\in R_{C\bar l}(\subst{T_2}{x}{u},X)}
\text{ si } T=\Pi(x:T_1). T_2}\\
\mcal{I}_{C'\bar s}& \text{ si }T=C'\,\bar s\text{, et }C'\,\bar s< C\,\bar l\\
\end{array}
\right.
\]
Et $\mcal{I}_{C\bar l}$ est le plus petit point fixe de $K_{C\bar l}$.
\item si $C$ est un symbole défini, $\bar l$ une suite de termes telle que $\valabs{\bar l}=\arity(C)$ et $C\,\bar l\in\SN(\to)$,
\[\mcal{I}_{C\bar l}=\left\{\begin{array}{ll}
\SN(\to\cup\surterm_{acc})&\text{si }C\,\bar l\text{ est en forme normale,}\\
\mcal{I}_{(C\bar l)\Downarrow}&\text{sinon.}
\end{array}
\right.\]
\end{itemize}
\end{defi}
\begin{lem}[Monotonie de $K_{C\bar l}$]
\label{InterpDBonneDef}
Pour tous $C$ et $\bar l$, $K_{C\bar l}$ est croissante.
\end{lem}
\begin{proof}
Soit $X\subseteq Y \in \Part{\Lambda}$ et $t\in K_{C\bar l}(X)$.
\begin{itemize}
\item
Si $t$ ne réduit vers aucun terme de la forme $c\,\bar s$$c$ est un constructeur d'un type dont la constante est dans $\bar C$,
alors $t\in K_{C\bar l}(Y)$, car $K_{C\bar l}(X)=\SN(\rew\cup\surterm_{acc})=K_{C\bar l}(Y)$.
\item
Si $t\reww c\,\bar v$ un constructeur pleinement appliqué d'un type dont la constante appartient à $\bar C$.
Alors $\tau(c)=\Pi\overline{(x:U)}. \,C_i\bar s$ et pour tout $j\in\Acc(c)$,
$v_j\in R_{C\bar l}(U_j,X)$.
Ici, par induction mutuelle sur le nombre de produit, on prouve que :
\begin{itemize}
\item pour tout $T\in\Froz_{\< C\bar l}$, $R_{C\bar l}(T,.)$ est croissante,
\item pour tout $T\in\Froz_{< C\bar l}$, $R_{C\bar l}(T,.)$ est décroissante.
\end{itemize}
Si $T$ n'est pas un produit, alors
\begin{itemize}
\item si $T\in\Froz_{< C\bar l}$, $R_{C\bar l}(T,X)$ est indépendant de $X$,
donc $R_{C\bar l}(T,.)$ est décroissante,
\item si $T\in\Froz_{\< C\bar l}$, $R_{C\bar l}(T,.)$ est croissante,
car la fonction constante et l'identité sont croissantes.
\end{itemize}
Si $T=\Pi(x:T_1). T_2$ est un produit, les arguments de contravariance-covariance,
avec l'hypothèse d'induction nous permettent de conclure.
Sans perdre en généralité, on suppose que $x$ n'apparaît pas dans $C\,\bar l$.
\begin{itemize}
\item Si $T\in\Froz_{<C\bar l}$.
Alors $T_1\in\Froz_{\<C\bar l}$ et $T_2\in\Froz_{<C\bar l}$.
Soit $X\subseteq Y\in\Part{\Lambda}$,
$t\in R_{C\bar l}(T,Y)$
et $u\in R_{C\bar l}(T_1,X)$.
Par hypothèse d'induction, $R_{C\bar l}(T_1,.)$ est croissante, donc $u\in R_{C\bar l}(T_1,Y)$.
Par définition de $R_{C\bar l}$,
$t\,u\in R_{C\bar l}(\subst{T_2}{x}{u},Y)$.
Puisque $x$ n'apparaît pas dans $C\,\bar l$,
si $T_2\in\Froz_{<C\bar l}$,
$\subst{T_2}{x}{u}\in\Froz_{<C\bar l}$ aussi.
Donc $R_{C\bar l}(\subst{T_2}{x}{u},.)$ est décroissante.
Par conséquent $t\,u\in R_{C\bar l}(\subst{T_2}{x}{u},X)$.
On peut alors conclure que $t\in R_{C\bar l}(T,X)$.
\item
Si $T\in\Froz_{\<C\bar l}$, la preuve est analogue.
\qedhere
\end{itemize}
\end{itemize}
\end{proof}
\begin{rmq}
Ce lemme nous garantit que $\mcal{I}_{C\bar l}$ est bien défini,
donc que la fonction $K_{C\bar l}$ elle-même est bien définie.
\end{rmq}
\begin{defi}[Fonction d'interprétation]
Soit
\[\deffonc{F}
{\mcal{F}_p(\Lambda,\Part{\Lambda})}{\mcal{F}_p(\Lambda,\Part{\Lambda})}
{I}{\enscond{(T,G(I)(T))}{T\in D(I)}}
\]
\begin{align*}
D : I \mapsto &
\enscond{T\in\Lambda_{inh}\cap\SN(\rew)}{\text{si }T\reww\Pi(x:A). B\text{, alors }
\begin{array}{l}
A\in\domain(I)\\
\text{pour tout } u\in I(A), \subst{B}{x}{u}\in \domain(I)
\end{array}}\\
G: (I,T) \mapsto &
\left\{\begin{array}{ll}
\mcal{I}_{C\bar u} &\text{si }T\Downarrow=C\,u_1\dots u_n\text{ avec }n\>\arity(C)\\
\enscond{t}{\text{pour tout }u\in I(A), t\,u\in I(\subst{B}{x}{u})} & \text{si }T\Downarrow=\Pi(x:A). B\\
\SN(\rew\cup\surterm_{acc}) & \text{si }T\Downarrow\in\NTyp\\
\end{array}\right.\\
\end{align*}
\end{defi}
\begin{lem}
$D$ est croissante.
\end{lem}
\begin{proof}
Soit $I\subseteq J$.
Soit $T\in D(I)$.
Donc $T\in\Lambda_{inh}\cap\SN$.
Si $T\reww \Pi(x:A). B$, on a $A\in\domain(I)$ et pour tout $u\in I(A)$, $\subst{B}{x}{u}\in\domain(I)$.
Comme $I\subseteq J$, on a $\domain(I)\subseteq\domain(J)$ et pour tout $U\in\domain(I)$, $I(U)=J(U)$.
Par conséquent, $A\in\domain(J)$ et pour tout $u\in J(A)$, $\subst{B}{x}{u}\in \domain(J)$,
donc $T\in D(J)$.
\end{proof}
\begin{lem}[Monotonie]
$F$ est croissante.
\end{lem}
\begin{proof}
Soit $I\subseteq J$.
Soit $T\in D(I)\subseteq D(J)$.
On doit prouver $G(I,T)=G(J,T)$.
\begin{itemize}
\item
Si $T\Downarrow=C\,v_1\dots v_n$$C\in\CTyp$,
alors $G(I,T)=\mcal{I}_{C\bar u}=G(J,T)$.
\item
Si $T\Downarrow\in\NTyp$,
alors $G(I,T)=\SN(\rew\cup\surterm_{acc})=G(J,T)$.
\item
Si $T\Downarrow=\Pi(x:A). B$,
comme $I\subseteq J$,
on a $I(A)=J(A)$ et pour tout $u\in I(A)$, $I(\subst{B}{x}{u})=J(\subst{B}{x}{u})$.
Donc $G(I,T)=
\enscond{t}{\text{pour tout }u\in I(A), t\,u\in I(\subst{B}{x}{u})}=
\enscond{t}{\text{pour tout }u\in J(A), t\,u\in J(\subst{B}{x}{u})}=
G(J,T)$.
\end{itemize}
Donc $F(I)\subseteq F(J)$.
\end{proof}
\begin{defi}[Plus petit point fixe $\mcal{J}$]
On nomme $\mcal{J}$ le plus petit point fixe de $F$.
\end{defi}
\begin{defi}[Interprétation des types]
On définit $\interp{\Type}$ comme étant le domaine de $\mcal{J}$,
et pour tout $A\in\interp{\Type}$, on définit $\interp{A}$ comme $\mcal{J}(A)$.
\end{defi}
\todo{Ici on utilise le théorème d'Abian et Brown (ou Markowski),
mais je préférerais utiliser des ordinaux (en pratique, ils apparaissent un peu plus loin).}
\begin{defi}[Interprétation de $\Kind$]
On définit $\interp{\Kind}$ comme le plus petit point fixe de la fonction croissante définit sur $\Part{\mbb{K}}$:
\[
X \mapsto \ens{\Type}\cup\enscond{\Pi(x:A).K}{A\in\interp{\Type}\text{ and for all }a\in\interp{A}, \subst{K}{x}{a}\in X}
\]
\end{defi}
\todo{On montre que cette fonction est croissante par induction sur le nombre de produits.
On peut faire ça dans les kinds, car les substitutions ne peuvent pas faire apparaître de produits.}
\begin{defi}[Interprétation des kinds]
On définit inductivement les interprétations des kinds dans $\interp{\Kind}$ par :
\begin{itemize}
\item $\interp{\Type}$ est défini plus haut,
\item $\interp{\Pi(x:A). K}=\enscond{t}{\text{pour tout }u\in\interp{A}, t\,u\in\interp{\subst{K}{x}{u}}}$.
\end{itemize}
\end{defi}
\todo{Encore une fois $\subst{K}{x}{u}$ est plus petit que $\Pi(x:A). K$.
Faire une induction sur le nombre de produits est possible dans les kinds.}
\begin{rmq}[Invariance par réduction]
Comme $\interp{T}$ est définie exclusivement à partir de $T\Downarrow$,
pour tout $T$ telle que $\interp{T}$ est définie,
pour tout $T'$ telle que $T\rew T'$, on a $\interp{T}=\interp{T'}$.
\end{rmq}
\section{Ordonnabilit\'e}
\begin{defi}[Constructeurs de type]
On se donne un pr\'e-ordre bien fond\'e $\preced$ sur $\FTyp$ .
\end{defi}
\todo{Est-ce que c'est vraiment utile de mettre tout le monde dans le pré-ordre ?}
\begin{defi}[Statut]
On munit chaque $C\in\FTyp$ d'arit\'e $k$ d'un tuple d'entiers inf\'erieurs \`a $k$, $(i_1,...,i_j)$.
\end{defi}
\begin{defi}[Ordre sur les constructeurs de type]
Soit $C$ de statut $(i_1,\dots,i_n)$ et $C'$ de statut $(j_1,\dots,j_{n'})$.
On a $C\,\bar l\>C'\,\bar u$ si l'une des 2 conditions suivantes est remplie :
\begin{itemize}
\item $C\succ C'$,
\item $C\approx C'$ et $(l_{i_1},\dots,l_{i_{\min(n,n')}})\trianglerighteq_{lex}(u_{j_1},\dots,u_{j_{\min(n,n')}})$,
\end{itemize}
\end{defi}
Remarquons que l'ordre strict est d\'efini comme l'ordre large, sauf que $\rhd$ remplace $\trianglerighteq$ dans la derni\`ere condition.
\todo{Si pour chaque classe d'\'equivalence pour $\approx$,
il existe un entier $n$ tel que les $st(C)$ sont de taille inf\'erieure \`a $n$,
alors $>$ est bien fond\'e.}
\begin{lem}
Pour tout $\sigma$, tout $C,D\in\FTyp$ et toutes familles de termes $\bar s,\bar t$ de la même taille que l'arité des symboles,
$C\,\bar s\>D\,\bar t$ implique $C\,(\bar s\sg)\>D\,(\bar t\sg)$.
\end{lem}
\begin{lem}
Pour tout $\sigma$, tout $C,D\in\FTyp$ et toutes familles de termes $\bar s,\bar t$ de la même taille que l'arité des symboles,
$C\,\bar s>D\,\bar t$ implique $C\,(\bar s\sg)>D\,(\bar t\sg)$.
\end{lem}
\begin{proof}
Cette propriété vient du fait que la même propriété est vraie pour $\trianglerighteq$ et $\rhd$.
\end{proof}
\begin{defi}[Frozen type]
Pour $C\in\FTyp$, on définit les grammaires suivantes :
\begin{align*}
T_{\<C\bar l}::=& \Pi(x:U_{<C\bar l}). T_{\<C\bar l}\,\mid\,C'\,u_1\dots u_{\arity(C')}&\text{}C'\,\bar u\< C\,\bar l\\
U_{<C\bar l}::=& \Pi(x:T_{\<C\bar l}). U_{<C\bar l}\,\mid\,C'\,u_1\dots u_{\arity(C')}&\text{}C'\,\bar u< C\,\bar l\\
\end{align*}
On note ces ensembles par $\Froz_{\<C\bar l}$ et $\Froz_{<C\bar l}$ respectivement.
\end{defi}
\begin{cond}{Frozen rewriting}
Pour tout $C\in\FTyp$, s'il y a une règle $C\,\bar l\rul r$, alors $\valabs{l}=\arity(C)$ et $r\in\Froz_{\<C\bar l}$.
\end{cond}
\todo{On d\'efinit ici la positivit\'e non-stricte.
Dans quelle mesure complique-t-elle les preuves ?
J'ai l'impression que tout marche bien.}
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