bla

new_system_beppe.tex

@@ -219,6 +219,8 @@ variant with more compact derivations.
   \eras {\tcase{e}{\tau}{e_1}{e_2}}&= \tcase{\eras e}{\tau}{\eras{e_1}}{\eras{e_2}}\\
   \eras {\letexp{x{:}\anns}{e_1}{e_2}} &= \eras{e_2}\subs{x}{\eras{e_1}}
 \end{align*}
+(notice the rule for the let).
+
 \subsubsection{Soundness of the algorithm}
 If $\Gamma\vdashA e:t$ then $\Gamma\vdash \eras e: t$
 \subsubsection{Completeness of the algorithm}
@@ -231,7 +233,7 @@ $e\reduces e'$ if and only if $\eras e \reduces \eras{e}$
 
 \subsection{Normalization}
 
-To every source term $e$ there exists many algorithmic terms $e'$ such
+For every source term $e$ there exist many algorithmic terms $e'$ such
 that $e=\eras{e'}$. The various $e'$ may vary for the annotations used
 and the use of let's. We want to eliminate the latter possibility of
 variability and consider only terms in which the let expressions are
@@ -248,7 +250,7 @@ in a particular form defined as follows.
   \end{array}
 \end{equation}
 Now it is possible to associate to every \emph{well-typed}
-explicitly-typed term $e$ a
+explicitly-typed term $e$ a particular
 normal form that has the same type and the same reduction
 semantics. This is done by induction on the derivation of the type for
 $e$. Since every well-typed explicitly-typed term has a unique type
@@ -256,16 +258,18 @@ $e$. Since every well-typed explicitly-typed term has a unique type
 the terms, where $\typof{e}$ denotes the unique type derived for $e$.
 \begin{align*}
   \norm {\lambda x{:}\anns.e} & = \lambda x{:}\anns.\norm e\\
-  \norm {e_1e_2} &= \letexp{x_1{:}\typof{e_1}}{\norm{e_1}}{\letexp{x_2{:}\typof{e_1}}{\norm{e_2}}{x_1x_2}}\\
-  \norm {(e_1,e_2)} &=   \letexp{x_1{:}\typof{e_1}}{\norm{e_1}}{\letexp{x_2{:}\typof{e_1}}{\norm{e_2}}{(x_1,x_2)}}\\
-  \norm {\pi_i e}&=  \letexp{x{:}\typof{e}}{\norm{e}}{\pi_ix} & i=1,2\\
-  \norm {\tcase{e}{\tau}{e_1}{e_2}}&=  \letexp{x{:}\typof{e}}{\norm{e}}{\tcase{x}{\tau}{\norm{e_1}}{\norm{e_2}}}\\
+  \norm {e_1e_2} &=
+  \letexp{x_1{:}\typof{e_1}}{\norm{e_1}}{\letexp{x_2{:}\typof{e_1}}{\norm{e_2}}{x_1x_2}}
+  &x_1,x_2\text{ fresh}\\
+  \norm {(e_1,e_2)} &=   \letexp{x_1{:}\typof{e_1}}{\norm{e_1}}{\letexp{x_2{:}\typof{e_1}}{\norm{e_2}}{(x_1,x_2)}} &x_1,x_2\text{ fresh}\\
+  \norm {\pi_i e}&=  \letexp{x{:}\typof{e}}{\norm{e}}{\pi_ix} \qquad x\text{ fresh}& i=1,2\\
+  \norm {\tcase{e}{\tau}{e_1}{e_2}}&=  \letexp{x{:}\typof{e}}{\norm{e}}{\tcase{x}{\tau}{\norm{e_1}}{\norm{e_2}}}&x\text{ fresh}\\
   \norm {e} &= e &\text{otherwise}
 \end{align*}
-The case apply only when the various $e$ $e_i$ are not already
+The cases apply only when the various $e$ $e_i$ are not already
 variables (all the other cases are long to write).
 
-Notice that $\eras e = \eras{\norm e}$.
+Notice that $\eras e = \eras{\norm e}$ (and that they have the same type).
 
 Therefore what we have is that the soundness but, above all, the
 completeness of the algorithm can be stated for normal forms: