Commit ca8a9517 authored by Guillaume G's avatar Guillaume G

Version sans dépendances dans l'ordonnancement des types

parent dbd2a9e1
\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,T_i,\Id)}\text{ with }\tau(f)=\Pi\overline{(x:T)}.U
\]
\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}
......@@ -4,14 +4,10 @@
\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)$,
where $f\in\CObj$, $i\in\Acc(f)$ and $\bar u$ is an arbitrary sequence of terms.
where $f\in\CObj$, $\tau(f)=\Pi\overline{(x:T)}.V$, $i\in\Acc(f)$, $T_i=\Pi\overline{(x:U)}.W$
and $\overline{\crochet{\sur{u}{x}}}\vDash\overline{(x:U)}$.
\end{defi}
\todo{
This definition is really violent.
It is not well-founded.
It does not seem to be a problem, but I must stay cautious.
}
\begin{defi}[Dependency pairs]
Let $f\bar l>g\bar m$ if there is a rule $f\bar l\rul r\in\mcal{R}$,
......@@ -219,11 +215,29 @@
There is a $i\in\Acc(f)$ such that $t_1=u_i\,\bar w$.
By definition of accessibility, $T_i\in\Froz_{\<C}$.
$u_i\in\interp{T_i}$, hence, if $T_i$ is not a product and $u_i$ is headed by a constructor, the constructor is fully applied,
\qedhere
$u_i\in\interp{T_i}$, hence,
\begin{itemize}
\item
if $T_i$ is not a product and $u_i$ is headed by a constructor,
the constructor is fully applied hence $\valabs{\bar w}=0$
so $u_i$ is a strict subterm of $t_0$.
\item
if $T_i$ is a product, since $T_i\in\Froz_{\<C}$,
the terms $\bar w$ are of type of the shape $\Pi\overline{(y:U)}.C'\,\bar v$ with $C'\prec C$.
Hence if they are headed by a constructor, it is a constructor of $C'\prec C$,
so by induction if we access in this term, the reduction sequence is finite.
\qedhere
\end{itemize}
\end{itemize}
\end{proof}
\todo{
I must make this proof more readable.
The spirit is quite simple: if $\surterm_{acc}$ goes in an invented term,
then the type constant is strictly smaller than before,
hence it can happen only finitely often (by well-foundedness of $\prec$).
}
\begin{thm}
$\tau$ is valid if $\call$ terminates on $\mbb{U}$ and all rules in $\mcal{R}$ are valid.
\end{thm}
......@@ -240,7 +254,7 @@
We now prove that, $f\,\bar t\in\interp{T'\pi}$ by induction on ${\rew_{arg}}\cup{\call}$.
\begin{itemize}
\item
If $f\in\FObj\setminus\CObj$, $f\,\bar t$ is neutral.
If $f\in\FObj\setminus\CObj$ or $f\in\FTyp\setminus\CTyp$, $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:
......@@ -252,7 +266,7 @@
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$.
Since all rules are valid, there is $\D$ such that $\D\vdash_{f\bar l} r:\paren{\Pi(x_{k+1}:T_{k+1})\dots(x_n:T_n).T'}\crochet{\sur{l_1}{x_1},\dots,\sur{l_k}{x_k}}$ and $\sg\vDash\D$.
Since all rules are valid, there is $\D$ such that $\sg\vDash\D$ and $\D\vdash_{f\bar l} r:\paren{\Pi(x_{k+1}:T_{k+1})\dots(x_n:T_n).T'}\crochet{\sur{l_1}{x_1},\dots,\sur{l_k}{x_k}}$.
Hence, by pseudo-adequacy (\indlem{lem-pseudo-adequacy}): \[r\sg\in\interp{\paren{\Pi(x_{k+1}:T_{k+1})\dots(x_n:T_n).T'}\crochet{\sur{l_1}{x_1},\dots,\sur{l_k}{x_k}}\sg}\]
......@@ -261,6 +275,22 @@
\end{itemize}
\item
If $f\in\CObj$, then $T'=C\,\bar u$ with $C\in\CTyp$.
\qedhere
If $f\,\bar t\reww c\,\bar v$ with $c\in\CObj$,
three options:
\begin{itemize}
\item
$f\,\bar t= c\,\bar v$, then by definition of $\mbb{U}$,
the condition on accessible arguments is fulfilled.
\item
there is a sequence such that $f\,bar t\call \dots\call c\,\bar v$.
Then we can conclude by induction hypothesis.
\item
otherwise, $c\,\bar v$ is obtained via a rewrite rule whose rhs is a variable.
In this case, we have that $c\,\bar v$ is occuring in the lhs of this rule, and we can conclude thanks to the hypothesis that all rules are valid.
\end{itemize}
\item
If $f\in\CTyp$, then $f\,\bar t\in\SN(\rew)$ and $f\,\bar t$ does not reduce to a product,
so $f\,\bar t\in\interp{\Type}$.
\qedhere
\end{itemize}
\end{proof}
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