Commit 1589fca0 authored by Mickael Laurent's avatar Mickael Laurent
Browse files

add some alternatives for worra + add Empty rule

parent aa97ba11
......@@ -80,6 +80,7 @@ Let $e$ be an expression, $t$ a type, $\Gamma$ a type environment, $\varpi\in\{0
&&\color{olive}(\arrow{\Gp p{\Gamma,e,t}{(\varpi.1)}}{\neg \Gp p {\Gamma,e,t} (\varpi)})\\
\color{teal} \typep{p}{\varpi.0}{\Gamma,e,t} & = & \color{teal}(\arrow{\dom{\occ e{\varpi.0}}}{\Gp p {\Gamma,e,t} (\varpi)})\setminus\\
&&\color{teal}(\arrow{\dom{\occ e{\varpi.0}}}{\neg \Gp p {\Gamma,e,t} (\varpi)})\\
\color{orange} \typep{p}{\varpi.0}{\Gamma,e,t} & = & \color{orange}\neg(\arrow{\Gp p{\Gamma,e,t}{(\varpi.1)}}{\neg \Gp p {\Gamma,e,t} (\varpi)})\\
\typep{p}{\varpi.1}{\Gamma,e,t} & = & \worra{\tyof{\occ e{\varpi.0}}\Gamma}{\Gp p {\Gamma,e,t} (\varpi)}\\ \\
\Gp p {\Gamma,e,t}(\varpi) &=& \typep p \varpi{\Gamma,e,t} \wedge \tyof {\occ e\varpi}\Gamma\\
\end{array}
......@@ -110,6 +111,11 @@ We define the following algorithmic system (we deduce at most one type for every
\begin{mathpar}
\Infer[Empty]
{ }
{\Gamma\vdash e:\Empty}
{\exists e' \in \dom\Gamma.\ \Gamma(e') \leq \Empty}
\\
\Infer[Occ]
{
}
......@@ -155,6 +161,8 @@ then
\begin{eqnarray*}
\dom{t} & = & \bigwedge_{i\in I}\bigvee_{p\in P_i}s_p\\[4mm]
t\circ s & = & \bigvee_{i\in I}\left(\bigvee_{\{Q\subsetneq P_i\alt s\not\leq\bigvee_{q\in Q}s_q\}}\left(\bigwedge_{p\in P_i\setminus Q}t_p\right)\right)\hspace*{1cm}\makebox[0cm][l]{(for $s\leq\dom{t}$)}\\[4mm]
\worra t s & = & \dom t \wedge\bigvee_{i\in I}\left(\bigvee_{\{p\in P_i\alt s\wedge t_p\not=\varnothing\}}s_p \setminus \bigvee_{\{p\in P_i\alt s\wedge t_p=\varnothing\}}s_p \right)
\worra t s & = & \dom t \wedge\bigvee_{i\in I}\left(\bigvee_{\{p\in P_i\alt s\wedge t_p\not=\varnothing\}}s_p \setminus \bigvee_{\{p\in P_i\alt s\wedge t_p=\varnothing\}}s_p \right)\\
\color{purple}\worra t s & = & \color{purple} {\dom t \wedge\bigvee_{i\in I}\left(\bigwedge_{\{p\in P_i\alt s\wedge t_p=\varnothing\}}\neg s_p \right)}\\
\color{orange}\worra t s & = & \color{orange} {\dom t \wedge\bigvee_{i\in I}\left(\bigwedge_{\{P\subset P_i\alt s\leq \bigvee_{p \in P} \neg t_p\}}\left(\bigvee_{p \in P} \neg s_p\right) \right)}
\end{eqnarray*}
\beppe{Explain, especially the last one}
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