Commit 57a438e4 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Until section 6: Validity

parent 33884413
......@@ -86,7 +86,7 @@
\end{mdframed}}
\newcommand\indcond[1]{(see Cond. \ref{#1})}
\title{Interprétation des types positifs}
\title{Interpretation of positive types}
\author{Guillaume Genestier}
\date{}
......@@ -100,7 +100,6 @@
\input{syntax}
\input{typing}
\input{ordonnabilite}
\input{acc}
\input{interpretation}
\input{cand}
......
\section{Accessibility}
\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{defi}[Frozen type]
For $C\in\CTyp$, we define the following grammars :
\begin{align*}
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_{\preced C}$ and $\Froz_{\prec C}$.
\end{defi}
\todo{
We define here non-strict positivity.
To what extend does it make the proof harder?
I don't see any difficulty.
}
\begin{defi}[Constructors]
\[\CObj=\enscond{f\in\FObj}{\tau(f)=\Pi\overline{(x:T)}. C\,t_1\dots t_{\arity(C)} \text{ with }C\in\CTyp}.\]
\end{defi}
......
......@@ -76,93 +76,103 @@
\item
Let $t$ be a neutral term such that $\enscond{u}{t\rew u}\subseteq R$.
We have to prove that $t\in R$.
Hence, we take $a\in P$ and prove that $t\,a\in Q(a)$.
Since $P\in\Candidates$, we have $a\in\SN(\rew)$ and $\enscond{u}{a\reww u}\subseteq P$.
We now prove that, for all $b\in\enscond{u}{a\reww u}$,
$t\,b\in Q(a)$, by induction on $\rew$.
Since $t$ is neutral, $t\,b$ is neutral too and it suffices to prove that $\enscond{u}{t\,b\rew u}\subseteq Q(a)$.
Since $t$ is neutral, $\enscond{u}{t\,b\rew u}=\enscond{u\,b}{t\rew u}\cup \enscond{t\,u}{b\rew u}$.
By induction hypothesis, $\enscond{t\,u}{b\rew u}\subseteq Q(a)$.
By assumption, $\enscond{u}{t\rew u}\subseteq R$.
So, $\enscond{u\,a}{t\rew u}\subseteq Q(a)$.
Since $Q(a)\in\Candidates$, $\enscond{u\,b}{t\rew u}\subseteq Q(a)$ too.
\begin{itemize}
\item
By induction hypothesis, $\enscond{t\,u}{b\rew u}\subseteq Q(a)$.
\item
By assumption, $\enscond{u}{t\rew u}\subseteq R$.
So, $\enscond{u\,a}{t\rew u}\subseteq Q(a)$.
Since $Q(a)\in\Candidates$, $\enscond{u\,b}{t\rew u}\subseteq Q(a)$ too.
\end{itemize}
Therefore, $t\,a\in Q(a)$ and $t\in R$.\qedhere
\end{itemize}
\end{proof}
\begin{lem}[Reducibility of types]
\begin{enumerate}
\item $\interp{\Type}$ is a reducibility candidate,
\item for all $T\in\interp{\Type}$, $\interp{T}$ is a reducibility candidate.
\end{enumerate}
\begin{lem}[Reducibility of $\Type$]
$\interp{\Type}$ is a reducibility candidate.
\end{lem}
\begin{proof}
We must note that $\interp{\Type}=\domain(\mcal{J})$ and $\mcal{J}=F(\mcal{J})$.
So $\interp{\Type}=D(\mcal{J})$.
\begin{itemize}
\item
By definition of $D$, we have $\domain(\mcal{J})\subseteq\SN(\to)$.
\item
Let $T\in\domain(\mcal{J})$ and $T'$ such that $T\rew T'$.
We have $T'\in\SN(\to)$ since $T\in\SN(\to)$.
Assume now that $T'\reww \Pi(x:A). B$.
Then, $T\reww \Pi(x:A). B$,
$A\in\domain(\mcal{J})$ and,
for all $a\in \mcal{J}(A)$, $\subst{B}{x}{a}\in\domain(\mcal{J})$.
Therefore, $T'\in\domain(\mcal{J})$.
\item
Let $T$ be a neutral term such that $\enscond{U}{T\rew U}\subseteq\domain(\mcal{J})$.
Since $\domain(\mcal{J})\subseteq\SN(\to)$, $T\in\SN(\to)$.
Assume now that $T\reww \Pi(x:A). B$.
Since $T$ is neutral, there is $U$ such that $T\rew U$ and
$U\reww \Pi(x:A). B$.
Therefore, $A\in\domain(\mcal{J})$ and,
for all $a\in \mcal{J}(A)$,
$\subst{B}{x}{a}\in\domain(\mcal{J})$.
Hence $T\in D(\mcal{J})$\qedhere
\end{itemize}
\end{proof}
\begin{lem}[Reducibility of types]
for all $T\in\interp{\Type}$, $\interp{T}$ is a reducibility candidate.
\end{lem}
\begin{proof}
\begin{enumerate}
\item
We must note that $\interp{\Type}=\domain(\mcal{I})$ and $\mcal{I}=F(\mcal{I})$.
So $\interp{\Type}=G(\mcal{I})$.
\begin{itemize}
\item
By definition of $G$, we have $\domain(\mcal{I})\subseteq\SN$.
\item
Let $T\in\domain(\mcal{I})$ and $T'$ such that $T\rew T'$.
We have $T'\in\SN$ since $T\in\SN$.
Assume now that $T'\reww \Pi(x:A). B$.
Then, $T\reww \Pi(x:A). B$, $A\in\domain(\mcal{I})$ and, for all $a\in \mcal{I}(A)$, $\subst{B}{x}{a}\in\domain(\mcal{I})$.
Therefore, $T'\in\domain(\mcal{I})$.
\item
Let $T$ be a neutral term such that $\enscond{U}{T\rew U}\subseteq\domain(\mcal{I})$.
Since $\domain(\mcal{I})\subseteq\SN$, $T\in\SN$.
Assume now that $T\reww \Pi(x:A). B$.
Since $T$ is neutral, there is $U$ such that $T\rew U$ and
$U\reww \Pi(x:A). B$.
Therefore, $A\in\domain(\mcal{I})$ and, for all $a\in \mcal{I}(A)$, $\subst{B}{x}{a}\in\domain(\mcal{I})$.
\end{itemize}
\item
Since $\mcal{F}_p(\Lambda,\Candidates)$ is a strictly inductive poset,
Since $\mcal{F}_p(\Lambda,\Candidates)$ is a strictly inductive poset,
it suffices to prove that $\mcal{F}_p(\Lambda,\Candidates)$ is closed by $F$.
Assume that $J\in\mcal{F}_p(\Lambda,\Candidates)$.
We have to prove that $F(J)\in\mcal{F}_p(\Lambda,\Candidates)$,
that is, for all $T\in G(J)$, $H(J)(T)\in\Candidates$.
that is, for all $T\in D(J)$, $G(J)(T)\in\Candidates$.
There are three cases:
\begin{itemize}
\item
If $T\Downarrow=\Pi(x:A). B$,
then $H(J)(T)=\enscond{t}{\text{for all }a\in J(A), t\,a\in J(\subst{B}{x}{a})}$.
then $G(J)(T)=\enscond{t}{\text{for all }a\in J(A), t\,a\in J(\subst{B}{x}{a})}$.
By assumption, $J(A)\in\Candidates$ and, for $a\in J(A)$, $J(\subst{B}{x}{a})\in\Candidates$.
Therefore, $H(J)(T)\in\Candidates$.
Therefore, $G(J)(T)\in\Candidates$.
\item
If $T\Downarrow$ is neutral, then $H(J)(T)=\SN(\rew\cup\surterm_{acc})\in\Candidates$.
If $T\Downarrow$ is neutral, then $G(J)(T)=\SN(\rew\cup\surterm_{acc})\in\Candidates$.
\item
Otherwise, $T\Downarrow$ is a fully applied set constructor,
and we have already seen that $\mcal{I}_0(T)$ is a candidate.
Otherwise, $T\Downarrow=C\,\bar t$ is a fully applied set constructor,
and we have already seen that $\mcal{I}_C$ is a candidate.
\qedhere
\end{itemize}
\end{enumerate}
\end{proof}
\todo{Here we must state that the empty function is in $\mcal{F}_p(\Lambda,\Candidates)$,
that applying iteratively $F$ on the empty function is the way to compute the least fix-point
and that the limit is the same in both cases.}
\begin{lem}[Reducibility of $\Kind$]
$\interp{\Kind}$ is a reducibility candidate.
\end{lem}
\begin{proof}
Being a stable by reduction subset of $\SN$ is stable by the function defining $\interp{Kind}$
and there is no neutral kind.
\end{proof}
\begin{lem}[Reducibility of kinds]
\begin{enumerate}
\item $\interp{\Kind}$ is a reducibility candidate,
\item for all $K\in\interp{\Kind}$, $\interp{K}$ is a reducibility candidate.
\end{enumerate}
For all $K\in\interp{\Kind}$, $\interp{K}$ is a reducibility candidate.
\end{lem}
\begin{proof}
\begin{enumerate}
\item
Being a stable by reduction subset of $\SN$ is stable by the function defining $\interp{Kind}$
and there is no neutral kind.
\item
It is already proved for $\Type$ and done easily by induction for arrows
(see \indlem{lem-product-candidate}).
\end{enumerate}
It is already proved for $\Type$
and the \indlem{lem-product-candidate} ensures us that we can take the products.
\end{proof}
\todo{This is only a proof sketch.}
\section{Ordering}
\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{defi}[Frozen type]
For $C\in\CTyp$, we define the following grammars :
\begin{align*}
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_{\preced C}$ and $\Froz_{\prec C}$.
\end{defi}
\todo{
We define here non-strict positivity.
To what extend does it make the proof harder?
I don't see any difficulty.
}
......@@ -6,18 +6,19 @@
\end{defi}
\begin{defi}[Valid typing map]
$\tau$ is valid if for all $f\in\CTyp\cup\FTyp\cup\FObj$,
$\tau$ is valid if for all $f\in\Func$,
such that $\vdash\tau(f):s(f)$ and $\tau(f)\in\interp{s(f)}$,
we have $f\in\interp{\tau(f)}$.
\end{defi}
\begin{thm}[Typable implies in the interpretation]\label{TypImpliInterp}
Let $\sg$ be a substitution.
\begin{thm}[Adequacy]\label{thm-adequacy}
Let $\sg$ be a substitution, $\tau$ a typing map, $\G$ an environment and $t$ and $T$ two terms.
If $\tau$ is valid, $\G\vdash t:T$ and $\sg\vDash\G$,
then $t\sg\in\interp{T\sg}$.
\end{thm}
\begin{proof}
Let $\sg$ be such that $\sg\vDash\G$.
We prove this lemma by induction on $\G\vdash t:T$:
\begin{itemize}
\item[(axSort)]
......@@ -37,29 +38,31 @@
So $(\lm(x:A).t)\sg=\lm(x:A\sg).t\sg$ and $(\Pi(x:A). B)\sg=\Pi(x:A\sg). B\sg$.
Let $a\in\interp{A\sg}$ and $\sg'=\crochet{\sur{a}{x},\sg}$.
By induction hypothesis, we have $t\sg'\in\interp{B\sg'}$.
So, $(\lm(x:A\sg).t\sg)\,a\in\interp{B\sg'}$ as we can prove by induction on the reduction of $(A\sg,t\sg,a)$.
Since $(\lm(x:A\sg).t\sg)\,a$ is neutral and $\interp{\Pi(x:A\sg). B\sg}\in\Candidates$,
Let $a'$ be such that $a\reww a'$.
We prove that $(\lm(x:A\sg).t\sg)\,a'\in\interp{B\sg'}$ by induction on the reduction of $(A\sg,t\sg,a')$.
Since $(\lm(x:A\sg).t\sg)\,a'$ is neutral and $\interp{\Pi(x:A\sg). B\sg}\in\Candidates$,
it suffices to prove that $\enscond{u}{(\lm(x:A\sg).t\sg)\,a\rew u}\subseteq\interp{B\sg'}$.
\begin{itemize}
\item For the $\beta$-reduction at the top, $(\lm(x:A\sg).t\sg)\,a\rew \subst{t\sg}{x}{a}=t\sg'$, we can conclude by the induction on the derivation.
\item Otherwise the reduction, takes place in $A\sg$, $t\sg$ or $a$, we conclude by induction hypothesis on the reduction sequences.
\item For the $\beta$-reduction at the top, $(\lm(x:A\sg).t\sg)\,a'\rew \subst{t\sg}{x}{a'}$.
By induction on the derivation, we have $t\sg'\in\interp{B\sg'}$.
Since this interpretation is a candidate, its reduct $\subst{t\sg}{x}{a'}$ is also in $\interp{B\sg'}$.
\item Otherwise the reduction, takes place in $A\sg$, $t\sg$ or $a'$, we conclude by induction hypothesis on the reduction sequences.
\end{itemize}
\item[(app)]
By induction hypothesis, $t\sg\in\interp{\Pi(x:A\sg). B\sg}$ and $u\sg\in\interp{A\sg}$.
By definition, of the interpretation of an arrow,
we have $(t\sg)\,u\sg=(t\,u)\sg\in\interp{\subst{B\sg}{x}{u}}=\interp{\subst{B}{x}{u}\sg}$,
By definition, of the interpretation of a product,
we have $(t\sg)\,u\sg=(t\,u)\sg\in\interp{\subst{B\sg}{x}{u\sg}}=\interp{\subst{B}{x}{u}\sg}$,
since $x$ can be chosen not in $\domain(\sg)\cup\FreeVar(\sg)$ by $\alpha$-renaming.
\item[(fun)]
By induction hypothesis, we have $\tau(f)\in\interp{s(f)}$.
So, since $\vdash\tau(f):s(f)$, we have $f\in\interp{\tau(f)}$ since $\tau$ is valid.
\item[(conv)]
We assume that $\G\vdash A:s$ can be added to the hypothesis of the rule.
By the stratification lemma (\indlem{lem-Stratification}), $\G\vdash A:s$ can be added to the hypothesis of the rule.
Then by induction hypothesis, $A\sg\in \interp{s}$ and $B\sg\in\interp{s}$.
Since they are convertible, they both have the same normal form,
so $\interp{A\sg}=\interp{B\sg}$ and
since by induction hypothesis $t\sg\in\interp{A\sg}$, we have $t\sg\in\interp{B\sg}$.
\qedhere
\end{itemize}
\end{proof}
\todo{Prove a property stating that $\G\vdash A:s$ in the (conv) case.
In fact, the inversion lemma was added for another purpose, but it fulfills this obligation.}
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