Merge branch 'str_pos_naif_en' of...

Merge branch 'str_pos_naif_en' of https://git.lsv.fr/genestier/bw_versionpositive into str_pos_naif_en

dp.tex

 
-\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$, $\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)}$. 
+ 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}
+
+\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}
+ There is no infinite sequence $(t_i)_{i\in\N}$ such that $t_0\in\mbb{U}$ and for all $i\in\N$, $t_i\surterm_{acc}t_{i+1}$.
+\end{lem}
+\begin{proof}
+ Let us assume that there is such an infinite sequence.
+
+ First note that every $t_i$ is headed by an element of $\CObj$, otherwise there is no $t$ such that $t_i\surterm_{acc}t$.
+
+ Hence, among every infinite sequence,
+ let us choose one such that $t_0=f\,\bar u$
+ where $\tau(f)=\Pi\overline{(x:T)}.C\,\bar v$
+ and for all $C'\prec C$, there is no infinite sequence starting by a constructor of $C'$.
+
+ We will prove that for every $i$, $t_i=t'_i\,\bar v$
+ where $t'_0=t_0$, for all $i$, $t'_i\surterm t'_{i+1}$ and $t'_i$ is headed by a constructor of a type equivalent to $C$.
+
+ Let $i$ be such that $t_i$ has this property.
+ Hence $t_i=t'_i\,\bar v$.
+ Since $t_i$ is headed by a constructor,
+ $t'_i$ too, $t'_i=c\,\bar u$.
+ Since $t'_i\,\bar v\surterm_{acc}t_{i+1}$, two options:
+ \begin{itemize}
+   \item
+    if $t_{i+1}=u_j\,\bar x$, then $u_j\subterm t'_{i}$ hence there is a $t'_{i+1}$ (namely $u_j$) such that $t_{i+1}=t'_{i+1}\,\bar x$ such that $t'_i\surterm t'_{i+1}$.
+    By definition of accessibility, if $\tau(c)=\Pi\overline{(x:T)}.C'\,\bar w$ with $C'\sim C$,
+    $T_j\in\Froz_{\<C}$.
+    In particular, $T_j=\Pi\overline{(y:V)}.C''\,\bar u'$,
+    with $C''\preceq C$.
+    Hence $u_j$ is headed by a constructor of $C''$.
+    \begin{itemize}
+      \item
+       If $C''\sim C$, we can conclude the induction,
+      \item
+       If $C''\prec C$, the minimality hypothesis is violated.
+    \end{itemize}
+
+   \item
+    if $t_{i+1}=v_j\,\bar x$, then we contradict the minimality hypothesis.
+
+    Indeed, $t_{i-1}=c_{i-1}\,\bar w$, with $c_{i-1}\in\CObj$,
+    $\tau(c_{i-1})=\Pi\overline{(x:T)}.C_{i-1}\,\bar u'$
+    and $C_{i-1}\sim C$.
+    Hence, for all $r\in\Acc(c_{i-1})$,
+    $T_r=\Pi\overline{(x:U)}.V$ where all $U_k$ are product ended by a $D_k\,\bar v'$ with $D_k\in\CTyp$ and $D_k\prec C$.
+
+    Hence, there is a $r$ such that $t'_i=w_r$ and $t_i=t'_i\,\bar v$ and for all $k$, $v_k\in\interp{U_k}$.
+
+    So, if $v_j$ is headed by a constructor,
+    this constructor is one of $D_k$ which violates the minimality property.
+ \end{itemize}
+ Hence the existence of such an infinite sequence leads to the existence of an infinite sequence of subterms of $t_0$,
+ contradicting the well-foundedness of $\subterm$.
+\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}$,
@@ -149,28 +236,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}$,
@@ -190,54 +255,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,
-   \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}
@@ -266,31 +289,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 $\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}}$.
-    
+    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$.
-   If $f\,\bar t\reww c\,\bar v$ with $c\in\CObj$,
-   three options:
+
+   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
-   	 $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.
+     \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 $f\,\bar t\in\SN(\rew)$ and $f\,\bar t$ does not reduce to a product,
-  so $f\,\bar t\in\interp{\Type}$.
-  \qedhere
+ \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}

sct.tex

@@ -45,7 +45,7 @@
   $\rew=(\rew_\beta\cup\rew_{\Rules})$ terminates on terms typable in $\lm\Pi/\Rules$
   if
   \begin{itemize}
-   \item $\rew$ is confluent,
+   \item $\rew$ is locally confluent,
    \item $\rew$ preserves typing,
    \item $\FTyp\cup\FObj$ is finite,
    \item $\Rules$ is valid (for instance AVO),