Commit 1e6b820d authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

acc et ordonnabilité in English

parent bc17dafe
\section{Accessibilité}
\section{Accessibility}
\begin{defi}[Constante de type]
$\CTyp=\enscond{C\in\FTyp}{C\text{ n'est défini par aucune règle}}$
\end{defi}
\begin{defi}[Constructeurs]
\[\CObj=\enscond{f\in\FObj}{\tau(f)=\Pi\overline{(x:T)}. C\,t_1\dots t_{\arity(C)} \text{ avec }C\in\CTyp}.\]
\begin{defi}[Constructors]
\[\CObj=\enscond{f\in\FObj}{\tau(f)=\Pi\overline{(x:T)}. C\,t_1\dots t_{\arity(C)} \text{ with }C\in\CTyp}.\]
\end{defi}
\begin{rmq}
La contrainte de totalité de l'application n'est pas une nouvelle contrainte.
En effet, si $C$ est partiellement appliqué, il n'habite pas dans une sorte,
et le produit ne peut être typé.
The constraint on the totality of the application is not a new constraint.
Indeed, if $C$ is partially applied it does not live in a sort,
hence the product cannot be typed.
\end{rmq}
\todo{
Il y a en revanche une vraie restriction ici,
un type défini ne peut pas avoir de constructeurs.
Il faudra se débarrasser de cette restriction.
There is a real restriction here, rewritable types do not have constructors.
}
\begin{defi}[Position accessible]
Pour $f\in\CObj$, où $\tau(f)=\Pi\overline{(x:T)}.C\,t_1\dots t_{\arity(C)}$,
on définit
\[\Acc(f)=\enscond{i\<\arity(f)}{T_i\in\Froz_{\< C\bar t}}.\]
\begin{defi}[Accessible position]
For $f\in\CObj$, where $\tau(f)=\Pi\overline{(x:T)}.C\,t_1\dots t_{\arity(C)}$,
we define
\[\Acc(f)=\enscond{i\<\arity(f)}{T_i\in\Froz_{\< C}}.\]
\end{defi}
\begin{defi}[Ordre associé aux sous-termes accessibles]
On définit $\surterm_{acc}$ comme étant la clôture transitive de
\begin{defi}[Order associated to accessible subterms]
We define $\surterm_{acc}$ as the transitive closure of
$\paren{f\,t_1\dots t_{\arity(c)}}\surterm_{acc}(t_i\,\bar u)$,
$f\in\CObj$, $i\in\Acc(f)$ et $\bar u$ est une suite arbitraire de termes.
where $f\in\CObj$, $i\in\Acc(f)$ and $\bar u$ is an arbitrary sequence of terms.
\end{defi}
\todo{
Cette définition a l'air vraiment violente.
Ce n'est peut-être pas optimale.
This definition is really violent.
It is not well-founded.
It does not seem to be a problem, but I must stay cautious.
}
\section{Ordonnabilit\'e}
\section{Ordering}
\begin{defi}[Constructeurs de type]
On se donne un pr\'e-ordre bien fond\'e $\preced$ sur $\FTyp$ .
\begin{defi}[Type constructors]
\[\CTyp=\enscond{C\in\FTyp}{C\text{ is not the head of any rule}}\]
We suppose given a well-founded pre-order $\preced$ on $\CTyp$ .
\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 :
For $C\in\CTyp$, we define the following grammars :
\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\\
T_{\<C}::=& \Pi(x:U_{<C}). T_{\<C}\,\mid\,C'\,u_1\dots u_{\arity(C')}&\text{ where }C'\< C\\
U_{<C}::=& \Pi(x:T_{\<C}). U_{<C}\,\mid\,C'\,u_1\dots u_{\arity(C')}&\text{ where }C'< C\\
\end{align*}
On note ces ensembles par $\Froz_{\<C\bar l}$ et $\Froz_{<C\bar l}$ respectivement.
We denote those sets respectively by $\Froz_{\<C}$ and $\Froz_{<C}$.
\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.}
\todo{
We define here non-strict positivity.
To what extend does it make the proof harder?
I don't see any difficulty.
}
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