Commit b28e6140 authored by Gaspard Ferey's avatar Gaspard Ferey

Added concept of subject conversion.

parent ae8b4805
......@@ -102,7 +102,7 @@ Note: \(\mathcal{T}_{\mathcal{\emptyset}}\) is the set of closed terms.
}
{\Gamma \vdash \tpi{x}{A}{B} : s}
\and
\inferrule*[Right=lambda]{
\inferrule*[right=lambda]{
\Gamma \vdash A : \ttype
\\
\Gamma, x : A \vdash B : s
......@@ -110,15 +110,15 @@ Note: \(\mathcal{T}_{\mathcal{\emptyset}}\) is the set of closed terms.
\Gamma, x : A \vdash t : B
}
{\Gamma \vdash \tabs{x}{A}{t} : \tpi{x}{A}{B}}
\and
\inferrule*[Right=app]{
\and
\inferrule*[right=app]{
\Gamma \vdash t : \tpi{x}{A}{B}
\\
\Gamma \vdash u : A
}
{\Gamma \vdash t~u : \subst{B}{x}{u}}
\and
\inferrule*[Right=conv]{
\inferrule*[right=conv]{
\Gamma \vdash t : A
\\
\Gamma \vdash B : s
......@@ -137,7 +137,7 @@ Note: \(\mathcal{T}_{\mathcal{\emptyset}}\) is the set of closed terms.
\end{proof}
\begin{lemma}
For any context $\Gamma$ and terms $t$ and $A$ such that $\Gamma \vdash t : A$, there exists $t'$ such that $t \convbg t'$ and $\tkind$ is not a subterm of $t'$.
For any well-formed context $\Gamma$ and terms $t$ and $A$ such that $\Gamma \vdash t : A$, there exists $t'$ such that $t \convbg t'$ and $\tkind$ is not a subterm of $t'$.
\end{lemma}
\begin{proof}
By induction on the derivation of $\Gamma \vdash t : A$.
......@@ -153,15 +153,70 @@ Note: \(\mathcal{T}_{\mathcal{\emptyset}}\) is the set of closed terms.
The induction hypothesis on the first premise gives us a $\tkind$-free $A'$ such that $A' \convbg A$. Two solutions to conclude for $u$ :
\begin{itemize}
\item Consider that the induction on the height of the derivation is "forall context $\Gamma$".
\item Proove that adding a variable to the context doesn't enrich $\conv$.\\
\item Prove that adding a variable to the context doesn't enrich $\conv$.\\
i.e. $\conv_{\beta\Gamma} \ = \ \conv_{\beta\Gamma, x : A}$.
\end{itemize}
\end{itemize}
\end{proof}
\begin{definition}[subject conversion]
A well-formed context $\Gamma$ satisfies the \emph{subject conversion} property
when for all terms $t_1, t_2, T_1, T_2$ such that
$t_1 \convbg t_2$, $\Gamma \vdash t_1 : T_1$ and $\Gamma \vdash t_2 : T_2$,
then $T_1 \convbg T_2$.
\end{definition}
Remark: when $T_1$ (resp. $T_2$) is typable with a sort, $\Gamma \vdash T_1 :s$ (resp. $\Gamma \vdash T_2 :s$), then it follows from $T_1 \convbg T_2$ that $\Gamma \vdash t_2 : T_1$ (resp. $\Gamma \vdash t_2 : T_1$).
\begin{lemma}
For any context \(\Gamma\), if \(\tkind \convbg t\) then \(t = \tkind\).
When the relation system is oriented (a rewriting system) then
\emph{subject conversion} and \emph{typability preservation} together
imply the \emph{subject reduction} property.
\end{lemma}
\begin{proof}
$\Gamma$ verify the \emph{subject reduction} property when
$$
\forall t_1, t_2, T, \quad
\left\{
\begin{aligned}
& t_1 \longrightarrow^{\Gamma} t_2 \\
& \Gamma \vdash t_1 : T
\end{aligned}
\right.
\quad \Longrightarrow \quad
\Gamma \vdash t_2 : T
$$
$\Gamma$ verify the \emph{typability preservation} property when
$$
\forall t_1, t_2, T_1, \quad
\left\{
\begin{aligned}
& t_1 \longrightarrow^{\Gamma} t_2 \\
& \Gamma \vdash t_1 : T_1
\end{aligned}
\right.
\quad \Longrightarrow \quad
\exists T_2, \ \Gamma \vdash t_2 : T_2
$$
$\Gamma$ verify the \emph{subject conversion} property when
$$
\forall t_1, t_2, T_1, T_2 \quad
\left\{
\begin{aligned}
& t_1 \convbg t_2 \\
& \Gamma \vdash t_1 : T_1 \\
& \Gamma \vdash t_2 : T_2
\end{aligned}
\right.
\quad \Longrightarrow \quad
T_1 \convbg T_2
$$
\end{proof}
\begin{lemma}[False]
For any well-formed context \(\Gamma\), and term $t$ such that \(\tkind \convbg t\) then \(t = \tkind\).
\end{lemma}
\begin{proof}
By induction on the length of \(\Gamma\).
......@@ -184,20 +239,4 @@ Note: \(\mathcal{T}_{\mathcal{\emptyset}}\) is the set of closed terms.
\end{proof}
% \newpage
% \section{A simple wellformedness condition}
% On could start studying a very simple wellformedness condition.
% \begin{rules}{A (perhaps too) simple rule for relation wellformedness}{Relation WF}
% \inferrule{
% \Gamma \vdash A : \ttype
% \\
% \Gamma \vdash t : A
% \\
% \Gamma \vdash u : A
% }
% {\Gamma \vdash \wf{\{(t,u)\}}}
% \end{rules}
\end{document}
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