Commit 12183920 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Typos 1,2 → 0,1

parent b8f74c00
......@@ -94,7 +94,7 @@ values. We write $v\in t$ if the most specific type of $v$ is a subtype of $t$ (
The dynamic semantics is defined as a classic left-to-right call-by-value reduction for a $\lambda$-calculus with pairs, enriched with specific rules for type-cases. We have the following notions of reduction:\vspace{-1.2mm}
\[
\begin{array}{rcll}
(\lambda^{\wedge_{i\in I}s_i\to t_i} x.e)v &\reduces& e\subst x v\\[-.4mm]
(\lambda^{\wedge_{i\in I}s_i\to t_i} x.e)\,v &\reduces& e\subst x v\\[-.4mm]
\pi_i(v_1,v_2) &\reduces& v_i & i=1,2\\[-.4mm]
\tcase{v}{t}{e_1}{e_2} &\reduces& e_1 &v\in t\\[-.4mm]
\tcase{v}{t}{e_1}{e_2} &\reduces& e_2 &v\not\in t\\[-1.3mm]
......@@ -291,7 +291,7 @@ 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 (for $i=1,2$, and undefined otherwise)\vspace{-.4mm}
the path $\varpi$, that is (for $i=0,1$, and undefined otherwise)\vspace{-.4mm}
%% \[
%% \begin{array}{l}
%% \begin{array}{r@{\downarrow}l@{\quad=\quad}l}
......@@ -307,8 +307,8 @@ the path $\varpi$, that is (for $i=1,2$, and undefined otherwise)\vspace{-.4mm}
%% \]
\[
\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&
e&\epsilon & e & (e_1,e_2)& l.\varpi & \occ{e_1}\varpi &\pi_1 e& f.\varpi & \occ{e}\varpi\\
e_0\,e_1& i.\varpi & \occ{e_i}\varpi \quad\qquad& (e_1,e_2)& r.\varpi & \occ{e_2}\varpi \quad\qquad&
\pi_2 e& s.\varpi & \occ{e}\varpi\\[-.4mm]
\end{array}
\]
......
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