Commit dbd2a9e1 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

g

parent 9d1d3259
\documentclass{article}
\input{enTeteArticle}
\usepackage{geometry}
\geometry{left=3cm, right=3cm, bottom=3cm}
\DeclareMathOperator{\Kind}{Kind}
\DeclareMathOperator{\Type}{Type}
\DeclareMathOperator{\support}{supp}
......
......@@ -3,9 +3,13 @@
\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}
\begin{cond}{cond-succ-well-founded}
We suppose given a well-founded pre-order $\preced$ on $\CTyp$ .
\end{cond}
\begin{defi}[Frozen type]
For $C\in\CTyp$, we define the following grammars :
\begin{align*}
......@@ -40,15 +44,3 @@
we define
\[\Acc(f)=\enscond{i\<\arity(f)}{T_i\in\Froz_{\preced C}}.\]
\end{defi}
\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.
\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.
}
\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}
......@@ -10,24 +10,24 @@
\end{itemize}
We denote by $\Candidates$ the set of reducibility candidates.
\end{defi}
\begin{lem}
$\SN(\rew\cup\surterm_{acc})$ is a candidate.
\end{lem}
\begin{proof}
\begin{itemize}
\item
By definition we have $\SN(\rew\cup\surterm_{acc})\subseteq\SN(\rew)$.
\item
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
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}
% $\SN(\rew\cup\surterm_{acc})$ is a candidate.
% \end{lem}
% \begin{proof}
% \begin{itemize}
% \item
% By definition we have $\SN(\rew\cup\surterm_{acc})\subseteq\SN(\rew)$.
% \item
% 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
% 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}[Reducibility of $\mcal{I}_C$]
......@@ -41,11 +41,11 @@
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.
Since $t\in\SN(\rew)$, $u\in\SN(\rew)$ 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})$.
$t\in\SN(\rew)$.
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}
......@@ -148,7 +148,7 @@ Since $\mcal{F}_p(\Lambda,\Candidates)$ is a strictly inductive poset,
By assumption, $J(A)\in\Candidates$ and, for $a\in J(A)$, $J(\subst{B}{x}{a})\in\Candidates$.
Therefore, $G(J)(T)\in\Candidates$.
\item
If $T\Downarrow$ is neutral, then $G(J)(T)=\SN(\rew\cup\surterm_{acc})\in\Candidates$.
If $T\Downarrow$ is neutral, then $G(J)(T)=\SN(\rew)\in\Candidates$.
\item
Otherwise, $T\Downarrow=C\,\bar t$ is a fully applied set constructor,
and we have already seen that $\mcal{I}_C$ is a candidate.
......
\section{Dependency pairs}
\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.
\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}$,
such that $g\,\bar m$ occurs in $r$, $\valabs{\bar m}\<\arity(g)$
......@@ -119,6 +131,17 @@
\UnaryInfC{$\G\vdash_{f\bar l}g:\tau(g)$}
\end{prooftree}
\begin{lem}\label{lem-order-typ}
For $f,g\in\Func$, $\bar l$, $\G$, $t$ and $T$, such that $g$ occurs in $t$
\begin{itemize}
\item if $\G\vdash_{f\bar l}t:T$ then $g\sqsubseteq f$,
\item if $\G\vdash_{\sqsubset f}t:T$ then $g\sqsubset f$.
\end{itemize}
\end{lem}
\begin{proof}
By induction on the proof tree.
\end{proof}
\begin{defi}[Valid rule]
......@@ -152,7 +175,55 @@
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}$,
then $u\sg\in\interp{U\sg}$.
\end{lem}
\begin{proof}
The proof is the same as for \indthm{thm-adequacy} except for (fun) replaced by (dp) and (const).
\begin{description}
\item[(dp)]
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}$.
\item[(const)]
There is a $h\in\Func$ occurring in $\tau(g)$.
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}
......@@ -160,7 +231,6 @@
\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}$.
......@@ -182,22 +252,15 @@
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{thm-adequacy} except for (fun) replaced by (dp).
\begin{description}
\item[(dp)]
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{description}
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$.
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}$
\end{itemize}
\item
If $f\in\CObj$, then $T'=C\,\bar u$ with $C\in\CTyp$.
\qedhere
\end{itemize}
\end{proof}
......@@ -43,14 +43,15 @@ Here a cast between set and tuple is left implicit.
{\Part{\Lambda}^n}
{\Part{\Lambda}^n}
{(X_i)_{i\<n}}
{\paren{\enscond{t\in\SN(\rew\cup\surterm_{acc})}
{\paren{\enscond{t\in\SN(\rew)}
{\begin{array}{l}
\text{if }t\reww c\,v_1\dots v_m\text{ where }
\left\{\begin{matrix}
c\in\CObj\\
\text{if }t\reww c\,v_1\dots v_m\text{ where }c\in\CObj\\
\text{then }
\left\{\begin{array}{l}
\tau(c)=\Pi\overline{(x:T)}.(C_i\,\bar s)\\
\end{matrix}\right.\\
\text{then for all }j\in\Acc(c),j\<m,v_j\in R_{\bar C}(T_j,(X_k)_{k\<n})\\
m\>\arity(c)\\
\text{for all }j\in\Acc(c),v_j\in R_{\bar C}(T_j,(X_k)_{k\<n})\\
\end{array}\right.\\
\end{array}}}_i
}
\]
......@@ -129,11 +130,11 @@ Here a cast between set and tuple is left implicit.
and $t\in\pi_k\paren{K_{\bar C}((X_i)_{i\<n})}$.
\begin{itemize}
\item
If $t$ does not reduce to any term of the shape $c\,\bar s$ where $c$ is a constructor of a type whose constant is $C_k$,
If $t$ does not reduce to any term of the shape $c\,\bar s$ where $c$ is a constructor,
then $t\in \pi_k\paren{K_{\bar C}((Y_i)_{i\<n})}$,
since $\pi_k\paren{K_{\bar C}((X_i)_{i\<n})}=\SN(\rew\cup\surterm_{acc})=\pi_k\paren{K_{\bar C}((Y_i)_{i\<n})}$.
since $\pi_k\paren{K_{\bar C}((X_i)_{i\<n})}=\SN(\rew)=\pi_k\paren{K_{\bar C}((Y_i)_{i\<n})}$.
\item
If $t\reww c\,v_1\dots v_r$ where $c$ ia a constructor of $C_k$.
If $t\reww c\,v_1\dots v_r$ where $c$ ia a constructor.
Then $\tau(c)=\Pi\overline{(x:U)}. \,C_k\,\bar s$ and for all $j\in\Acc(c)$ with $j\<r$,
$v_j\in R_{\bar C}(U_j,(X_i)_{i\<n})$.
......@@ -169,7 +170,7 @@ Here a cast between set and tuple is left implicit.
\left\{\begin{array}{ll}
\mcal{I}_{C} &\text{if }T\Downarrow=C\,\bar u\text{ with }C\in\CTyp\\
\enscond{t}{\text{for all }u\in I(A), t\,u\in I(\subst{B}{x}{u})} & \text{if }T\Downarrow=\Pi(x:A). B\\
\SN(\rew\cup\surterm_{acc}) & \text{if }T\Downarrow\in\NTyp\\
\SN(\rew) & \text{if }T\Downarrow\in\NTyp\\
\end{array}\right.\\
\end{align*}
\end{defi}
......@@ -205,7 +206,7 @@ Here a cast between set and tuple is left implicit.
then $G(I,T)=\mcal{I}_{C}=G(J,T)$.
\item
If $T\Downarrow\in\NTyp$,
then $G(I,T)=\SN(\rew\cup\surterm_{acc})=G(J,T)$.
then $G(I,T)=\SN(\rew)=G(J,T)$.
\item
If $T\Downarrow=\Pi(x:A). B$,
since $I\subseteq J$,
......@@ -232,7 +233,7 @@ Here a cast between set and tuple is left implicit.
\end{defi}
\todo{
Her we use Abian and Brown theorem (or Markowski's, or one on dcpo),
Here we use Abian and Brown theorem (or Markowski's, or one on dcpo),
but I think for more general case, ordinals are the good way to intricate things in a readable way.
(Furthermore, it is necessary to explicit how we compute the fixpoint, later in this draft).
}
......
......@@ -36,7 +36,7 @@
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}$.
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_{arg}\cup\surterm_{acc})$ is well-founded on $\mbb{U}$.
\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