Commit 9319ca46 authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

added defintion of \worra

parent 873f6e7f
......@@ -9,5 +9,5 @@ pairs, list
\subsection{Adding polymorphism}
Problem, polymorphic types as infinite intersection. So for instance $\worra{\alpha\to\alpha}{t} = t$
Problem, polymorphic types as infinite intersection. So for instance $\worra{(\alpha\to\alpha)}{t} = t$
......@@ -44,7 +44,7 @@ Let $t$ be a functional type (i.e., $t\leq\Empty\to\Any$) then
\apply t s = \min \{ u \alt t\leq s\to u\}
\]
\[
\worra t s = \max\{u\leq \dom t\alt t\circ(\dom t\setminus u)\leq \neg s\}
\worra t s = \min\{u\leq \dom t\alt t\circ(\dom t\setminus u)\leq \neg s\}
\]
......@@ -88,3 +88,13 @@ Given an expression $e$ and a type $t$ we use $\Gamma^p_{\Gamma,e,t}$ to denote
{ \ite e t {e_1}{e_2}\not\in\dom\Gamma}
\\\end{mathpar}
The side condition for constants is probably interesting only for functional constants that have union and/or intersection arrow types
\subsection{Algorithms}
Define how to compute $t\circ s$ and $\worra t s$
If
\[ t \simeq \bigvee_{j\in J}\left(\bigwedge_{i\in P_j}(s_i\to t_i)\bigwedge_{i\in N_j}\neg(s_i'\to t_i')\right) \]
then
\[
\worra t s = \dom t \wedge\bigvee_{j\in J}\bigvee_{\{i\in P_j\alt u\wedge t_i\not=\varnothing\}}s_i
\]
......@@ -50,7 +50,20 @@
\newcommand{\ite}[4]{\ensuremath{\texttt{if}\;#1\in#2\;\texttt{then}\;#3\;\texttt{else}\;#4}}
\newcommand{\alt}{~|~}
\newcommand{\arrow}[2]{#1\to #2}
\newcommand{\worra}[2]{#1\mathop{\,\square\,} #2}
\DeclareFontFamily{U}{mathb}{}
\DeclareFontShape{U}{mathb}{m}{n}{
<-5.5> mathb5
<5.5-6.5> mathb6
<6.5-7.5> mathb7
<7.5-8.5> mathb8
<8.5-9.5> mathb9
<9.5-11.5> mathb10
<11.5-> mathb12
}{}
\DeclareSymbolFont{mathb}{U}{mathb}{m}{n}
\DeclareMathSymbol{\sqdot}{\mathbin}{mathb}{"0D}% name to be checked
\newcommand{\worra}[2]{#1\mathop{\,\sqdot\,} #2}
\newcommand{\apply}[2]{#1\circ#2}
\newcommand {\Empty} {\textsf{Empty}}%\MyMathBb{0}}
\newcommand {\Any} {\textsf{Any}}%\MyMathBb{1}}
......
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