Commit d28d9f3c authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files

typos

parent 5e32401a
......@@ -252,7 +252,7 @@ with
{\ite {(2, \true)} {\pair \Int \Bool} {2} {0} \idleadsto 2}
{(2, \true) \in \valsemantic {\pair \Int \Bool}}
\end{mathpar}
Notice that the rule \Rule{$\kappa$} applies a substitution from expressions to expressions (rather than from variables to expressions). This is formally defined as follows:
Notice that the rule \Rule{$\kappa$} applies a substitution from an expression to an expressions (rather than from a variable to an expressions). This is formally defined as follows:
\begin{definition}[Expression substitutions]
Expression substitutions, ranged over by $\rho$, map an expression into another expression. The application of an expressions substitution $\rho$ to an expression $e$, noted $e\rho$ is the capture avoiding replacement defined as follows:
\begin{itemize}
......
......@@ -135,12 +135,12 @@ For the ELSE branch we proceed as the above but considering the test $x_1x_2\in
In summary the algorithm is defined as follows:
\begin{description}
\item [THEN:] $\exists \sigma$ such that $t\sigma\leq\neg\tau$?
\item [THEN branch:] $\exists \sigma$ such that $t\sigma\leq\neg\tau$?
\begin{description}
\item[no:] no specialization is possible
\item[yes:] find $\sigma_\circ$ such that $\tau\leq t\sigma_\circ$ and refine in the ``then'' branch the type of $x_2$ as $u\sigma_\circ$, of $x_1$ as $s\sigma_\circ\to t\sigma_\circ$, and of $x_1x_2$ as $t\sigma_\circ$.
\end{description}
\item [ELSE:] $\exists \sigma$ such that $t\sigma\leq\tau$?
\item [ELSE branch:] $\exists \sigma$ such that $t\sigma\leq\tau$?
\begin{description}
\item[no:] no specialization is possible
\item[yes:] find $\sigma_\circ$ such that $\neg\tau\leq t\sigma_\circ$ and refine in the ``else'' branch the type of $x_2$ as $u\sigma_\circ$, of $x_1$ as $s\sigma_\circ\to t\sigma_\circ$, and of $x_1x_2$ as $t\sigma_\circ$.
......@@ -161,5 +161,5 @@ In other terms we want to enrich occurrence typing by instantiating
types in a particular way, only if we know that those types will be
instantiated all in the same way. For that we have to syntactically
distinguish polymorphic functions from monomorphic ones, so as to
deduce that $x_2$ in the example above as type
deduce that $x_2$ in the example above has type
$\forall\alpha.\alpha\to\alpha$, rather than $\alpha\to\alpha$.
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