Skip to content

GitLab

Commit d81024c4 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

introduce type shcemes in the proofs (in progress)

parent 80385819
Hide whitespace changes
Inline Side-by-side
language.tex
View file @ d81024c4
......@@ -855,7 +855,7 @@ for variables.
The algorithmic system above is sound with respect to the deductive one of Section~\ref{sec:static}
\begin{theorem}[Soundness]
For every $\Gamma$, $e$, $t$, $n_o$, if $\Gamma\vdashA e: \ts$, then $\Gamma \vdash e:t$ for every $t\in\ts$.
For every $\Gamma$, $e$, $\ts$, $n_o$, if $\Gamma\vdashA e: \ts$, then $\Gamma \vdash e:t$ for every $t\in\ts$.
\end{theorem}
We were not able to prove full completeness, just a partial form of it. As
anticipated, the problems are twofold: $(i)$ the recursive nature of
......
proofs.tex
View file @ d81024c4
......@@ -952,62 +952,62 @@ that associates to an expression a type scheme instead of a regular type.
This allows to type expressions more precisely and thus to have a more powerful completeness theorem in regards to the
declarative type system.
The results about this new type system will be used in section TODO in order to obtain a soundness and completeness
The results about this new type system will be used in \ref{sec:proofs_algorithmic_without_ts} in order to obtain a soundness and completeness
theorem for the algorithmic type system presented in \ref{sec:algorules}.
\begin{mathpar}
\Infer[Efq\Aa]
{ }
{ \Gamma, (e:\Empty) \vdashA e': \Empty }
{ \Gamma, (e:\Empty) \vdashAts e': \Empty }
{ \begin{array}{c}\text{\tiny with priority over}\\[-1.8mm]\text{\tiny all the other rules}\end{array}}
\qquad
\Infer[Var\Aa]
{ }
{ \Gamma \vdashA x: \Gamma(x) }
{ \Gamma \vdashAts x: \Gamma(x) }
{ x\in\dom\Gamma}
\\
\Infer[Env\Aa]
{ \Gamma\setminus\{e\} \vdashA e : \ts }
{ \Gamma \vdashA e: \Gamma(e) \tsand \ts }
{ \Gamma\setminus\{e\} \vdashAts e : \ts }
{ \Gamma \vdashAts e: \Gamma(e) \tsand \ts }
{ e\in\dom\Gamma \text{ and } e \text{ not a variable}}
\qquad
\Infer[Const\Aa]
{ }
{\Gamma\vdashA c:\basic{c}}
{\Gamma\vdashAts c:\basic{c}}
{c\not\in\dom\Gamma}
\\
\Infer[Abs\Aa]
{\Gamma,x:s_i\vdashA e:\ts_i'\\ \ts_i'\leq t_i}
{\Gamma,x:s_i\vdashAts e:\ts_i'\\ \ts_i'\leq t_i}
{
\Gamma\vdashA\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\textstyle\tsfun {\arrow {s_i} {t_i}}_{i\in I}
\Gamma\vdashAts\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e:\textstyle\tsfun {\arrow {s_i} {t_i}}_{i\in I}
}
{\lambda^{\wedge_{i\in I}\arrow {s_i} {t_i}}x.e\not\in\dom\Gamma}
\\
\Infer[App\Aa]
{
\Gamma \vdashA e_1: \ts_1\\
\Gamma \vdashA e_2: \ts_2\\
\Gamma \vdashAts e_1: \ts_1\\
\Gamma \vdashAts e_2: \ts_2\\
\ts_1 \leq \arrow \Empty \Any\\
\ts_2 \leq \dom {\ts_1}
}
{ \Gamma \vdashA {e_1}{e_2}: \ts_1 \circ \ts_2 }
{ \Gamma \vdashAts {e_1}{e_2}: \ts_1 \circ \ts_2 }
{ {e_1}{e_2}\not\in\dom\Gamma}
\\
\Infer[Case\Aa]
{\Gamma\vdashA e:\ts_0\\
\Refine {e,t} \Gamma \vdashA e_1 : \ts_1\\
\Refine {e,\neg t} \Gamma \vdashA e_2 : \ts_2}
{\Gamma\vdashA \tcase {e} t {e_1}{e_2}: \ts_1\tsor \ts_2}
{\Gamma\vdashAts e:\ts_0\\
\Refine {e,t} \Gamma \vdashAts e_1 : \ts_1\\
\Refine {e,\neg t} \Gamma \vdashAts e_2 : \ts_2}
{\Gamma\vdashAts \tcase {e} t {e_1}{e_2}: \ts_1\tsor \ts_2}
{ \tcase {e} {t\!} {\!e_1\!}{\!e_2}\not\in\dom\Gamma}
\\
\Infer[Proj\Aa]
{\Gamma \vdashA e:\ts\and \ts\leq\pair\Any\Any}
{\Gamma \vdashA \pi_i e:\bpi_{\mathbf{i}}(\ts)}
{\Gamma \vdashAts e:\ts\and \ts\leq\pair\Any\Any}
{\Gamma \vdashAts \pi_i e:\bpi_{\mathbf{i}}(\ts)}
{\pi_i e\not\in\dom\Gamma}
\Infer[Pair\Aa]
{\Gamma \vdashA e_1:\ts_1 \and \Gamma \vdashA e_2:\ts_2}
{\Gamma \vdashA (e_1,e_2):{\ts_1}\tstimes{\ts_2}}
{\Gamma \vdashAts e_1:\ts_1 \and \Gamma \vdashAts e_2:\ts_2}
{\Gamma \vdashAts (e_1,e_2):{\ts_1}\tstimes{\ts_2}}
{(e_1,e_2)\not\in\dom\Gamma}
\end{mathpar}
......@@ -1015,7 +1015,7 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
\begin{align*}
\tyof e \Gamma =
\left\{\begin{array}{ll}
\ts & \text{if } \Gamma \vdashA e:\ts \\
\ts & \text{if } \Gamma \vdashAts e:\ts \\
\tsempty & \text{otherwise}
\end{array}\right.
\end{align*}
......@@ -1044,7 +1044,7 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
\end{align*}
\subsection{Proofs for the algorithmic type system}
\subsection{Proofs for the algorithmic type system with type schemes}
This section is about the algorithmic type system with type schemes (soundness and some completeness properties).
......@@ -1053,7 +1053,7 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
\begin{align*}
\tyof e \Gamma =
\left\{\begin{array}{ll}
\ts & \text{if } \Gamma \vdashA e:\ts \\
\ts & \text{if } \Gamma \vdashAts e:\ts \\
\tsempty & \text{otherwise}
\end{array}\right.
\end{align*}
......@@ -1066,7 +1066,7 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
\subsubsection{Soundness}
\begin{theorem}[Soundness of the algorithm]
\begin{theorem}[Soundness of the algorithm]\label{soundnessAts}
For every $\Gamma$, $e$, $t$, $n_o$, if $\tyof e \Gamma \leq t$, then we can derive $\Gamma \vdash e:t$.
More precisely:
......@@ -1554,15 +1554,6 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
\end{description}
\end{description}
\end{proof}
\[
\begin{array}{lrcl}
\textbf{Simple type} & t_{s} & ::= & b \alt \pair {t_{s}} {t_{s}} \alt t_{s} \vee t_{s} \alt \neg t_{s} \alt \Empty \alt \arrow \Empty \Any\\
\textbf{Positive type} & t_+ & ::= & t_{s} \alt t_+ \vee t_+ \alt t_+ \land t_+ \alt \arrow {t_+} {t_+} \alt \arrow {t_+} {\neg t_+}\\
\textbf{Positive abstraction type} & t^\lambda_+ & ::= & \arrow {t_+} {t_+} \alt \arrow {t_+} {\neg t_+} \alt t^\lambda_+ \land t^\lambda_+\\
\textbf{Positive expression} & e_+ & ::= & c\alt x\alt e_+ e_+\alt\lambda^{t^\lambda_+} x.e_+\alt \pi_j e_+\alt(e_+,e_+)\alt\tcase{e_+}{t_{s}}{e_+}{e_+}
\end{array}
\]
From this result, we will now prove a stronger but more complex completeness theorem.
We were not able to prove full completeness, just a partial form of it. Indeed,
......@@ -1700,18 +1691,49 @@ theorem for the algorithmic type system presented in \ref{sec:algorules}.
\end{description}
\end{proof}
\subsection{The algorithmic type system without type schemes}
\subsection{Proofs for the algorithmic type system without type schemes}\label{sec:proofs_algorithmic_without_ts}
In this section, we consider the algorithmic type system without type schemes, as defined in \ref{sec:algorules}.
\subsubsection{Soundness}
\begin{lemma}
For every $\Gamma$, $e$, $t$, $n_o$, if $\Gamma\vdashA e: t$, then there exists $\ts \leq t$ such that $\Gamma \vdashAts e: \ts$.
\end{lemma}
\begin{proof}
Straightforward induction over the structure of $e$.
\end{proof}
\begin{theorem}[Soundness of the algorithmic type system without type schemes]\label{soundnessA}
For every $\Gamma$, $e$, $t$, $n_o$, if $\Gamma\vdashA e: t$, then $\Gamma \vdash e:t$.
\end{theorem}
\begin{proof}
Trivial by using the previous lemma and the theorem \ref{soundnessAts}.
\end{proof}
\subsubsection{Completeness}
\[
\begin{array}{lrcl}
\textbf{Simple type} & t_{s} & ::= & b \alt \pair {t_{s}} {t_{s}} \alt t_{s} \vee t_{s} \alt \neg t_{s} \alt \Empty \alt \arrow \Empty \Any\\
\textbf{Positive type} & t_+ & ::= & t_{s} \alt t_+ \vee t_+ \alt t_+ \land t_+ \alt \arrow {t_+} {t_+} \alt \arrow {t_+} {\neg t_+}\\
\textbf{Positive abstraction type} & t^\lambda_+ & ::= & \arrow {t_+} {t_+} \alt \arrow {t_+} {\neg t_+} \alt t^\lambda_+ \land t^\lambda_+\\
\textbf{Positive expression} & e_+ & ::= & c\alt x\alt e_+ e_+\alt\lambda^{t^\lambda_+} x.e_+\alt \pi_j e_+\alt(e_+,e_+)\alt\tcase{e_+}{t_{s}}{e_+}{e_+}
\end{array}
\]
\begin{theorem}[Completeness of the algorithmic type system for positive expressions]\label{completenessA}
If we restrict the language to positive expressions $e_+$,
the algorithmic type system without type schemes is complete.
TODO: states the inclusion between the regular type system and the one with type schemes
\begin{corollary}\label{app:completeness}
If we restrict the language to positive expressions $e_+$, the algorithmic type system is complete and type schemes can be removed from it (we can use regular types instead).
More precisely:
$\forall \Gamma, e_+, t.\ \Gamma \vdash e_+:t \Rightarrow \tyof {e_+} \Gamma \neq \tsempty$
\end{corollary}
$\forall \Gamma, e_+, t.\ \Gamma \vdash e_+:t \Rightarrow \exists t'.\ \Gamma \vdashA e_+ : t'$
\end{theorem}
\begin{proof}
\begin{proof} TODO: ADAPT IT. INDUCTION HYPOTHESIS MUST BE STRONGER.
With such restrictions, the rule \Rule{Abs-} is not needed anymore
because the negative part of functional types (i.e. the $N_i$ part of their DNF) is useless.
......
setup.sty
View file @ d81024c4
......@@ -180,6 +180,7 @@
\newcommand{\tsrep}[1]{\textsf{\textup{Repr}}(#1)}
\newcommand{\vdashA}{\vdash_{\!\scriptscriptstyle\mathcal{A}}}
\newcommand{\vdashAts}{\vdash_{\!\scriptscriptstyle\mathcal{A}_{ts}}}
\newcommand{\vdashp}{\vdash^{\texttt{Path}}}
\newcommand{\pvdash}[3]{\vdashp_{#1,#2,#3}}%\mathcal{P}
\newcommand{\evdash}[2]{\vdash^{\texttt{Env}}_{#1,#2}}
......
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