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

some precisions

parent 3be82ddc
......@@ -60,10 +60,12 @@ e_0e_1& i.\varpi & \occ{e_i}\varpi\qquad i=0,1\\
undefined otherwise
A type environment $\Gamma$ is a mapping from occurrences (i.e., expressions) to types. We use $\Gamma_1,\Gamma_2$ for the type environment obtained by unioning the two type environments giving priority to $\Gamma_2$ (define formally)
A type environment $\Gamma$ is a mapping from occurrences (i.e., expressions) to types, up to alpha-renaming (i.e., $\lambda^tx.x$ and $\lambda^ty.y$ are mapped to the same type, if any).
It is necessary to map alpha-equivalent expressions to the same type in order for our type system to be invariant by alpha-renaming.
We use $\Gamma_1,\Gamma_2$ for the type environment obtained by unioning the two type environments giving priority to $\Gamma_2$ (define formally).
We suppose w.l.o.g that all variables abstracted in $\lambda$-abstractions are distincts (otherwise we should add an extra parameter in our definitions for the variables).
We suppose w.l.o.g that all variables abstracted in $\lambda$-abstractions are distincts (otherwise we can alpha-rename $\lambda$-abstractions).
Let $e$ be an expression, $t$ a type, $\Gamma$ a type environment, $\varpi\in\{0,1\}^*$ and $p\in\{+,-\}$, we define $\typep p \varpi {\Gamma,e,t}$ and $\Gp p {\Gamma,e,t}(\varpi)$ as follows
......@@ -148,6 +150,7 @@ Define how to compute $t\circ s$ and $\worra t s$
If
\[ 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) \]
with \[\forall i\in I.\ \bigwedge_{p\in P_i}(s_p\to t_p)\bigwedge_{n\in N_i}\neg(s_n'\to t_n') \not\simeq \Empty\]
then
\begin{eqnarray*}
\dom{t} & = & \bigwedge_{i\in I}\bigvee_{p\in P_i}s_p\\[4mm]
......
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