Commit d5d992b6 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

division du fichier

parent 879a88f2
......@@ -5,3 +5,4 @@
*.aux
*.log
*.out
*.backup
\ No newline at end of file
This diff is collapsed.
\section{Accessibilité}
\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}.\]
\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é.
\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.
}
\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}}.\]
\end{defi}
\begin{defi}[Ordre associé aux sous-termes accessibles]
On définit $\surterm_{acc}$ comme étant la clôture transitive de
$\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.
\end{defi}
\todo{
Cette définition a l'air vraiment violente.
Ce n'est peut-être pas optimale.
}
\section{Accessible Only rules}
\begin{defi}[Accessible position]
We define the function:
\[
\text{If }
\left\{\begin{array}{l}
t=c\,u_1\dots u_k\\
c\in\CObj\\
\tau(c)=\Pi(y_1:U_1)\dots(y_r:U_r). C\,\bar v\\
\exists W_{k+1}\dots W_{r},\bar v', T\theta\conv
\Pi(y_{k+1}:W_{k+1})\dots(y_r:W_r). C\,\bar v'
\end{array} \right.\]
\begin{align*}
\text{then: }\AccPosCstr : (t,T,\theta) &\mapsto
\ens{\eps}\cup\bigcup_{i\in\Acc(c)}\enscond{i.p}{p\in\AccPosCstr\paren{u_i,U_i,(\crochet{\overline{\sur{u}{y}}};\theta)}}\\
\text{else: }\AccPosCstr : (t,T,\theta) &\mapsto\ens{\eps}
\end{align*}
and the function:
\[
\AccPosHd : (f\,\bar t) \mapsto \bigcup_{i}\enscond{i.x}{x\in\AccPosCstr(t_i)}
\]
\end{defi}
\begin{defi}[Inferred type]
We now define the functions:
\begin{align*}
\InferTypeCstr : (p,c\,\bar u,\pi) &\mapsto
\left\{\begin{array}{ll}
T_i\crochet{\overline{\sur{u}{y}}}\pi&\text{ if }p=i\text{ and }\tau(c)=\Pi\overline{(y:T)}. U\\
\InferTypeCstr(p',u_i,(\crochet{\overline{\sur{u}{y}}};\pi))&\text{ if }p=i.p', p'\neq\eps\text{ and }\tau(c)=\Pi\overline{(y:T)}. U\\
\end{array}\right.\\
\InferTypeHd : (p,f\,\bar t) &\mapsto
\left\{\begin{array}{ll}
T_i\crochet{\overline{\sur{t}{x}}}&\text{ if }p=i\text{ and }\tau(f)=\Pi\overline{(x:T)}. U\\
\InferTypeCstr(p',t_i,\crochet{\overline{\sur{t}{x}}})&\text{ if }p=i.p', p'\neq\eps\text{ and }\tau(f)=\Pi\overline{(x:T)}. U\\
\end{array}\right.\\
\end{align*}
We must note here that if $p\in\AccPosHd(f\,\bar t)$ then $\InferTypeHd(p,f\,\bar t)$ is well-defined.
\end{defi}
\begin{defi}[AVO rules]
A rule $f\,l_1\dots l_n\rul r$ is \emph{Accessible Variables Only (AVO)} if
\begin{itemize}
\item there is a function $\phi:\FreeVar(r)\to\AccPosHd(f\,\bar l)$ such that $(f\,\bar l)|_{\phi(x)}=x$, for all $x\in\FreeVar(r)$.
\item $\D_r\vdash r:T_r$, where
\begin{itemize}
\item
$\D_r=\enscond{x:\InferTypeHd(\phi(x),f\,\bar l)}{x\in\FreeVar(r)}$ ordered by the alphabetical order on $\phi(x)$.
\item
$T_r=U\crochet{\overline{\sur{l}{x}}}$, where $\tau(f)=\Pi(x_1:T_1)\dots(x_n:T_n). U$.
\end{itemize}
\end{itemize}
\todo{What is the implication of these constraints on the form of rules?}
\end{defi}
\begin{lem}
AVO rules are valid.
\end{lem}
\begin{proof}
Let $f\,\bar l\rul r$ be a AVO rule with $\tau(f)=\Pi\overline{(x:T)}. U$, $\G=\overline{(x:T)}$ and $\pi=\crochet{\overline{\sur{l}{x}}}$.
Let $\sg$ be such that $\pi\sg\vDash\G$.
\begin{itemize}
\item
We have to prove that, $\sg\vDash\D_r$, meaning that for all $(y:V)\in\D_r$, $y\sg\in\interp{V\sg}$.
\begin{itemize}
\item
If $\phi(y)=i$, then by hypothesis, $x_i\pi\sg=y\sg\in\interp{T_i\pi\sg}$.
Yet $V=\InferTypeHd(i,f\,\bar l)=T_i\pi$.
So we have indeed $y\sg\in\interp{V\sg}$.
\item
If $\phi(y)=i.p'$ with $p'\neq\eps$, then by hypothesis, there is a $c\in\CObj$ and $u_1\dots u_k$ such that $l_i=c\,u_1\dots u_k$ since $p\in\AccPosHd(f\,\bar l)$.
Besides, $x_i\pi\sg=(c\,u_1\dots u_k)\sg\in\interp{T_i\pi\sg}$.
Since $T_i\pi\conv \Pi(y_{k+1}:V_{k+1})\dots(y_{\arity(c)}:V_{\arity(c)}). C\,\bar v$ for some $\bar v$, where $\tau(c)=\Pi(\overline{z:A}).C\,\bar v'$, we know that $(c\,\bar u)\sg\in\interp{\Pi\paren{(y_{k+1}:V_{k+1})\dots(y_{\arity(c)}:V_{\arity(c)}). C\,\bar v}\sg}$,
so for $j\in\Acc(c)$ with $j\<k$, we have $u_j\sg\in\interp{A_j\sg}=\interp{\InferTypeHd(i.j,f\,\bar l)\sg}$.
Following $p'$, we finally reach $y\sg\in\interp{V\sg}$.
\end{itemize}
\item
And to prove that $\D_r\vdash_{f\bar l}r:U\pi$.
This is the same typing as the one of $\D_r\vdash r:U\pi$,
but where (fun) followed by (app) is replaced by (fun') since the definition of a dependency pair ensures us that all the application in $r$ are smaller than $f\,\bar l$.
\end{itemize}
\end{proof}
\section{Candidats}
\begin{defi}[Candidats de réductibilité]
$S\in\Part{\Lambda}$ est un \emph{candidat de réductibilité} si
\begin{itemize}
\item $S\subseteq\SN(\rew)$,
\item $\enscond{u}{\text{il y a }t\in S,t\rew u}\subseteq S$,
\item si $t$ est neutre et $\enscond{u}{t\rew u}\subseteq S$ alors $t\in S$.
\end{itemize}
On note $\Candidates$ l'ensemble des candidats de réductibilité.
\end{defi}
\begin{lem}
$\SN(\rew\cup\surterm_{acc})$ est candidat.
\end{lem}
\begin{proof}
\begin{itemize}
\item
Par définition, on a $\SN(\rew\cup\surterm_{acc})\subseteq\SN(\rew)$.
\item
Soit $t\in\SN(\rew\cup\surterm_{acc})$ et $t'$ tel que $t\rew t'$.
On a $t'\in\SN(\rew\cup\surterm_{acc})$.
\item
Soit $t$ un terme neutre tel que $\enscond{u}{t\rew u}\subseteq\SN(\rew\cup\surterm_{acc})$.
Comme $t$ est neutre, il n'a pas en tête un symbole de $\CObj$,
donc $\enscond{u}{t(\rew\cup\surterm_{acc}) u}=\enscond{u}{t\rew u}$.
Par conséquent, $t\in\SN(\rew\cup\surterm_{acc})$.
\end{itemize}
\end{proof}
\begin{lem}[Reductibilité de $\mcal{J}$]
Pour tout $C\,\bar u$ avec $C\in\FTyp$ et $\valabs{u}=\arity(C)$, alors $\mcal{I}_{C\bar u}\in\Candidates$.
\end{lem}
\begin{proof}
\begin{itemize}
\item
Si $C\in \CTyp$.
On a $\mcal{I}_{C\bar u}=K_{C\bar u}(\mcal{I}_{C\bar u})$.
\begin{itemize}
\item
Par définition de $K_{C\bar u}$, on a $K_{C\bar u}(\mcal{I}_{C\bar u})\subseteq\SN(\rew)$.
\item
Soit $t\in\mcal{I}_{C\bar u}$ et $u$ tel que $t\rew u$.
Comme $t\in\SN(\rew\cup\surterm_{acc})$, $u\in\SN(\rew\cup\surterm_{acc})$ aussi.
Si $u\reww c\,\bar v$, alors $t\reww c\,\bar v$ donc la contrainte de réductibilité des arguments accessibles est remplie.
\item
Let $t$ be a neutral term such that $\enscond{u}{t\rew u}\subseteq\mcal{I}_0(T)$.
Since $t$ is neutral, $\enscond{u}{t(\rew\cup\surterm_{acc}) u}=\enscond{u}{t\rew u}$, so $t\in\SN(\rew\cup\surterm_{acc})$.
If $t\reww c\,\bar v$, then there is a $u\in\enscond{u}{t\rew u}$ such that $u\reww c\,\bar v$ so the constraint on the reducibility of the accessible arguments are fulfilled.
\end{itemize}
\item
\end{itemize}
\end{proof}
\begin{lem}[Product of candidates]\label{lem-product-candidate}
If $P\in\Candidates$ and, for all $a\in P$, $Q(a)\in\Candidates$, then $\enscond{t}{\text{for all }a\in P. t\,a\in Q(a)}\in\Candidates$.
\end{lem}
\begin{proof}
Let $R=\enscond{t}{\text{for all }a\in P. t\,a\in Q(a)}$.
\begin{itemize}
\item
Let $t\in R$.
We have to prove that $t\in\SN(\rew)$.
Let $x\in\Var$.
Since $P\in\Candidates$, $x\in P$.
So, $t\,x\in Q(x)$.
Since $Q(x)\in\Candidates$, $Q(x)\subseteq\SN(\rew)$.
Therefore, $t\,x\in\SN(\rew)$, and $t\in\SN(\rew)$.
\item
Let $t\in R$ and $t'$ such that $t\rew t'$.
We have to prove that $t'\in R$.
Let $a\in P$.
We have to prove that $t'\,a\in Q(a)$.
By definition, $t\,a\in Q(a)$ and $t\,a\rew t'a$.
Since $Q(a)\in\Candidates$, $t'a\in Q(a)$.
\item
Let $t$ be a neutral term such that $\enscond{u}{t\rew u}\subseteq R$.
We have to prove that $t\in R$.
Hence, we take $a\in P$ and prove that $t\,a\in Q(a)$.
Since $P\in\Candidates$, we have $a\in\SN(\rew)$ and $\enscond{u}{a\reww u}\subseteq P$.
We now prove that, for all $b\in\enscond{u}{a\reww u}$,
$t\,b\in Q(a)$, by induction on $\rew$.
Since $t$ is neutral, $t\,b$ is neutral too and it suffices to prove that $\enscond{u}{t\,b\rew u}\subseteq Q(a)$.
Since $t$ is neutral, $\enscond{u}{t\,b\rew u}=\enscond{u\,b}{t\rew u}\cup \enscond{t\,u}{b\rew u}$.
By induction hypothesis, $\enscond{t\,u}{b\rew u}\subseteq Q(a)$.
By assumption, $\enscond{u}{t\rew u}\subseteq R$.
So, $\enscond{u\,a}{t\rew u}\subseteq Q(a)$.
Since $Q(a)\in\Candidates$, $\enscond{u\,b}{t\rew u}\subseteq Q(a)$ too.
Therefore, $t\,a\in Q(a)$ and $t\in R$.\qedhere
\end{itemize}
\end{proof}
\begin{lem}[Reducibility of types]
\begin{enumerate}
\item $\interp{\Type}$ is a reducibility candidate,
\item for all $T\in\interp{\Type}$, $\interp{T}$ is a reducibility candidate.
\end{enumerate}
\end{lem}
\begin{proof}
\begin{enumerate}
\item
We must note that $\interp{\Type}=\domain(\mcal{I})$ and $\mcal{I}=F(\mcal{I})$.
So $\interp{\Type}=G(\mcal{I})$.
\begin{itemize}
\item
By definition of $G$, we have $\domain(\mcal{I})\subseteq\SN$.
\item
Let $T\in\domain(\mcal{I})$ and $T'$ such that $T\rew T'$.
We have $T'\in\SN$ since $T\in\SN$.
Assume now that $T'\reww \Pi(x:A). B$.
Then, $T\reww \Pi(x:A). B$, $A\in\domain(\mcal{I})$ and, for all $a\in \mcal{I}(A)$, $\subst{B}{x}{a}\in\domain(\mcal{I})$.
Therefore, $T'\in\domain(\mcal{I})$.
\item
Let $T$ be a neutral term such that $\enscond{U}{T\rew U}\subseteq\domain(\mcal{I})$.
Since $\domain(\mcal{I})\subseteq\SN$, $T\in\SN$.
Assume now that $T\reww \Pi(x:A). B$.
Since $T$ is neutral, there is $U$ such that $T\rew U$ and
$U\reww \Pi(x:A). B$.
Therefore, $A\in\domain(\mcal{I})$ and, for all $a\in \mcal{I}(A)$, $\subst{B}{x}{a}\in\domain(\mcal{I})$.
\end{itemize}
\item
Since $\mcal{F}_p(\Lambda,\Candidates)$ is a strictly inductive poset,
it suffices to prove that $\mcal{F}_p(\Lambda,\Candidates)$ is closed by $F$.
Assume that $J\in\mcal{F}_p(\Lambda,\Candidates)$.
We have to prove that $F(J)\in\mcal{F}_p(\Lambda,\Candidates)$,
that is, for all $T\in G(J)$, $H(J)(T)\in\Candidates$.
There are three cases:
\begin{itemize}
\item
If $T\Downarrow=\Pi(x:A). B$,
then $H(J)(T)=\enscond{t}{\text{for all }a\in J(A), t\,a\in J(\subst{B}{x}{a})}$.
By assumption, $J(A)\in\Candidates$ and, for $a\in J(A)$, $J(\subst{B}{x}{a})\in\Candidates$.
Therefore, $H(J)(T)\in\Candidates$.
\item
If $T\Downarrow$ is neutral, then $H(J)(T)=\SN(\rew\cup\surterm_{acc})\in\Candidates$.
\item
Otherwise, $T\Downarrow$ is a fully applied set constructor,
and we have already seen that $\mcal{I}_0(T)$ is a candidate.
\end{itemize}
\end{enumerate}
\end{proof}
\todo{Here we must state that the empty function is in $\mcal{F}_p(\Lambda,\Candidates)$,
that applying iteratively $F$ on the empty function is the way to compute the least fix-point
and that the limit is the same in both cases.}
\begin{lem}[Reducibility of kinds]
\begin{enumerate}
\item $\interp{\Kind}$ is a reducibility candidate,
\item for all $K\in\interp{\Kind}$, $\interp{K}$ is a reducibility candidate.
\end{enumerate}
\end{lem}
\begin{proof}
\begin{enumerate}
\item
Being a stable by reduction subset of $\SN$ is stable by the function defining $\interp{Kind}$
and there is no neutral kind.
\item
It is already proved for $\Type$ and done easily by induction for arrows
(see \indlem{lem-product-candidate}).
\end{enumerate}
\end{proof}
\todo{This is only a proof sketch.}
\section{Dependency pairs}
\begin{defi}[Dependency pairs]
Let $f\bar l>g\bar m$ if there are a rule $f\bar l\rul r\in\mcal{R}$,
such that $g\,\bar m$ occurs in $r$, $\valabs{\bar m}\<\arity(g)$
and if $\valabs{\bar m}<\arity(g)$ then $\bar m$ are all the arguments to which $g$ is applied (ie. $\bar m$ are the arguments to which $g$ is applied truncated to the arity of $g$).
\end{defi}
\begin{defi}[Instantiated call relation]
$f\,t_1\dots t_{\arity(f)} \call g\,u_1\dots u_{\arity(g)}$ if there are a dependency pair $f\,l_1\dots l_i>g\, m_1\dots m_j$
and a substitution $\sg$ such that for all $k\<i$, $t_k\reww l_k\sg$
and for all $k\<j$, $m_k\sg=u_k$.
\end{defi}
\begin{defi}[Computability closure]
Given $f\bar l$, let $\vdash_{f\bar l}$ be the relation defined as $\vdash$,
except the rules (app) and (fun) replaced by
\begin{prooftree}
\AxiomC{$\Gamma\vdash_{f\bar l} t: \Pi(x:A). B$}
\AxiomC{$\Gamma\vdash_{f\bar l} u:A$}
\RightLabel{
\begin{tabular}{l}
$t$ not of the form $g\,\bar l$\\
with $g$ a symbol of the signature
\end{tabular}}
\BinaryInfC{$\Gamma\vdash_{f\bar l} t\,u:\subst{B}{x}{u}$}
\end{prooftree}
\begin{prooftree}
\def\defaultHypSeparation{\hskip 0em}
\AxiomC{$\vdash_{f\bar l} \tau(g):s(g)$}
\AxiomC{$\overline{\G\vdash_{f\bar l} u:U\g}$}
\RightLabel{
$\left\{\begin{matrix}
\tau(g)=\Pi\overline{(x:U)}. V\\
\g=\crochet{\overline{\sur{u}{x}}}\\
g\,\bar u<f\,\bar l
\end{matrix}\right.$}
\BinaryInfC{$\Gamma\vdash_{f\bar l} g\,\bar u:V\g$}
\end{prooftree}
\end{defi}
\begin{defi}[Valid rule]
A rule $f\,\bar l\rul r$ with $\tau(f)=\Pi\overline{(x:T)}. U$, $\G=\overline{(x:T)}$ and $\pi=\crochet{\overline{\sur{l}{x}}}$ is \emph{valid} if
there is a context $\Delta$ such that :
\begin{itemize}
\item $\Delta\vdash_{f\,\bar l}r:U\pi$,
\item for all $\sg$ such that $\pi\sg\vDash\G$, we have $\sg\vDash\D$.
\end{itemize}
\end{defi}
\begin{defi}[Function applied to reducible terms]
Let
\[
\mbb{U}=\enscond{f\,\bar t}{
\begin{matrix}
\vdash\tau(f):s(f),\\
\tau(f)\in\interp{s(f)},\\
\tau(f)=\Pi\overline{(x:T)}. T',\\
T'\text{ is not an arrow}\\
\crochet{\overline{\sur{t}{x}}}\vDash\overline{(x:T)}
\end{matrix}
}
\]
\end{defi}
\begin{thm}
$\tau$ is valid if $\call$ terminates on $\mbb{U}$ and all rules in $\mcal{R}$ are valid.
\end{thm}
\begin{proof}
Let us take an $f\,\bar t\in\mbb{U}$.
Let $\tau(f)=\Pi\overline{(x:T)}. T'$.
Let $\G=\overline{(x:T)}$.
Let $\pi=\crochet{\overline{\sur{t}{x}}}$.
We want to prove that $f\in\interp{\Pi\overline{(x:T)}. T'}$ which by definition of the interpretation of a product is equivalent to show that $f\,\bar t\in\interp{T'\pi}$.
Since $\rew_{arg}$ and $\call$ terminate on $\mbb{U}$ and $\rew_{arg}\call \subseteq{\call}$,
we have that $\rew_{arg}\cup{\call}$ terminates on $\mbb{U}$.
We now prove that, $f\,\bar t\in\interp{T'\pi}$ by induction on ${\rew_{arg}}\cup{\call}$.
Because of the assumptions we have on rules, $f\,\bar t$ is neutral.
Hence, it suffices to prove that,
for all $u$ such that $f\,\bar t\rew u$, we have $u\in\interp{T'\pi}$.
There are two cases:
\begin{itemize}
\item $u=f\bar u$ with $\bar t\rew\bar u$.
Then, we can conclude by induction hypothesis.
\item There are $fl_1\dots l_k\rul r\in\mcal{R}$ and $\sg$ such that
$u=(r\sg)\,t_{k+1}\dots t_n$ and,
for all $i\in\{1,\dots,k\}$, $t_i=l_i\sg$.
Then, $\crochet{\overline{\sur{l}{x}}}\sg\vDash\G$.
Since all rules are valid, there is $\D$ such that $\D\vdash_{f\bar l} r:T'\pi$ and $\sg\vDash\D$.
We now prove that, for all $\G$, $u$ and $U$, if $\G\vdash_{f\bar l} u:U$ and
$\sg\vDash\G$, then $u\sg\in\interp{U\sg}$.
The proof is the same as for \indthm{TypImpliInterp} except for (fun) replaced by (fun').
In this case, for all $i$, we have $\G\vdash_{f\bar l} u_i:U_i\g$.
By induction hypothesis, $u_i\sg\in\interp{U_i\g\sg}$.
So, $\g\sg\vDash\Sg$ and $g\,\bar u\sg\in\mbb{U}$.
Now, $g\,\bar u\sg\tilde{<}f\,\bar l\sg$ since $g\,\bar u<f\,\bar l$.
Therefore, by induction hypothesis, $g\,\bar u\sg\in\interp{V\g\sg}$.
\end{itemize}
\end{proof}
\section{Size-Change Termination}
\begin{defi}[Size Matrix]
To a dependency pair $f\,l_1\dots l_p>g\,m_1\dots m_q$.
We associate the matrix $(a_{i,j})_{i\leq\arity{f},j\leq\arity{g}}$ where:
\begin{itemize}
\item if $l_i\surterm_{acc} m_j$, then $a_{i,j}=-1$;
\item if $l_i=m_j$, then $a_{i,j}=0$;
\item otherwise $a_{i,j}=\infty$ (in particular if $i>p$ or $j>q$).
\end{itemize}
\end{defi}
\begin{defi}[Call graph]
The \emph{call graph} $\mcal{G}(\Rules)$ associated to $\Rules$ is the directed labeled graph on the defined symbols of $\FObj\cup\FTyp$ such that there is an edge between $f$ and $g$ iff there is a dependency pair $f\,l_1\dots l_p>g\,m_1\dots m_q$.
This edge is labeled with the size matrix associated to this dependency pair.
\end{defi}
\begin{defi}[Size-Change Termination]
$\Rules$ is \emph{size-change terminating (SCT)} if,
in the transitive closure of $\mcal{G}(\Rules)$ (using the max-plus semi-ring to multiply the matrices labeling the edges),
all idempotent matrices labeling a loop have some $-1$ on the diagonal.
\end{defi}
\begin{lem}\label{lem-sct}
$\call$ terminates on $\mbb{U}$ if $\FTyp\cup\FObj$ is finite and $\Rules$ is SCT.
\end{lem}
\begin{proof}
Suppose that there is an infinite sequence
$\chi=f_1\,\bar t_1\call f_2\,\bar t_2\call\dots$.
Then, there is an infinite path in the call graph going through nodes labeled by $f_1,f_2,\dots$.
Since $\FTyp\cup\FObj$ is finite, there is a symbol $g$ occurring infinitely often in this path.
So, there is an infinite sequence $(g\,\bar u_1),(g\,\bar u_2),\dots$ extracted from $\chi$.
Hence, for every $i,j\in\N^*$, there is a matrix in the transitive closure of the graph which labels the loops of $g$ corresponding to the relation between $\bar u_i$ and
$\bar u_{i+j}$.
By Ramsey's theorem, there is an infinite sequence $\phi_i$ and a matrix $M$ such that $M$ corresponds to all the transitions $(g,\bar u_{\phi_i}),(g,\bar u_{\phi_j})$ with
$i\neq j$.
$M$ is idempotent, since $(g,\bar u_{\phi_i}),(g,\bar u_{\phi_{i+2}})$ is labeled by $M^2$ by definition of the transitive closure and by $M$ due to Ramsey's theorem, so $M=M^2$.
Since, by hypothesis $\Rules$ satisfies SCT, there is $j$ such that $M_{j,j}$ is $-1$. So, for all $i$, $u^{(j)}_{\phi_{i}}(\reww\surterm_{acc})^{+} u^{(j)}_{\phi_{i+1}}$, which contradicts the fact that $(\rew\cup\surterm_{acc})$ is well-founded on $\mbb{U}$.
\end{proof}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{thm}\label{thm-sn}
$\rew=(\rew_\beta\cup\rew_{\Rules})$ terminates on terms typable in $\lm\Pi/\Rules$
if
\begin{itemize}
\item $\rew$ is confluent,
\item $\rew$ preserves typing,
\item $\FTyp\cup\FObj$ is finite,
\item $\Rules$ is valid (for instance AVO),
\item $\Rules$ is $\SCT(\surterm_{acc})$.
\end{itemize}
\end{thm}
\section{Syntaxe}
\begin{defi}[Sortes]
On considère $\Sort=\ens{\Type,\Kind}$.
\end{defi}
\begin{defi}[Variables]
Soit $\Var$ un ensemble infini de \emph{variables}.
\end{defi}
\begin{defi}[Signature]
Soit $\Func$ un ensemble de symboles de fonction.
\end{defi}
\begin{cond}{SymbolSetsDistinct}
On impose que $\Sort$, $\Var$, $\FTyp$ et $\FObj$ soient 2 à 2 disjoints.
\end{cond}
\begin{defi}[Fonction de sortage]
On suppose donnée une \emph{fonction de sortage} $s:\Func\to\Sort$.
On note alors $\FObj=\enscond{f\in\Func}{s(f)=\Type}$ et $\FTyp=\enscond{f\in\Func}{s(f)=\Kind}$.
\end{defi}
\begin{defi}[Termes (version non-stratifiée)]
On a la grammaire :
\begin{center}
\begin{tabular}{rlr}
$t,u$ & $::=\Kind\mid\Type\mid\Pi(x:t). u\mid\lambda (x:t). u\mid t\,u\mid f\mid x$&$f\in\Func$, $x\in\Var$\\
\end{tabular}
\end{center}
On note $\Terms$ l'ensemble des termes.
\end{defi}
\begin{defi}[Contextes]
On définit la grammaire suivante, où $x$ est une variable et $T$ est un terme :
\begin{center}
\begin{tabular}{rl}
$\Gamma$ & $::=[]\mid\Gamma,x:T$
\end{tabular}
\end{center}
\end{defi}
\begin{defi}[Fonction de typage]
On suppose donnée une fonction $\tau:\Func\to\Terms$.
\end{defi}
\begin{cond}{Types clos}
Pour tout symbole $f$, $\tau(f)$ est clos.
\end{cond}
\begin{defi}[Terme restreint à une position]
Soit $t$ un terme et $p$ un mot sur l'alphabet $\ens{\circ,\bullet}\cup\N$.
\[
\restrict{t}{\eps}=t \qquad
\restrict{t}{a::s}=\left\{\begin{array}{l}
\restrict{t_a}{s} \text{ si } t=t_0\,t_1\dots t_n, n>0, t_0\text{ n'est pas une application et }a\in\ens{0\dots n}\\
\restrict{T_a}{s} \text{ si } t=\Pi(x_1:T_1)\dots T_n, n>1, T_n\text{ n'est pas un produit et }a\in\ens{1\dots n}\\
\restrict{A}{s} \text{ si } t=\lm (x:A).\,u\text{ et }a=\circ\\
\restrict{u}{s} \text{ si } t=\lm (x:A).\,u\text{ et }a=\bullet\\
\text{n'est pas défini} \text{ sinon}
\end{array}\right.
\]
\end{defi}
\todo{
Tous les sous-termes ne sont pas accessibles par cette définition de la position.
C'est volontaire ici et je considère que ce n'est pas un bug, mais il existe des applications pour lesquelles cette définition ne convient pas.
}
\begin{defi}[Arité]
Soit $F$ un symbole de la signature tel que $\tau(F)=\Pi(x_1:T_1)\dots(x_n:T_n). U$,
$U$ ne contient pas de produit.
$n$ est alors appelée \emph{arité} de $F$.
\end{defi}
\begin{defi}[Symbole appliqué partiellement et pleinement]
Soit $f$ un symbole de la signature et $t$ un terme.
$f$ est \emph{pleinement appliqué} dans $t$ si, pour toute position $a$ telle que $\restrict{t}{a}=f$,
$a=a'.0$ et $\restrict{t}{a'}$ est de la forme $f\,t_1\dots t_n$ avec $n\>\arity(f)$.
Sinon, $f$ est dit \emph{partiellement appliqué} dans $t$.
\end{defi}
\begin{defi}[Règle de réécriture]
On suppose donnée un ensemble $\Rules$ de \emph{règles de réécriture} de la forme
\[f\,t_1\dots t_n\rul r\]
où :
\begin{cond}{HeadDef}(Tête définissable).
$f\in \FTyp\cup\FObj$,
\end{cond}
\begin{cond}{Arity}(Arité).
$n\<\arity(f)$,
\end{cond}
\todo{On est triste d'avoir cette condition,
mais elle nous garantit qu'une fonction pleinement appliqu\'ee est un terme neutre,
ce qui nous aide grandement dans nos preuves,
on cherchera \`a la supprimer un peu plus tard.}
\end{defi}
\begin{defi}[Relation de réécriture]
On note $\rew$ la \emph{relation de réécriture} qui est l'union de la $\beta$-réduction
et de la plus petite relation close par substitution et contexte contenant $\Rules$.
\end{defi}
\begin{cond}{Confluence}(Confluence locale).
La relation de réécriture est supposée localement confluente.
\end{cond}
\section{Typage}
\subsection*{Formation des contextes}
\begin{center}
\begin{tabular}{rcl}
\AxiomC{$\phantom{\Gamma\vdash A}$}
\UnaryInfC{$[]$ bien formé}
\DisplayProof&&
\AxiomC{$\Gamma\vdash A:s$}
\RightLabel{$\sys{x\notin\support(\Gamma)}{s\in\Sort}$}
\UnaryInfC{$\Gamma,x:A$ bien formé}
\DisplayProof
\end{tabular}
\end{center}
\subsection*{Axiomes}
\begin{center}
\begin{tabular}{rcl}
\AxiomC{$\Gamma$ bien formé}
\UnaryInfC{$\Gamma\vdash \Type:\Kind$}
\DisplayProof&&
\AxiomC{$\Gamma$ bien formé}
\RightLabel{$x:A\in\Gamma$}
\UnaryInfC{$\Gamma\vdash x:A$}
\DisplayProof
\end{tabular}
\end{center}
\todo{
On peut remplacer ce prédicat bien formé par une règle d'affaiblissement (cf FSCD).
Quel impact ce changement a-t-il ?
}
\subsection*{Produit}
\begin{prooftree}
\AxiomC{$\Gamma\vdash A:\Type$}
\AxiomC{$\Gamma,x:A\vdash B:s$}
\RightLabel{$s\in\Sort$}
\BinaryInfC{$\Gamma\vdash \Pi(x:A).B:s$}
\end{prooftree}
\subsection*{Lambda-abstraction}
\begin{prooftree}
\AxiomC{$\Gamma\vdash\Pi(x:A).B:s$}
\AxiomC{$\Gamma,x:A\vdash t:B$}
\RightLabel{$s\in\Sort$}
\BinaryInfC{$\Gamma\vdash\lambda(x:A).t: \Pi(x:A).B$}
\end{prooftree}
\subsection*{Application}
\begin{prooftree}
\AxiomC{$\Gamma\vdash t: \Pi(x:A).B$}
\AxiomC{$\Gamma\vdash u:A$}
\BinaryInfC{$\Gamma\vdash t\,u:\subst{B}{x}{u}$}
\end{prooftree}
\subsection*{Symbole de la signature}
\begin{prooftree}
\def\defaultHypSeparation{\hskip 0em}
\AxiomC{$\Gamma\vdash \tau(f):s(f)$}
\UnaryInfC{$\Gamma\vdash f:\tau(f)$}
\end{prooftree}
\todo{Si l'on a l'affaiblissement, $\G$ peut être supprimé dans cette règle.}
\subsection*{Conversion}
\begin{prooftree}
\AxiomC{$\Gamma\vdash t:A$}
\AxiomC{$\Gamma\vdash B:s$}
\RightLabel{$\sys{A\downarrow B}{s\in\Sort}$}
\BinaryInfC{$\Gamma\vdash t:B$}
\end{prooftree}
\begin{cond}{SubjectReduction}(Subject reduction).
On suppose que les règles préservent le typage, \cad que
pour tous termes $t$ et $t'$ tels que $t\rew t'$,
pour tout $T$,
pour tout contexte $\Gamma$ tel que $\Gamma\vdash t:T$,
on a $\Gamma\vdash t':T$.
\end{cond}
\begin{rmq}
Subject reduction implique que pour toute règle $f\,\bar l\rul r$,
$\FreeVar(r)\subseteq\FreeVar(f\,\bar l)$.
\end{rmq}
\begin{defi}[Termes (version stratifiée)]
On donne les 3 grammaires suivantes :
\begin{center}
\begin{tabular}{rrlr}
kinds & $K$ & $::=\Type\mid\Pi(x:U). K$\\
familles & $T,U$ & $::=\lambda (x:U).\,T\mid\Pi(x:U).T\mid T\,t\mid F$&$F\in\FTyp$\\
objets & $t,u$ & $::=x\mid\lambda (x:T).\,t\mid t\,u\mid f$&$f\in\FObj$, $x\in\Var$\\
\end{tabular}
\end{center}
Un \emph{terme} est $\Kind$, une \emph{kind}, une \emph{famille} ou un \emph{objet}.
\end{defi}
\todo{Rajouter un item pour les types qui sont des familles d'arité 0 et mettre cela au bon endroit (mais ça fait une 3e grammaire) ?}
\begin{nots}
$\mbb{K}$ désigne l'ensemble des kinds, $\mbb{F}$ l'ensemble des familles et $\mbb{O}$ l'ensemble des objets.
De plus, $\Terms$ désigne l'ensemble de tous les termes.
\end{nots}
\begin{cond}{ConsistTypSort}(Cohérence typage sortage)
$\tau$ associe :
\begin{itemize}
\item une kind à chaque symbole de $\FTyp$ ;
\item une famille à chaque symbole de $\FObj$.
\end{itemize}
\end{cond}
\begin{defi}[Forme normale]
Soit $t\in\SN$, on note $t\Downarrow$ sa forme normale,
qui est le terme $u$ tel que $t\reww u$ et il n'existe pas de $v$ tel que $u\rew v$.
\end{defi}
\begin{rmq}
Grâce à l'hypothèse de confluence locale et lemme de Newman, la forme si elle existe est unique.
\end{rmq}