Commit 48216085 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

take five

parent f28d2d2f
\section{TAKE FIVE}
\subsection{Declarative}
\subsubsection{Types}
\[
\begin{array}{lrcl}
\textbf{Types} & t & ::= & b\alt t\to t\alt t\times t\alt t\vee t \alt \neg t \alt \Empty
\end{array}
\]
We write $\Any$ for $\neg\Empty$ and $t_1\wedge t_2$ for $\neg(\neg
t_1\vee\neg t_2)$
\subsubsection{Terms}
\begin{equation}
\begin{array}{lrclr}
\textbf{Test Types} &\tau &::=& b\alt \Empty\to \Any\alt \tau\times \tau\alt \tau\vee \tau \alt \neg \tau \alt \Empty\\
\textbf{Expressions} &e &::=& c\alt x\alt\lambda x.e
\alt e e\alt (e,e)\alt \pi_i e \alt
\tcase{e}{\tau}{e}{e}\\[.3mm]
\textbf{Values} & v &::=& c\alt\lambda x.e\alt (v,v)
\end{array}
\end{equation}
\subsubsection{Type Tests for values}
We define $\typof c = \basic{c}$, $\typof {\lambda x.e} = \Empty\to\Any$,
$\typof{(v_1,v_2)}=\typof{v_1}\times\typof{v_2}$. Finally $v\in t$ iff
$\typof v\leq t$.
\subsubsection{Semantics}
\begin{eqnarray}
(\lambda x.e)v &\reduces& e\subs x{v}\\[-1mm]
\pi_1 (v_1,v_2) &\reduces& v_1\\[-1mm]
\pi_2 (v_1,v_2) &\reduces& v_2\\[-1mm]
\tcase{v}{\tau}{e_1}{e_2} &\reduces& e_1\qquad\qquad\qquad v\in\tau\\[-1mm]
\tcase{v}{\tau}{e_1}{e_2} &\reduces& e_2\qquad\qquad\qquad v\not\in\tau
\end{eqnarray}
\subsubsection{Type System}
\begin{mathpar}
\Infer[Const]
{ }
{\Gamma\vdash c:\basic{c}}
{ }
\quad
\Infer[Ax]
{ }
{ \Gamma \vdash x: \Gamma(x) }
{ x\in\dom\Gamma }
\\
\Infer[$\to$I]
{\Gamma,x:t_1\vdash e:t_2}
{\Gamma\vdash\lambda x.e: \arrow{t_1}{t_2}}
{ }
\qquad \Infer[$\to$E]
{
\Gamma \vdash e_1: \arrow {t_1}{t_2}\quad
\Gamma \vdash e_2: t_1
}
{ \Gamma \vdash {e_1}{e_2}: t_2 }
{ }
\\
\Infer[$\times$I]
{\Gamma \vdash e_1:t_1 \and \Gamma \vdash e_2:t_2}
{\Gamma \vdash (e_1,e_2):\pair {t_1} {t_2}}
{ }
\qquad
\Infer[$\times$E$_1$]
{\Gamma \vdash e:\pair{t_1}{t_2}}
{\Gamma \vdash \pi_1 e:t_1}
{ } \quad
\Infer[$\times$E$_2$]
{\Gamma \vdash e:\pair{t_1}{t_2}}
{\Gamma \vdash \pi_2 e:t_2}
{ }
\\
\Infer[$\wedge$]
{\Gamma \vdash e:t_1 \and \Gamma \vdash e:t_2}
{\Gamma \vdash e: {t_1}\wedge {t_2}}
{ }
\and
\Infer[$\vee$]
{ \Gamma \vdash e':t_1\vee t_2 \and
\Gamma, x:t_1\vdash e:t\and \Gamma, x:t_2\vdash e:t
}
{
\Gamma\vdash e\subs x {e'} : t
}
{ }
\\
\Infer[$\neg_1$]
{
\Gamma \vdash e:t \and \Gamma\vdash e_1: t_1
}
{\Gamma\vdash \tcase {e} t {e_1}{e_2}: t_1}
{ }
\qquad
\Infer[$\neg_2$]
{
\Gamma \vdash e:\neg t \and \Gamma\vdash e_2: t_2
}
{\Gamma\vdash \tcase {e} t {e_1}{e_2}: t_2}
{ }
\\
\Infer[Subsumption]
{ \Gamma \vdash e:t\\t\leq t' }
{ \Gamma \vdash e: t' }
{ }
\end{mathpar}
Variant with more compact derivations:
\begin{mathpar}
\Infer[$\wedge$]
{{\small(\forall i\in I)}\quad\Gamma \vdash e:t_i}
{\Gamma \vdash e: \textstyle\bigwedge_{i\in I}{t_i}}
{ }
\and
\Infer[$\vee$]
{\Gamma \vdash e':\textstyle\bigvee_{i\in I} t_i
\and {\small(\forall i\in I)} \quad \Gamma, x:t_i\vdash e:t
}
{
\Gamma\vdash e\subs x {e'} : t
}
{ }
\end{mathpar}
\subsection{Algorithmic system}
\subsubsection{Explicitly annotated terms}
\begin{equation}
\begin{array}{lrclr}
\textbf{Annotations} & \anns &::=& \{\ann\Gamma t,\ldots{,}\ann\Gamma t\}\\
\textbf{Expressions} &e &::=& c\alt x\alt\lambda x{:}\anns.e
\alt e e\alt (e,e)\alt \pi_i e \alt
\tcase{e}{\tau}{e}{e} \alt \letexp{x{:}\anns}{e}{e}\\[.3mm]
\textbf{Values} & v &::=& c\alt\lambda x{:}\anns.e\alt (v,v)
\end{array}
\end{equation}
For annotations we write $\{t_1,\ldots{,} t_n\}$ for
$\{\ann\varnothing{t_1},\ldots{,}\ann\varnothing{t_n}\}$ and just $t$
for $\{\ann\varnothing{t}\}$. So for instance we write $\lambda
x{:}t.e$ for $\lambda x{:}\{\ann\varnothing{t}\}.e$ and
$\letexp{x{:}\{t_1,\ldots{,} t_n\}}{e}{e}$ instead of $\letexp{x{:}\{\ann\varnothing{t_1},\ldots{,}\ann\varnothing{t_n}\}}{e}{e}$
\subsubsection{Algorithmic typing rules} This system correspond to the
variant with more compact derivations.
\begin{mathpar}
\Infer[Const\AR]
{ }
{\Gamma\vdashA c:\basic{c}}
{ }
\quad
\Infer[Ax\AR]
{ }
{ \Gamma \vdashA x: \Gamma(x) }
{ x\in\dom\Gamma }
\\
\Infer[$\to$I\AR]
{{\small(\forall j\in J)} \\\Gamma,x:t_j\vdashA e:s_j}
{\Gamma\vdashA\lambda
x{:}\{\ann{\Gamma_i}{t_i}\}_{i \in I}.e:
\textstyle\bigwedge_{j\in J}\arrow{t_j}{s_j}}
{ J=\{i\in I\alt \Gamma\leq\Gamma_i\}}
\and
\Infer[$\to$E\AR]
{
\Gamma \vdashA e_1: {t_1}\quad
\Gamma \vdashA e_2: t_2
}
{\Gamma \vdashA {e_1}{e_2}: t_1\circ t_2 }
{\begin{array}{l}t_1\leq\Empty\to\Any\\[-1mm]t_2\leq\dom{t_1}\end{array} }
\\
\Infer[$\times$I\AR]
{\Gamma \vdashA e_1:t_1 \and \Gamma \vdashA e_2:t_2}
{\Gamma \vdashA (e_1,e_2):\pair {t_1} {t_2}}
{ }
\qquad
\Infer[$\times$E$_1$\AR]
{\Gamma \vdashA e:t\leq(\Any\times\Any)}
{\Gamma \vdashA \pi_1 e:\pi_1(t_1)}
{ } \quad
\Infer[$\times$E$_2$\AR]
{\Gamma \vdashA e:t\leq(\Any\times\Any)}
{\Gamma \vdashA \pi_2 e:\pi_2(t)}
{ }
\\
\Infer[$\neg_1$\AR]
{
\Gamma \vdash e:t_0\leq t \and \Gamma\vdash e_1: t_1
}
{\Gamma\vdash \tcase {e} t {e_1}{e_2}: t_1}
{ }
\qquad
\Infer[$\neg_2$\AR]
{
\Gamma \vdashA e:t_0\leq\neg t \and \Gamma\vdash e_2: t_2
}
{\Gamma\vdashA \tcase {e} t {e_1}{e_2}: t_2}
{ }
\\
\Infer[Let\AR]
{\Gamma\vdashA e_1:\textstyle\bigvee_{j\in J}t_j\\{\small(\forall j\in J)} \\ \Gamma, x:t_j\vdashA e_2:s_j}
{
\Gamma\vdashA\letexp {x{:}\{\ann{\Gamma_i}{t_i}\}_{i\in I}} {e_1}
{e_2} :\textstyle \bigvee_{j\in J}s_j
}
{ J=\{i\in I\alt \Gamma\leq\Gamma_i\}}
\end{mathpar}
\subsection{Properties}
\subsubsection{Type erasure}
\begin{align*}
\eras c & = c\\
\eras x & = x\\
\eras {\lambda x{:}\anns.e} & = \lambda x.\eras e\\
\eras {e_1e_2} &= \eras {e_1}\eras{e_2}\\
\eras {(e_1,e_2)} &= (\eras {e_1},\eras{e_2})\\
\eras {\pi_i e}&= \pi_i\eras e & i=1,2\\
\eras {\tcase{e}{\tau}{e_1}{e_2}}&= \tcase{\eras e}{\tau}{\eras{e_1}}{\eras{e_2}}\\
\eras {\letexp{x{:}\anns}{e_1}{e_2}} &= \eras{e_2}\subs{x}{\eras{e_1}}
\end{align*}
\subsubsection{Soundness of the algorithm}
If $\Gamma\vdashA e:t$ then $\Gamma\vdash \eras e: t$
\subsubsection{Completeness of the algorithm}
If $\Gamma\vdash e:t$ then $\exists e',t'$ such that $\eras{e'}=e$,
$t'\leq t$, and $\Gamma\vdashA e': t'$
\subsubsection{Preservation of the reductions}
Write the reduction rule for let and then note that
$e\reduces e'$ if and only if $\eras e \reduces \eras{e}$
(details to be checked, should we rather use $v$?)
\subsection{Normalization}
To every source term $e$ there exists many algorithmic terms $e'$ such
that $e=\eras{e'}$. The various $e'$ may vary for the annotations used
and the use of let's. We want to eliminate the latter possibility of
variability and consider only terms in which the let expressions are
in a particular form defined as follows.
\subsubsection{Normal form terms with explicit annotations}
\begin{equation}\label{expressions2}
\begin{array}{lrclr}
\textbf{Atomic expr} &a &::=& c\alt x\alt\lambda x{:}\anns.e\alt x x\alt \pi_i x\alt (x,x)
\alt \tcase{x}{t}{e}{e}\\[.3mm]
\textbf{Expressions} &e &::=& \letexp{x{:}\anns}{a}{e}\alt a \\[.3mm]
\textbf{Values} &v &::=& c\alt\lambda x{:}\anns.e\alt (v,v)\\
\end{array}
\end{equation}
Now it is possible to associate to every \emph{well-typed}
explicitly-typed term $e$ a
normal form that has the same type and the same reduction
semantics. This is done by induction on the derivation of the type for
$e$. Since every well-typed explicitly-typed term has a unique type
(and type derivation) then this can be done directly by induction on
the terms, where $\typof{e}$ denotes the unique type derived for $e$.
\begin{align*}
\norm {\lambda x{:}\anns.e} & = \lambda x{:}\anns.\norm e\\
\norm {e_1e_2} &= \letexp{x_1{:}\typof{e_1}}{\norm{e_1}}{\letexp{x_2{:}\typof{e_1}}{\norm{e_2}}{x_1x_2}}\\
\norm {(e_1,e_2)} &= \letexp{x_1{:}\typof{e_1}}{\norm{e_1}}{\letexp{x_2{:}\typof{e_1}}{\norm{e_2}}{(x_1,x_2)}}\\
\norm {\pi_i e}&= \letexp{x{:}\typof{e}}{\norm{e}}{\pi_ix} & i=1,2\\
\norm {\tcase{e}{\tau}{e_1}{e_2}}&= \letexp{x{:}\typof{e}}{\norm{e}}{\tcase{x}{\tau}{\norm{e_1}}{\norm{e_2}}}\\
\norm {e} &= e &\text{otherwise}
\end{align*}
The case apply only when the various $e$ $e_i$ are not already
variables (all the other cases are long to write).
Notice that $\eras e = \eras{\norm e}$.
Therefore what we have is that the soundness but, above all, the
completeness of the algorithm can be stated for normal forms:
If $\Gamma\vdash e:t$ then $\exists e',t'$ such that $e'$ is in normal
form, $\eras{e'}=e$,
$t'\leq t$, and $\Gamma\vdashA e': t'$
Summing up we have proved that a term of the source language is
typeable if and only if there exists a typeable normal form whose
erasure is that term. Given a term of the source language then we know
the structure of the candidate for the normal form (just apply the
same transformation above without type annotations) : it remains to
check wheter an annotation exists that makes that term typed. The
soundness of the solution then will be immediate (since by
construction the erasure will give the source language expression);
completeness is more difficult since first we have to prove that if we
did not find an annotation, then there does not exist an annotation
that make that term typeable and second that if that particular normal
form is not typeable then there cannot be any other normal form that
is typeable and whose erasure it the source language expression.
\newpage
\section{TAKE FOUR}
\subsection{Declarative system}
\subsubsection{Types}
\[
......
......@@ -80,6 +80,7 @@
\newcommand{\occ}[2]{#1{\downarrow}#2}
\newcommand{\basic}[1]{\text{\fontshape{\itdefault}\fontseries{\bfdefault}\selectfont b}_{#1}}
\newcommand{\tyof}[2]{\textsf{\textup{typeof}}_{#2}(#1)}
\newcommand{\typof}[1]{\textsf{\textup{typeof}}(#1)}
\newcommand{\typep}[3]{\textsf{\textup{Constr}}^{#1}_{#3}(#2)}
\newcommand{\Gp}[2]{\textsf{Env}^{#1}_{#2}}
\newcommand{\ite}[4]{\ensuremath{\texttt{if}\;#1\in#2\;\texttt{then}\;#3\;\texttt{else}\;#4}}
......@@ -152,6 +153,7 @@
\newcommand{\Even} {\textsf{Even}}
\newcommand{\Odd} {\textsf{Odd}}
\newcommand{\subst}[2]{\{#1 \mapsto #2\}}
\newcommand{\subs}[2]{\{#2/#1\}}
\newcommand{\fv}{\textsf{fv}}
\newcommand{\bv}{\textsf{bv}}
\newcommand{\var}{\textsf{var}}
......@@ -175,8 +177,9 @@
\newcommand{\values}[0]{\mathcal{V}}
\newcommand{\valsemantic}[1]{{\llbracket #1 \rrbracket}_{\values}}
\newcommand{\vvdash}[0]{\vdash_\values}
\newcommand{\AR}[0]{\ensuremath{_\mathcal{A}}}
\newcommand{\AR}{-Alg}%\ensuremath{_\mathcal{A}}}
\newcommand{\eras}[1]{\lceil#1\rceil}
\newcommand{\norm}[1]{\textsf{N}(#1)}
%\newcommand{\norm}[1]{\textsf{Norm}(#1)}
\newcommand{\semantic}[1]{{\llbracket #1 \rrbracket}}
\newcommand{\tenv}[0]{\vec \alpha}
......
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