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

bla

parent 5b431ab8
......@@ -12,14 +12,38 @@
\begin{equation}
\begin{array}{lrclr}
\textbf{Test Types} &\tau &::=& b\alt \Empty\to \neg\Empty\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 \letexp{x}{e}{e} \alt
\tcase{e}{t}{e}{e}\\[.3mm]
\tcase{x}{\tau}{e}{e}\\[.3mm]
\textbf{Values} & v &::=& c\alt\lambda x.e\alt (v,v)
\end{array}
\end{equation}
This essentially are the terms of the CDuce language with three
differences.
First, the type case expression in CDuce is of the form $\tcase
{x\,{:}{=}\,e} t {e_1}{e_2}$. It allows to test the type of the value
result of a generic
expression $e$; this value is bound to the variable $x$ in the
branches $e_1$ and $e_2$. Here we generalize this expression using two
distinct expression for binding (the let-expression) and the
test (which is just on variables). Thus the CDuce expression is
nothing but syntactic sugar for $\letexp x {e}{\tcase {x} t
{e_1}{e_2}}$ in our system.
The second important difference is that $\lambda$-abstractions do not
have an explicit type annotation. The consequence of this is that we
restrict all the arrow type present in a type-case to be of the form
$\Empty\to\neg\Empty$. In practice this means that whenever we test
the type of a value we can only check whther it or some of its
subcomponent are functions or not (i.e., they have the type
$\Empty\to\neg\Empty$ or not) but we cannot test the precise type of
that subcomponent. The reason is that CDuce resorts to the explicit
annotations to determine whether ...
\subsubsection{Dynamic semantics}
add rules for projections and typecase
\begin{equation}
(\lambda x.e)v\reduces e\subst x{v}
\end{equation}
......@@ -188,76 +212,79 @@ definition.
\end{array}
\end{equation}
\subsubsection{Dynamic semantics}
The dynamic semantics is the same as before modulo de presence of the
annotations (which are not used for the reduction)
\begin{equation}
(\lambda x.e)v\reduces e\subst x{v}
(\lambda x{:}A.e)v\reduces e\subst x{v}
\end{equation}
plus context rules to implement an leftmost outermost weak reduction semantics.
\subsubsection{Algorithmic typing rules}
\begin{mathpar}
\Infer[Const]
\Infer[Const\AR]
{ }
{\Gamma\vdash c:\basic{c}}
{\Gamma\vdashA c:\basic{c}}
{ }
\quad
\Infer[Ax]
\Infer[Ax\AR]
{ }
{ \Gamma \vdash x: \Gamma(x) }
{ \Gamma \vdashA x: \Gamma(x) }
{ x\in\dom\Gamma }
\\
\Infer[$\to$I]
{\forall j\in J \\\Gamma,x:t_j\vdash e:s_j}
{\Gamma\vdash\lambda
\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\}}
\\\Infer[$\to$E]
\\\Infer[$\to$E\AR]
{
\Gamma \vdash e_1: \arrow {t_1}\quad
\Gamma \vdash e_2: t_2
\Gamma \vdashA e_1: \arrow {t_1}\quad
\Gamma \vdashA e_2: t_2
}
{ \Gamma \vdash {e_1}{e_2}: t_1\circ t_2 }
{ \Gamma \vdashA {e_1}{e_2}: t_1\circ t_2 }
{t_1\leq\Empty\to\Any,t_2\leq\dom{t_1} }
\\
\Infer[$\times$I]
{\Gamma \vdash x_1:t_1 \and \Gamma \vdash x_2:t_2}
{\Gamma \vdash (x_1,x_2):\pair {t_1} {t_2}}
\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$]
{\Gamma \vdash x:t\leq(\Any\times\Any)}
{\Gamma \vdash \pi_1 x:\pi_1(t_1)}
\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$]
{\Gamma \vdash x:t\leq(\Any\times\Any)}
{\Gamma \vdash \pi_2 x:\pi_2(t)}
\Infer[$\times$E$_2$\AR]
{\Gamma \vdashA e:t\leq(\Any\times\Any)}
{\Gamma \vdashA \pi_2 e:\pi_2(t)}
{ }
\\
\Infer[$\neg_1$]
\Infer[$\neg_1$\AR]
{
\Gamma \vdash e_1: t' \\ \Gamma(x)\leq t
\Gamma \vdashA e_1: t' \\ \Gamma(x)\leq t
}
{\Gamma\vdash \tcase {x} t {e_1}{e_2}: t'}
{\Gamma\vdashA \tcase {x} t {e_1}{e_2}: t'}
{x\in\dom{\Gamma}}
\quad
\Infer[$\neg_2$]
\Infer[$\neg_2$\AR]
{
\Gamma\vdash e_2: t' \\ \Gamma(x)\leq\neg t
\Gamma\vdashA e_2: t' \\ \Gamma(x)\leq\neg t
}
{\Gamma\vdash \tcase {x} t {e_1}{e_2}: t'}
{\Gamma\vdashA \tcase {x} t {e_1}{e_2}: t'}
{x\in\dom{\Gamma}}
%% \and
%% \Infer[$\neg$]
%% \Infer[$\neg$\AR]
%% {
%% \Gamma, x: t_0{\wedge} t\vdash e_1: t' \\ \Gamma, x: t_0{\wedge}
%% \neg t\vdash e_2: t'
%% \Gamma, x: t_0{\wedge} t\vdashA e_1: t' \\ \Gamma, x: t_0{\wedge}
%% \neg t\vdashA e_2: t'
%% }
%% {\Gamma,x:t_0\vdash \tcase {x} t {e_1}{e_2}: t'}
%% {\Gamma,x:t_0\vdashA \tcase {x} t {e_1}{e_2}: t'}
%% {\text{(otherwise)}}
\\
\Infer[Let]
{\Gamma\vdash e_1:\textstyle\bigvee_{j\in J}t_j\\j\in J \\ \Gamma, x:t_j\vdash e_2:s_j}
\Infer[Let\AR]
{\Gamma\vdashA e_1:\textstyle\bigvee_{j\in J}t_j\\j\in J \\ \Gamma, x:t_j\vdashA e_2:s_j}
{
\Gamma\vdash\letexp {x{:}\{\ann{\Gamma_i}{t_i}\}_{i\in I}} {e_1}
\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\}}
......
......@@ -175,7 +175,8 @@
\newcommand{\values}[0]{\mathcal{V}}
\newcommand{\valsemantic}[1]{{\llbracket #1 \rrbracket}_{\values}}
\newcommand{\vvdash}[0]{\vdash_\values}
%\newcommand{\tvdash}[0]{\vdash_G}
\newcommand{\AR}[0]{\ensuremath{_\mathcal{A}}}
%\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