PFPL Chapter 7 Evaluation Dynamics

Posted on In Disqus:

Please refer this link from page 55 to 60.

Another Forms of Dynamics

An evaluation dynamics is a relation between a phase and its value that is defined without detailing step-by-step evaluation process with notation $e \Downarrow v​$.

Cost dynamics enriched evaluation dynamics with cost measure specifying resource usage for evaluation as $e \Downarrow ^k v​$.

Evaluation Dynamics

The inductive definition of evaluation dynamics of E has notation $e \Downarrow v​$ stating that the closed expression $e​$ evaluates to the value $v​$ with following rules
$$
\dfrac{}{\text{num}[n] \Downarrow \text{num}[n]}\\
\dfrac{}{\text{str}[s] \Downarrow \text{str}[s]}\\
\dfrac{e_1 \Downarrow \text{num}[n_1] \phantom{“”}e_2 \Downarrow \text{num}[n_2] \phantom{“”}n_1 + n_2 = n}{\text{plus}(e_1;e_2)\Downarrow \text{num}[n]}\\
\dfrac{e_1 \Downarrow \text{str}[s_1] \phantom{“”}e_2 \Downarrow \text{str}[s_2] \phantom{“”}s_1 \wedge s_2 = s}{\text{str}(s_1;s_2)\Downarrow \text{str}[s]}\\
\dfrac{e \Downarrow \text{str}[s] \phantom{“”}|s| = n}{\text{len}(e)\Downarrow \text{num}[n]}\\
$$
The rule for let is a little bit tricky since it is not syntax-directed (since the premise of let is not sub-expression of the expression in the conclusion of that rule), also considering the by-value and by-name interpretation method.

The by-name and by-value versions are shown as
$$
\begin{aligned}
&\dfrac{[e_1/x]e \Downarrow v}{\text{let}(e_1;x.e) \Downarrow v}\\
&\dfrac{e_1 \Downarrow v_1 \phantom{“”}[v_1 / x]e\Downarrow v}{\text{let}(e_1;x.e)\Downarrow v}
\end{aligned}
$$

Induction on Evaluation Dynamics

To show $\mathcal P(e \Downarrow v)​$ holds, it is enough to show that $\mathcal P​$ is closed under

  • $\mathcal P(\text{num}[n] \Downarrow \text{num}[n])​$
  • $\mathcal P(\text{str}[s] \Downarrow \text{str}[s])​$
  • $\mathcal P(\text{plus}(e_1;e_2)\Downarrow \text{num}[n])​$ if $\mathcal P(e_1 \Downarrow \text{num}[n_1])​$, $\mathcal P(e_2 \Downarrow \text{num}[n_2])​$ and $n_1 + n_2 = n​$.
  • $\mathcal P(\text{cat}(e_1;e_2)\Downarrow \text{str}[s])​$ if $\mathcal P(e_1 \Downarrow \text{str}[s_1])​$, $\mathcal P(e_2 \Downarrow \text{str}[s_2])​$ and $s_1 \wedge s_2 = s​$.
  • $\mathcal P(\text{len}(e)\Downarrow \text{num}[n])$ if $\mathcal P(e \Downarrow \text{str}[s])$ and $|s| = n$.
  • $\mathcal P(\text{let}(e_1;x.e)\Downarrow v)$ if
    • (by-name) $\mathcal P([e_1 / x]e\Downarrow v)​$
    • (by-value) $\mathcal P(e_1 \Downarrow v_1)$ and $\mathcal P([v_1 / x]e\Downarrow v)$

Structural Dynamics is syntax-directed, while evaluation dynamics is not, thus the proof differs.

Lemma

If $e \Downarrow v​$, then $v \text{ val}​$.

About the deterministic part of the evaluation, we can prove that if $e \Downarrow v_1$ and $e \Downarrow v_2$, then $v_1 = v_2$.

By induction, we can see that $e \Downarrow v$ is deterministic. Suppose $e \Downarrow v_1$, $e \Downarrow v_2$ and $v_1 \neq v_2$, then it doesn’t follow the behavior of induction of evaluation dynamics, thus causes contradiction.

Relation with Structural Dynamics

The structural dynamics describes a step-by-step process of execution.

The evaluation dynamics focuses on the initial and final states.

Thus the equivalence is established between the complete execution sequences in structural dynamics and the execution judgment in evaluation dynamics.

Equivalence Theorem and Lemma

For all the closed expressions $e$ and value $v$, $e \longmapsto^\ast v \iff e \Downarrow v$.

  • $e \Downarrow v \Rightarrow e \longmapsto^\ast v$ can be established since $v\text{ val}$ is always a final state, thus $\longmapsto^*$ complete transform always holds.
  • $e \longmapsto^\ast v \Rightarrow e \Downarrow v$ can be decomposed into
    • $e \longmapsto e’, e’\Downarrow v \Rightarrow e \Downarrow v$.
      • The syntax-directed part, take $v = \text{num}[n], e=\text{plus}(e_0;e_1), e’=\text{plus}(e_0’;e_1)$, then by induction we can see $e_0’ \Downarrow \text{num}[n_0], e_1 \Downarrow \text{num}[n_1], n_0 + n_1 = n$. Then by induction $e_0 \Downarrow \text{num}[n_0]$.
      • The not syntax-directed part, we take by-value form of let definition to ensure the same construction. $e = \text{let}(e_0;x.e_1), e’=\text{let}(e_0’;x.e_1)$, then we get $e_o’\Downarrow v_0, [v_0/x]e_1\Downarrow v$. By induction, $e_0 \longmapsto e_0’$ and $e_0 \Downarrow v_0$, thus let part holds.
    • $e \longmapsto e’, e’ \text{ val} \Rightarrow e \Downarrow e’$ holds by previous lemma and $e’ \text{ val} \Rightarrow e’ \Downarrow e’​$.

Revisit Type Safety

Consider the type safety provided on structural dynamics, then we can see that it relies on the state transform feature. In this way we tries to move the preservation and progress feature on evaluation dynamics.

For preservation the analog might be $e : \tau, e\Downarrow v \Rightarrow v:\tau$. For progress the analog “$e :\tau \Rightarrow e \Downarrow v$ for some $v$”. But it requires more than progress itself. It implies every closed expression $e$ must be evaluated to a value.

So we can instrument the dynamics with explicit checks for dynamic types and say an expression with dynamic type error must be statically ill-typed. In contrapositive we say a statically well-typed program do not cause a dynamic type error. The difficulty is to set explicitly consider a form of errors to ensure that it cannot exist. In this way, a semblance or analogy of type safety is established with evaluation dynamics.

Judgment $e ??$ states that the expression $e$ goes wrong when executed, with example definition like
$$
\dfrac{}{\text{plus}(\text{str}[s];e_2)??}\\
\dfrac{e_1 \text{ val}}{\text{plus}(e_1;\text{str}[s])??}
$$

Theorem and Corollary

If $e??$, then $\not \exists \tau$ that $e:\tau$.

If $e : \tau$, then $\neg (e ??)$.

Cost Dynamics

The cost dynamics is enriched by specifying the resource, quantify by $k$ of evaluation steps with definition
$$
\dfrac{}{\text{num}[n] \Downarrow^0 \text{num}[n]}\\
\dfrac{}{\text{str}[s] \Downarrow^0 \text{str}[s]}\\
\dfrac{e_1 \Downarrow^{k_1} \text{num}[n_1] \phantom{“”}e_2 \Downarrow^{k_2} \text{num}[n_2] \phantom{“”}n_1 + n_2 = n}{\text{plus}(e_1;e_2)\Downarrow^{k_1 + k_2 + 1} \text{num}[n]}\\
\dfrac{e_1 \Downarrow^{k_1} \text{str}[s_1] \phantom{“”}e_2 \Downarrow^{k_2} \text{str}[s_2] \phantom{“”}s_1 \wedge s_2 = s}{\text{str}(s_1;s_2)\Downarrow^{k_1 + k_2 + 1} \text{str}[s]}\\
\dfrac{e \Downarrow^k \text{str}[s] \phantom{“”}|s| = n}{\text{len}(e)\Downarrow^{k+1} \text{num}[n]}\\
$$
The by-name and by-value versions are shown as
$$
\begin{aligned}
&\dfrac{[e_1/x]e \Downarrow^k v}{\text{let}(e_1;x.e) \Downarrow^{k+1} v}\\
&\dfrac{e_1 \Downarrow^{k_1} v_1 \phantom{“”}[v_1 / x]e\Downarrow^{k_2} v}{\text{let}(e_1;x.e)\Downarrow^{k_1 + k_2 + 1} v}
\end{aligned}
$$

Theorem

For any closed expression $e$ and closed value $v$ of same type $\tau$, $e \Downarrow ^k v\iff e \longmapsto ^k v$.

Exercise

7.4

If we use $e ??​$ for checked error, then we mix checked error and unchecked error together, which make the progress theorem extend to both unchecked and checked error. Also in Type Safety this chapter, the theorem and its corollary won’t hold. The obvious alternative is to separate one notation into two, one for checked (solely for express safety) and the other is for unchecked (allow for run-time error in well-typed expressions).

7.5

Example of the environmental evaluation dynamics are shown as
$$
\dfrac{\Delta \vdash x_1 \Downarrow \text{num}[n_1] \phantom{“”}\Delta \vdash x_2 \Downarrow \text{num}[n_2]}{\Delta\vdash\text{plus}(x_1;x_2)\Downarrow \text{num}[n_1+n_2]}
$$
with no usage of substitution, let can be defined as
$$
\dfrac{\Delta \vdash e_1 \Downarrow v_1\phantom{“”}\Delta,x\Downarrow v_1 \vdash e \Downarrow v}{\Delta \vdash \text{let}(e_1;x.e)\Downarrow v}
$$
To show $x_1 \Downarrow v_1,\dots,x_n\Downarrow v_n\vdash e \Downarrow v\iff [v_1,\dots,v_n/x_1,\dots,x_n]e \Downarrow v​$:

  • $\Rightarrow​$: we can use induction to show by rule induction to see that:

    Inspired by Chapter 4 Substitution lemma.

    Suppose $[v_1,\dots,v_n/x_1,\dots,x_n]e \Downarrow v$, then

    • Suppose $e = \text{plus}(x_1;x_2), v=\text{num}[n_1+n_2],v_1=\text{num}[n_1], v_2=\text{num}[n_2]$, then it holds.

    • Suppose $e = \text{let}(e_1;x.e_2), x \notin x_1,\dots,x_n​$, then

      $$
      [v_1,\dots,v_n/x_1,\dots,x_n]e = \text{let}([v_1,\dots,v_n/x_1,\dots,x_n]e_1;x.[v_1,\dots,v_n/x_1,\dots,x_n]e_2)
      $$

      By induction of let rule, $[v_1,\dots,v_n/x_1,\dots x_n]e \Downarrow v$ holds if $[v_1,\dots,v_n/x_1,\dots x_n]e_1 \Downarrow v_1$ holds and $\Delta, x\Downarrow v_1 \vdash[v_1,\dots,v_n/x_1,\dots x_n]e_2\Downarrow v $. Thus it holds.

  • $\Leftarrow$: Also use induction and focus on the structure of $e$:

    Suppose $x_1 \Downarrow v_1,\dots,x_n\Downarrow v_n\vdash e\Downarrow v$, then consider the $e$ as plus or let, then it seems trivial that the induction holds.