Commit 33884413 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Everything is in English, proofs are verified until p9

parent 1e6b820d
......@@ -18,7 +18,7 @@
\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}}.\]
\[\Acc(f)=\enscond{i\<\arity(f)}{T_i\in\Froz_{\preced C}}.\]
\end{defi}
\begin{defi}[Order associated to accessible subterms]
......
\section{Candidats}
\section{Candidates}
\begin{defi}[Candidats de réductibilité]
$S\in\Part{\Lambda}$ est un \emph{candidat de réductibilité} si
\begin{defi}[Reducibility candidates]
$S\in\Part{\Lambda}$ is a \emph{reducibility candidate} if
\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$.
\item $\enscond{u}{\text{there is a }t\in S,t\rew u}\subseteq S$,
\item if $t$ is neutral and $\enscond{u}{t\rew u}\subseteq S$ then $t\in S$.
\end{itemize}
On note $\Candidates$ l'ensemble des candidats de réductibilité.
We denote by $\Candidates$ the set of reducibility candidates.
\end{defi}
\begin{lem}
$\SN(\rew\cup\surterm_{acc})$ est candidat.
$\SN(\rew\cup\surterm_{acc})$ is a candidate.
\end{lem}
\begin{proof}
\begin{itemize}
\item
Par définition, on a $\SN(\rew\cup\surterm_{acc})\subseteq\SN(\rew)$.
By definition we have $\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})$.
Let $t\in\SN(\rew\cup\surterm_{acc})$ and $t'$ such that $t\rew t'$.
We have $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})$.
Let $t$ be a neutral term such that $\enscond{u}{t\rew u}\subseteq\SN(\rew\cup\surterm_{acc})$.
Since $t$ is neutral, it is not headed by an element of $\CObj$,
so $\enscond{u}{t(\rew\cup\surterm_{acc}) u}=\enscond{u}{t\rew u}$.
Hence, $t\in\SN(\rew\cup\surterm_{acc})$.\qedhere
\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$.
\begin{lem}[Reducibility of $\mcal{I}_C$]
If $C\in\CTyp$, then $\mcal{I}_C\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
First note that $\mcal{I}_C=K_{\bar C}(\mcal{I}_C)$.
\begin{itemize}
\item
By definition of $K_{\bar C}$, we have $K_{\bar C}(\mcal{I}_C)\subseteq\SN(\rew)$.
\item
Let $t\in\mcal{I}_C$ and $u$ be such that $t\rew u$.
Since $t\in\SN(\rew\cup\surterm_{acc})$, $u\in\SN(\rew\cup\surterm_{acc})$ too.
If $u\reww c\,\bar v$, then $t\reww c\,\bar v$ so the constraint on the reducibility of the accessible arguments are fulfilled.
\item
Let $t$ be a neutral term such that $\enscond{u}{t\rew u}\subseteq\mcal{I}_C$.
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.\qedhere
\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}
......
This diff is collapsed.
\section{Ordering}
\begin{defi}[Type constructors]
\begin{defi}[Type constants]
\[\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}
......@@ -8,10 +8,10 @@
\begin{defi}[Frozen type]
For $C\in\CTyp$, we define the following grammars :
\begin{align*}
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\\
T_{\preced C}::=& \Pi(x:U_{\prec C}). T_{\preced C}\,\mid\,C'\,u_1\dots u_{\arity(C')}&\text{ where }C'\preced C\\
U_{\prec C}::=& \Pi(x:T_{\preced C}). U_{\prec C}\,\mid\,C'\,u_1\dots u_{\arity(C')}&\text{ where }C'\prec C\\
\end{align*}
We denote those sets respectively by $\Froz_{\<C}$ and $\Froz_{<C}$.
We denote those sets respectively by $\Froz_{\preced C}$ and $\Froz_{\prec C}$.
\end{defi}
\todo{
......
......@@ -138,7 +138,7 @@ A \emph{term} is $\Kind$, a \emph{kind}, a \emph{family} or an \emph{object}.
\end{rmq}
\begin{propo}[Stratification lemma]
\begin{propo}[Stratification lemma]\label{lem-Stratification}
If $\D\vdash t:A$ then we are in one of the following cases:
\begin{itemize}
\item $t$ is an object, $A$ a family and $\D\vdash A:\Type$,
......
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