Commit 567d8968 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

Explained formula worra

parent f42df3a1
......@@ -601,10 +601,16 @@ t_p)\bigwedge_{n\in N_i}\neg(s_n'\to t_n') \not\simeq \Empty$ for all
$i$ in $I$. For such a $t$ and any type $s$ then we have:
%
\begin{equation}
\worra t s = \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)
\worra t s = \dom t \wedge\bigvee_{i\in I}\left(\bigwedge_{\{P\subseteq P_i\alt s\leq \bigvee_{p \in P} \neg t_p\}}\left(\bigvee_{p \in P} \neg s_p\right) \right)
\end{equation}
\beppe{Explain the formula?}
The proof that this type satisfies \eqref{worra} is given in the Appendix~\ref{app:worra}.
The formula considers only the positive arrows of each summand that
forms $t$ and states that, for each summand, whenever you take a subset
$P$ of its positive arrows that cannot yield results in
$s$ (since $s$ does not overlap the intersection of the codomains of these arrows), then
the success of the test cannot depend on these arrows and therefore
the intersection of the domains of these arrows---i.e., the values that would precisely select that set of arrows---can be removed from $\dom t$. The proof
that this type satisfies \eqref{worra} is given in the
Appendix~\ref{app:worra}.
......
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