Commit 06e28f12 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

new system

parent 81d24f66
......@@ -12,13 +12,22 @@
\begin{equation}
\begin{array}{lrclr}
\textbf{Expressions} &a &::=& 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]
\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]
\textbf{Values} & v &::=& c\alt\lambda x.e\alt (v,v)
\end{array}
\end{equation}
\subsubsection{Dynamic semantics}
\begin{equation}
(\lambda x.e)v\reduces e\subst x{v}
\end{equation}
plus context rules to implement an leftmost outermost weak reduction semantics.
\subsubsection{Typing rules}
Rules of Definition 3.5 of Barbanera Dezani + pairs + negation
Rules of Definition 3.5 of Barbanera Dezani + different union rule + pairs + negation
\begin{mathpar}
\Infer[Const]
......@@ -62,20 +71,24 @@ Rules of Definition 3.5 of Barbanera Dezani + pairs + negation
{\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}}
{ }
\qquad
\Infer[$\vee$]
{\Gamma, x:t_1\vdash e:t\and \Gamma, x:t_2\vdash e:t\and
\Gamma \vdash e':t_1\vee t_2 }
\Infer[Let]
{\Gamma \vdash e':t\and\Gamma, x:t'\vdash e:t}
{
\Gamma\vdash\letexp x {e'} e : t
}
{ }
\Infer[$\vee$]
{\Gamma, x:t_1 \vdash e:t \and \Gamma,x:t_2 \vdash e:t}
{\Gamma x:t_1\vee t_2 \vdash e: t}
{ }
\qquad
\\
\Infer[$\neg_1$]
\Infer[$\wedge$]
{\Gamma \vdash e:t_1 \and \Gamma \vdash e:t_2}
{\Gamma \vdash e: {t_1}\wedge {t_2}}
{ }
\qquad
\Infer[$\neg_1$]
{
\Gamma \vdash e:t \and \Gamma\vdash e_1: t_1
}
......@@ -95,6 +108,36 @@ Rules of Definition 3.5 of Barbanera Dezani + pairs + negation
{ }
\end{mathpar}
A different union rule, closer to the one by Barbanera Dezani is the
following one, which is meant to replace both the union rule and the
let rule above.
\begin{mathpar}
\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\letexp x {e'} e : t
}
{ }
\end{mathpar}
or better the following one that allows to deduce nested unions
without reserting to nested let's.
\begin{mathpar}
\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\letexp x {e'} e : t
}
{ }
\end{mathpar}
here however we can express less typings essentially because we use
the let expression instead of the substitution meta-notation as in
Barbanera-Dezani. However the idea is that on closed terms the two
systems should be equivalent.
\subsection{Algorithmic type system}
......@@ -127,6 +170,96 @@ just syntactic sugar for $\letexp x {e}{\tcase {x} t {e_1}{e_2}}$ and
So we find exactly the typing rule for Cduce's typecase.
Now we want to find a way to find a way to encode the derivations of
the previous system so that every term has a unique type derivation
that represent a family of type derivations in the previous system. To
that end we add to the terms of the previous system explicit type
annotations (ranged over by \anns) yielding the following
definition.
\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 \letexp{x{:}\anns}{e}{e} \alt
\tcase{e}{t}{e}{e}\\[.3mm]
\textbf{Values} & v &::=& c\alt\lambda x{:}\anns.e\alt (v,v)
\end{array}
\end{equation}
\subsubsection{Dynamic semantics}
\begin{equation}
(\lambda x.e)v\reduces e\subst x{v}
\end{equation}
plus context rules to implement an leftmost outermost weak reduction semantics.
\begin{mathpar}
\Infer[Const]
{ }
{\Gamma\vdash c:\basic{c}}
{ }
\quad
\Infer[Ax]
{ }
{ \Gamma \vdash x: \Gamma(x) }
{ x\in\dom\Gamma }
\\
\Infer[$\to$I]
{i=1..n\\\Gamma,x:t_i\vdash e:s_i}
{\Gamma\vdash\lambda x{:}\{t_1,...,t_n\}.e: \textstyle\bigwedge_{i=1..n}\arrow{t_i}{s_i}}
{ }
\qquad \Infer[$\to$E]
{
\Gamma \vdash e_1: \arrow {t_1}\quad
\Gamma \vdash e_2: t_2
}
{ \Gamma \vdash {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}}
{ }
\qquad
\Infer[$\times$E$_1$]
{\Gamma \vdash x:t\leq(\Any\times\Any)}
{\Gamma \vdash \pi_1 x:\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[$\neg_1$]
{
\Gamma \vdash e_1: t' \\ \Gamma(x)\leq t
}
{\Gamma\vdash \tcase {x} t {e_1}{e_2}: t'}
{x\in\dom{\Gamma}}
\quad
\Infer[$\neg_2$]
{
\Gamma\vdash e_2: t' \\ \Gamma(x)\leq\neg t
}
{\Gamma\vdash \tcase {x} t {e_1}{e_2}: t'}
{x\in\dom{\Gamma}}
%% \and
%% \Infer[$\neg$]
%% {
%% \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\vdash \tcase {x} t {e_1}{e_2}: t'}
%% {\text{(otherwise)}}
\\
\Infer[$\vee$]
{\Gamma\vdash e':\textstyle\bigvee_{i=1..n}s_i\\i=1..n \\ \Gamma, x:s_i\vdash e:t_i}
{
\Gamma\vdash\letexp {x{:}\{s_1,...,s_n\}} {e'} e :\textstyle \bigvee_{i=1..n}t_i
}
{ }
\end{mathpar}
\subsubsection{Normal form terms with explicit annotations}
\begin{equation}\label{expressions2}
......
......@@ -84,6 +84,8 @@
\newcommand{\Gp}[2]{\textsf{Env}^{#1}_{#2}}
\newcommand{\ite}[4]{\ensuremath{\texttt{if}\;#1\in#2\;\texttt{then}\;#3\;\texttt{else}\;#4}}
\newcommand{\Let}[3]{\ensuremath{\texttt{let}\;#1\;\texttt{=}\;#2\;\texttt{in}\;#3}}
\newcommand{\anns}{\ensuremath{A}}
\newcommand{\ann}[2]{#1{\triangleright}#2}
\newcommand{\alt}{~|~}
\newcommand{\arrow}[2]{#1\to #2}
\newcommand{\pair}[2]{#1\times #2}
......@@ -313,4 +315,4 @@
\makeatletter % allow us to mention @-commands
\def\arcr{\@arraycr}
\makeatother
\ No newline at end of file
\makeatother
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