Commit 3c6c2c26 by Giuseppe Castagna

 \subsection{Declarative system} \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}$ \subsubsection{Terms} \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] \end{array} \subsubsection{Typing rules} Rules of Definition 3.5 of Barbanera Dezani + pairs + negation \begin{mathpar} \Infer[Const] { } {\Gamma\vdash c:\basic{c}} { } \quad \Infer[Ax] { } { \Gamma \vdash x: \Gamma(x) } { x\in\dom\Gamma } % \qquad % \Infer[Inter] % { \Gamma \vdash e:t_1\\\Gamma \vdash e:t_2 } % { \Gamma \vdash e: t_1 \wedge t_2 } % { } \\ \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}} { } \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 } { \Gamma\vdash\letexp x {e'} 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} \subsection{Algorithmic type system} The idea is to translate terms above in to explicitly annotated notrmal form and prove that a term above is well typed if and only if its translation is well typed for a suitable annotation. In particular the typing rule for cases will be obtained by combining the union rule with the case rule and using two subsumption rules. Intuitively \begin{mathpar} \inferrule*{ \inferrule*{ \inferrule*{\Gamma, x: t{\wedge} t_\circ\vdash x: t{\wedge} t_\circ\quad t\wedge t_\circ\leq t}{\Gamma, x: t\wedge t_\circ\vdash x: t} \Gamma, x: t{\wedge} t_\circ\vdash e_1: t'} {\Gamma, x: t\wedge t_\circ\vdash \tcase {x} t {e_1}{e_2}:t'} \inferrule{ \inferrule*{...}{\Gamma, x: \neg t\wedge t_\circ\vdash x: \neg t} \Gamma, x: \neg t{\wedge} t_\circ\vdash e_2: t} {\Gamma, x:\neg t\wedge t_\circ\vdash \tcase {x} t {e_1}{e_2}:t'} \Gamma\vdash e:t_\circ } {\Gamma\vdash \letexp x {e}{\tcase {x} t {e_1}{e_2}:t'}} \end{mathpar} Note: $t_\circ =(t\wedge t_\circ)\vee(\neg t\wedge t_\circ$) \subsubsection{Normal form terms with explicit annotations} \label{expressions2} \begin{array}{lrclr} \textbf{Atomic expr} &a &::=& c\alt x\alt\lambda x{:}\{t,...,t\}.e\alt x x\alt \pi_i x\alt (x,x) \alt \tcase{x}{t}{e}{e}\\[.3mm] \textbf{Expressions} &e &::=& \letexp{x{:}\{t,...,t\}}{a}{e}\alt a \\[.3mm] \textbf{Values} &v &::=& c\alt\lambda x{:}\{t,...,t\}.e\alt (v,v)\\ \end{array} \subsubsection{Algorithmic typing rules} \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, x: t_0{\wedge} t\vdash e_1: t' } {\Gamma,x:t_0\vdash \tcase {x} t {e_1}{e_2}: t'} {t_0\wedge\neg t = \Empty} \quad \Infer[$\neg_2$] { \Gamma, x: t_0{\wedge} \neg t\vdash e_2: t' } {\Gamma,x:t_0\vdash \tcase {x} t {e_1}{e_2}: t'} {t_0\wedge t = \Empty} \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}t_i\\i=1..n \\ \Gamma, x:t_i\vdash e:t} { \Gamma\vdash\letexp {x{:}\{t_1,...,t_n\}} {e'} e : t } { } \end{mathpar}