Commit 92584f9a authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

final cleaning?

parent f92f321b
......@@ -333,4 +333,7 @@ The authors thank Paul-André Melliès for his help on type ranking.
\end{document}
\newcommand{\negspace}{\vspace{-.5mm}}
As we explained in the introduction, both TypeScript and Flow deduce the type
\code{(number$\vee$string) $\to$ (number$\vee$string)} for the first definition of the function \code{foo} in~\eqref{foo}, and the more precise type\vspace{-3pt}
\begin{equation}\label{tyinter}
\code{(number$\to$number)$\,\wedge\,$(string$\to$string)}\vspace{-3pt}
\end{equation}
can be deduced by these languages only if they are instructed to do so: the
programmer has to explicitly annotate \code{foo} with the
type \eqref{tyinter}: we did it in \eqref{foo2} using Flow---the TypeScript annotation for it is much heavier. But this seems like overkill, since a simple
analysis of the body of \code{foo} in \eqref{foo} shows that its execution may have
two possible behaviors according to whether the parameter \code{x} has
type \code{number} or not (i.e., or \code{(number$\vee$string)$\setminus$number}, that is \code{string}), and this is
should be enough for the system to deduce the type \eqref{tyinter}
even in the absence the annotation given in \eqref{foo2}.
%
In this section we show how to do it by using the theory of occurrence
typing we developed in the first part of the paper. In particular, we
collect the different types that are assigned to the parameter of a function
in its body, and use this information to partition the domain of the function
and to re-type its body. Consider a more involved example in a pseudo
TypeScript that uses our notation
\begin{alltt}\color{darkblue}\morecompact
function (x \textcolor{darkred}{: \(\tau\)}) \{
return (x \(\in\) Real) ? ((x \(\in\) Int) ? x+1 : sqrt(x)) : !x; \refstepcounter{equation} \mbox{\color{black}\rm(\theequation)}\label{foorefine}
\}
\end{alltt}
where we assume that \code{Int} is a
subtype of \code{Real}. When $\tau$ is \code{Real$\vee$Bool} we want to deduce for this function the
type
\code{$(\Int\to\Int)\wedge(\Real\backslash\Int\to\Real)\wedge(\Bool\to\Bool)$}.
When $\tau$ is \Any,
then the function must be rejected (since it tries to type
\code{!x} under the assumption that \code x\ has type
\code{$\neg\Real$}). Notice that typing the function under the
hypothesis that $\tau$ is \Any,
allows us to capture user-defined discrimination as defined
by~\citet{THF10} since, for instance
\begin{alltt}\color{darkblue}\morecompact
let is_int x = (x\(\in\)Int)? true : false
in if is_int z then z+1 else 42
\end{alltt}
is well typed since the function \code{is\_int} is given type
$(\Int\to\True)\wedge(\neg\Int\to\False)$. We propose a more general
approach than the one by~\citet{THF10} since we allow the programmer to hint a particular type for the
argument and let the system deduce, if possible, an intersection type for the
function.
We start by considering the system where $\lambda$-abstractions are
typed by a single arrow and later generalize it to the case of
intersections of arrows. First, we define the auxiliary judgement
%\begin{displaymath}
\(
\Gamma \vdash e\triangleright\psi
\)
%\end{displaymath}
where $\Gamma$ is a typing environement, $e$ an expression and $\psi$
a mapping from variables to sets of types. Intuitively $\psi(x)$ denotes
the set that contains the types of all the occurrences of $x$ in $e$. This
judgement can be deduced by the following deduction system
that collects type information on the variables that are $\lambda$-abstracted
(i.e., those in the domain of $\Gamma$, since lambdas are our only
binders):\vspace{-1.5mm}
\begin{mathpar}
\Infer[Var]
{
}
{ \Gamma \vdash x \triangleright\{x \mapsto \{ \Gamma(x) \} \} }
{}
\hfill
\Infer[Const]
{
}
{ \Gamma \vdash c \triangleright \varnothing }
{}
\hfill
\Infer[Abs]
{\Gamma,x:s\vdash e\triangleright\psi}
{
\Gamma\vdash\lambda x:s.e\triangleright\psi\setminus\{x\}
}
{}
\vspace{-2.3mm}\\
\Infer[App]
{
\Gamma \vdash e_1\triangleright\psi_1 \\
\Gamma\vdash e_2\triangleright\psi_2
}
{ \Gamma \vdash {e_1}{e_2}\triangleright\psi_1\cup\psi_2 }
{}
\hfill
\Infer[Pair]
{\Gamma \vdash e_1\triangleright\psi_1 \and \Gamma \vdash e_2\triangleright\psi_2}
{\Gamma \vdash (e_1,e_2)\triangleright\psi_1\cup\psi_2}
{}
\hfill
\Infer[Proj]
{\Gamma \vdash e\triangleright\psi}
{\Gamma \vdash \pi_i e\triangleright\psi}
{}
\vspace{-2.3mm}\\
\Infer[Case]
{\Gamma\vdash e\triangleright\psi_\circ\\
\Gamma \evdash e t \Gamma_1\\ \Gamma_1\vdash e_1\triangleright\psi_1\\
\Gamma \evdash e {\neg t} \Gamma_2 \\ \Gamma_2\vdash e_2\triangleright\psi_2}
{\Gamma\vdash \ifty{e}{t}{e_1}{e_2}\triangleright\psi_\circ\cup\psi_1\cup\psi_2}
{}\vspace{-1.4mm}
\end{mathpar}
Where $\psi\setminus\{x\}$ is the function defined as $\psi$ but undefined on $x$ and $\psi_1\cup \psi_2$ denotes component-wise union%
\iflongversion%
, that is :
\begin{displaymath}
(\psi_1\cup \psi_2)(x) = \left\{\begin{array}{ll}
\psi_1 (x) & \text{if~} x\notin
\dom{\psi_2}\\
\psi_2 (x) & \text{if~} x\notin
\dom{\psi_1}\\
\psi_1(x)\cup\psi_2(x) & \text{otherwise}
\end{array}\right.
\end{displaymath}
\noindent
\else.~\fi
All that remains to do is to replace the rule [{\sc Abs}+] with the
following rule\vspace{-.8mm}
\begin{mathpar}
\Infer[AbsInf+]
{\Gamma,x:s\vdash e\triangleright\psi
\and
\Gamma,x:s\vdash e:t
\and
T = \{ (s,t) \} \cup \{ (u,w) ~|~
u\in\psi(x) \land \Gamma,x:u\vdash e:w \}}
{
\Gamma\vdash\lambda x{:}s.e:\textstyle\bigwedge_{(u,w) \in T}u\to w
}
{}\vspace{-2.5mm}
\end{mathpar}
Note the invariant that the domain of
$\psi$ is always conatined in the
domain of $\Gamma$ restricted to variables.
Simply put, this rule first collects all possible types that are deduced
for a variable $x$ during the typing of the body of the $\lambda$ and then uses them to re-type the body
under this new refined hypothesis for the type of
$x$. The re-typing ensures that the type safety property
carries over to this new rule.
This system is enough to type our case study \eqref{foorefine} for the case $\tau$
defined as \code{Real$\vee$Bool}. Indeed, the analysis of the body yields
$\psi(x)=\{\Int,\Real\setminus\Int\}$ for the branch \code{(x\,$\in$\,Int) ? x+1 : sqrt(x)} and, since
\code{$(\Bool\vee\Real)\setminus\Real = \Bool$}, yields
$\psi(x)=\{\Bool\}$ for the branch \code{!x}. So the function
will be checked for the input types $\Int$, $\Real\setminus\Int$, and
\Bool, yielding the expected result.
It is not too difficult to generalize this rule when the lambda is
typed by an intersection type:\vspace{-.8mm}
\begin{mathpar}
\Infer[AbsInf+] {\forall i\in I\hspace*{2mm}\Gamma,x:s_i\vdash
e\triangleright\psi_i
\and
\Gamma,x:s_i\vdash
e : t_i
\and
T_i = \{ (u, w) ~|~ u\in\psi_i(x) \land \Gamma, x:u\vdash e : w\}
} {\textstyle \Gamma\vdash\lambda^{\bigwedge_{i\in
I}s_i\to t_i} x.e:\bigwedge_{i\in I}(s_i\to
t_i)\land\bigwedge_{(u, w)\in T_i}(u\to w) } {}\vspace{-3mm}
\end{mathpar}
For each arrow declared in the interface of the function, we
first typecheck the body of the function as usual (to check that the
arrow is valid) and collect the refined types for the parameter $x$.
Then we deduce all possible output types for this refined set of input
types and add the resulting arrows to the type deduced for the whole
function (see Appendix~\ref{app:optimize} for an even more precise rule).
\kim{We define the rule on the type system not the algorithm. I think
we could do the same (by collecting type scheme) in $\psi$ but we
then need to choose a candidate in the type scheme \ldots }
In summary, in order to type a
function we use the type-cases on its parameter to partition the
domain of the function and we type-check the function on each single partition rather
than on the union thereof. Of course, we could use much a finer
partition: the finest (but impossible) one is to check the function
against the singleton types of all its inputs. But any finer partition
would return, in many cases, not a much better information, since most
partitions would collapse on the same return type: type-cases on the
parameter are the tipping points that are likely to make a difference, by returning different
types for different partitions thus yielding more precise typing.
Even though type cases in the body of a
function are tipping points that may change the type of the result
of the function, they are not the only ones: applications of overloaded functions play exactly the same role. We
therefore add to our deduction system a last further rule:\\[1mm]
\centerline{\(
\Infer[OverApp]
{
\Gamma \vdash e : \textstyle\bigvee \bigwedge_{i \in I}t_i\to{}s_i\\
\Gamma \vdash x : t\\
\Gamma \vdash e\triangleright\psi_1\\
\Gamma \vdash x\triangleright\psi_2\\
}
{ \Gamma \vdash\textstyle
{e}{~x}\triangleright\psi_1\cup\psi_2\cup\bigcup_{i\in I}\{
x\mapsto t\wedge t_i\} }
{(t\wedge t_i\not\simeq\Empty)}
\)}\\
Whenever a function parameter is the argument of an
overloaded function, we record as possible types for this parameter
all the domains $t_i$ of the arrows that type the overloaded
function, restricted (via intersection) by the static type $t$ of the parameter and provided that the type is not empty ($t\wedge t_i\not\simeq\Empty$). We show the remarkable power of this rule on some practical examples in Section~\ref{sec:practical}.
\ignore{\color{darkred} RANDOM THOUGHTS:
A delicate point is the definition of the union
$\psi_1\cup\psi_2$. The simplest possible definition is the
component-wise union. This definition is enough to avoid the problem
of typecases on casted values and it is also enough to type our case
study, as we showed before. However if we want a more precise typing
discipline we may want to consider a more sophisticated way of
combining the information collected by the various $\psi$. For
instance, consider the following pair
\[\code{( \ite x s {e_1}{e_2} , \ite x t {e_3}{e_4} )}\]
Then we have $x:\Any\vdash \code{( \ite x s {e_1}{e_2} , \ite x t
{e_3}{e_4} )}\triangleright x\mapsto\{s,\neg s, t, \neg t\}$. However if this
code is the body of a function with parameter $x$, then it may be
tempting to try to produce a finer-grained analysis: for example,
instead of checking as input type just $s$ and $t$ one could check
instead $s\setminus t$, $t\setminus s$, and $s\wedge t$, whenever these
three types are not empty. This can be obtained by defining the union
operation as follows:
\[ (\psi_0\cup\psi_1)(x)=\{ t \alt \exists t_1\in\psi_1(x), t_2\in\psi_2(x), t=t_1\setminus t_2 \text{ or } t=t_2\setminus t_1 \text{ or } t=t_1\wedge t_2\text{ and } t\not\simeq\Empty\}\]
Do we really gain in precision? I think the gain is minimum. All we may obtain just come from a polymorphic use of the variable, but we can hardly gain more. Probably it is not worth the effort. As a concrete case consider
\[\code{function x \{ ( \ite x {\texttt{String|Bool}} {x}{x} , \ite x {\texttt{Bool|Int}} {x}{x} )} \}\]
So what?
A simple solution would be to define the union as follows
\begin{equation}
(\psi_0\cup\psi_1)(x)=
\left\{\begin{array}{ll}
\psi_i(x) &\text{ if }\psi_i(x)\subseteq\psi_{((i+1)\,\text{mod}\,2)}(x)\\
\psi_0(x)\cup\psi_1(x) &\text{ otherwise}
\end{array}\right.
\end{equation}
and $\psi_1(x)\subseteq\psi_2(x)\iff \forall\tau\in\psi_1(x),\exists \tau'\in\psi_2(x),\tau\leq\tau'$
This would be interesting to avoid to use as domains those in
$\psi_\circ$ that would be split in two in the $\psi_1$ and $\psi_2$
of the ``if'' ... but it is probably better to check it by modifying
the rule of ``if'' (that is, add $\psi_\circ$ only for when it brings new
information).
}
\subsection{Some issues and reflexions...}
\paragraph{PROBLEM WITH THE Case RULE} The refinement rules of section \ref{sec:refining} cannot type precisely the following function:
\begin{equation}\label{exptre}
\lambda (x:\Any).\ \ifty{x}{\Int}{\true}{\false}
\end{equation}
Indeed, no occurence of $x$ appears in the then branch nor in the else branch.
The only occurence of $x$ is within the test and is typed under the initial environment
where $x$ is $\Any$.
NOTE: the implementation in the prototype differs from the rules,
that's why this function can be typed precisely with the prototype.
\paragraph{PROBLEM WITH THE OverApp RULE}
The OverApp rule of section \ref{sec:refining} has two weaknesses:
\begin{itemize}
\item It ignores what is done with the value of $f x$ (maybe the result of $f x$ does not matter)
\item It might not be general enough in some cases. For instance, when the type system will support polymorphism,
it will be hard to deduce anything about $x$ for the expression $f (\texttt{id } x)$ (with $\texttt{id}$ being the identity).
\end{itemize}
In the alternative system below, I propose a generalization of the OverApp rule that
improves these two points.
\paragraph{REFLEXIONS ABOUT \ref{app:flowanalysis}}
\begin{itemize}
\item The rules establish relations between variables (by using multiples environments),
but at the end, when typing a lambda abstraction $\lambda x.\ e$,
only the data about the $x$ variable is used.
When a function takes two parameters $x$ and $y$ ($\lambda x.\ \lambda y.\ e$),
the rules apply to the outer lambda abstraction first, and only then,
when the type of $x$ has been splitted,
the inner lambda abstraction is typed and refined under all possible
types for $x$, in an independent way.
So, is it really worth it to remember relations between all variables each time?\\
This remark also applies to the
system in \ref{sec:refining} : why do we remember data about all variables in $\Psi$
whereas only the data about $x$ is used ?
\item For the $\texttt{let}$, it annoys me to preemptively split the environment into many
almost-"atomic" environments.
I have the feeling that we loose some of the power of set theoretic types:
we treat "atomic" environments separately instead of using the power of the union operator.
Splitting the environment should be done only when we know that it matters.
\item It does not work on this simple example:
$\lambda (x:\Any).\ \texttt{let }y \texttt{\,=\,} x \texttt{\,in\,} \ifty{y}{Int}{x}{0}$\\
In order to deduce that it might be interesting to consider the case $y\in \Int$,
the $\texttt{let}$ rule should look at what is done with $y$ after the $\texttt{in}$
instead of blindly splitting the environments just by looking at the definition of $y$.
\end{itemize}
\subsection{Alternative rules for refining function types (with control flow support?)}
\begin{mathpar}
\Infer[Base]
{
}
{ \Gamma \vdash e \triangleright_x \varnothing }
{e\text{ a variable or constant}}
\hfill
\Infer[Abs]
{\Gamma,(y:s)\vdash e\triangleright_x\psi}
{
\Gamma\vdash\lambda y:s.e\triangleright_x\psi
}
{}
\vspace{-2.3mm}\\
\Infer[Pair]
{\Gamma \vdash e_1\triangleright_x\psi_1 \and \Gamma \vdash e_2\triangleright_x\psi_2}
{\Gamma \vdash (e_1,e_2)\triangleright_x\psi_1\cup\psi_2}
{}
\hfill
\Infer[Proj]
{\Gamma \vdash e\triangleright_x\psi}
{\Gamma \vdash \pi_i e\triangleright_x\psi}
{}
\vspace{-2.3mm}\\
\Infer[Case]
{\Gamma\vdash e\triangleright_x\psi_\circ\\
\Gamma \evdash e t \{\Gamma_1^i\}_{i\in I}\\ \forall i\in I.\ \Gamma_1^i\vdash e_1\triangleright_x\psi_1^i\\
\Gamma \evdash e {\neg t} \{\Gamma_2^j\}_{j\in J}\\ \forall j\in J.\ \Gamma_2^j\vdash e_2\triangleright_x\psi_2^j}
{\Gamma\vdash \ifty{e}{t}{e_1}{e_2}\triangleright_x\psi_\circ
\cup\bigcup_{i\in I}(\psi_1^i\cup \{\Gamma_1^i(x)\})
\cup\bigcup_{j\in J}(\psi_2^j\cup \{\Gamma_2^j(x)\})}
{}
\vspace{-2.3mm}\\
% \Infer[App]
% {
% \Gamma \vdash e_1\triangleright_x\psi_1 \\
% \Gamma\vdash e_2\triangleright_x\psi_2
% }
% { \Gamma \vdash {e_1}{e_2}\triangleright_x\psi_1\cup\psi_2 }
% {e_2\text{ not an occurence}}
% \vspace{-2.3mm}\\
\Infer[OverApp]
{
\Gamma \vdash e_1 : \textstyle\bigvee \bigwedge_{i \in I}t_i\to{}s_i\\
\Gamma \vdash e_1\triangleright_x\psi_1\\
\forall i\in I.\ \Gamma\evdash{e_2}{t_i}\{\Gamma_i^j\}_{j\in J_i}
}
{ \Gamma \vdash\textstyle
{e_1}{e_2}\triangleright_x\psi_1\cup\bigcup_{i\in I}
%\{\bigvee_{j\in J_i}\Gamma_i^j(x)\} }
\bigcup_{j\in J_i}\{\Gamma_i^j(x)\} }
% {e_2\text{ an occurence}}
{}
\vspace{-2.3mm}\\
% \Infer[Let]
% {
% \Gamma \vdash e_1\triangleright_x\psi_1 \\
% \Gamma\vdash e_2\triangleright_x\psi_2
% }
% { \Gamma \vdash \texttt{let }y\texttt{\,=\,}e_1\texttt{\,in\,}e_2\triangleright_x\psi_1\cup\psi_2 }
% {e_1\text{ not an occurence}}
% \vspace{-2.3mm}\\
\Infer[OverLet]
{
\Gamma \vdash e_1: t\\
\Gamma, (y:t) \vdash e_2\triangleright_x\psi_x\\
\Gamma, (y:t) \vdash e_2\triangleright_y\psi_y\\
\forall u\in \psi_y.\ \Gamma\evdash{e_1}{u}\{\Gamma_u^i\}_{i\in I_u}
}
{ \Gamma \vdash\textstyle
\texttt{let }y\texttt{\,=\,}e_1\texttt{\,in\,}e_2\triangleright_x
\psi_x\cup\bigcup_{u\in \psi_y}
%\{\bigvee_{i\in I_u}\Gamma_u^i(x)\} }
\bigcup_{i\in I_u}\{\Gamma_u^i(x)\} }
% {e_1\text{ an occurence}}
{}
\vspace{-1.4mm}
\end{mathpar}
\[\begin{array}{l}
{\small\Rule{AbsInf++}}
\frac
{ \begin{array}{c}
T = \{ (s\setminus\bigvee_{s'\in\psi}s',t) \} \cup \{ (s',t') ~|~
s'\in\psi \land \Gamma,x:s'\vdash e:t' \}\\
\textstyle\Gamma,x:s\vdash e\triangleright_x\psi
\qquad
\Gamma,x:s\setminus\bigvee_{s'\in\psi}s'\vdash e:t
\end{array}
}
{
\textstyle\Gamma\vdash\lambda x{:}s.e:{\bigwedge_{(s',t') \in T}s'\to t'}
}
\end{array}\]
Typing rule for the LET:
\begin{mathpar}
\Infer[Let]
{
\Gamma \vdash e_1: t_1\\
\Gamma,y:t_1\vdash e_2\triangleright_y \psi\\
\psi' = \psi\cup\{t_1\setminus(\bigvee_{u\in\psi}u)\}\\
\forall u\in\psi'.\ \Gamma\evdash{e_1}{u}\{\Gamma_u^i\}_{i\in I_u}\\
\forall u\in\psi'.\ \forall i\in I_u.\ \Gamma_u^i, (y:u)\vdash e_2:t
}
{ \Gamma \vdash\textstyle
\texttt{let }y\texttt{\,=\,}e_1\texttt{\,in\,}e_2:t}
{}
\vspace{-1.4mm}
\end{mathpar}
TODO: $\triangleright$ should return a set of environments (mapping variables only) instead
of a set of types for a given variable?
TODO: The $\evdash e t$ operator is used in the Case, OverApp and OverLet rules,
but what we would actually need is an operator that computes the other direction:
which environments can surely lead to $e$ having the type $t$?
(instead of: which environments are implied by $e$ having the type $t$)
TODO: Should we totally remove the Abs- rule and the type schemes from the paper
(and from the proof) and restricts the arrow type tests accordingly?
It would simplify a lot, it would match the implementation,
and we wouldn't have to bother with weird completeness results.
TODO: With control flow, we can get rid of occurences in the environment if we
work with a normal form.
\subsection{Declarative system}
\begin{mathpar}
\Infer[Case]
{\Gamma\vdash e:t_0\\
\Gamma \evdash e t \{\Gamma^1_i\}_{i\in I} \\ \forall i\in I.\ \Gamma^1_i \vdash e_1:t'\\
\Gamma \evdash e {\neg t} \{\Gamma^2_j\}_{j\in J} \\ \forall j\in J.\ \Gamma^2_j \vdash e_2:t'}
{\Gamma\vdash \tcase {e} t {e_1}{e_2}: t'}
{ }
\\
\Infer[Id]
{ }
{\Gamma\evdash e t \{\Gamma\subst{e}{t}\}}
{ }
\qquad
\Infer[Comp]
{\Gamma\evdash e t \{\Gamma_i\}_{i\in I} \\ \forall i.\ \Gamma_i\evdash e t \bbGamma_i}
{\Gamma\evdash e t \bigcup_{i\in I}\bbGamma_i}
{ }
\qquad
\Infer[Inter]
%{\Gamma\vdash e:t' \\ \Gamma\subst{e}{t\wedge t'}\evdash e {t\wedge t'} \bbGamma}
{\Gamma\vdash e:t' \\ \Gamma\evdash e {t\wedge t'} \bbGamma}
{\Gamma\evdash e t \bbGamma}
{ }
\\
\Infer[EFQ]
{ }
{\Gamma,(e:\Empty)\evdash e t \{\}}
{ }
\qquad
\Infer[Pair]
{\forall i\in I.\ \Gamma\evdash{e_1}{t_i}\bbGamma_1^i \\ \forall i\in I.\ \Gamma\evdash{e_2}{s_i}\bbGamma_2^i}
{\Gamma\evdash {(e_1,e_2)} {\bigcup_{i\in I}(t_i,s_i)} \bigcup_{i\in I}\{\Gamma_1\land\Gamma_2\ |\ \Gamma_1\in\bbGamma_1^i, \Gamma_2\in\bbGamma_2^i\}}
{ }
\\
\Infer[App]
{\Gamma\vdash e_1:\bigvee_{i\in I}t_i \\ \forall i\in I.\ t_i\leq \arrow{\neg s_i}{s_i'} \text{ with } s_i'\land t = \varnothing \\ \forall i\in I.\ \Gamma\evdash{e_1}{t_i}\bbGamma_1^i \\ \forall i\in I.\ \Gamma\evdash{e_2}{s_i}\bbGamma_2^i}
{\Gamma\evdash {(e_1\ e_2)} {t} \bigcup_{i\in I}\{\Gamma_1\land\Gamma_2\ |\ \Gamma_1\in\bbGamma_1^i, \Gamma_2\in\bbGamma_2^i\}}
{ }
\\
\Infer[Case]
{\Gamma \evdash e {t_e} \{\Gamma^1_i\}_{i\in I} \\ \forall i\in I.\ \Gamma^1_i \evdash {e_1} {t} \bbGamma_i^1\\
\Gamma \evdash e {\neg t_e} \{\Gamma^2_j\}_{j\in J} \\ \forall j\in J.\ \Gamma^2_j \evdash {e_2} {t} \bbGamma_j^2}
{\Gamma\evdash {\tcase {e} {t_e} {e_1}{e_2}}{t} \left(\bigcup_{i\in I}\bbGamma_i^1\right) \cup \left(\bigcup_{j\in J}\bbGamma_j^2\right)}
{ }
\end{mathpar}
\subsection{Algorithmic system}
\[ t \simeq \bigvee_{i\in I}\left(\bigwedge_{p\in P_i}(s_p\to t_p)\bigwedge_{n\in N_i}\neg(s_n'\to t_n')\right) \]
\begin{eqnarray*}
\dom{t} & = & \bigwedge_{i\in I}\bigvee_{p\in P_i}s_p\\[4mm]
\apply t 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(\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)\\[4mm]
\worra t s & = & \left\{\left(\bigwedge_{p\in P_i}(s_p\to t_p)\bigwedge_{n\in N_i}\neg(s_n'\to t_n'),\ \dom t \wedge\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)\ |\ i\in I\right\}
\end{eqnarray*}
\begin{align*}
\Raux{\Gamma}((e_1\ e_2),t) =&\ \bigcup_{i\in I}\left\{\Gamma_1\land\Gamma_2\ |\ \Gamma_1\in\Raux{\Gamma}'(e_1,t_i),\ \Gamma_2\in\Raux{\Gamma}'(e_2,s_i)\right\}\\
&\text{ with } \{(t_i, s_i)\}_{i\in I}=\worra{\tyof{e_1}\Gamma}{t}\\
\Raux{\Gamma}((e_1,e_2),\bigvee_{i\in I}(t_i,s_i)) =&\ \bigcup_{i\in I}\left\{\Gamma_1\land\Gamma_2\ |\ \Gamma_1\in\Raux{\Gamma}'(e_1,t_i),\ \Gamma_2\in\Raux{\Gamma}'(e_2,s_i)\right\}\\
\Raux{\Gamma}(\tcase{e}{t_e}{e_1}{e_2},t) =&\ \left(\bigcup_{\Gamma_1\in\Raux{\Gamma}'(e,t_e)}\Raux{\Gamma_1}'(e_1,t)\right) \cup \left(\bigcup_{\Gamma_2\in\Raux{\Gamma}'(e,\neg t_e)}\Raux{\Gamma_2}'(e_2,t)\right)\\
%\Raux{\Gamma}'(e,t) =&\ \Raux{\Gamma\subst{e}{t\land\tyof{e}\Gamma}}(e, t\land\tyof{e}\Gamma)
\Raux{\Gamma}'(e,t) =&\ \{\Gamma'\ |\ \Gamma'\in \Raux{\Gamma\subst{e}{t\land\tyof{e}{\Gamma}}}(e, t\land\tyof{e}\Gamma),\ \Gamma'\text{ not empty}\}
\end{align*}
\begin{align*}
\RRefineStep{e,t}(\bbGamma) =&\ \bigcup_{\Gamma\in\bbGamma}{\Raux{\Gamma}'(e,t)}\\
\RRefine{e,t}(\Gamma) =&\ \lfp{\{\Gamma\}}(\RRefineStep{e,t})
\end{align*}
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