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

write valsemantic in paper instead of refering to appendix

parent 4e1e83e5
......@@ -139,13 +139,15 @@ call-by-value weak reduction for a $\lambda$-calculus with pairs, enriched with
\end{array}
\]
where $\valsemantic t$ denotes, intuitively, the set of values that have type $t$
(see \Appendix\ref{app:parallel} for a formal definition
where $\valsemantic t$ denotes, intuitively, the set of values that have type $t$.
Formally, $\valsemantic t$ is inductively defined by as: $\valsemantic c \eqdef \{\basic{c}\}$,\,\,\,
$\valsemantic{\lambda^{\wedge_{i\in I}s_i\to t_i} x.e} \eqdef \{t\alt t\simeq (\wedge_{i\in I}s_i\to t_i)\wedge(\wedge_{j\in J}s_j'\to t_j'), t\not\leq\Empty\}$,\,\,\,
$\valsemantic{(v_1,v_2)} \eqdef \valsemantic{v_1}\times\valsemantic{v_2}$
\footnote{This definition may look
complicated but it is necessary to handle some corner cases for
negated arrow types (cf.\ rule \Rule{Abs-} in
Section~\ref{sec:static}). For instance, it states that $\lambda^{\Int{\to}\Int}.x\in
(\Int{\to}\Int)\wedge\neg(\Bool{\to}\Int)$.}).\\
\valsemantic{(\Int{\to}\Int)\wedge\neg(\Bool{\to}\Int)}$.}.\\
Contextual reductions are
defined by the following evaluation contexts:
......
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