Commit 09bb37e7 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Lundi 8

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}
\section{Dependency pairs}
\section{Fully applied signature symbol and structural order}
\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)}.U$,
$i\in\Acc(f)$, $T_i=\Pi\overline{(y:V)}.W$
and $\overline{\crochet{\sur{u}{y}}}\vDash\overline{(y:V)}$.
\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}[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}\\
\valabs{\bar t}=\arity(f)\\
\crochet{\overline{\sur{t}{x}}}\vDash\overline{(x:T)}
\end{matrix}
}
\]
\end{defi}
\begin{defi}[$\rew_{arg}$]
Let $f\,\bar t\in\mbb{U}$.
$f\,\bar t\rew_{arg}u$ if $u=f\,\bar t'$, there is a $i$ such that $t_i\rew t'_i$
and for all $j\neq i$, $t_j=t'_j$.
\end{defi}
\begin{lem}\label{lem-subacc-wf}
$\surterm_{acc}$ is well-founded on $\mbb{U}$.
\end{lem}
\begin{proof}
Let $f\,\bar u\in\mbb{U}$.
We want to show there is no infinite sequence $(t_i)_{i\in\N}$ such that $t_0=f\,\bar u$ and for all $i\in\N$, $t_i\surterm_{acc}t_{i+1}$.
\begin{itemize}
\item
If $f\notin\CObj$, then there is no $t$ such that $f\,\bar u\surterm_{acc}t$.
\item
So, let us consider $f\in\CObj$.
Then $\tau(f)=\Pi\overline{(x:T)}.C\,\bar v$.
By induction on $\succ$,
let's assume that for all $C'\prec C$,
for all terms headed by a constructor of $C'$,
there is no infinite sequence with the expected property.
There is a $j\in\Acc(f)$ such that $t_1=u_j\,\bar w$.
$u_j\in\interp{T_j}$, hence:
\begin{itemize}
\item
if $T_j$ is not a product and $u_j$ is headed by a constructor,
the constructor is fully applied, so $\valabs{\bar w}=0$.
\item
if $T_j$ is a product,
then by definition of accessibility, $T_j\in\Froz_{\<C}$.
So all the element of $\bar w$ headed by a constructor
are headed by a constructor of a type constant $C'\prec C$.
So if we choose to access an element of $\bar w$ we can apply the induction hypothesis on $\prec$.
\end{itemize}
We see that $\surterm_{acc}$ is well-founded on $\mbb{U}$
because $\surterm$ is well-founded and we can access finitely many invented terms, by well-foundedness of $\succ$.
\qedhere
\end{itemize}
\end{proof}
\begin{lem}
$\surterm_{acc}\cup\to_{arg}$ is well-founded on $\mbb{U}$.
\end{lem}
\begin{proof}
If the reduction takes place in a non-invented term it can happen before any $\surterm_{acc}$ and if it happens in an invented term,
we could have invented the reducted form.
\end{proof}
\section{Dependency pairs}
\begin{defi}[Dependency pairs]
Let $f\bar l>g\bar m$ if there is a rule $f\bar l\rul r\in\mcal{R}$,
......@@ -153,28 +219,6 @@
\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}\\
\valabs{\bar t}=\arity(f)\\
\crochet{\overline{\sur{t}{x}}}\vDash\overline{(x:T)}
\end{matrix}
}
\]
\end{defi}
\begin{defi}[$\rew_{arg}$]
Let $f\,\bar t\in\mbb{U}$.
$f\,\bar t\rew_{arg}u$ if $u=f\,\bar t'$, there is a $i$ such that $t_i\rew t'_i$
and for all $j\neq i$, $t_j=t'_j$.
\end{defi}
\begin{lem}[Pseudo-adequacy]\label{lem-pseudo-adequacy}
For all $f\,\bar l$, $\G$, $u$ and $U$,
if $\G\vdash_{f\bar l} u:U$, $\sg\vDash\G$ and for all $g\sqsubset f$, $g\in\interp{\tau(g)\sg}$,
......@@ -194,36 +238,12 @@
Hence, $g\sqsubseteq h$.
Furthermore, by \indlem{lem-order-typ}, $h\sqsubset f$ because $\G\vdash_{\sqsubset f}\tau(g):s(g)$.
Hence by transitivity, $g\sqsubset f$.
We then have $g\in\interp{\tau(g)\sg}$ by hypothesis.
\qedhere
\end{description}
\end{proof}
\begin{lem}\label{lem-subacc-wf}
Let $f\,\bar u\in\mbb{U}$.
There is no infinite sequence $(t_i)_{i\in\N}$ such that $t_0=f\,\bar u$ and for all $i\in\N$, $t_i\surterm_{acc}t_{i+1}$.
\end{lem}
\begin{proof}
\begin{itemize}
\item
If $f\notin\CObj$, then there is no $t$ such that $f\,\bar u\surterm_{acc}t$.
\item
So, let us consider $f\in\CObj$.
Then $\tau(f)=\Pi\overline{(x:T)}.C\,\bar v$.
By induction on $\succ$,
let's assume that for all $C'\prec C$,
for all terms headed by a constructor of $C'$,
there is no infinite sequence with the expected property.
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
\end{itemize}
\end{proof}
\begin{thm}
$\tau$ is valid if $\call$ terminates on $\mbb{U}$ and all rules in $\mcal{R}$ are valid.
\end{thm}
......@@ -240,7 +260,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,15 +272,38 @@
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}\]
Which by definition of the interpretation of a product implies that
$(r\sg)\,t_{k+1}\dots t_{n}=u\in\interp{T'\pi}$
$(r\sg)\,t_{k+1}\dots t_{n}=u\in\interp{T'\pi}$
\end{itemize}
\item
If $f\in\CObj$, then $T'=C\,\bar u$ with $C\in\CTyp$.
\qedhere
We have to show that for every $c\,\bar u$ such that $f\,\bar t\reww c\,\bar u$ with $c\in\CObj$,
for all $j\in\Acc(c)$, $u_j$ is in the interpretation of the expected time.
Three cases can occur:
\begin{itemize}
\item
$c\,\bar u=f\,\bar t$,
then by defintion of $\mbb{U}$,
every $t_i$ is in the interpretation of the expected type;
\item
The first reduction to go between $f\,\bar t$ and $c\,\bar u$ occurs in an argument.
We can conclude by induction hypothesis on $\rew_{arg}$;
\item
Otherwise, the first reduction occurs in the head.
We can do as in the case of non-constructors to prove that the direct reduct is in $\interp{T'\pi}$.
We conclude thanks to the stability by reduction of the interpretations.
\end{itemize}
\item
If $f\in\CTyp$, then all reductions occur in arguments and we can conclude by induction hypothesis,
since we have the guarantee that $f\,\bar t\in\SN(\rew)$ and does not reduce to a product
\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