PFPL Chapter 5 Dynamics

Posted on In Disqus:

Please refer this link from page 41 to 48.

Dynamics Keywords

Dynamics of a language describes how programs are executed.

  • Structural Dynamics: Defines transition system inductively specifies step-by-step process of executing a program.
  • Contextual Dynamics: A variation of structural dynamics.
  • Equational Dynamics: A collection of rules defining when one program is definitionally equivalent to another.

Transition System

Four Forms of Judgments

  1. $s \text{ state}$ for $s$ is a state for transition system.
  2. $s \text{ final}​$ where $s \text{ state}​$ and $s​$ is a final state.
  3. $s \text{ initial}$ where $s \text{ state}$ and $s$ is a initial state.
  4. $s\longmapsto s’$ where $s \text{ state}$ and $s’ \text{ state}$ asserting that $s$ may transition to state $s’$.

Concepts

If $s \text{ final}$, then there are no $s’ \text{ state}$ such that $s \longmapsto s’$.

Stuck

A state with no transition is possible is a stuck.

Thus all final states are stuck, not all stuck states are final.

Deterministic

A transition system is deterministic iff $\forall s \text{ state}$ there exists at most one state $s’$ such that $s \longmapsto s’$.

Otherwise it is non-deterministic.

Transition Sequence

A sequence of states $s_0, \dots, s_n$ such that $s_0 \text{ initial}$ and $s_i \longmapsto s_{i +1}$ for $0 \leq i \leq n - 1$.

Maximal and Complete

Transition sequence is maximal iff there is no such $s$ that $s_n \longmapsto s$ for a transition sequence.

Transition sequence is complete iff it is maximal and $s_n \text{ final}$.

The judgment $s \downarrow$ means that there’s a complete transition from $s$, meaning there exists $s’ \text{ final}$ such that $s \longmapsto^\ast s’​$.

Iteration

$$
\dfrac{}{s \longmapsto^\ast s}
$$

$$
\dfrac{s \longmapsto^\ast {s’}\phantom{“”} {s’}\longmapsto^\ast s’’}{s\longmapsto^\ast s’’}
$$

If we want to show that $P(s, s’)$ holds when $s \longmapsto s’$, it is enough to show two properties of $P​$:

  • $P(s, s)$ for reflexivity.
  • If $s \longmapsto s’​$ and $P(s’, s’’)​$, then $P(s, s’’)​$. This shows $P​$ is closed under head expansion for transitivity.

N-Times Iteration

$$
\dfrac{}{s \longmapsto^0 s}\\
\dfrac{s \longmapsto s’\phantom{“”}s’\longmapsto^n s’’}{s\longmapsto^{n+1} s’’}
$$

Lemma

$\forall s \text{ state}, s’ \text{ state}$, $s \longmapsto^\ast s’ \iff s \longmapsto^k s’$ for some $k \geq 0$.

Structural Dynamics

Structural dynamics of E is given by a transition system whose states are closed expressions.

All states are initial with final states are closed values, representing completed computations.

Judgment $e \text{ val}​$ is inductively defined by rules
$$
\dfrac{}{\text{num}[n]\text{ num}}\\
\dfrac{}{\text{str}[s]\text{ str}}
$$
The transition judgment $e \longmapsto e’$ between states is defined by rules
$$
\begin{align}
&\dfrac{n_1 + n_2 = n}{\text{plus}(\text{num}[n_1];\text{num}[n_2])\longmapsto \text{num}[n]}\\
&\dfrac{e_1 \longmapsto e_1’}{\text{plus}(e_1;e_2)\longmapsto \text{plus}(e_1’;e_2)}\\
&\dfrac{e_1 \text{ val}\phantom{“”}e_2 \longmapsto e_2’}{\text{plus}(e_1;e_2)\longmapsto \text{plus}(e_1;e_2’)}\\
&\dfrac{s_1 \wedge s_2 = s}{\text{cat}(\text{str}[s_1]; \text{str}[s_2])\longmapsto \text{str}[s]}\\
&\dfrac{e_1 \longmapsto e_1’}{\text{cat}(e_1;e_2)\longmapsto\text{cat}(e_1’;e_2)}\\
&\dfrac{e_1 \text{ val}\phantom{“”}e_2 \longmapsto e_2’}{\text{cat}(e_1;e_2)\longmapsto\text{cat}(e_1;e_2’)}\\
&\left[\dfrac{e_1 \longmapsto e_1’}{\text{let}(e_1;x.e_2)\longmapsto\text{let}(e_1’;x.e_2)}\right]\\
&\dfrac{\left[e_1\text{ val}\right]}{\text{let}(e_1;x.e_2)\longmapsto \left[e_1/x\right]e_2}
\end{align}
$$

1/4/8 are instruction transitions, corresponding to primitive steps of evaluations.

The rest are search transitions, determining the order of execution instructions.

By-Name and By-Value

The bracketed last 2 rules stands for by-value interpretation.

By-Name By-Value
Bind the variable to unevaluated expression Evaluates an expression before binding it to defined variable
Save the work if defined variable is not used Save the work if defined variable is used once
Waste work if the variable is needed Waste work if it is not used

Rule Induction

To show $P(e \longmapsto e’)$ when $e \longmapsto e’$, it is enough to show that $P$ is closed under the rules.

Finality of Values

Lemma: $\neg \exists e\text{ exp}$ that $e \text { val}$ and $e \longmapsto e’$ for some $e’$.

Determinacy

Lemma: If $e \longmapsto e’$ and $e \longmapsto e’’$, then $e’ =_\alpha e’’$.

Inversion Principle

The rule exemplify the inversion principle: the elimination forms are inverse to the introduction forms of a language.

Search rules determine the principal arguments of each elimination form.

Instruction rules determine how to evaluate the elimination form when its principal arguments are all in introduction form.

Contextual Dynamics

The main difference from structural dynamics to contextual dynamics is that C isolated instruction steps as instruction transition and formalize the process of locating the next instruction with evaluation context.

Instruction Transition

Instruction transition judgment $e_1 \to e_2$ for E is defined as
$$
\dfrac{m + n = p}{\text{plus}(\text{num}[m];\text{num}[n])\to \text{num}[p]}\\
\dfrac{s \wedge t = u}{\text{cat}(\text{str}[s];\text{str}[t])\to \text{str}[u]}\\
\dfrac{}{\text{let}(e_1;x.e_2)\to \left[e_1/x\right]e_2}
$$

Hole and Evaluation Context

Judgment $\mathcal{E} \text{ ectxt}$ determines the location of next instruction to execute in a larger expression.

The position of next instruction step is specified by “hole” $\circ$, into which the next instruction is placed.
$$
\dfrac{}{\circ \text{ ectxt}}\\
\dfrac{\mathcal{E}_1 \text{ ectxt}}{\text{plus}(\mathcal{E}_1;e_2) \text{ ectxt}}\\
\dfrac{e_1 \text{ val}\phantom{“”}\mathcal{E}_2\text{ ectxt}}{\text{plus}(e_1;\mathcal{E}_2)\text{ ectxt}}
$$
In this way, we can exemplify how hole and $\mathcal{E} \text{ ectxt}$ works.

Evaluation Context Judgment

An evaluation context is achieved by replacing a “hole” with an instruction to be executed.

The judgment $e’ = \mathcal{E}\lbrace e\rbrace$ states that the result of filling the hole in evaluation context $\mathcal E$ with expression $e$.

Thus
$$
\dfrac{}{e = \circ\lbrace e\rbrace}\\
\dfrac{e_1 = \mathcal{E}_1 \lbrace e\rbrace}{\text{plus}(e_1;e_2) =\text{plus}(\mathcal{E}_1;e_2)\lbrace e\rbrace}\\
\dfrac{e_1 \text{ val}\phantom{“”}e_2=\mathcal{E}_2\lbrace e\rbrace}{\text{plus}(e_1;e_2) =\text{plus}(e_1;\mathcal{E}_2)\lbrace e\rbrace}
$$
We can use a single rule for contextual dynamics of E:
$$
\dfrac{e_0 = \mathcal{E}\lbrace e\rbrace\phantom{“”}e\to e’\phantom{“”}e_1=\mathcal{E}\lbrace e’\rbrace}{e_0\longmapsto e_1}
$$

  1. Decompose $e_0​$ into a evaluation context $\mathcal E​$ and an instruction $e​$.
  2. Execute the instruction $e$.
  3. Replace the result $e’$ of $e$ to $\mathcal E$ and get $e_1$.

Connection to Structural Dynamics

Donate $e \longmapsto_s e’$ for transition relation defined by structural dynamics and $e\longmapsto_c e’$ be transition relation defined by contextual dynamics.

$e \longmapsto_s e’ \iff e\longmapsto_c e’$

In this way the two transition judgments coincide, contextual dynamics can be considered to be another presentation for structural dynamics.

Two advantages over structural dynamics:

  • The previous rule for contextual dynamics can be simplified to
    $$
    \dfrac{e \to e’}{\mathcal E\lbrace e\rbrace \longmapsto\mathcal E\lbrace e’\rbrace}
    $$

  • All the transitions are between complete programs, which means one do not have to consider any other types than observable types.

Equational Dynamics

Equation has the concept of definition, computation and equivalence. Thus this give rise to equational dynamics, with donation $\mathcal X | \Gamma \vdash e \equiv e’ : \tau$. Since only well-typed expressions are considered, we tacitly assume $\Gamma \vdash e : \tau$ and $\Gamma \vdash e’:\tau$.

Definition of E‘s equational dynamics under the by-name interpretation of let is inductively defined

Equivalence Relation

$$
\dfrac{}{\Gamma \vdash e \equiv e : \tau}\\
\dfrac{\Gamma \vdash e’ \equiv e : \tau}{\Gamma \vdash e \equiv e’ : \tau}\\
\dfrac{\Gamma \vdash e \equiv e’ : \tau \phantom{“”}\Gamma \vdash e’ \equiv e’’:\tau}{\Gamma \vdash e \equiv e’’:\tau}
$$

Congruence Relation

$$
\dfrac{\Gamma \vdash e_0 \equiv e_0’ : \text{num}\phantom{“”}\Gamma \vdash e_1\equiv e_1’:\text{num}}{\Gamma \vdash \text{plus}(e_0;e_1)\equiv \text{plus}(e_0’;e_1’):\text{num}}\\
\dfrac{\Gamma \vdash e_0 \equiv e_0’ : \text{str}\phantom{“”}\Gamma \vdash e_1\equiv e_1’:\text{str}}{\Gamma \vdash \text{cat}(e_0;e_1)\equiv \text{cat}(e_0’;e_1’):\text{str}}\\
\dfrac{\Gamma \vdash e_0 \equiv e_0’ : \tau_1 \phantom{“”}\Gamma, x:\tau_1 \vdash e_1\equiv e_1’:\tau}{\Gamma \vdash \text{let}(e_0;x.e_1)\equiv \text{let}(e_0’;x.e_1’):\tau}
$$

Primitive Constructions

$$
\dfrac{m + n = p}{\Gamma \vdash \text{plus}(\text{num}[m];\text{num}[n])\equiv \text{num}[p]:\text{num}}\\
\dfrac{s \wedge t = u}{\Gamma \vdash\text{cat}(\text{str}[s];\text{str}[t])\equiv \text{str}[u]:\text{str}}\\
\dfrac{}{\Gamma \vdash\text{let}(e_1;x.e_2)\equiv \left[e_1/x\right]e_2 : \tau}
$$

We say the rules define the strongest congruence under the primitive construction rules.

The definitional equality is relatively weak since many features of equality cannot derive from the previous rules, e.g., $x_1:\text{num}, x_2:\text{num}\vdash x_1 + x_2\equiv x_2 + x_1 :\text{num}$.

The gap can be filled with enriched notion of equivalence to a principle of proof by mathematical induction. Such notion is semantic equivalence.

Theorem

For E the relationship $e \equiv e’ : \tau \iff \exists e_0\text{ val} ​$ that $e \longmapsto^\ast e_0​$ and $e’ \longmapsto^\ast e_0​$.

Exercises

Prove for if $s \longmapsto^\ast s’​$ and $s’ \longmapsto^\ast s’’​$, then $s \longmapsto^\ast s’’​$.

  • If $s’$ is $s$, then $s \longmapsto^\ast s’ ‘$.

  • Suppose $s \longmapsto ^\ast s’,s’\longmapsto^\ast s’’ \Rightarrow s \longmapsto^\ast s’’​$, then $s_0 \to s,s\longmapsto^\ast s’ \Rightarrow s_0 \longmapsto^\ast s’​$.

    Thus we can get $s_0 \longmapsto ^\ast s’’​$ inductively.

Use $\longmapsto^k​$ method

  • Proof transfer to if $s \longmapsto ^ks’​$ and $s’ \longmapsto^{k’}s’’​$, then $s \longmapsto^{k + k’} s’’​$.
  • The rest is almost the same by induction.

Prove $\equiv$ theorem

  • Focus on Let congruence relation proof, if we want to prove it, we must ensure that $e_i$ and $e_i’$ do not cause complication to the proof when considering for $x_i$.
  • The rest are just similar.