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

trying some new rules... (wip)

parent 11b0b876
......@@ -82,24 +82,25 @@ x\in\dom\Gamma\\
\\
\Infer[AbsBase]
{
\textstyle {\dt'=\dt\cup\left\{s\setminus\bigcup_{s'\in\dt}s'\right\}}\\
T=\{(s',t')\,|\,s'\in\dt' \text{ and } \Gamma,(x:s')\vdash e:t'\}}
\Gamma,(x:t')\vdash e:t}
{
\Gamma\vdash_\dt\lambda x:s.e:\textstyle \bigwedge_{(s',t')\in T}\arrow {s'} {t'}
\Gamma\vdash_{t'}\lambda x:s.e:\arrow {t'} {t}
}
{ }
\\
\Infer[AbsSplit]
{\forall u\in\dt.\ \Gamma,(x:u)\vdash e\triangleright_x\dt_u\\
\Gamma\textstyle\vdash_{\bigcup_{u\in\dt_u}\dt_u}\lambda x:s.e: t
{
\Gamma,(x:t')\vdash e\triangleright_x\dt\\
\textstyle {\dt'=\dt\cup\left\{t'\setminus\bigcup_{s'\in\dt}s'\right\}}\\
\forall u\in\dt'.\ \Gamma\textstyle\vdash_u \lambda x:s.e: t_u
}
{
\Gamma\vdash_\dt\lambda x:s.e: t
\Gamma\vdash_{t'}\lambda x:s.e: \textstyle\bigwedge_{u\in\dt'}t_u
}
{ }
\\
\Infer[Abs]
{\Gamma\vdash_{\{s\}} \lambda x:s.e: t}
{\Gamma\vdash_{s} \lambda x:s.e: t}
{
\Gamma\vdash\lambda x:s.e: t
}
......@@ -181,13 +182,30 @@ TODO: Algorithmic rules
}
{ \Gamma \vdash c \triangleright_x \{\} }
{}
% \hfill
% \Infer[Abs]
% {\Gamma,(y:s)\vdash e\triangleright_x\dt}
% {
% \Gamma\vdash\lambda y:s.\ e\triangleright_x\dt
% }
% {x\neq y}
\\
\Infer[AbsBase]
{\Gamma,(y:t)\vdash e\triangleright_x\dt}
{
\Gamma\vdash_t\lambda y:s.e\triangleright_x \dt
}
{ }
\qquad
\Infer[AbsSplit]
{
\Gamma,(y:t)\vdash e\triangleright_y\dt\\
\forall u\in\dt.\ \Gamma\vdash_u\lambda y:s.e\triangleright_x \dt_u
}
{
\Gamma\vdash_t\lambda y:s.e\triangleright_x \textstyle\bigcup_{u\in\dt}\dt_u
}
{ }
\\
\Infer[Abs]
{\Gamma\vdash_s \lambda x:s.e \triangleright_x \dt}
{
\Gamma\vdash\lambda y:s.e\triangleright_x\dt
}
{ y\neq x }
\\
\Infer[Pair]
{i\in\{1,2\}\\
......@@ -273,8 +291,6 @@ TODO: Algorithmic rules
{ }
\end{mathpar}
TODO: update rule ABS
TODO: Candidates for a variable should be a special "all splits".
Otherwise, $\letexp{x}{\cdots}{x}$ will never be splitted.
......
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