Structural and Contextual Dynamics.

It is a common refrain here at Carnegie Mellon University that structural operational semantics (SOS) is the best form of dynamics, and that contextual dynamics (“Indiana-style semantics”) do not combat the bureaucratic tendency in the way that they are usually claimed to do. This is true in one formulation of contextual dynamics, but I would like to demonstrate a more fine-grained approach that is an improvement on both SOS and standard contextual dynamics.

structural dynamics

First, allow me to describe the controversy. Structural dynamics are based on two forms of judgment, \({{{\color{MidnightBlue}{M}}}\ \mathit{val}}\) and \({{{\color{MidnightBlue}{M}}}\mapsto{{\color{Maroon}{M'}}}}\). It is very simple to define a structural dynamics for a simple programming language: \[\begin{align} {{\color{MidnightBlue}{M}}} &::= {{\color{Maroon}{x}}} \mid {{\color{Maroon}{{\mathsf{tt}}}}} \mid {{\color{Maroon}{{\mathsf{ff}}}}} \mid {{\color{Maroon}{{\lambda x. {{\color{MidnightBlue}{M}}}}}}} \mid {{\color{Maroon}{{\mathsf{if}({{\color{MidnightBlue}{M}}};{{\color{MidnightBlue}{M}}};{{\color{MidnightBlue}{M}}})}}}} \mid {{\color{Maroon}{{\mathsf{ap}({{\color{MidnightBlue}{M}}};{{\color{MidnightBlue}{M}}})}}}} \end{align}\] \[ {\frac{ }{ {{{\color{MidnightBlue}{{\mathsf{tt}}}}}\ \mathit{val}} }} \qquad {\frac{ }{ {{{\color{MidnightBlue}{{\mathsf{ff}}}}}\ \mathit{val}} }} \qquad {\frac{ }{ {{{\color{MidnightBlue}{{\lambda x. M}}}}\ \mathit{val}} }} \] \[ {\frac{ {{{\color{MidnightBlue}{M}}}\mapsto{{\color{Maroon}{M'}}}} }{ {{{\color{MidnightBlue}{{\mathsf{if}(M;M_t;M_f)}}}}\mapsto{{\color{Maroon}{{\mathsf{if}(M';M_t;M_f)}}}}} }} \qquad {\frac{ }{ {{{\color{MidnightBlue}{{\mathsf{if}({\mathsf{tt}};M_t;M_f)}}}}\mapsto{{\color{Maroon}{M_t}}}} }} \qquad {\frac{ }{ {{{\color{MidnightBlue}{{\mathsf{if}({\mathsf{ff}};M_t;M_f)}}}}\mapsto{{\color{Maroon}{M_f}}}} }} \] \[ {\frac{ {{{\color{MidnightBlue}{M}}}\mapsto{{\color{Maroon}{M'}}}} }{ {{{\color{MidnightBlue}{{\mathsf{ap}(M;N)}}}}\mapsto{{\color{Maroon}{{\mathsf{ap}(M';N)}}}}} }} \qquad {\frac{ }{ {{{\color{MidnightBlue}{{\mathsf{ap}({\lambda x. M};N)}}}}\mapsto{{\color{Maroon}{M[N/x]}}}} }} \]

There are three classes of rules above: rules that declare something to be a value, rules that execute a “principal cut” (e.g. applying a lambda, or branching on a literal boolean), and rules that search for an applicable cut (computing the boolean argument to a conditional, or computing the function argument to an application). In a more elaborate language, this last kind of rule (often called “congruence rules”) gets completely out of control in SOS and comes to dominate your definition. This in turn causes further problems in formalization, because proofs that reason by induction on reduction trees must account for numerous nearly identical cases.

naïve contextual dynamics

One way to improve this state of affairs is to introduce an abstraction (confusingly) called an “evaluation context”. The way the story usually goes is that you take your existing grammar and extend it in the following way with a new sort for evaluation contexts and “instructions”: \[\begin{align} {{\color{MidnightBlue}{M}}} &::= {{\color{Maroon}{x}}} \mid {{\color{Maroon}{{\mathsf{tt}}}}} \mid {{\color{Maroon}{{\mathsf{ff}}}}} \mid {{\color{Maroon}{{\lambda x. {{\color{MidnightBlue}{M}}}}}}} \mid {{\color{Maroon}{{\mathsf{if}({{\color{MidnightBlue}{M}}};{{\color{MidnightBlue}{M}}};{{\color{MidnightBlue}{M}}})}}}} \mid {{\color{Maroon}{{\mathsf{ap}({{\color{MidnightBlue}{M}}};{{\color{MidnightBlue}{M}}})}}}} \\ {{\color{MidnightBlue}{E}}} &::= {{\color{Maroon}{\bullet}}} \mid {{\color{Maroon}{{\mathsf{if}({{\color{MidnightBlue}{E}}};{{\color{MidnightBlue}{M}}};{{\color{MidnightBlue}{M}}})}}}} \mid {{\color{Maroon}{{\mathsf{ap}({{\color{MidnightBlue}{E}}};{{\color{MidnightBlue}{N}}})}}}}\\ {{\color{MidnightBlue}{I}}} &::= {{\color{Maroon}{{{\color{MidnightBlue}{E}}}[{{\color{MidnightBlue}{M}}}]}}} \end{align}\]

Following Harper’s presentation in Practical Foundations for Programming Languages, you then have to define a judgment that relates terms to instructions: \[ {\frac{ }{ {{{\color{MidnightBlue}{M}}}\ltimes{{\color{MidnightBlue}{\bullet[M]}}}} }} \qquad {\frac{ {{{\color{MidnightBlue}{M_1}}}\ltimes{{\color{MidnightBlue}{E[N]}}}} }{ {{{\color{MidnightBlue}{{\mathsf{ap}(M_1;M_2)}}}}\ltimes{{\color{MidnightBlue}{{\mathsf{ap}(E;M_2)}[N]}}}} }} \qquad {\frac{ {{{\color{MidnightBlue}{M_1}}}\ltimes{{\color{MidnightBlue}{E[N]}}}} }{ {{{\color{MidnightBlue}{{\mathsf{if}(M_1;M_2;M_3)}}}}\ltimes{{\color{MidnightBlue}{{\mathsf{if}(E;M_2;M_3)}[N]}}}} }} \]

Then, we can define a dynamics basis on expressions: \[ {\frac{ }{ {{{\color{MidnightBlue}{{\mathsf{tt}}}}}\ \mathit{val}} }} \qquad {\frac{ }{ {{{\color{MidnightBlue}{{\mathsf{ff}}}}}\ \mathit{val}} }} \qquad {\frac{ }{ {{{\color{MidnightBlue}{{\lambda x. M}}}}\ \mathit{val}} }} \] \[ {\frac{ }{ {{{\color{MidnightBlue}{{\mathsf{if}({\mathsf{tt}};M_t;M_f)}}}}\mapsto{{\color{Maroon}{M_t}}}} }} \qquad {\frac{ }{ {{{\color{MidnightBlue}{{\mathsf{if}({\mathsf{ff}};M_t;M_f)}}}}\mapsto{{\color{Maroon}{M_f}}}} }} \qquad {\frac{ }{ {{{\color{MidnightBlue}{{\mathsf{ap}({\lambda x. M};N)}}}}\mapsto{{\color{Maroon}{M[N/x]}}}} }} \]

Next, we add to our basis all necessary congruence rules in one fell swoop: \[ {\frac{ {{{\color{MidnightBlue}{M}}}\ltimes{{\color{MidnightBlue}{{{\color{Maroon}{E[N]}}}}}}} \quad {{{\color{MidnightBlue}{N}}}\mapsto{{\color{Maroon}{N'}}}} \quad {{{\color{MidnightBlue}{{{\color{Maroon}{M'}}}}}}\ltimes{{\color{MidnightBlue}{E[N']}}}} }{ {{{\color{MidnightBlue}{M}}}\mapsto{{\color{Maroon}{M'}}}} }} \]

Now, let’s take stock. We have achieved our goal of factoring out the duplication caused by congruence rules, but at what cost? We have had to define a judgment that relates terms to instructions (“plugged contexts”), and our single congruence rule relies on fairly sophisticated reasoning. For instance, in order for our operational semantics to even be algorithmic, we must prove that \({{{\color{MidnightBlue}{M}}}\ltimes{{\color{MidnightBlue}{I}}}}\) is well-moded as both \({{{\color{MidnightBlue}{M}}}\ltimes{{\color{MidnightBlue}{{{\color{Maroon}{I}}}}}}}\) and \({{{\color{MidnightBlue}{{{\color{Maroon}{M}}}}}}\ltimes{{\color{MidnightBlue}{I}}}}\).

Whatever we have saved in the area of congruence appears to have merely shifted the bureaucracy elsewhere. If this is the case, why do presentations of contextual dynamics usually suggest otherwise? Precisely because much of the difficult part is usually elided: as an abuse of notation, terms are identified with plugged contexts.

So, can we say that contextual dynamics was not worth it? I intend to argue that this is not in fact the ideal formulation of this concept, and that we can give a version of conextual dynamics that really does eliminate bureaucracy by moving toward a syntax that is closer to that of a certain kind of abstract machine.

Advanced Contextual Dynamics

Let us define our syntax from scratch following my program. Note how this representation is completely canonical: each term of the original lambda calculus that we defined has only a single representative, which is already a massive improvement on the naïve contextual dynamics. \[\begin{align} {{\color{MidnightBlue}{V}}} &::= {{\color{Maroon}{{\mathsf{tt}}}}} \mid {{\color{Maroon}{{\mathsf{ff}}}}} \mid {{\color{Maroon}{{\lambda x. {{\color{MidnightBlue}{M}}}}}}}\\ {{\color{MidnightBlue}{K}}} &::= {{\color{Maroon}{{\mathsf{if}(-;{{\color{MidnightBlue}{M}}};{{\color{MidnightBlue}{M}}})}}}} \mid {{\color{Maroon}{{\mathsf{ap}(-;{{\color{MidnightBlue}{M}}})}}}}\\ {{\color{MidnightBlue}{M}}} &::= {{\color{Maroon}{{{\color{MidnightBlue}{\overline{V}}}}}}} \mid {{\color{Maroon}{{{\color{MidnightBlue}{K}}}[{{\color{MidnightBlue}{M}}}]}}} \end{align}\]

Next, we define our dynamics \({{{\color{MidnightBlue}{M}}}\ \mathit{val}}\) and \({{{\color{MidnightBlue}{M}}}\mapsto{{\color{Maroon}{M'}}}}\): \[ {\frac{ }{ {{{\color{MidnightBlue}{\overline{V}}}}\ \mathit{val}} }}\mathfrak{val} \qquad {\frac{ {{{\color{MidnightBlue}{M}}}\mapsto{{\color{Maroon}{M'}}}} }{ {{{\color{MidnightBlue}{K[M]}}}\mapsto{{\color{Maroon}{K[M']}}}} }}\mathfrak{cong} \] \[ {\frac{ }{ {{{\color{MidnightBlue}{{\mathsf{if}(-;M_t;M_f)}[\overline{{\mathsf{tt}}}]}}}\mapsto{{\color{Maroon}{M_t}}}} }}\mathfrak{if/tt} \qquad {\frac{ }{ {{{\color{MidnightBlue}{{\mathsf{if}(-;M_t;M_f)}[\overline{{\mathsf{ff}}}]}}}\mapsto{{\color{Maroon}{M_f}}}} }}\mathfrak{if/ff} \qquad {\frac{ }{ {{{\color{MidnightBlue}{{\mathsf{ap}(-;N)}[\overline{{\lambda x. M}}]}}}\mapsto{{\color{Maroon}{M[N/x]}}}} }}\mathfrak{ap/lam} \]

In fact, this is a lot closer to what contextual dynamics look like in the wild, and I would argue that something along these lines is what is really intended when the bureaucratic work necessitated by the style of contextual dynamics in the previous section is elided. Let me stress that there are no bureaucratic lemmas necessary to associate “terms” with “instructions”, because we view the concrete term syntax given in the first section as a mere notation for the completely canonizing representation given here.

Example: Progress and Preservation

As an example, to demonstrate the perspicuity of our representation, let’s define a very simple type system and show that we have the type safety property. \[\begin{align} {{\color{MidnightBlue}{\tau}}} &::= {{\color{Maroon}{{\mathsf{bool}}}}} \mid {{\color{Maroon}{{{\color{MidnightBlue}{\tau}}}\to{{\color{MidnightBlue}{\tau}}}}}} \end{align}\]

We will define three typing judgments, \({{{\color{MidnightBlue}{\Gamma}}}\vdash{{\color{MidnightBlue}{V}}}:{{\color{MidnightBlue}{\tau}}}}\) (values), \({{{\color{MidnightBlue}{\Gamma}}}\vdash{{\color{MidnightBlue}{K}}}:{{\color{MidnightBlue}{\sigma}}} > {{\color{MidnightBlue}{\tau}}}}\) (continuations) and \({{{\color{MidnightBlue}{\Gamma}}}\vdash{{\color{MidnightBlue}{M}}}:{{\color{MidnightBlue}{\tau}}}}\) (programs): \[ {\frac{ }{ {{{\color{MidnightBlue}{\Gamma}}}\vdash{{\color{MidnightBlue}{{\mathsf{tt}}}}}:{{\color{MidnightBlue}{{\mathsf{bool}}}}}} }}\mathfrak{tt} \qquad {\frac{ }{ {{{\color{MidnightBlue}{\Gamma}}}\vdash{{\color{MidnightBlue}{{\mathsf{ff}}}}}:{{\color{MidnightBlue}{{\mathsf{bool}}}}}} }}\mathfrak{ff} \qquad {\frac{ {{{\color{MidnightBlue}{\Gamma,x:\sigma}}}\vdash{{\color{MidnightBlue}{M}}}:{{\color{MidnightBlue}{\tau}}}} }{ {{{\color{MidnightBlue}{\Gamma}}}\vdash{{\color{MidnightBlue}{{\lambda x. M}}}}:{{\color{MidnightBlue}{\sigma\to\tau}}}} }}\mathfrak{lam} \] \[ {\frac{ {{{\color{MidnightBlue}{\Gamma}}}\vdash{{\color{MidnightBlue}{M_t}}}:{{\color{MidnightBlue}{\tau}}}} \quad {{{\color{MidnightBlue}{\Gamma}}}\vdash{{\color{MidnightBlue}{M_f}}}:{{\color{MidnightBlue}{\tau}}}} }{ {{{\color{MidnightBlue}{\Gamma}}}\vdash{{\color{MidnightBlue}{{\mathsf{if}(-;M_t;M_f)}}}}:{{\color{MidnightBlue}{{\mathsf{bool}}}}} > {{\color{MidnightBlue}{\tau}}}} }}\mathfrak{if} \qquad {\frac{ {{{\color{MidnightBlue}{\Gamma}}}\vdash{{\color{MidnightBlue}{N}}}:{{\color{MidnightBlue}{\sigma}}}} }{ {{{\color{MidnightBlue}{\Gamma}}}\vdash{{\color{MidnightBlue}{{\mathsf{ap}(-;N)}}}}:{{\color{MidnightBlue}{\sigma\to\tau}}} > {{\color{MidnightBlue}{\tau}}}} }}\mathfrak{ap} \] \[ {\frac{ }{ {{{\color{MidnightBlue}{\Gamma,x:\tau}}}\vdash{{\color{MidnightBlue}{x}}}:{{\color{MidnightBlue}{\tau}}}} }}\mathfrak{var} \qquad {\frac{ {{{\color{MidnightBlue}{\Gamma}}}\vdash{{\color{MidnightBlue}{V}}}:{{\color{MidnightBlue}{\tau}}}} }{ {{{\color{MidnightBlue}{\Gamma}}}\vdash{{\color{MidnightBlue}{\overline{V}}}}:{{\color{MidnightBlue}{\tau}}}} }}\mathfrak{ret} \qquad {\frac{ {{{\color{MidnightBlue}{\Gamma}}}\vdash{{\color{MidnightBlue}{K}}}:{{\color{MidnightBlue}{\sigma}}} > {{\color{MidnightBlue}{\tau}}}} \quad {{{\color{MidnightBlue}{\Gamma}}}\vdash{{\color{MidnightBlue}{M}}}:{{\color{MidnightBlue}{\sigma}}}} }{ {{{\color{MidnightBlue}{\Gamma}}}\vdash{{\color{MidnightBlue}{K[M]}}}:{{\color{MidnightBlue}{\tau}}}} }}\mathfrak{cut} \]


Lemma 1 (Critical Progress). If \({{{\color{MidnightBlue}{\cdot}}}\vdash{{\color{MidnightBlue}{K[\overline{V}]}}}:{{\color{MidnightBlue}{\tau}}}}\), then \({{{\color{MidnightBlue}{K[\overline{V}]}}}\mapsto{{\color{Maroon}{M}}}}\) for some \(M\).

Proof. By inversion, we have \({{{\color{MidnightBlue}{\cdot}}}\vdash{{\color{MidnightBlue}{K}}}:{{\color{MidnightBlue}{\sigma}}} > {{\color{MidnightBlue}{\tau}}}}\) with \({{{\color{MidnightBlue}{\cdot}}}\vdash{{\color{MidnightBlue}{\overline{V}}}}:{{\color{MidnightBlue}{\sigma}}}}\). By simultaneous case on \(K,V\):

Case \({{{\color{MidnightBlue}{K}}}\equiv{{\color{Maroon}{{\mathsf{if}(-;M_t;M_f)}}}}}\), \({{{\color{MidnightBlue}{V}}}\equiv{{\color{Maroon}{{\mathsf{tt}}}}}}\). Then let \({{{\color{MidnightBlue}{M}}}\triangleq{{\color{Maroon}{M_t}}}}\) and apply \(\mathfrak{if/tt}\).

Case \({{{\color{MidnightBlue}{K}}}\equiv{{\color{Maroon}{{\mathsf{if}(-;M_t;M_f)}}}}}\), \({{{\color{MidnightBlue}{V}}}\equiv{{\color{Maroon}{{\mathsf{ff}}}}}}\). Then let \({{{\color{MidnightBlue}{M}}}\triangleq{{\color{Maroon}{M_f}}}}\) and apply \(\mathfrak{if/ff}\).

Case \({{{\color{MidnightBlue}{K}}}\equiv{{\color{Maroon}{{\mathsf{ap}(-;N)}}}}}\), \({{{\color{MidnightBlue}{V}}}\equiv{{\color{Maroon}{{\lambda x. M'}}}}}\). Then let \({{{\color{MidnightBlue}{M}}}\triangleq{{\color{Maroon}{M'[N/x]}}}}\) and apply \(\mathfrak{ap/lam}\).

All other cases discharged by inversion on the premise.


Lemma 2 (Progress). If \({{{\color{MidnightBlue}{\cdot}}}\vdash{{\color{MidnightBlue}{M}}}:{{\color{MidnightBlue}{\tau}}}}\), then either \({{{\color{MidnightBlue}{M}}}\ \mathit{val}}\) or \({{{\color{MidnightBlue}{M}}}\mapsto{{\color{Maroon}{M'}}}}\).

Proof. By induction.

Case \(\mathfrak{var}\). Impossible, by inversion.

Case \(\mathfrak{ret}\). Then apply \(\mathfrak{val}\).

Case \(\mathfrak{cut}\). Then \({{{\color{MidnightBlue}{M}}}\equiv{{\color{Maroon}{K[M']}}}}\); by induction, either \({{{\color{MidnightBlue}{M'}}}\ \mathit{val}}\) or \({{{\color{MidnightBlue}{M'}}}\mapsto{{\color{Maroon}{M''}}}}\). If the former, then by inversion we have \({{{\color{MidnightBlue}{M}}}\equiv{{\color{Maroon}{K[V]}}}}\), so appeal to Lemma 1; otherwise apply \(\mathfrak{cong}\).


Lemma 3 (Preservation). If \({{{\color{MidnightBlue}{\cdot}}}\vdash{{\color{MidnightBlue}{M}}}:{{\color{MidnightBlue}{\tau}}}}\) and \({{{\color{MidnightBlue}{M}}}\mapsto{{\color{Maroon}{M'}}}}\), then \({{{\color{MidnightBlue}{\cdot}}}\vdash{{\color{MidnightBlue}{M'}}}:{{\color{MidnightBlue}{\tau}}}}\).

Proof. Proceed by induction on \({{{\color{MidnightBlue}{M}}}\mapsto{{\color{Maroon}{M'}}}}\).

Case \(\mathfrak{cong}\). Then \({{{\color{MidnightBlue}{M}}}\equiv{{\color{Maroon}{K[N]}}}}\) and \({{{\color{MidnightBlue}{M'}}}\equiv{{\color{Maroon}{K[N']}}}}\) and \({{{\color{MidnightBlue}{N}}}\mapsto{{\color{Maroon}{N'}}}}\). By inversion on the typing judgment, we have \({{{\color{MidnightBlue}{\cdot}}}\vdash{{\color{MidnightBlue}{K}}}:{{\color{MidnightBlue}{\sigma}}} > {{\color{MidnightBlue}{\tau}}}}\) and \({{{\color{MidnightBlue}{\cdot}}}\vdash{{\color{MidnightBlue}{N}}}:{{\color{MidnightBlue}{\sigma}}}}\); by induction, we have \({{{\color{MidnightBlue}{\cdot}}}\vdash{{\color{MidnightBlue}{N'}}}:{{\color{MidnightBlue}{\sigma}}}}\). Therefore, by \(\mathfrak{cut}\), we also have \({{{\color{MidnightBlue}{\Gamma}}}\vdash{{\color{MidnightBlue}{K[N']}}}:{{\color{MidnightBlue}{\tau}}}}\).

Case \(\mathfrak{if/tt}\). Then \({{{\color{MidnightBlue}{M}}}\equiv{{\color{Maroon}{{\mathsf{if}(-;M_t;M_f)}[\overline{{\mathsf{tt}}}]}}}}\) and \({{{\color{MidnightBlue}{M'}}}\equiv{{\color{Maroon}{M_t}}}}\); by inverting the program typing judgment and then inverting the continuation typing judgment, we have \({{{\color{MidnightBlue}{\cdot}}}\vdash{{\color{MidnightBlue}{M_t}}}:{{\color{MidnightBlue}{\tau}}}}\).

Case \(\mathfrak{if/ff}\). Analogous.

Case \(\mathfrak{ap/lam}\). Then \({{{\color{MidnightBlue}{M}}}\equiv{{\color{Maroon}{{\mathsf{ap}(-;M_2)}[\overline{{\lambda x. M_1}}]}}}}\) and \({{{\color{MidnightBlue}{M'}}}\equiv{{\color{Maroon}{M_1[M_2/x]}}}}\). By multiple inversions, we have \({{{\color{MidnightBlue}{\cdot}}}\vdash{{\color{MidnightBlue}{M_2}}}:{{\color{MidnightBlue}{\sigma}}}}\) and \({{{\color{MidnightBlue}{x:\sigma}}}\vdash{{\color{MidnightBlue}{M_1}}}:{{\color{MidnightBlue}{\sigma\to\tau}}}}\). By the substitution lemma (exercise), we have \({{{\color{MidnightBlue}{\cdot}}}\vdash{{\color{MidnightBlue}{M_1[M_2/x]}}}:{{\color{MidnightBlue}{\tau}}}}\).


Theorem 4 (Safety).

Proof. By Lemma 2 and Lemma 3.

Concluding Remarks

By arranging the algebraic/syntactic aspects of our language carefully, we were able to ensure that our rules involve a minimum of bureaucracy; this representation also leads to a clean type-safety proof. This approach also lends itself almost immediately to a simple machine dynamics.

There are some disadvantages to this style of doing things, which might be resolved separately: currently, valuehood is decided by the head operator of a term, but the simplifying power of this assumption is not immediately compatible with languages that have eager canonical forms (like ML). There are multiple ways to resolve this problem, one of which would be to add continuations in addition to canonical forms for strict data constructors.

To summarize, contextual dynamics are useful! But you have to do it right in order to get the pay-off.