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

Merge branch 'master' of gitlab.math.univ-paris-diderot.fr:beppe/occurrence-typing

parents 11ec4aef 1c1bf33b
......@@ -356,7 +356,10 @@ The authors thank Paul-André Melliès for his help on type ranking.
%\input{new_system2}
\newpage
\section{New Formalization (Beppe)}
\input{new_system_beppe}
\newpage
\section{New system with normal form}
\input{new_system3}
......
\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{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]
\end{array}
\end{equation}
\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 of CDuce will be obtained by combining
the union rule with the case rule and using two subsumption
rules. Intuitively we have that Cduce's $\tcase {x\,{:}{=}\,e} t {e_1}{e_2}$ is
just syntactic sugar for $\letexp x {e}{\tcase {x} t {e_1}{e_2}}$ and
we have that:
\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$)]
So we find exactly the typing rule for Cduce's typecase.
\subsubsection{Normal form terms with explicit annotations}
\begin{equation}\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}
\end{equation}
\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}
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