small fixes

extensions.tex

@@ -21,7 +21,7 @@ following syntactic sugar and that form the \emph{record types} of our language\
 \item $\orecord{\ell_1=t_1, \ldots, \ell_n=t_n}$ for $\record{\ell_1=t_1 \ldots \ell_n=t_n}{\Any \vee \Undef}$ (open records).
 \end{itemize}
 plus the notation $\mathtt{\ell \eqq t}$ to denote optional fields,
-which corresponds to using in the quasi-constant function notation de
+which corresponds to using in the quasi-constant function notation the
 field $\ell = t \vee \Undef$. 
 
 
@@ -73,7 +73,7 @@ Expressions are then typed by the following rules (already in algorithmic form).
         {e.\ell\not\in\dom\Gamma}
 
 \end{mathpar}
-To extend occorrence typing to records we add the paths the following values: $\varpi\in\{\ldots,a_\ell,u_\ell^1,u_\ell^2,r_\ell\}^*$, with 
+To extend occurrence typing to records we add the paths the following values: $\varpi\in\{\ldots,a_\ell,u_\ell^1,u_\ell^2,r_\ell\}^*$, with 
 \(e.\ell\downarrow a_\ell.\varpi =\occ{e}\varpi\), 
 \(\recdel e \ell\downarrow r_\ell.\varpi = \occ{e}\varpi\), and
 \(\recupd{e_1}\ell{e_2}\downarrow u_\ell^i.\varpi = \occ{e_i}\varpi\)
@@ -91,17 +91,17 @@ and add the following rules for the new paths:
 
         \\
         
-    \Infer[PExt1]
+    \Infer[PUpd1]
         { \pvdash \Gamma e t \varpi:t'}
         { \pvdash \Gamma e t \varpi.u_\ell^1: (\recdel {t'} \ell) + \crecord{\ell \eqq \Any}}
         { }
         
-    \Infer[PExt2]
+    \Infer[PUpd2]
         { \pvdash \Gamma e t \varpi:t}
         { \pvdash \Gamma e t \varpi.u_\ell^2: \proj \ell t'}
         { }
 \end{mathpar}
-Derving the algorithm from these rules is then straightforward:
+Deriving the algorithm from these rules is then straightforward:
 \[
 \begin{array}{lcl}
   \constr{\varpi.a_\ell}{\Gamma,e,t} & = & \orecord {\ell: \env {\Gamma,e,t} (\varpi)}\\
@@ -126,7 +126,7 @@ Derving the algorithm from these rules is then straightforward:
 Notice that the effect of doing $\recdel t \ell + \crecord{\ell \eqq
   \Any}$ corresponds to setting the field $\ell$ of the (record) type
 $t$ to the type $\Any\vee\Undef$, that is, to the type of all
-undefined fields in an open record. So \Rule{PDel} and \Rule{PExt1}
+undefined fields in an open record. So \Rule{PDel} and \Rule{PUpd1}
 mean that if we remove, add, or redefine a field $\ell$ in an expression $e$
 then all we can deduce for $e$ is that its field $\ell$ is undefined: since the original field was destroyed we do not have any information on it apart from the static one.
 For instance, consider the test:

language2.tex

@@ -146,7 +146,7 @@ core and the use of subtyping, given by the following typing rules:
 %            {\Gamma\vdash \ite {e} t {e_1}{e_2}: t'}
 %            { }
  \\
-      \Infer[Proj]
+      \Infer[Sel]
   {\Gamma \vdash e:\pair{t_1}{t_2}}
   {\Gamma \vdash \pi_i e:t_i}
   { }
@@ -287,30 +287,34 @@ root of the tree).
 
 Let $e$ be an expression and $\varpi\in\{0,1,l,r,f,s\}^*$ a
 \emph{path}; we denote $\occ e\varpi$ the occurrence of $e$ reached by
-the path $\varpi$, that is
+the path $\varpi$, that is (for $i=1,2$, and undefined otherwise)
+%% \[
+%% \begin{array}{l}
+%% \begin{array}{r@{\downarrow}l@{\quad=\quad}l}
+%% e&\epsilon & e\\
+%% e_0e_1& i.\varpi & \occ{e_i}\varpi\qquad i=0,1\\
+%% (e_0,e_1)& l.\varpi & \occ{e_0}\varpi\\
+%% (e_0,e_1)& r.\varpi & \occ{e_1}\varpi\\
+%% \pi_1 e& f.\varpi & \occ{e}\varpi\\
+%% \pi_2 e& s.\varpi & \occ{e}\varpi\\
+%% \end{array}\\
+%% \text{undefined otherwise}
+%% \end{array}
+%% \]
 \[
-\begin{array}{l}
-\begin{array}{r@{\downarrow}l@{\quad=\quad}l}
-e&\epsilon & e\\
-e_0e_1& i.\varpi & \occ{e_i}\varpi\qquad i=0,1\\
-(e_0,e_1)& l.\varpi & \occ{e_0}\varpi\\
-(e_0,e_1)& r.\varpi & \occ{e_1}\varpi\\
-\pi_1 e& f.\varpi & \occ{e}\varpi\\
+\begin{array}{r@{\downarrow}l@{\quad=\quad}lr@{\downarrow}l@{\quad=\quad}lr@{\downarrow}l@{\quad=\quad}l}
+e&\epsilon & e & (e_0,e_1)& l.\varpi & \occ{e_0}\varpi &\pi_1 e& f.\varpi & \occ{e}\varpi\\
+e_0e_1& i.\varpi & \occ{e_i}\varpi \quad\qquad& (e_0,e_1)& r.\varpi & \occ{e_1}\varpi \quad\qquad&
 \pi_2 e& s.\varpi & \occ{e}\varpi\\
-\end{array}\\
-\text{undefined otherwise}
 \end{array}
 \]
-
-
 To ease our analysis we used different directions for each kind of
 term. So we have $0$ and $1$ for the function and argument of an
 application, $l$ and $r$ for the $l$eft and $r$ight expressions forming a pair,
 and $f$ and $s$ for the argument of a $f$irst or of a $s$econd projection. Note also that we do not consider occurrences
 under $\lambda$'s (since their type is frozen in their annotations) and type-cases (since they reset the analysis).\beppe{Is it what I wrote here true?}
 
-The judgments  $\Gamma \evdash e t \Gamma'$ are then deduced by the following two rules: 
-\begin{mathpar}
+The judgments  $\Gamma \evdash e t \Gamma'$ are then deduced by the following two rules: \begin{mathpar}
 %        \Infer[Base]
 %            { \Gamma \vdash e':t' }
 %            { \Gamma \cvdash p e t e':t' }
@@ -346,7 +350,6 @@ algorithmic viewpoint, this will imply the computation of a fix-point
 judgements of the form $\pvdash {\Gamma}  e t \varpi:t'$ where
 $\varpi$ is a path to an expression occurring in $e$. This is given by the following set
 of rules.
-
 \begin{mathpar}
     \Infer[PSubs]
         { \pvdash \Gamma e t \varpi:t_1 \\ t_1\leq t_2 }