Characterizing closure under expansion/reduction for big-step semantics?

Question

Two common ways of formulating operational semantics for programming languages based on lambda-calculus are big-step and small-step semantics.

1. In a big step semantics, you give a relation $e \Downarrow v$ which directly relates an expression to the value it computes.
2. In a small-step semantics, you give a transition relation $e \mapsto e'$ which does one step of evaluation, and you get to a value by iterating the transition relation. $e \mapsto^{*} v$.

These two relations are equivalent, in the sense that $e \Downarrow v$ if and only if $e \mapsto^{*} v$.

However, some things are easier to define one way or another. For example, we can say that a set of terms $R \subseteq \mathrm{Exp}$ is closed under expansion if it satisfies the property that: $$\forall e \in R, e' \in \mathrm{Exp}.\;e' \mapsto e \;\mathrm{implies}\; e' \in R$$

Likewise, a set $R$ is closed under reduction if if satisfies:

$$\forall e \in R, e' \in \mathrm{Exp}.\;e \mapsto e' \;\mathrm{implies}\; e' \in R$$

It's not immediately obvious to me how to formulate expansion or contraction in terms of a big-step semantics. Does anyone know how?

Answer 1

The notion of "next" and "last" - prior to the idea of "expansion" and "reduction" - are essentially lost when we read a big-step operational semantics as an inductive definition, which is too bad because the way we usually prove things about big-step operational semantics is by reading it as an inductive definition!

You can prove a "full expansion" property (big step preservation) that $e \Downarrow v$ and $e \in R$ imply $v \in R$, and then observe that the proof of this property actually proves a small-step expansion property. This is because computational structure of the proof actually recovers the small-step evaluation process that Prolog/Twelf would use to execute the big-step semantics as a logic program! But for appropriately tricky semantics (especially non-deterministic ones), I've noticed it's frequently the case that you can prove a big-step property when it doesn't hold for the small-step evaluation process that Prolog/Twelf proof proof search would imply.

In my view, the best option - if we want to use big-step specifications but recover the information that was lost when we treated the big-step semantics as inductive definition - to characterize the small-step evaluation process that Prolog/Twelf would use. (This ends up basically or exactly being an abstract machine semantics.) This may not be satisfying depending on what it is you're trying to do, of course. There are a couple of versions of this: see Hannan and Miller or Ager, for instance. (There's also a bit about this in my thesis, some work I did with Ian Zerny, but I'll link to that when there's a thing to link to.) You could also carefully characterize a set of partial derivations of $e_1 \Downarrow v_1, \ldots, e_n \Downarrow v_n \vdash e \Downarrow v$ that corresponded to partial executions, but when I've contemplated this the details have seemed fraught enough that the abstract machine interpretation seems like a safer bet.